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