魚羊 發(fā)自 凹非寺
量子位 | 公眾號 QbitAI

字節(jié)最新數(shù)學(xué)推理專用模型，剛剛刷新戰(zhàn)績：拿下IMO金牌成績。

Scaling Law加持下，這個名為Seed Prover 1.5的模型，在16.5小時內(nèi)，順利解決IMO 2025的前5道題目，在僅失一題的情況下拿到35分，達(dá)到今年IMO的金牌線。

這一成績與7月官方認(rèn)證的IMO金牌“選手”谷歌Gemini打平。而字節(jié)自己的前代模型，當(dāng)時的成績是3天完成了6道題目中的4道，以及一道題的部分證明，達(dá)到銀牌成績。

同時，Seed Prover 1.5也在北美本科級別數(shù)學(xué)競賽Putnam這一基準(zhǔn)上，大幅刷新了SOTA成績。

模型尚未開源，但技術(shù)報告已經(jīng)公開。

值得關(guān)注的是，Seed Prover 1.5強調(diào)了大規(guī)模強化學(xué)習(xí)給數(shù)學(xué)模型帶來的性能提升，也證明，在推理階段增加計算資源，可以顯著提高解題率。

即，驗證了測試時Scaling和強化學(xué)習(xí)訓(xùn)練時的Scaling的有效性。

草稿引導(dǎo)的高效形式化證明

具體來看技術(shù)報告。Seed Prover 1.5的參數(shù)規(guī)模與Seed 1.6相同，230B總參數(shù)，23B激活。

主要創(chuàng)新有兩點：

• Agentic Prover：一種新的形式化數(shù)學(xué)推理范式
• Sketch Model：自然語言到形式語言的翻譯器

Agentic Prover

相較于通用模型用自然語言解答數(shù)學(xué)問題的方式，數(shù)學(xué)推理專用模型采用的是形式化數(shù)學(xué)推理，也就是用Lean等形式語言，構(gòu)建可在公理系統(tǒng)中機械驗證的證明，以確保結(jié)果更加可靠。

其難點在于，形式化證明比自然語言證明更加困難。根據(jù)“De Bruijn factor”經(jīng)驗法則，一行普通的數(shù)學(xué)推導(dǎo)，通常需要擴展成4到10行復(fù)雜的代碼。

這要求模型不僅懂?dāng)?shù)學(xué)，還要精通編程和類型論，而這一高門檻導(dǎo)致形式化證明在效率和成功率上一直遠(yuǎn)落后于自然語言推理。

以往的研究中，形式化證明器通常分為兩類：

• Step-prover：一步一步證明，效率很低；
• Whole-prover：一次性生成完整證明，但中間一旦出錯就會前功盡棄。

Seed Prover 1.5為了平衡兩種方法的優(yōu)缺點，提出了一種全新的Agentic Prover架構(gòu)：

模型將Lean語言視為一種工具，且在證明過程中可以自主地調(diào)用其他多種工具。

• Mathlib搜索工具：類似于程序員查閱技術(shù)文檔，模型可以主動檢索Lean龐大的數(shù)學(xué)庫 Mathlib，尋找可用的定理和定義，而非依賴不可靠的隱式記憶。
• Python代碼執(zhí)行：遇到需要計算的部分，模型可以編寫并運行Python腳本來輔助驗證直覺。
• 增量式引理驗證：模型不再被迫一次性生成整個證明，而是將復(fù)雜問題拆解為若干引理。每證明出一個引理，系統(tǒng)就會將其保留并復(fù)用，作為后續(xù)推理的基石。

這樣一來，模型既可以像人類一樣先使用“草稿紙”（自然語言）進(jìn)行推理，又能夠與Lean環(huán)境及多種工具進(jìn)行交互，隨時調(diào)用工具來驗證猜想。

就是說，Seed Prover 1.5采用的是基于引理的交互方式，既不是一次性生成整個證明，也無需每一步都做交互驗證。

官方技術(shù)報告中還提到，Seed Prover 1.5進(jìn)行了大規(guī)模的Agentic RL。

實驗證明，隨著強化學(xué)習(xí)訓(xùn)練步數(shù)的增加，模型在訓(xùn)練集上的證明通過率從初始的50%升至接近90%。

Agentic RL還帶來了大幅的效率提升。在對比測試中，Seed Prover 1.5僅需少量的計算資源，就能在Putnam和Fate等高難度數(shù)據(jù)集上，擊敗消耗大量算力的上一代Seed Prover模型。

Sketch Model

為了讓模型能更好地“打草稿”，研究人員還專門訓(xùn)練了Sketch Model，來模擬人類數(shù)學(xué)家解決問題的方式：

數(shù)學(xué)家在證明一個復(fù)雜定理時，通常不會直接寫出每一步嚴(yán)絲合縫的代碼。他們會先在紙上寫下一個非形式化的證明草稿，列出關(guān)鍵的中間步驟、引理和大致思路。

Sketch Model同樣不糾結(jié)于具體的語法細(xì)節(jié)，而是專注于邏輯路徑的規(guī)劃。它可以將自然語言證明拆解為若干個獨立的、難度更低的引理，并暫時跳過具體證明，僅保留整體的邏輯骨架。

這就將原本不可解的復(fù)雜命題，轉(zhuǎn)化成了難度更低的子目標(biāo)。

研究人員采用混合獎勵信號的強化學(xué)習(xí)策略，來訓(xùn)練這一模型：

• 信號一：Lean編譯器驗證生成的草圖是否完全正確。
• 信號二：自然語言Prover會逐一檢查引理，一旦發(fā)現(xiàn)任一引理在數(shù)學(xué)上不成立，整個草稿即被否決。
• 信號三：引入基于長思維鏈的Rubric評分模型，從語義層面評估草稿的質(zhì)量——考量引理是否與自然語言證明對齊、拆解的粒度是否合適、是否真正降低了原題的難度。

當(dāng)草稿在形式驗證、數(shù)學(xué)正確性和整體評分上均滿足要求時，才會獲得正向獎勵。

測試時工作流

以上創(chuàng)新最終構(gòu)成了一個分層級的多智能體協(xié)作系統(tǒng)：

• Natural Language Prover負(fù)責(zé)提供高層的數(shù)學(xué)直覺和自然語言證明。
• Sketch Model將自然語言轉(zhuǎn)化為形式化的引理結(jié)構(gòu)。
• Agentic Prover并行地攻克每一個被拆解出的引理。

如果某個引理太難證明，系統(tǒng)還會遞歸地調(diào)用Sketch Model再次進(jìn)行拆解。這不僅規(guī)避了長文本生成的錯誤累積問題，更提升了推理的并行度和成功率。

研究人員還驗證了這一工作流的測試時Scaling特性。

如上圖所示，投入更多的計算資源，Seed Prover 1.5對問題的解決率會呈對數(shù)線性增長。

這項研究來自字節(jié)Seed AI4Math團隊。

量子位捕捉到了其中幾位作者的蹤跡。

Zheng Yuan，清華統(tǒng)計學(xué)博士。今年6月剛剛加入字節(jié)，此前在阿里Qwen團隊負(fù)責(zé)對齊和推理方向工作。

Hanwen Zhu，本科畢業(yè)于牛津大學(xué)數(shù)學(xué)與計算機科學(xué)專業(yè)，目前在CMU讀研，即將加入字節(jié)Seed。

鄭澤宇，CMU在讀博士，字節(jié)Seed實習(xí)生，專業(yè)方向同樣是數(shù)學(xué)與計算機科學(xué)聯(lián)合方向。

論文鏈接：
https://arxiv.org/pdf/2512.17260
參考鏈接：
[1]https://mp.weixin.qq.com/s/vcciJWK9KfDBM4FBIJwTfw?click_id=2
[2]https://x.com/GanjinZero/status/2001948751871815741

— 完 —