近日，字节跳动 Seed 团队推出了其最新的形式化数学推理模型 Seed Prover1.5，标志着在数学推理领域的一次重要突破。此次模型的推出，得益于对大规模 Agentic 强化学习的深入探索，使得其在推理能力和效率方面都取得了显著提升。
在参加2025年国际数学奥林匹克（IMO）比赛时，Seed Prover 展现了其强大的性能。在短短三天内，该模型成功解决了六道题目中的四道，并对其中一道进行了部分证明，最终获得了官方认证的银牌成绩。相比之下，Seed Prover1.5在16.5小时内针对 IMO2025的前五道题目生成了完整的可编译验证的 Lean 证明代码，达到金牌分数线的标准。
更值得注意的是，Seed Prover1.5在2025年普特南数学竞赛中的表现同样出色，仅用时9小时便完成了12道题目中的11道生成可编译验证的 Lean 代码。这一成绩刷新了形式化数学推理模型在多个评测集上的最佳表现，特别是在包含硕士和博士生数学难度的评估集上，分别解决了80% 和33% 的问题。
Seed Prover1.5的创新之处在于其全新的 Agentic Prover 架构，这一架构将自然语言推理与形式化证明的优势相结合。与以往的形式化证明器不同，Seed Prover1.5能够在证明过程中灵活调用多种工具，例如主动检索庞大的数学库 Mathlib 和执行 Python 代码来辅助验证。通过增量式引理验证，该模型将复杂问题拆解为若干引理，逐步构建形式化证明。
此外，Seed Prover1.5还引入了 Sketch Model，该模型模拟了人类数学家的解决思路，将自然语言证明转化为高层的证明框架，从而大大降低了复杂定理证明的难度。通过这种 “分而治之” 的策略，Seed Prover1.5能够有效避免生成长文本时的错误累积。
技术报告:
https://arxiv.org/abs/2512.17260
Lean 证明代码:
https://github.com/ByteDance-Seed/Seed-Prover/blob/main/SeedProver-1.5/Putnam2025.zip
