超越DeepSeek推理，效率更高！斯坦福馬騰宇新作：有限數據，無限迭代

原標題：超越DeepSeek推理，效率更高！斯坦福馬騰宇新作：有限數據，無限迭代
文章來源：新智元
內容字數：5932字

斯坦福大學提出自博弈定理證明器STP：解決大型語言模型推理能力瓶頸

大型語言模型（LLM）的推理能力是當前自然語言處理領域的核心難題，其主要瓶頸在于缺乏高質量的訓練數據。現有方法如強化學習和專家迭代，雖然能夠提升模型推理能力，但存在通過率低、計算資源浪費嚴重等問題。斯坦福大學研究人員提出了一種名為自博弈定理證明器（STP）的新方法，有效解決了這些問題。

STP的核心思想：模仿數學家的學習方式
STP模仿數學家學習和發展數學的方式，讓模型同時扮演“猜想者”和“證明者”兩個角色，通過互相提供訓練信號，在有限的數據下實現無限自我改進。猜想者提出新的猜想，證明者嘗試證明，驗證器選擇正確的證明用于訓練，從而形成一個閉環的自我迭代過程。
STP的訓練流程：五個步驟
STP的訓練流程包含五個步驟：1. 使用監督微調（SFT）初始化模型；2. 猜想者生成新的猜想；3. 證明者嘗試證明猜想和未證明命題；4. 驗證器驗證證明的正確性并分配獎勵；5. 基于驗證結果重新訓練模型。其中，獎勵函數的設計是STP的核心技術難點，旨在激勵猜想者生成多樣化、具有挑戰性但可行的猜想。
STP的優勢：顯著提升證明成功率和推理速度
實驗結果表明，STP在Lean和Isabelle驗證器上的表現顯著優于現有方法。在LeanWorkbook數據集上，STP的證明成功率達到26.3%，是專家迭代方法的兩倍。在miniF2F-test、ProofNet-test和PutnamBench等公共基準測試中，STP也實現了最先進的性能，顯著提升了推理速度。
STP的創新點：無限自我改進和高效利用數據
STP的核心創新在于其自博弈機制，它能夠在有限的數據集上不斷生成新的猜想和證明，從而實現無限自我改進。這種機制有效解決了現有方法中數據稀缺和計算資源浪費的問題，并能夠逐漸提升猜想和證明的難度。
STP的未來展望：推動LLM推理能力發展
STP為解決LLM推理能力瓶頸提供了一種新的思路，其高效的數據利用方式和強大的自我改進能力，有望推動LLM在數學推理等領域的應用發展。未來的研究可以進一步探索STP在其他領域（例如，程序驗證、知識圖譜推理）的應用，并改進獎勵函數設計，提升模型的性能和魯棒性。