字节跳动推出 Seed Prover1.5：形式化数学推理再进一步

近期，字节跳动 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 架构，把自然语言推理与形式化证明有机结合。不同于传统形式化证明器，它能在证明过程中灵活调用多种工具，例如主动检索庞大的 Mathlib 数学库，以及执行 Python 代码进行辅助校验。通过采用增量式引理验证，模型将复杂问题拆分为多个引理，逐步拼合出完整的形式化证明。

此外，Seed Prover1.5 引入了 Sketch Model，模拟人类数学家的解题思路，先把自然语言证明转化为高层的证明框架，大幅降低复杂定理的证明难度。借助“分而治之”的策略，模型能有效减少长文本生成时的错误累积。

技术报告:

https://arxiv.org/abs/2512.17260

Lean 证明代码:

https://github.com/ByteDance-Seed/Seed-Prover/blob/main/SeedProver-1.5/Putnam2025.zip