123,123

字節(jié)跳動推理專用模型 Seed Prover 1.5：擁有更強數(shù)學推理表現(xiàn)

2025-12-25 18:14

據(jù)學者觀察，大型語言模型在形式語言中進行定理證明仍然面臨挑戰(zhàn)，且計算成本高昂。

近日，字節(jié)跳動 Seed 團隊今日宣布推出新一代形式化數(shù)學推理專用模型 Seed Prover 1.5，該模型通過大規(guī)模智能強化學習進行訓練，并配備了高效的測試時擴展（TTS）工作流程。

通過和其他工具的廣泛交互，該模型在強化學習過程中不斷積累經(jīng)驗，從而顯著提升了形式定理證明的能力和效率。

此外，TTS 工作流程有效地彌合了自然語言和形式語言之間的鴻溝。與現(xiàn)有方法相比，Seed-Prover 1.5 以更小的計算預算實現(xiàn)了更優(yōu)異的性能。該系統(tǒng)能夠解決 PutnamBench（本科水平）88% 的問題、Fate-H（研究生水平）80% 的問題以及 Fate-X（博士水平）33% 的問題。

值得注意的是，利用該系統(tǒng)，Seed 團隊在 9 小時內(nèi)解決了 Putnam 2025 中的 12 道題中的 11 道。研究結(jié)果表明，以高質(zhì)量形式化反饋為驅(qū)動的經(jīng)驗學習規(guī)模化，對未來形式化數(shù)學推理的發(fā)展具有巨大的潛力。

訓練方法

與之前的智能體證明器不同，團隊提出了一種更高效的策略，通過增量調(diào)用多個工具來逐步構(gòu)建形式化證明。一旦引理編譯成功，它就會被緩存到內(nèi)存中，并在后續(xù)的推理步驟中重用，從而無需重新生成先前已驗證的代碼。

與基于完整證明生成的方法相比，這種增量緩存機制能夠更有效地利用上下文窗口。這種表示方法具有以下幾個優(yōu)點：

與模態(tài)證明的一致性：與之前提出的引理式證明無縫銜接。
復雜度分解：減輕了模型生成完整證明的必要性。相反，模型可以專注于解決眼前的子目標
上下文效率：通過順序緩存有效引理，與必須迭代地重新生成完整證明歷史的方法相比，顯著降低了上下文開銷。
靈活的推理控制：能夠?qū)崿F(xiàn)各種推理策略，例如剪除不相關(guān)的中間步驟或回溯到特定點重新開始對話。

研究人員設計了幾種強化學習訓練任務形式，包括直接從形式化語句進行證明、基于自然語言證明概要進行證明，以及基于先前失敗嘗試的總結(jié)進行證明。

他們還提出訓練一個草圖模型。該模型從形式化語句及其自然語言證明中合成一個引理風格的 Lean 草圖。

為了訓練這個草圖模型，研究團隊使用了 VAPO 和混合獎勵信號。Lean 編譯器確保草圖結(jié)構(gòu)的正確性，而 LLM 作為評判標準則作為語義價值模型，采用長鏈思維 (Long-CoT) 來實現(xiàn)比基于標量模型更好的泛化能力。

Seed-Prover 1.5 協(xié)調(diào)三個專門的 Agents，包括：

自然語言證明器：一個針對自然語言證明優(yōu)化的 LLM。
Sketch 模型：一種經(jīng)過訓練的翻譯代理，可以將自然語言證明轉(zhuǎn)換為 token 的 Lean 草圖，有效地彌合非正式推理和正式語法之間的差距。
智能精益證明器：工具集成代理，負責驗證每個單獨的引理。

實驗結(jié)果

強化學習訓練的準確率從初始化時的約 50% 提升至 1000 步后的近 90%。這一提升主要歸功于精心挑選的訓練數(shù)據(jù)集與來自 Lean 驗證的準確獎勵信號。

平均函數(shù)調(diào)用次數(shù)從約 15 次下降到 10 次，這與平均序列長度的持續(xù)減少相一致。這表明模型正在學習更策略性地使用工具，避免冗余或“試錯”調(diào)用。

盡管調(diào)用次數(shù)有所減少，但模型的推理能力卻有所提升。優(yōu)化步驟的改進表明，智能體處理復雜、長時程問題的能力也日益增強。然而，在 32K–64K 范圍內(nèi)持續(xù)存在負分表明，有效處理極長上下文仍然是一個挑戰(zhàn)。

Seed-Prover 1.5 在 PutnamBench 上解決了 87.9% 的問題，在 Fate-H 上解決了 80% 的問題，證明了其在處理本科和研究生水平數(shù)學形式化證明方面的能力。然而，該系統(tǒng)在處理博士及更高級別的問題時仍然面臨挑戰(zhàn)，這主要是由于問題復雜性的增加以及 Mathlib 支持的限制。

研究人員表示，系統(tǒng)目前還無法做出與人類專家相媲美的重大數(shù)學貢獻，這一局限性源于前沿數(shù)學研究中固有的關(guān)鍵依賴性問題。

關(guān)鍵的區(qū)別在于數(shù)學任務的性質(zhì)：IMO 或 Putnam 數(shù)學競賽的問題經(jīng)過精心設計，求解者無需了解特定的先前研究論文，而推動數(shù)學領域取得重大進展通常依賴于對眾多相關(guān)論文的綜合分析。

要取得這樣的進展，需要應對三個相互關(guān)聯(lián)的挑戰(zhàn)：