如果想訓(xùn)練LLM證明定理的能力，你會(huì)怎么做？

既然模型可以通過(guò)海量語(yǔ)料學(xué)會(huì)生成文本，那如果我們能喂給它足夠數(shù)量的形式證明數(shù)據(jù)，定理證明能力自然水到渠成？

然而，我們看到的事實(shí)是，無(wú)論用符號(hào)形式還是自然語(yǔ)言，GPT等大模型的推理能力都不如人意。

兩句話，讓LLM邏輯推理瞬間崩潰！最新「愛(ài)麗絲夢(mèng)游仙境」曝出GPT、Claude等重大缺陷

就像GPT-4o自信表示13.11比13.8大一樣，AI再聰明卻依舊會(huì)在簡(jiǎn)單的算術(shù)上犯蠢。

然而，LLM的數(shù)學(xué)能力弱，不代表自動(dòng)化的定理證明器對(duì)數(shù)學(xué)沒(méi)用。

前段時(shí)間剛剛被破解的「忙碌海貍」問(wèn)題中，4萬(wàn)行Coq代碼功不可沒(méi)。

陶哲軒也曾在采訪中強(qiáng)調(diào)，使用Lean等自動(dòng)化工具可以徹底顛覆數(shù)學(xué)家們的工作方式。這是一股不可小覷的力量。

最近，CMU和清華的一項(xiàng)研究就致力于讓LLM的「自然語(yǔ)言思維鏈」和Lean的形式化證明結(jié)合在一起。

論文地址：https://arxiv.org/abs/2407.10040

論文提出，Lean、Coq、Isabelle等基于形式語(yǔ)言（代碼）的自動(dòng)化證明方法，忽略了大量可能對(duì)推理過(guò)程有用的「非形式化信息」。

比如，每個(gè)證明步驟之前的潛在思維過(guò)程是必不可少的，但卻不會(huì)形式化地體現(xiàn)在最終的公式和代碼中。

比如，圖1中右側(cè)的推理思路，在左側(cè)的證明步驟中完全「無(wú)處安放」。

因此，作者提出了Lean-STaR訓(xùn)練框架，讓語(yǔ)言模型既學(xué)會(huì)逐步推理的思維，也學(xué)會(huì)形式化的證明方式。

這意味著，需要將自然語(yǔ)言和形式語(yǔ)言交織在一起，也將「思考」和「證明」的過(guò)程交織在一起。

方法：Lean-STaR

顧名思義，Lean-STaR這個(gè)方法同時(shí)結(jié)合了之前的兩項(xiàng)成果——Lean和STaR。

Lean是一種函數(shù)式編程語(yǔ)言，可以用作交互式定理證明器（Interactive Theorem Prover）。

項(xiàng)目主頁(yè)：https://lean-lang.org/

這是由Leonardo de Moura在微軟研究院期間發(fā)起的開(kāi)源項(xiàng)目，目前已經(jīng)更新到Lean 4。

比如，要想形式化證明，能從n≤m推斷出n+k≤m+k，就可以用Lean寫(xiě)為如下形式（圖6）：

首先給出一種高級(jí)的「策略」（tactic，圖中所示為歸納策略k），將當(dāng)前要證明的目標(biāo)狀態(tài)簡(jiǎn)化為多個(gè)子目標(biāo)（下圖中的case 0和case ih）。

這些子目標(biāo)又會(huì)形成新的「狀態(tài)」（state）。當(dāng)所有子目標(biāo)都得到證明時(shí)，我們就給出了定理的完整證明。

STaR則是來(lái)源于斯坦福和谷歌研究院在2022年發(fā)表的一篇論文，全稱是「自學(xué)推理器」（Self-Taught Reasoner）。

論文地址：https://arxiv.org/abs/2203.14465

其基本思想就是用到了「自舉法」（bootstrapping）。

首先根據(jù)訓(xùn)練數(shù)據(jù)中的問(wèn)題和答案，提示語(yǔ)言模型，生成能解釋答案的「原理」（rationale）。

之后，再用這個(gè)包含了問(wèn)題、答案和原理的混合數(shù)據(jù)集對(duì)LM進(jìn)行微調(diào)，提升模型的推理能力（圖1）。

Lean-STaR模型的微調(diào)也是采用了「漸進(jìn)優(yōu)化」的思路，逐步將以上兩個(gè)相關(guān)工作的成果融合在一起，完善底層的策略預(yù)測(cè)模型。模型構(gòu)建的流水線如圖4所示。

直接策略預(yù)測(cè)（Direct Tactic Prediction）

首先，將定理證明問(wèn)題簡(jiǎn)單地定義為馬爾科夫決策過(guò)程（MDP）。

從這個(gè)角度來(lái)看，證明過(guò)程是狀態(tài)s_i、策略a_i和獎(jiǎng)勵(lì)r_i∈R等3個(gè)變量組成的軌跡(s₁，a₁，r₁) (s₂，a₂，r₂)?其中，ITP（比如Lean）用于提供每個(gè)新?tīng)顟B(tài)s_i+1。

在這種經(jīng)典設(shè)置中，證明定理的過(guò)程包括向LM提供狀態(tài)s，讓模型M生成策略??_???(??|??) 。

因此，可以使用僅包含成功證明軌跡的基本數(shù)據(jù)集

對(duì)基本模型進(jìn)行監(jiān)督微調(diào)，得到SFT模型。

思維增強(qiáng)策略預(yù)測(cè)（Thought-augmented Tactic Prediction）

結(jié)合之前所述的研究動(dòng)機(jī)，我們假設(shè)「潛在想法」可以提高模型的策略預(yù)測(cè)能力，因此引入一個(gè)表示「思維」的隱變量t_i，然后將模型擴(kuò)展為：

此時(shí)，根據(jù)狀態(tài)預(yù)測(cè)下一個(gè)策略的分布可以表示為：

如果用這種方式預(yù)測(cè)，我們就需要一個(gè)全新的數(shù)據(jù)集

用于訓(xùn)練模型M，然而Lean給出的證明步驟只包含s_i和a_i。

論文的解決方法是：借助一個(gè)強(qiáng)大的語(yǔ)言模型G（如GPT-4）作為「預(yù)言家」，讓它在給定當(dāng)前狀態(tài)s_i和真實(shí)策略a_i的情況下生成t_i，從而創(chuàng)建出新的數(shù)據(jù)集D_T（即圖4中的CoT Dataset）。

作者將這種方法稱為「回顧性原理生成」（retrospective rationale generation）。

將SFT模型在D_T數(shù)據(jù)集上再進(jìn)行一次微調(diào)后，就得到了第一個(gè)思維增強(qiáng)的策略預(yù)測(cè)模型Lean-CoT。

自舉思維增強(qiáng)定理證明（Bootstrapping Thought-augmented Theorem Proving）

在Lean-CoT模型的基礎(chǔ)上，作者提出，可以應(yīng)用「專家迭代」（expert iteration）方法進(jìn)一步提升性能。

具體來(lái)說(shuō)，從初始的Lean-CoT模型M₀以及初始數(shù)據(jù)集D開(kāi)始，讓M₀對(duì)每個(gè)問(wèn)題進(jìn)行K次采樣，每次采樣都會(huì)產(chǎn)生一個(gè)證明軌跡 [(s₀,t₀,a₀),(s₁,t₁,a₁),?,(s_n,t_n,a_n)]，之后過(guò)濾出成功的證明軌跡并去重，得到新數(shù)據(jù)集D₁。

接下來(lái)，在數(shù)據(jù)集D_T∪D₁上進(jìn)一步微調(diào)M₀模型以得到Lean-STaR模型M₁。

將上述過(guò)程進(jìn)行多次迭代，即可不斷更新Lean-STaR模型。

評(píng)估實(shí)驗(yàn)

為了測(cè)試Lean-STaR的具體性能，研究使用了可用的最佳開(kāi)放語(yǔ)言模型Lean語(yǔ)料庫(kù) (InternLM2-Math-base-7b) 上進(jìn)行預(yù)訓(xùn)練，并遵循Lean的Mathlib作為底層訓(xùn)練集的標(biāo)準(zhǔn)實(shí)踐。

首先以LeanDojo Benchmark 4 v9作為監(jiān)督微調(diào)(SFT)數(shù)據(jù)集，包含超過(guò)23.1萬(wàn)個(gè)示例，進(jìn)行1輪微調(diào)以獲得SFT模型。

之后從數(shù)據(jù)集中隨機(jī)選擇17256個(gè)不同的成功證明軌跡，并使用GPT-4-0125模型注釋出52438個(gè)想法，并且執(zhí)行兩次專家迭代。

實(shí)驗(yàn)在MiniF2F基準(zhǔn)上評(píng)估Lean-STaR，使用了與之前的實(shí)驗(yàn)工作類似的評(píng)估設(shè)置，但主要使用的是采樣方法（sampling）而不是最佳優(yōu)先搜索（best-first search）來(lái)進(jìn)行評(píng)估。

實(shí)驗(yàn)結(jié)果表明，回顧性原理生成和專家迭代都顯著提高了模型的定理證明能力。

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

實(shí)驗(yàn)的主要結(jié)果如下表所示，Lean-STaR比之前基于Lean的SOTA模型有了顯著的改進(jìn)。

例如，在類似的推理預(yù)算下，同樣使用best-first search，Lean-STaR從InternLM2的30.3%提升至34.8%，也同樣高于使用GPT-4的COPRA（30.7%）。

隨著計(jì)算預(yù)算的增加，Lean-STAR的性能進(jìn)一步提升至36.1%。

思維增強(qiáng)改進(jìn)定理證明

Lean-STaR的第一階段在思維增強(qiáng)的合成數(shù)據(jù)集上進(jìn)行微調(diào)，訓(xùn)練模型來(lái)交替生成思維和策略。

此階段的微調(diào)模型（在表1中表示為L(zhǎng)ean-CoT）達(dá)到了32.8%的通過(guò)率，高于此階段之前的模型（表示為 SFT，29.5%）。

可以證明，第一階段的思維增強(qiáng)能提高語(yǔ)言模型的定理證明能力，即使對(duì)于已經(jīng)專門用于生成Lean策略的語(yǔ)言模型（例如SFT）也依舊成立。

自舉法（Bootstrapping）進(jìn)一步改進(jìn)

Lean-STaR的第二階段包括使用當(dāng)前語(yǔ)言模型生成新的思維和策略，保存正確結(jié)果，并結(jié)合初始數(shù)據(jù)集進(jìn)行訓(xùn)練。

從表1結(jié)果來(lái)看，每次迭代都會(huì)提高模型的定理證明性能，從32.8%（初始模型）到34%（迭代1次后的L-STR）再到34.8%（迭代2次后的L-STR）。

此外，我們發(fā)現(xiàn)該模型可以通過(guò)額外采樣進(jìn)一步改進(jìn)，將采樣的K值加倍后，分?jǐn)?shù)能進(jìn)一步提升至36.1%。

無(wú)CoT的專家迭代實(shí)驗(yàn)

表5顯示了沒(méi)有CoT的專家迭代結(jié)果（即僅使用狀態(tài)和策略，沒(méi)有思維增強(qiáng)），對(duì)比Lean-CoT和Lean-STaR的表現(xiàn)。

僅用專家迭代時(shí)，準(zhǔn)確率就達(dá)到了43.0%，低于Lean-STaR (45.5%)。

這表明Lean-STaR的性能提升不僅僅來(lái)自于專家迭代的使用，思維增強(qiáng)也有不可忽略的效果。

問(wèn)題類型與難度

MiniF2F-test中的問(wèn)題有多個(gè)來(lái)源，包括AIME、AMC、IMO等數(shù)學(xué)競(jìng)賽以及MATH數(shù)據(jù)集，并進(jìn)行了手動(dòng)形式化處理。

這些問(wèn)題可能有不同的難度和類型。表2展示了成功證明的問(wèn)題數(shù)量，按類型和難度劃分。

Lean-CoT提高了解決所有類別難題的表現(xiàn)，尤其是數(shù)學(xué)競(jìng)賽中的難題。

除了這些改進(jìn)之外，Lean-STAR的改進(jìn)主要集中在數(shù)論方面。

搜索和抽樣預(yù)算

表4說(shuō)明了問(wèn)題通過(guò)率與搜索規(guī)模或抽樣預(yù)算S×K的關(guān)系。

實(shí)驗(yàn)發(fā)現(xiàn)，Lean-STAR性能與K值的大小成正比，特別是當(dāng)K值相對(duì)較大時(shí)。

對(duì)比前兩列和Lean-STaR可以發(fā)現(xiàn)，附帶思維的額外采樣能提高定理證明性能，而沒(méi)有思維的額外采樣可能會(huì)飽和。

作者猜測(cè)，可能是因?yàn)椤杆季S」增加了輸出的多樣性，并有助于對(duì)定理證明空間進(jìn)行探索。

因此，Lean-STaR更具可擴(kuò)展性（就推理階段算力而言），并且可以通過(guò)額外的專家迭代進(jìn)一步改進(jìn)。

更強(qiáng)基礎(chǔ)模型和更多數(shù)據(jù)實(shí)驗(yàn)

實(shí)驗(yàn)還使用了更強(qiáng)的語(yǔ)言模型InternLM2-Math-plus-7b訓(xùn)練LeanSTaR，來(lái)測(cè)試不同語(yǔ)言模型性能的影響。

不僅基座模型更強(qiáng)，為數(shù)據(jù)集注釋「思維」的模型也從GPT-4升級(jí)到GPT-4o，生成了1.4萬(wàn)條想法。

實(shí)驗(yàn)只執(zhí)行一次專家迭代，收集了大約6萬(wàn)條（證明狀態(tài)、思維、下一步策略）正確的數(shù)據(jù)，命名為「STaR 數(shù)據(jù)集」。

在STaR數(shù)據(jù)集上進(jìn)一步微調(diào)得到Lean-STAR模型，其測(cè)評(píng)結(jié)果如表3所示，可以看到Lean-STaR仍然比基線有了顯著的改進(jìn)。

結(jié)論和局限性

研究團(tuán)隊(duì)提出了Lean-STaR，這是一種新穎的方法，通過(guò)將思維鏈 (CoT) 原理集成到每個(gè)證明步驟中，顯著增強(qiáng)了語(yǔ)言模型用形式化數(shù)學(xué)語(yǔ)言進(jìn)行定理證明的能力。

方法首先根據(jù)ground truth回顧性地為證明步驟生成「原理」，然后微調(diào)語(yǔ)言模型，訓(xùn)練模型學(xué)會(huì)生成「原理」并預(yù)測(cè)后續(xù)策略，從而得到Lean-CoT模型。

然后使用專家迭代進(jìn)一步改進(jìn)該模型，根據(jù)被證明為正確的采樣結(jié)果進(jìn)行微調(diào)，并使用Lean solver進(jìn)行驗(yàn)證。

研究的貢獻(xiàn)包括引入第一個(gè)思維增強(qiáng)的定理證明數(shù)據(jù)集，并證明專家迭代可以進(jìn)一步提高性能。得到的模型在miniF2F測(cè)試上取得最新SOTA，將通過(guò)率從30.3%提高到36.1%。

這些進(jìn)步不僅提高了自動(dòng)化定理證明的準(zhǔn)確性，而且還提供了一個(gè)可擴(kuò)展且高效的框架來(lái)促進(jìn)對(duì)數(shù)學(xué)的理解，這可能會(huì)對(duì)教育、科學(xué)發(fā)現(xiàn)和程序驗(yàn)證產(chǎn)生重大影響。

方法的主要限制在于，其性能可能受限于計(jì)算可擴(kuò)展性，實(shí)驗(yàn)中用于微調(diào)Lean-CoT和Lean-STaR模型的數(shù)據(jù)集都不是很大。

需要注意的是，專家迭代的速度也存在嚴(yán)重瓶頸，會(huì)受限于Lean ITP的緩慢進(jìn)程。

此外，使用GPT-4生成合成數(shù)據(jù)成本較大，并可能引入偏差。