近日，字節跳動 Seed 團隊推出了其最新的形式化數學推理模型 Seed Prover1.5，標誌着在數學推理領域的一次重要突破。此次模型的推出，得益於對大規模 Agentic 強化學習的深入探索，使得其在推理能力和效率方面都取得了顯著提升。

在參加2025年國際數學奧林匹克（IMO）比賽時，Seed Prover 展現了其強大的性能。在短短三天內，該模型成功解決了六道題目中的四道，並對其中一道進行了部分證明，最終獲得了官方認證的銀牌成績。相比之下，Seed Prover1.5在16.5小時內針對 IMO2025的前五道題目生成了完整的可編譯驗證的 Lean 證明代碼，達到金牌分數線的標準。

QQ20251224-141739.png

更值得注意的是，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