近日，字节跳动旗下的 Seed AI 团队发布了一款名为 Seed Prover1.5的数学推理模型，该模型在国际数学奥林匹克（IMO）比赛中表现卓越，成功获得金牌，标志着人工智能在数学领域的又一突破。
Seed Prover1.5采用了 Scaling Law 理论，并在16.5小时内解决了 IMO2025的前五道题，仅失一题，最终以35分的成绩达到了金牌标准。这一成绩与谷歌 Gemini 并驾齐驱，而字节之前的模型在当时需用三天才完成四道题，最终仅获得银牌。显然，Seed Prover1.5的表现无疑为 AI 数学推理模型设定了新标杆。
这款模型的成功并非偶然，其核心在于大规模强化学习的引入。通过训练，模型在证明题目的成功率从最初的50% 跃升至接近90%。此外，Seed Prover1.5还在北美数学竞赛 Putnam 中刷新了以往的最佳成绩，显示出其超强的解决问题能力。
Seed Prover1.5的技术报告中介绍了两项重要创新:Agentic Prover 和 Sketch Model。Agentic Prover 采用了一种新的形式化数学推理方式，利用 Lean 等形式语言进行可验证的证明。这种方法相比传统的自然语言推理更为严谨，但也更具挑战性。为了克服这一难点，Seed Prover1.5支持模型在推理过程中调用多个工具，比如检索 Lean 的数学库 Mathlib 和编写 Python 脚本进行计算。
而 Sketch Model 则是为了帮助模型更好地 “打草稿”。该模型模拟了人类数学家解决问题的思路，允许其先进行非正式的证明草稿，列出关键的引理和思路，再转化为形式化证明。通过混合奖励信号的强化学习策略，Sketch Model 不仅提高了整体逻辑的规划能力，还有效降低了复杂问题的难度。
总的来说，Seed Prover1.5不仅展示了字节在 AI 数学推理领域的创新与实力，也为未来的数学研究和教育提供了新的可能性。
论文地址：https://arxiv.org/pdf/2512.17260
