字節(jié)跳動旗下Seed團(tuán)隊近日正式發(fā)布新一代形式化數(shù)學(xué)推理專用模型——Seed Prover 1.5。該模型通過大規(guī)模Agentic強(qiáng)化學(xué)習(xí)（RL）訓(xùn)練，在數(shù)學(xué)推理能力與效率方面實(shí)現(xiàn)突破性提升，成為形式化數(shù)學(xué)推理領(lǐng)域的重要進(jìn)展。

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

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

技術(shù)層面，Seed Prover 1.5通過創(chuàng)新的Agentic RL訓(xùn)練框架，實(shí)現(xiàn)了推理路徑的自主規(guī)劃與優(yōu)化。其核心突破在于將形式化證明過程分解為可動態(tài)調(diào)整的子任務(wù)鏈，使模型能夠根據(jù)問題特征靈活選擇策略，顯著提升了復(fù)雜數(shù)學(xué)問題的求解效率。團(tuán)隊公開的技術(shù)報告詳細(xì)披露了模型架構(gòu)與訓(xùn)練方法，為學(xué)術(shù)界與工業(yè)界提供了可復(fù)現(xiàn)的研究范式。

目前，Seed Prover 1.5的技術(shù)報告已對外發(fā)布，相關(guān)代碼庫與演示接口即將陸續(xù)開放。開發(fā)者可通過官方渠道獲取Lean證明代碼示例，體驗(yàn)?zāi)Ｐ驮谧詣踊瘮?shù)學(xué)推理領(lǐng)域的實(shí)際應(yīng)用能力。這一進(jìn)展不僅為數(shù)學(xué)研究提供新型輔助工具，也為人工智能在科學(xué)推理領(lǐng)域的拓展奠定了技術(shù)基礎(chǔ)。