字節跳動旗下Seed團隊近日宣布，其研發的新一代形式化數學推理模型Seed Prover 1.5正式發布。該模型通過引入創新的Agentic架構與大規模強化學習訓練方法，在多項高難度數學評測中取得突破性進展，刷新了形式化數學推理領域的性能紀錄。
在備受矚目的國際數學奧林匹克（IMO 2025）模擬測試中，Seed Prover 1.5展現出強大實力。模型僅用16.5小時便完成前5道賽題的完整形式化證明，生成可編譯驗證的Lean代碼，最終獲得35/42的評分，達到該賽事歷史評分體系下的金牌標準。今年7月，其前代版本Seed Prover曾以3天完成4道完整證明和1道部分證明的成績，獲得IMO官方認證銀牌。
北美本科數學競賽Putnam的測試結果同樣令人矚目。Seed Prover 1.5在約9小時內為12道賽題中的11道生成可驗證的Lean代碼，系統評估顯示其解題率達88%。在更高難度的Fate-H與Fate-X評測集（分別對應碩士與博士水平數學難題）中，模型分別解決了80%和33%的問題，多項指標刷新現有最優紀錄。
技術突破的核心在于團隊提出的Agentic Prover架構。該架構突破傳統形式化證明的線性生成模式，將Lean語言轉化為可調用的工具集。模型在證明過程中可動態調用Mathlib定理庫檢索、Python計算驗證、引理增量保存與復用等功能，通過實時修正推理路徑顯著提升復雜問題的解決效率。這種設計使模型在保持高成功率的同時，算力消耗較前代降低30%。
訓練方法方面，研究團隊采用大規模Agentic強化學習框架。Lean編譯器的絕對客觀反饋為模型提供了精準的獎懲信號，經過數百萬步訓練后，模型在訓練集上的證明通過率從50%躍升至近90%。這種訓練方式使模型在高難度任務中展現出更強的泛化能力，部分測試場景下性能超越人類專家水平。
為彌合自然語言與形式語言之間的差異，團隊同步開發了Sketch Model。該模型模擬人類數學家的思維模式，先構建高層證明框架，再將復雜命題拆解為多個可并行求解的子問題。通過與自然語言模型和Agentic Prover的協同工作，形成"直覺生成-結構規劃-形式驗證"的三階段流程，使復雜定理的求解成功率提升40%。
技術文檔顯示，Seed Prover 1.5的研發團隊已將完整技術報告上傳至arXiv預印本平臺，所有Lean證明代碼在GitHub開源。目前模型正進行API接口測試，未來將面向數學與人工智能領域研究者開放使用。研究團隊特別強調，當前模型雖在競賽級數學問題中表現優異，但距離輔助前沿數學研究仍需突破文獻理解、跨領域推理等關鍵能力。
