背景

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

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

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

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

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

隨著這一過程的演進，數學家對更復雜的問題擁有更強大的工具和更深刻的理解，最終才能解決先前無法解決的困難問題。

為了解決這一問題，模擬人類數學家在進行定理證明時通常進行的分解復雜問題、引用已有知識，并積累成功證明的新定理的迭代過程，中山大學和華為等機構的研究者提出了 LEGO-Prover，實現了數學定理的生成、整理、儲存、檢索和復用的全流程閉環。

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

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

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

方法

LEGO-Prover 采取了一系列的流程來實現對定理證明的規劃、實施和可復用定理庫的收集：

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

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

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

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

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

實驗

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

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

LEGO-Prover 探索了如何以塊狀的方式證明定理。然而數據稀缺問題在定理證明這個領域內依舊非常嚴重。因此，與此同時，中山大學聯合北京大學還推出了基于三角函數的定理證明基準數據集 TRIGO (https://arxiv.org/abs/2310.10180)，發表于EMNLP 2023。

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

此外，TRIGO 還開發了基于 lean-gym 的自動生成器，用以創建不同難度和分布的數據集拆分，以全面分析模型的泛化能力。TRIGO 在定理證明領域提供了新的挑戰，同時也提供了一種研究生成式語言模型在形式和數學推理方面能力的新工具。

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

針對現有數據集的問題，FIMO 探索了使用反饋信息的自動形式化方法，使用 GPT-4 和自動、手動兩種反饋信息，將數量較為豐富的 IMO Shortlisted 候選題轉換為了 Lean 語言描述的形式語言。

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