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

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

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

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

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

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

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

即，驗證了測試時Scaling和強化學習訓練時的Scaling的有效性。

草稿引導的高效形式化證明

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

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

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

Agentic Prover

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

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

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

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

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

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

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

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

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

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

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

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

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

Sketch Model

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

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

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

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

研究人員采用混合獎勵信號的強化學習策略，來訓練這一模型：

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

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

測試時工作流

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

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

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

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

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

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

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

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

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

鄭澤宇，CMU在讀博士，字節(jié)Seed實習生，專業(yè)方向同樣是數(shù)學與計算機科學聯(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

— 完 —