據學者觀察，大型語言模型在形式語言中進行定理證明仍然面臨挑戰，且計算成本高昂。
近日，字節跳動 Seed 團隊今日宣布推出新一代形式化數學推理專用模型 Seed Prover 1.5，該模型通過大規模智能強化學習進行訓練，并配備了高效的測試時擴展（TTS）工作流程。
通過和其他工具的廣泛交互，該模型在強化學習過程中不斷積累經驗，從而顯著提升了形式定理證明的能力和效率。
此外，TTS 工作流程有效地彌合了自然語言和形式語言之間的鴻溝。與現有方法相比，Seed-Prover 1.5 以更小的計算預算實現了更優異的性能。該系統能夠解決 PutnamBench（本科水平）88% 的問題、Fate-H（研究生水平）80% 的問題以及 Fate-X（博士水平）33% 的問題。
值得注意的是，利用該系統，Seed 團隊在 9 小時內解決了 Putnam 2025 中的 12 道題中的 11 道。研究結果表明，以高質量形式化反饋為驅動的經驗學習規模化，對未來形式化數學推理的發展具有巨大的潛力。
訓練方法
與之前的智能體證明器不同，團隊提出了一種更高效的策略，通過增量調用多個工具來逐步構建形式化證明。一旦引理編譯成功，它就會被緩存到內存中，并在后續的推理步驟中重用，從而無需重新生成先前已驗證的代碼。
與基于完整證明生成的方法相比，這種增量緩存機制能夠更有效地利用上下文窗口。這種表示方法具有以下幾個優點：
與模態證明的一致性：與之前提出的引理式證明無縫銜接。
復雜度分解：減輕了模型生成完整證明的必要性。相反，模型可以專注于解決眼前的子目標
上下文效率：通過順序緩存有效引理，與必須迭代地重新生成完整證明歷史的方法相比，顯著降低了上下文開銷。
靈活的推理控制：能夠實現各種推理策略，例如剪除不相關的中間步驟或回溯到特定點重新開始對話。
研究人員設計了幾種強化學習訓練任務形式，包括直接從形式化語句進行證明、基于自然語言證明概要進行證明，以及基于先前失敗嘗試的總結進行證明。
他們還提出訓練一個草圖模型。該模型從形式化語句及其自然語言證明中合成一個引理風格的 Lean 草圖。
為了訓練這個草圖模型，研究團隊使用了 VAPO 和混合獎勵信號。Lean 編譯器確保草圖結構的正確性，而 LLM 作為評判標準則作為語義價值模型，采用長鏈思維 (Long-CoT) 來實現比基于標量模型更好的泛化能力。
Seed-Prover 1.5 協調三個專門的 Agents，包括：
自然語言證明器：一個針對自然語言證明優化的 LLM。
Sketch 模型：一種經過訓練的翻譯代理，可以將自然語言證明轉換為 token 的 Lean 草圖，有效地彌合非正式推理和正式語法之間的差距。
智能精益證明器：工具集成代理，負責驗證每個單獨的引理。
實驗結果
強化學習訓練的準確率從初始化時的約 50% 提升至 1000 步后的近 90%。這一提升主要歸功于精心挑選的訓練數據集與來自 Lean 驗證的準確獎勵信號。
平均函數調用次數從約 15 次下降到 10 次，這與平均序列長度的持續減少相一致。這表明模型正在學習更策略性地使用工具，避免冗余或“試錯”調用。
盡管調用次數有所減少，但模型的推理能力卻有所提升。優化步驟的改進表明，智能體處理復雜、長時程問題的能力也日益增強。然而，在 32K–64K 范圍內持續存在負分表明，有效處理極長上下文仍然是一個挑戰。
Seed-Prover 1.5 在 PutnamBench 上解決了 87.9% 的問題，在 Fate-H 上解決了 80% 的問題，證明了其在處理本科和研究生水平數學形式化證明方面的能力。然而，該系統在處理博士及更高級別的問題時仍然面臨挑戰，這主要是由于問題復雜性的增加以及 Mathlib 支持的限制。
研究人員表示，系統目前還無法做出與人類專家相媲美的重大數學貢獻，這一局限性源于前沿數學研究中固有的關鍵依賴性問題。
關鍵的區別在于數學任務的性質：IMO 或 Putnam 數學競賽的問題經過精心設計，求解者無需了解特定的先前研究論文，而推動數學領域取得重大進展通常依賴于對眾多相關論文的綜合分析。
要取得這樣的進展，需要應對三個相互關聯的挑戰：
首先，識別最具影響力和最相關的論文；
其次，基于這些論文進行自然語言證明；
第三，開發可擴展的方法，將論文本身及其推導出的結果形式化。
解決這三大挑戰將能夠大規模生成形式化的數學研究——這一進步最終可能有助于解決某些懸而未決的數學猜想。
參考資料：
https://arxiv.org/abs/2512.17260
分享
