Full text · 原文
2,596 字
鱼羊 发自 凹非寺<br>
量子位 | 公众号 QbitAI<br>
字节最新数学推理专用模型，刚刚刷新战绩：拿下IMO金牌成绩。<br>
Scaling Law加持下，这个名为Seed Prover 1.5的模型，在16.5小时内，顺利解决IMO 2025的前5道题目，在仅失一题的情况下拿到35分，达到今年IMO的金牌线。<br>
这一成绩与7月官方认证的IMO金牌“选手”谷歌Gemini打平。而字节自己的前代模型，当时的成绩是3天完成了6道题目中的4道，以及一道题的部分证明，达到银牌成绩。<br>
同时，Seed Prover 1.5也在北美本科级别数学竞赛Putnam这一基准上，大幅刷新了SOTA成绩。<br>
模型尚未开源，但技术报告已经公开。<br>
值得关注的是，Seed Prover 1.5强调了大规模强化学习给数学模型带来的性能提升，也证明，在推理阶段增加计算资源，可以显著提高解题率。<br>
即，验证了测试时Scaling和强化学习训练时的Scaling的有效性。<br>
草稿引导的高效形式化证明<br>
具体来看技术报告。Seed Prover 1.5的参数规模与Seed 1.6相同，230B总参数，23B激活。<br>
主要创新有两点：<br>
Agentic Prover：一种新的形式化数学推理范式<br>
Sketch Model：自然语言到形式语言的翻译器<br>
Agentic Prover<br>
相较于通用模型用自然语言解答数学问题的方式，数学推理专用模型采用的是形式化数学推理，也就是用Lean等形式语言，构建可在公理系统中机械验证的证明，以确保结果更加可靠。<br>
其难点在于，形式化证明比自然语言证明更加困难。根据“De Bruijn factor”经验法则，一行普通的数学推导，通常需要扩展成4到10行复杂的代码。<br>
这要求模型不仅懂数学，还要精通编程和类型论，而这一高门槛导致形式化证明在效率和成功率上一直远落后于自然语言推理。<br>
以往的研究中，形式化证明器通常分为两类：<br>
Step-prover：一步一步证明，效率很低；<br>
Whole-prover：一次性生成完整证明，但中间一旦出错就会前功尽弃。<br>
Seed Prover 1.5为了平衡两种方法的优缺点，提出了一种全新的Agentic Prover架构：<br>
模型将Lean语言视为一种工具，且在证明过程中可以自主地调用其他多种工具。<br>
Mathlib搜索工具：类似于程序员查阅技术文档，模型可以主动检索Lean庞大的数学库 Mathlib，寻找可用的定理和定义，而非依赖不可靠的隐式记忆。<br>
Python代码执行：遇到需要计算的部分，模型可以编写并运行Python脚本来辅助验证直觉。<br>
增量式引理验证：模型不再被迫一次性生成整个证明，而是将复杂问题拆解为若干引理。每证明出一个引理，系统就会将其保留并复用，作为后续推理的基石。<br>
这样一来，模型既可以像人类一样先使用“草稿纸”（自然语言）进行推理，又能够与Lean环境及多种工具进行交互，随时调用工具来验证猜想。<br>
就是说，Seed Prover 1.5采用的是基于引理的交互方式，既不是一次性生成整个证明，也无需每一步都做交互验证。<br>
官方技术报告中还提到，Seed Prover 1.5进行了大规模的Agentic RL。<br>
实验证明，随着强化学习训练步数的增加，模型在训练集上的证明通过率从初始的50%升至接近90%。<br>
Agentic RL还带来了大幅的效率提升。在对比测试中，Seed Prover 1.5仅需少量的计算资源，就能在Putnam和Fate等高难度数据集上，击败消耗大量算力的上一代Seed Prover模型。<br>
Sketch Model<br>
为了让模型能更好地“打草稿”，研究人员还专门训练了Sketch Model，来模拟人类数学家解决问题的方式：<br>
数学家在证明一个复杂定理时，通常不会直接写出每一步严丝合缝的代码。他们会先在纸上写下一个非形式化的证明草稿，列出关键的中间步骤、引理和大致思路。<br>
Sketch Model同样不纠结于具体的语法细节，而是专注于逻辑路径的规划。它可以将自然语言证明拆解为若干个独立的、难度更低的引理，并暂时跳过具体证明，仅保留整体的逻辑骨架。<br>
这就将原本不可解的复杂命题，转化成了难度更低的子目标。<br>
研究人员采用混合奖励信号的强化学习策略，来训练这一模型：<br>
信号一：Lean编译器验证生成的草图是否完全正确。<br>
信号二：自然语言Prover会逐一检查引理，一旦发现任一引理在数学上不成立，整个草稿即被否决。<br>
信号三：引入基于长思维链的Rubric评分模型，从语义层面评估草稿的质量——考量引理是否与自然语言证明对齐、拆解的粒度是否合适、是否真正降低了原题的难度。<br>
当草稿在形式验证、数学正确性和整体评分上均满足要求时，才会获得正向奖励。<br>
测试时工作流<br>
以上创新最终构成了一个分层级的多智能体协作系统：<br>
Natural Language Prover负责提供高层的数学直觉和自然语言证明。<br>
Sketch Model将自然语言转化为形式化的引理结构。<br>
Agentic Prover并行地攻克每一个被拆解出的引理。<br>
如果某个引理太难证明，系统还会递归地调用Sketch Model再次进行拆解。这不仅规避了长文本生成的错误累积问题，更提升了推理的并行度和成功率。<br>
研究人员还验证了这一工作流的测试时Scaling特性。<br>
如上图所示，投入更多的计算资源，Seed Prover 1.5对问题的解决率会呈对数线性增长。<br>
这项研究来自字节Seed AI4Math团队。<br>
量子位捕捉到了其中几位作者的踪迹。<br>
Zheng Yuan，清华统计学博士。今年6月刚刚加入字节，此前在阿里Qwen团队负责对齐和推理方向工作。<br>
Hanwen Zhu，本科毕业于牛津大学数学与计算机科学专业，目前在CMU读研，即将加入字节Seed。<br>
郑泽宇，CMU在读博士，字节Seed实习生，专业方向同样是数学与计算机科学联合方向。<br>
论文链接：https://arxiv.org/pdf/2512.17260参考链接：[1]https://mp.weixin.qq.com/s/vcciJWK9KfDBM4FBIJwTfw?click_id=2[2]https://x.com/GanjinZero/status/2001948751871815741<br>
— 完 —