背景

作為長鏈條嚴(yán)格推理的典范，數(shù)學(xué)推理被認(rèn)為是衡量語言模型推理能力的重要基準(zhǔn)，GSM8K 和 MATH 等數(shù)學(xué)文字問題（math word problem）數(shù)據(jù)集被廣泛應(yīng)用于語言模型的測評(píng)和比較中。事實(shí)上，數(shù)學(xué)作為一項(xiàng)科學(xué)研究并不僅僅包括計(jì)算具體實(shí)例，還包括推演一般性的定理。不同于簡單的計(jì)算問題僅僅需要驗(yàn)證最終的結(jié)果與答案是否匹配，定理的證明要求對數(shù)學(xué)概念擁有更嚴(yán)格的理解，而這種定理證明的正確性是難以通過直接的自然語言生成和判別或是簡單的程序調(diào)用就能夠完成的。

正如自然語言處理希望能夠使用計(jì)算機(jī)直接對人類語言進(jìn)行數(shù)字化計(jì)算一樣，對于數(shù)學(xué)對象的數(shù)字化也有著數(shù)十年的探索，甚至現(xiàn)代形式邏輯的誕生在很大程度上也正是源于對數(shù)學(xué)命題進(jìn)行演算的想法。從事形式化驗(yàn)證的計(jì)算機(jī)科學(xué)家致力于為數(shù)學(xué)論述構(gòu)造表達(dá)自然且計(jì)算高效的形式語言和證明驗(yàn)證器，人工編寫的形式化數(shù)學(xué)代碼在通過計(jì)算機(jī)的形式化驗(yàn)證后被認(rèn)為具有高度的嚴(yán)格性。然而，這一過程需要大量的人工成本，著名的 Flyspeck project 甚至花費(fèi)了二十年的時(shí)間才完成開普勒猜想的證明，而自動(dòng)化的證明搜索算法則面臨著搜索空間的組合爆炸問題，導(dǎo)致非平凡的定理證明往往超出了當(dāng)前的計(jì)算能力限制。

深度學(xué)習(xí)的發(fā)展為形式化數(shù)學(xué)和自動(dòng)定理證明提供了新的機(jī)遇。近年來，一種名為神經(jīng)定理證明（neural theorem proving）的新范式以兩種方式嘗試將神經(jīng)網(wǎng)絡(luò)與形式定理證明相結(jié)合：使用神經(jīng)網(wǎng)絡(luò)對數(shù)學(xué)庫中的定理和當(dāng)前的證明目標(biāo)分別進(jìn)行向量表征并進(jìn)行匹配，篩選出最可能被使用的定理，幫助純符號(hào)計(jì)算的自動(dòng)定理證明器縮小證明搜索空間；或者將證明目標(biāo)作為提示輸入語言模型，使其直接生成相應(yīng)的形式化數(shù)學(xué)證明代碼，再使用相應(yīng)的形式化驗(yàn)證器來判斷該證明的正確性，這種直接代替人類編碼者完成主要證明內(nèi)容書寫的直接模式在大語言模型取得突破后備受關(guān)注。

然而，與數(shù)學(xué)文字問題一樣，當(dāng)前進(jìn)行定理證明的方法通常是 “一次性的”，也即推理過程和中間結(jié)論僅僅作為通向最終證明的臨時(shí)性路徑，在完成證明的驗(yàn)證后即被丟棄、并不對后續(xù)的定理證明產(chǎn)生貢獻(xiàn)。這種方式更像是對大語言模型進(jìn)行靜態(tài)測試，而沒有對其能力的持續(xù)提升做出貢獻(xiàn)。

事實(shí)上，數(shù)學(xué)的發(fā)展并不僅僅是簡單的重復(fù)嘗試解題，還包括從實(shí)例中「抽象」出普遍的數(shù)學(xué)結(jié)構(gòu)和定理、從特殊的定理推廣到一般的定理和根據(jù)已有的定理演繹地「推出」新的結(jié)論。

隨著這一過程的演進(jìn)，數(shù)學(xué)家對更復(fù)雜的問題擁有更強(qiáng)大的工具和更深刻的理解，最終才能解決先前無法解決的困難問題。

為了解決這一問題，模擬人類數(shù)學(xué)家在進(jìn)行定理證明時(shí)通常進(jìn)行的分解復(fù)雜問題、引用已有知識(shí)，并積累成功證明的新定理的迭代過程，中山大學(xué)和華為等機(jī)構(gòu)的研究者提出了 LEGO-Prover，實(shí)現(xiàn)了數(shù)學(xué)定理的生成、整理、儲(chǔ)存、檢索和復(fù)用的全流程閉環(huán)。

LEGO-Prover 使 GPT-3.5 在形式化定理證明數(shù)據(jù)集 miniF2F-valid（證明成功率從 48.0% 提高到 57.0%）和 miniF2F-test（證明成功率從 45.5% 提高到 50.0%）上都達(dá)到了新的 SOTA。在證明過程中，LEGO-Prover 還成功地生成了超過 20,000 個(gè)引理并將它們添加到了不斷增長的定理庫中。

消融研究表明，這些新添加的技能確實(shí)對證明定理有幫助，在 miniF2F-valid 上的證明成功率從 47.1% 提高到 50.4%。

• 論文地址：https://arxiv.org/abs/2310.00656
• 代碼地址：https://github.com/wiio12/LEGO-Prover

方法

LEGO-Prover 采取了一系列的流程來實(shí)現(xiàn)對定理證明的規(guī)劃、實(shí)施和可復(fù)用定理庫的收集：

1. 給定一個(gè)以自然語言描述的數(shù)學(xué)定理及其人類編寫的形式化描述，使用 GPT-3.5（informal solver）直接生成的自然語言證明。

2. 使用分解器（decomposer）將這一自然語言證明分解為具體的證明步驟，并以引理的形式對這些證明步驟中的子目標(biāo)進(jìn)行對應(yīng)的形式語言描述（作為檢索的 request）。

3. 利用這些以形式語言描述的子目標(biāo)嘗試從定理庫（也即 skill library）中檢索相關(guān)的已證明定理，將其與上述內(nèi)容一同輸入 GPT-3.5（formalizer），在這些提示的基礎(chǔ)上進(jìn)行目標(biāo)定理的形式化證明，并使用形式化驗(yàn)證器檢驗(yàn)證明的正確性。

4. 從通過驗(yàn)證的形式化證明中，提取出除目標(biāo)定理外的其他通過驗(yàn)證的定理（或引理）和在分解過程后得到的子目標(biāo)形式語言描述，對它們進(jìn)行 embedding 后加入到維護(hù)的定理庫中。

此外，LEGO-Prover 還對定理庫進(jìn)行了專門的整理和維護(hù)流程，對分解過程中收集到的子目標(biāo)進(jìn)行單獨(dú)的證明嘗試，通過多種類別的 prompt 引導(dǎo) GPT-3.5 對證明過程中收集到的成功證明的定理進(jìn)行演化，從具體的證明實(shí)例抽象出一般的數(shù)學(xué)命題，以增進(jìn)定理庫中命題的多樣性、概括性和可復(fù)用性：

實(shí)驗(yàn)

實(shí)驗(yàn)表明，這些演化得到的新定理在后續(xù)的定理證明中起到了關(guān)鍵性的作用，miniF2F 數(shù)據(jù)集中的許多定理都是在利用這些從定理庫中抽取得到的結(jié)果才得以證明的。使用收集和演化得到的定理庫后，LEGO-Prover 的證明成功率從 47.1% 提高到 50.4%，而在使用定理庫的情形下，有 24% 的問題是在技能庫的幫助下完成的，這表明技能庫的使用對于大語言模型進(jìn)行定理證明任務(wù)而言幫助很大。此外，使用定理庫技術(shù)的優(yōu)勢在較小的嘗試次數(shù)下具有較高的比例，表明這一方法對于計(jì)算資源相當(dāng)有限的情形下具有相當(dāng)可觀的使用價(jià)值。

最后，實(shí)驗(yàn)結(jié)果表明 LEGO-Prover 在 miniF2F 數(shù)據(jù)集上的證明成功率顯著優(yōu)于基于先前的方法。使用人類編寫的證明，LEGO-Prover 在驗(yàn)證集和測試集上的證明成功率分別比先前最好的方法高出 19% 和 3.5%。當(dāng)使用模型生成的非正式證明替代人類編寫的非正式證明時(shí)，LEGO-Prover 在驗(yàn)證集上的證明成功率仍然達(dá)到了 52.4%，接近于使用人類編寫的非正式證明的證明成功率 55.3%。

LEGO-Prover 探索了如何以塊狀的方式證明定理。然而數(shù)據(jù)稀缺問題在定理證明這個(gè)領(lǐng)域內(nèi)依舊非常嚴(yán)重。因此，與此同時(shí)，中山大學(xué)聯(lián)合北京大學(xué)還推出了基于三角函數(shù)的定理證明基準(zhǔn)數(shù)據(jù)集 TRIGO (https://arxiv.org/abs/2310.10180)，發(fā)表于EMNLP 2023。

TRIGO 對自動(dòng)引理生成以及如何從合成的引理數(shù)據(jù)的分布泛化到真實(shí)世界數(shù)據(jù)的分布進(jìn)行了進(jìn)一步的探索。當(dāng)前的自動(dòng)定理證明數(shù)據(jù)集主要側(cè)重于符號(hào)推理，很少涉及復(fù)雜數(shù)字組合推理的理解。TRIGO 不僅要求模型通過逐步證明來簡化三角函數(shù)表達(dá)式，還評(píng)估了生成式語言模型在公式和數(shù)字術(shù)語的操作、分組和因式分解方面的推理能力。研究團(tuán)隊(duì)從網(wǎng)絡(luò)上收集了三角函數(shù)表達(dá)式及其簡化形式，人工標(biāo)注了簡化過程，然后將其轉(zhuǎn)化為 LEAN 形式系統(tǒng)下的語言。在有一定的來自于真實(shí)世界的形式化定理數(shù)據(jù)后，研究團(tuán)隊(duì)利用引理生成器，從已標(biāo)注的樣本中初始化 Lean-gym 來自動(dòng)生成新的引理以擴(kuò)展數(shù)據(jù)集。

此外，TRIGO 還開發(fā)了基于 lean-gym 的自動(dòng)生成器，用以創(chuàng)建不同難度和分布的數(shù)據(jù)集拆分，以全面分析模型的泛化能力。TRIGO 在定理證明領(lǐng)域提供了新的挑戰(zhàn)，同時(shí)也提供了一種研究生成式語言模型在形式和數(shù)學(xué)推理方面能力的新工具。

此外，為了探索定理證明模型的能力在更難的數(shù)據(jù)集上的表現(xiàn)，中山大學(xué)聯(lián)合北京大學(xué)還提出了 FIMO 基準(zhǔn)數(shù)據(jù)集（https://arxiv.org/abs/2309.04295）。形式化數(shù)學(xué)數(shù)據(jù)稀缺，手工形式化成本非常高昂。當(dāng)前主流的數(shù)據(jù)集主要聚焦于初高中水平的應(yīng)用題，難度普遍偏低，對于 IMO 等需要高水平解題技巧的數(shù)學(xué)競賽題目關(guān)注較少，而且常常不包括自然語言題解。

針對現(xiàn)有數(shù)據(jù)集的問題，F(xiàn)IMO 探索了使用反饋信息的自動(dòng)形式化方法，使用 GPT-4 和自動(dòng)、手動(dòng)兩種反饋信息，將數(shù)量較為豐富的 IMO Shortlisted 候選題轉(zhuǎn)換為了 Lean 語言描述的形式語言。

實(shí)驗(yàn)結(jié)果表明，反饋機(jī)制的加入大大緩解了先前自動(dòng)形式化的語法錯(cuò)誤和語義錯(cuò)誤，顯著提升了自動(dòng)形式化的成功率（32.6%→60.8），成功形式化了 89 道代數(shù)和 60 道數(shù)論的高難度題目。進(jìn)一步的實(shí)驗(yàn)表明，雖然 GPT-4 無法直接生成 IMO 級(jí)別題目的形式化題解，但是它可以跟隨自然語言答案的解題思路，暗示了使用自然語言輔助機(jī)器定理證明的可能性。