字節跳動旗下Seed團隊近日正式發布新一代形式化數學推理專用模型——Seed Prover 1.5。該模型通過大規模Agentic強化學習（RL）訓練，在數學推理能力與效率方面實現突破性提升，成為形式化數學推理領域的重要進展。

在針對國際數學奧林匹克競賽（IMO）的測試中，Seed Prover 1.5展現出強勁實力。僅用16.5小時，該模型便為IMO 2025前5道題目生成完整可編譯驗證的Lean證明代碼，按競賽評分標準換算后取得35分的成績，達到金牌分數線（滿分42分）。這一表現較前代模型有顯著提升，標志著自動化數學推理向人類頂尖水平邁進一步。

面向北美本科數學競賽Putnam的測試同樣驗證了模型的泛化能力。在9小時內，Seed Prover 1.5成功為Putnam 2025的12道賽題中的11道生成可驗證的Lean代碼，解題效率與準確性均達到競賽級標準。更全面的評估顯示，該模型在完整的Putnam歷史題庫中解決了88%的問題，在代表碩士數學難度的Fate-H評估集和博士生數學難度的Fate-X評估集中，分別攻克了80%和33%的題目，刷新了形式化數學推理模型在多項權威評測中的最優表現（SOTA）。

技術層面，Seed Prover 1.5通過創新的Agentic RL訓練框架，實現了推理路徑的自主規劃與優化。其核心突破在于將形式化證明過程分解為可動態調整的子任務鏈，使模型能夠根據問題特征靈活選擇策略，顯著提升了復雜數學問題的求解效率。團隊公開的技術報告詳細披露了模型架構與訓練方法，為學術界與工業界提供了可復現的研究范式。

目前，Seed Prover 1.5的技術報告已對外發布，相關代碼庫與演示接口即將陸續開放。開發者可通過官方渠道獲取Lean證明代碼示例，體驗模型在自動化數學推理領域的實際應用能力。這一進展不僅為數學研究提供新型輔助工具，也為人工智能在科學推理領域的拓展奠定了技術基礎。