大型語言模型的「推理能力」現在成了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%的性能。