【量子位 2025年12月26日讯】AI数学推理再迎里程碑突破！12月25日，字节跳动Seed AI4Math团队发布数学推理专用模型Seed Prover 1.5，在2025年国际数学奥林匹克竞赛（IMO）模拟测试中，以16.5小时解决前5道题目、总分35分的成绩达到金牌线，与谷歌Gemini并列成为目前唯一拿下IMO金牌的AI模型。更值得关注的是，这款模型通过独创的“草稿引导+多工具协作”架构，彻底打破了形式化数学推理“效率低、易出错”的行业痛点，同时在北美本科数学竞赛Putnam等基准测试中刷新SOTA，标志着AI在高难度数学推理领域正式迈入“实用化”阶段。
目前，Seed Prover 1.5的技术报告已公开，模型虽暂未开源，但字节透露其核心创新可复用于物理、工程等需要严密逻辑推理的领域，未来将通过火山引擎向科研机构开放能力。
战绩突破：从IMO银牌到金牌，效率提升超10倍
作为衡量AI数学推理能力的“终极考场”，IMO题目因需要深度抽象思维、多步逻辑推导，长期以来是AI的“硬骨头”。此前字节前代模型Seed Prover 1.0需3天才能完成IMO 6道题中的4道（含1道部分证明），仅获银牌；而Seed Prover 1.5凭借架构革新，实现了“速度+准确率”的双重飞跃：
-
IMO金牌级表现：在2025年IMO模拟测试中，模型16.5小时内完整证明前5道题目，仅第6题因涉及超复杂几何构造未完成，最终得分35分（IMO金牌线通常为32-36分），与谷歌Gemini同期成绩持平，成为全球仅有的两款达到IMO金牌水平的AI模型。
-
Putnam竞赛刷新纪录：在北美本科数学竞赛Putnam基准测试中，Seed Prover 1.5以359/660的得分大幅超越前代模型（331/660）及其他开源模型（如Goedel-Prover-V2-32B仅86/660），在Fate-H、Fate-X等细分数据集上，正确率分别达57%、10%，较上一代提升63%、11%。
-
效率碾压同类模型：对比测试显示，Seed Prover 1.5仅需“pass@8×8”的计算资源（即每道题8组测试、每组8次尝试），就能击败消耗18个H20 GPU日算力的前代模型，算力成本降低超90%，证明其“高效推理”能力的实用性。
核心创新：两大技术破解形式化推理“两难困境”
形式化数学推理需用Lean等形式语言构建可机械验证的证明，一行自然语言推导常需扩展为4-10行代码，既要求模型懂数学，又需精通编程与类型论，长期面临“分步证明效率低、一次性证明易出错”的两难。Seed Prover 1.5通过“Agentic Prover架构+Sketch Model草稿引导”两大创新，彻底打破这一困局：
1. Agentic Prover：像人类一样“调用工具+拆解问题”
不同于传统“分步验证”（Step-prover）或“一次性生成”（Whole-prover）的单一模式，Agentic Prover将Lean语言视为工具，构建“多工具协作+增量验证”的推理闭环，完美复刻人类数学家“查资料、算数据、拆难题”的思考过程：
-
Mathlib搜索工具：告别“记忆依赖”模型可主动检索Lean庞大的数学库Mathlib，精准调取所需定理与定义（如证明群论问题时自动查找“有限指数子群”相关引理），无需依赖易出错的隐式记忆，避免因“记错定理”导致的证明中断。
-
Python代码执行：解决“计算瓶颈”遇到需要数值验证或复杂计算的步骤（如验证函数单调性、求解方程近似解），模型会自动编写Python脚本并运行，例如在数论题目中，通过代码快速验证“某数是否为素数”，替代人工计算，准确率达100%。
-
增量式引理验证：拆解“复杂命题”模型不强迫一次性生成完整证明，而是将原题拆解为若干子引理，每证明一个引理就保存为“临时公理”，作为后续推理的基础。例如证明“不等式恒成立”问题时，先拆解出“中间变量范围”“导数符号判断”等子引理，逐一验证后再整合，大幅降低单次推理难度，证明成功率从50%提升至90%。
2. Sketch Model：自然语言到形式语言的“草稿翻译官”
为让模型更高效地规划推理路径，字节团队专门训练Sketch Model，模拟人类数学家“先写草稿、再补细节”的工作方式：
-
逻辑骨架优先，跳过语法细节Sketch Model不纠结于Lean代码的语法正确性，而是专注于拆解逻辑路径——将自然语言证明转化为“关键引理+推导顺序”的草稿框架，例如证明几何题时，先列出“作辅助线→证明三角形全等→推导角度关系”的步骤，暂时跳过具体代码实现。
-
三重奖励信号确保草稿质量团队采用混合奖励策略训练Sketch Model：① Lean编译器验证草稿逻辑是否闭环；② 自然语言Prover检查引理数学正确性（任一引理错误则否决草稿）；③ Rubric评分模型从“引理粒度、语义对齐度”评估草稿质量，只有三者均达标才给予正向奖励，确保草稿“逻辑通顺、难度可控”。
-
递归拆解：复杂问题“降维打击”若某子引理仍难度过高，系统会递归调用Sketch Model再次拆解，将“不可解”的大问题转化为“可解”的小目标。例如证明“复杂函数连续性”时，先拆解为“局部有界性”“极限存在性”两个引理，若“极限存在性”仍难证明，再拆解为“左极限=右极限”的子引理，层层递进直至可验证。
技术逻辑：强化学习+测试时Scaling，解锁推理潜力
Seed Prover 1.5的突破，还得益于字节团队对“Scaling Law（缩放定律）”的深度验证，证明“训练时强化学习缩放+测试时计算资源缩放”可显著提升推理能力：
-
大规模Agentic RL：训练步数决定性能上限模型通过Agentic强化学习（RL）训练，随着训练步数增加，训练集证明通过率从初始50%升至90%，且泛化能力同步提升——在未见过的IMO模拟题中，正确率提升幅度与训练集一致，证明RL不仅是“过拟合训练”，而是真正提升了模型的推理能力。
-
测试时Scaling：算力投入与解题率正相关实验显示，Seed Prover 1.5的解题率随计算资源投入呈“对数线性增长”：当计算预算从1个H20 GPU日增至45个时，Putnam基准的解题数量从300道增至500道，证明其能力可通过增加算力进一步释放，为解决更复杂的数学问题（如哥德巴赫猜想局部验证）提供可能。
团队与未来：清华+CMU智囊团，瞄准多领域推理落地
Seed Prover 1.5的研发团队汇聚了数学与AI领域的顶尖人才：负责人郑泽宇为CMU数学与计算机科学联合博士，核心成员包括清华统计学博士郑源（前阿里Qwen团队对齐方向负责人）、牛津本科+CMU硕士朱文轩（专注形式化验证），跨学科背景确保模型既懂数学本质，又具备工程落地能力。
字节Seed AI4Math团队表示，未来将从三方向推进技术落地：① 扩展模型对物理、工程等领域的形式化推理能力，助力科研机构验证理论假设；② 优化Lean之外的形式语言支持（如Isabelle/HOL），覆盖更广泛的科研场景；③ 探索“数学推理+多模态”融合，例如结合图像理解解决几何证明题，进一步贴近人类科研习惯。
从IMO银牌到金牌，Seed Prover 1.5的突破不仅是AI数学推理的里程碑，更证明“复刻人类思考过程”的AI架构，能在需要深度逻辑的领域实现“从理论到实用”的跨越。正如技术报告中所言：“当AI能像人类一样查资料、算数据、拆难题，它就不再是简单的计算工具，而是能与科学家协作的‘数学助手’。”
