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

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

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

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

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