新智元報道
新智元報道
編輯：LRS
【新智元導讀】STP（自博弈定理證明器）讓模型扮演「猜想者」和「證明者」，互相提供訓練訊號，在有限的資料下實現了無限自我改進，在Lean和Isabelle驗證器上的表現顯著優於現有方法，證明成功率翻倍，並在多個基準測試中達到最先進的效能。
大型語言模型的「推理能力」現在成了NLP皇冠上的明珠，其核心難題在於「缺乏高質量訓練資料」，標註資料需要領域專家，成本非常高昂且難以擴充套件；現有高等數學論文和定理的數量也非常有限，遠少於其他任務的資料來源。
DeepSeek-Prover和DeepSeek R1等模型的思路非常巧妙，在沒有逐步解決方案的資料集（如定理命題）上進行強化學習，可以極大提升其推理能力；和專家迭代（expert iteration）類似，交替進行「LLMs生成證明」和「正確生成的證明上進行微調」，部分緩解了資料稀缺（data scarcity）的問題。
不過，強化學習和專家迭代都存在一個嚴重問題：透過率（pass rate）過低，對「未證明的定理」生成「正確證明」所需的樣本量呈指數級增長，大量的計算資源被浪費在生成錯誤的證明上，無法為模型提供訓練訊號。
比如在LeanWorkbook上的透過率為13.2%，其中98.5%的計算資源都浪費在生成錯誤證明上了，也就是說，在經過幾輪專家迭代後，由於缺乏新的成功證明，重新訓練模型的效果會大大降低。
此外，強化學習從原理上就受到訓練資料集中「定理難度水平」的限制，一個模型不可能從「解決高中水平的問題」中學習到「大學水平的證明技巧」，也無法解決「開放性」的數學問題，需要持續收集高水平的定理命題和數學問題。
斯坦福的研究人員提出了一個自博弈定理證明器（STP），模仿數學家學習和發展數學的方式，同時承擔兩個角色（猜想者和證明器），互相提供訓練訊號，可以在「有限資料」的情況下「無限執行並自我改進」。
論文連結：https://arxiv.org/pdf/2502.00212
猜想者（conjecturer）在給定一個帶有證明的種子定理後，提出一個新的相關猜想（步驟1），而證明器（prover）則嘗試證明現有資料集中的猜想和命題（步驟2）；然後，驗證器（verifier）選擇正確的證明（步驟3）來使用標準RL訓練證明器，並識別出正確、可行、優雅但具有挑戰性的猜想來指導猜想者的訓練（步驟4）。
在每次迭代中，猜想者會在之前生成的猜想上進行訓練，生成的猜想對於當前證明器來說只能「勉強證明」，即證明器相對於其隨機種子的成功機率為一個較小的正值；迭代過程會逐漸增加猜想和證明的難度，而無需額外資料，可以看作是猜想者和證明器之間的自我博弈演算法，或是自動化的課程學習。
研究人員在Lean和Isabelle上對該方法進行了實證評估，使用DeepSeek-Prover-V1.5-SFT作為STP的基礎模型，在大約1.2億個生成的證明和200萬個生成的猜想的自我博弈訓練後，成功證明了訓練資料集LeanWorkbook中26.3%的命題，是之前專家迭代效能（13.2%）的兩倍！
在推理速度上，研究人員在公共基準測試miniF2F-test上對現有模型和使用STP訓練的最終模型進行多次獨立取樣，該模型在各種取樣預算下均顯著優於DeepSeek-Prover-V1.5模型，還在miniF2F-test（61.1%，pass@3200）、ProofNet-test（23.1%，pass@3200）和PutnamBench（8/644，pass@64）上實現了最先進的效能。
作者馬騰宇是斯坦福大學的助理教授，本科畢業於清華姚班，於普林斯頓大學獲得博士學位，研究興趣包括機器學習和深度學習，深度強化學習和高維統計。曾獲得NIPS'16最佳學生論文獎，COLT'18最佳論文獎、ACM博士論文獎榮譽獎和2021斯隆研究獎。
方法
透過有監督微調進行模型初始化
研究人員透過在現有的證明庫（例如Mathlib）上構建的監督微調（SFT）資料集，對一個通用的大型語言模型（如Llama）進行微調，初始化「猜想者」和「證明器」模型，其中證明庫包含人類編寫的已知數學定理的正式證明，每個檔案都形式化了一個相對獨立的結果，比如教科書的一章。
自博弈（self-play）訓練
第1步和第2步：生成猜想和證明
研究人員使用驗證器從證明中提取一個種子引理，去重後隨機丟棄一些頻繁出現的引理，輸入到大模型中生成猜想；隨機選擇一組猜想，其數量不超過給定資料集中剩餘未證明陳述的數量，以便證明器的計算資源在猜想和陳述之間平均分配；生成的猜想與現有資料集中未證明的陳述合併作為證明器的輸入。
在第2步證明過程，為每個陳述/猜想獨立取樣K個證明。
第3步：用Lean等驗證證明的正確性
第4步：獎勵分配
STP的主要技術難點是為猜想者設計獎勵函式，最終目標是激勵猜想者生成多樣化、相關、可行但又有一定挑戰性的猜想，以便為證明器提供足夠的訓練訊號。
研究人員首先將所有生成的猜想和證明整理成一個示例列表，使用證明器透過K個獨立生成的證明估計的（經驗）透過率來判斷猜想的挑戰性。
然後設計一個啟發式的過濾器，防止模型生成具有複雜目標的、沒有實際價值的難題，即移除最小證明長度除以猜想長度處於最低20%的猜想。
最後對選定的猜想進行重新加權，以保持猜想者的多樣性，猜想者的獎勵不能僅依賴於單獨生成的猜想，否則猜想者的最優策略可能會退化為單一分佈：將選定猜想的分佈推向現有資料集中未證明的陳述，最小化與未證明定理的均勻分佈的Wasserstein距離，以保持多個模式之間的平衡。
第5步：LLM訓練
對於證明資料集，根據對應陳述/猜想的驗證證明數量的倒數對樣本進行加權，在猜想或證明上計算加權交叉熵損失，引入長度懲罰以鼓勵生成更簡單的證明。
最終再訓練（re-training）
為了避免自博弈過程中資料分佈變化導致的訓練不穩定，研究人員從基礎模型（SFT階段之前）開始，對最終模型進行再訓練，再訓練使用的資料集包括SFT資料集以及在自博弈訓練過程中生成的所有正確證明。
證明對應命題或猜想的經驗透過率不超過1/4；對於每一個陳述或猜想，隨機保留最多16個不同的證明，以加快訓練速度。
實驗結果
研究人員使用專家迭代後的DeepSeek-Prover-V1.5-SFT作為基礎模型，訓練資料包括公共資料集（例如LeanWorkbook、miniF2F-valid、ProofNet-valid）以及其他專有資料集中的證明。運行了24次STP迭代後，總共生成了200萬條猜想、1.2億個證明和198億個token，用累積透過率（即在整個訓練過程中證明的陳述的比例）作為衡量訓練進展的主要指標。
STP、專家迭代和平行取樣方法在LeanWorkbook訓練資料集上的累積透過率實驗可以看到，STP的擴充套件效能明顯優於專家迭代。
為了在常見基準測試中取得最佳效能，研究人員還使用LeanWorkbook、miniF2F-valid和ProofNet-valid中的陳述對模型進行了額外8次迭代的訓練，與以往工作在miniF2F-test和ProofNet-test測試集相比，STP顯著優於DeepSeek-Prover-V1.5-RL，在各種推理時間樣本預算下均實現了最先進的效能。
消融實驗
生成的猜想提供了更多訓練訊號
在Isabelle實驗中，研究人員使用中間模型對LeanWorkbook中的未證明命題和生成猜想的經驗透過率進行了直方圖分析。在為79000條未證明陳述生成的250萬條證明中，只有131條是正確的，所以僅在正確證明上對模型進行微調幾乎沒有任何效果，專家迭代的效果停滯。
相比之下，STP生成的猜想具有更高的透過率，提供了更多的訓練訊號，進而實現了更好的擴充套件效能。
使用生成的猜想再訓練仍然有助於下游效能
在最終的再訓練階段，除了LeanWorkbook中成功證明的陳述之外，使用生成的猜想進行重新訓練仍然有益，即使對於在miniF2F-test和ProofNet-test上的效能也是如此，pass@128指標上大約提高了1%的效能。
參考資料：
https://arxiv.org/pdf/2502.00212
