大型語(yǔ)言模型的「推理能力」現(xiàn)在成了NLP皇冠上的明珠，其核心難題在于「缺乏高質(zhì)量訓(xùn)練數(shù)據(jù)」，標(biāo)注數(shù)據(jù)需要領(lǐng)域?qū)＜遥杀痉浅８甙呵译y以擴(kuò)展；現(xiàn)有高等數(shù)學(xué)論文和定理的數(shù)量也非常有限，遠(yuǎn)少于其他任務(wù)的數(shù)據(jù)源。

DeepSeek-Prover和DeepSeek R1等模型的思路非常巧妙，在沒有逐步解決方案的數(shù)據(jù)集（如定理命題）上進(jìn)行強(qiáng)化學(xué)習(xí)，可以極大提升其推理能力；和專家迭代（expert iteration）類似，交替進(jìn)行「LLMs生成證明」和「正確生成的證明上進(jìn)行微調(diào)」，部分緩解了數(shù)據(jù)稀缺（data scarcity）的問題。

不過，強(qiáng)化學(xué)習(xí)和專家迭代都存在一個(gè)嚴(yán)重問題：通過率（pass rate）過低，對(duì)「未證明的定理」生成「正確證明」所需的樣本量呈指數(shù)級(jí)增長(zhǎng)，大量的計(jì)算資源被浪費(fèi)在生成錯(cuò)誤的證明上，無法為模型提供訓(xùn)練信號(hào)。

比如在LeanWorkbook上的通過率為13.2%，其中98.5%的計(jì)算資源都浪費(fèi)在生成錯(cuò)誤證明上了，也就是說，在經(jīng)過幾輪專家迭代后，由于缺乏新的成功證明，重新訓(xùn)練模型的效果會(huì)大大降低。

此外，強(qiáng)化學(xué)習(xí)從原理上就受到訓(xùn)練數(shù)據(jù)集中「定理難度水平」的限制，一個(gè)模型不可能從「解決高中水平的問題」中學(xué)習(xí)到「大學(xué)水平的證明技巧」，也無法解決「開放性」的數(shù)學(xué)問題，需要持續(xù)收集高水平的定理命題和數(shù)學(xué)問題。

斯坦福的研究人員提出了一個(gè)自博弈定理證明器（STP），模仿數(shù)學(xué)家學(xué)習(xí)和發(fā)展數(shù)學(xué)的方式，同時(shí)承擔(dān)兩個(gè)角色（猜想者和證明器），互相提供訓(xùn)練信號(hào)，可以在「有限數(shù)據(jù)」的情況下「無限運(yùn)行并自我改進(jìn)」。

論文鏈接：https://arxiv.org/pdf/2502.00212

猜想者（conjecturer）在給定一個(gè)帶有證明的種子定理后，提出一個(gè)新的相關(guān)猜想（步驟1），而證明器（prover）則嘗試證明現(xiàn)有數(shù)據(jù)集中的猜想和命題（步驟2）；然后，驗(yàn)證器（verifier）選擇正確的證明（步驟3）來使用標(biāo)準(zhǔn)RL訓(xùn)練證明器，并識(shí)別出正確、可行、優(yōu)雅但具有挑戰(zhàn)性的猜想來指導(dǎo)猜想者的訓(xùn)練（步驟4）。

在每次迭代中，猜想者會(huì)在之前生成的猜想上進(jìn)行訓(xùn)練，生成的猜想對(duì)于當(dāng)前證明器來說只能「勉強(qiáng)證明」，即證明器相對(duì)于其隨機(jī)種子的成功概率為一個(gè)較小的正值；迭代過程會(huì)逐漸增加猜想和證明的難度，而無需額外數(shù)據(jù)，可以看作是猜想者和證明器之間的自我博弈算法，或是自動(dòng)化的課程學(xué)習(xí)。

研究人員在Lean和Isabelle上對(duì)該方法進(jìn)行了實(shí)證評(píng)估，使用DeepSeek-Prover-V1.5-SFT作為STP的基礎(chǔ)模型，在大約1.2億個(gè)生成的證明和200萬個(gè)生成的猜想的自我博弈訓(xùn)練后，成功證明了訓(xùn)練數(shù)據(jù)集LeanWorkbook中26.3%的命題，是之前專家迭代性能（13.2%）的兩倍！

在推理速度上，研究人員在公共基準(zhǔn)測(cè)試miniF2F-test上對(duì)現(xiàn)有模型和使用STP訓(xùn)練的最終模型進(jìn)行多次獨(dú)立采樣，該模型在各種采樣預(yù)算下均顯著優(yōu)于DeepSeek-Prover-V1.5模型，還在miniF2F-test（61.1%，pass@3200）、ProofNet-test（23.1%，pass@3200）和PutnamBench（8/644，pass@64）上實(shí)現(xiàn)了最先進(jìn)的性能。

作者馬騰宇是斯坦福大學(xué)的助理教授，本科畢業(yè)于清華姚班，于普林斯頓大學(xué)獲得博士學(xué)位，研究興趣包括機(jī)器學(xué)習(xí)和深度學(xué)習(xí)，深度強(qiáng)化學(xué)習(xí)和高維統(tǒng)計(jì)。曾獲得NIPS'16最佳學(xué)生論文獎(jiǎng)，COLT'18最佳論文獎(jiǎng)、ACM博士論文獎(jiǎng)榮譽(yù)獎(jiǎng)和2021斯隆研究獎(jiǎng)。

方法

通過有監(jiān)督微調(diào)進(jìn)行模型初始化

研究人員通過在現(xiàn)有的證明庫(kù)（例如Mathlib）上構(gòu)建的監(jiān)督微調(diào)（SFT）數(shù)據(jù)集，對(duì)一個(gè)通用的大型語(yǔ)言模型（如Llama）進(jìn)行微調(diào)，初始化「猜想者」和「證明器」模型，其中證明庫(kù)包含人類編寫的已知數(shù)學(xué)定理的正式證明，每個(gè)文件都形式化了一個(gè)相對(duì)獨(dú)立的結(jié)果，比如教科書的一章。

自博弈（self-play）訓(xùn)練

第1步和第2步：生成猜想和證明

研究人員使用驗(yàn)證器從證明中提取一個(gè)種子引理，去重后隨機(jī)丟棄一些頻繁出現(xiàn)的引理，輸入到大模型中生成猜想；隨機(jī)選擇一組猜想，其數(shù)量不超過給定數(shù)據(jù)集中剩余未證明陳述的數(shù)量，以便證明器的計(jì)算資源在猜想和陳述之間平均分配；生成的猜想與現(xiàn)有數(shù)據(jù)集中未證明的陳述合并作為證明器的輸入。

在第2步證明過程，為每個(gè)陳述/猜想獨(dú)立采樣K個(gè)證明。

第3步：用Lean等驗(yàn)證證明的正確性

第4步：獎(jiǎng)勵(lì)分配

STP的主要技術(shù)難點(diǎn)是為猜想者設(shè)計(jì)獎(jiǎng)勵(lì)函數(shù)，最終目標(biāo)是激勵(lì)猜想者生成多樣化、相關(guān)、可行但又有一定挑戰(zhàn)性的猜想，以便為證明器提供足夠的訓(xùn)練信號(hào)。

研究人員首先將所有生成的猜想和證明整理成一個(gè)示例列表，使用證明器通過K個(gè)獨(dú)立生成的證明估計(jì)的（經(jīng)驗(yàn)）通過率來判斷猜想的挑戰(zhàn)性。

然后設(shè)計(jì)一個(gè)啟發(fā)式的過濾器，防止模型生成具有復(fù)雜目標(biāo)的、沒有實(shí)際價(jià)值的難題，即移除最小證明長(zhǎng)度除以猜想長(zhǎng)度處于最低20%的猜想。

最后對(duì)選定的猜想進(jìn)行重新加權(quán)，以保持猜想者的多樣性，猜想者的獎(jiǎng)勵(lì)不能僅依賴于單獨(dú)生成的猜想，否則猜想者的最優(yōu)策略可能會(huì)退化為單一分布：將選定猜想的分布推向現(xiàn)有數(shù)據(jù)集中未證明的陳述，最小化與未證明定理的均勻分布的Wasserstein距離，以保持多個(gè)模式之間的平衡。

第5步：LLM訓(xùn)練

對(duì)于證明數(shù)據(jù)集，根據(jù)對(duì)應(yīng)陳述/猜想的驗(yàn)證證明數(shù)量的倒數(shù)對(duì)樣本進(jìn)行加權(quán)，在猜想或證明上計(jì)算加權(quán)交叉熵?fù)p失，引入長(zhǎng)度懲罰以鼓勵(lì)生成更簡(jiǎn)單的證明。

最終再訓(xùn)練（re-training）

為了避免自博弈過程中數(shù)據(jù)分布變化導(dǎo)致的訓(xùn)練不穩(wěn)定，研究人員從基礎(chǔ)模型（SFT階段之前）開始，對(duì)最終模型進(jìn)行再訓(xùn)練，再訓(xùn)練使用的數(shù)據(jù)集包括SFT數(shù)據(jù)集以及在自博弈訓(xùn)練過程中生成的所有正確證明。

證明對(duì)應(yīng)命題或猜想的經(jīng)驗(yàn)通過率不超過1/4；對(duì)于每一個(gè)陳述或猜想，隨機(jī)保留最多16個(gè)不同的證明，以加快訓(xùn)練速度。

實(shí)驗(yàn)結(jié)果

研究人員使用專家迭代后的DeepSeek-Prover-V1.5-SFT作為基礎(chǔ)模型，訓(xùn)練數(shù)據(jù)包括公共數(shù)據(jù)集（例如LeanWorkbook、miniF2F-valid、ProofNet-valid）以及其他專有數(shù)據(jù)集中的證明。運(yùn)行了24次STP迭代后，總共生成了200萬條猜想、1.2億個(gè)證明和198億個(gè)token，用累積通過率（即在整個(gè)訓(xùn)練過程中證明的陳述的比例）作為衡量訓(xùn)練進(jìn)展的主要指標(biāo)。

STP、專家迭代和平行采樣方法在LeanWorkbook訓(xùn)練數(shù)據(jù)集上的累積通過率實(shí)驗(yàn)可以看到，STP的擴(kuò)展性能明顯優(yōu)于專家迭代。

為了在常見基準(zhǔn)測(cè)試中取得最佳性能，研究人員還使用LeanWorkbook、miniF2F-valid和ProofNet-valid中的陳述對(duì)模型進(jìn)行了額外8次迭代的訓(xùn)練，與以往工作在miniF2F-test和ProofNet-test測(cè)試集相比，STP顯著優(yōu)于DeepSeek-Prover-V1.5-RL，在各種推理時(shí)間樣本預(yù)算下均實(shí)現(xiàn)了最先進(jìn)的性能。

消融實(shí)驗(yàn)

生成的猜想提供了更多訓(xùn)練信號(hào)

在Isabelle實(shí)驗(yàn)中，研究人員使用中間模型對(duì)LeanWorkbook中的未證明命題和生成猜想的經(jīng)驗(yàn)通過率進(jìn)行了直方圖分析。在為79000條未證明陳述生成的250萬條證明中，只有131條是正確的，所以僅在正確證明上對(duì)模型進(jìn)行微調(diào)幾乎沒有任何效果，專家迭代的效果停滯。

相比之下，STP生成的猜想具有更高的通過率，提供了更多的訓(xùn)練信號(hào)，進(jìn)而實(shí)現(xiàn)了更好的擴(kuò)展性能。

使用生成的猜想再訓(xùn)練仍然有助于下游性能

在最終的再訓(xùn)練階段，除了LeanWorkbook中成功證明的陳述之外，使用生成的猜想進(jìn)行重新訓(xùn)練仍然有益，即使對(duì)于在miniF2F-test和ProofNet-test上的性能也是如此，pass@128指標(biāo)上大約提高了1%的性能。