字节跳动发布 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 架构，它融合了自然语言推理与形式化证明的优势。与传统证明器不同，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