本文第一作者為香港大學博士研究生趙學亮，主要研究方向為形式化數學定理證明，檢索增強生成以及多模態(tài)推理。該工作由香港大學與 AI 芯片公司 SambaNova Systems 共同完成。

背景介紹：形式化定理證明的新挑戰(zhàn)

大語言模型（LLMs）在形式化定理證明中正面臨兩個核心挑戰(zhàn)：

1. 形式化證明數據的稀缺性：當前數據集有限，難以支持模型在專門的數學和定理證明任務中的高效學習。

2. 多步驟推理的復雜性：形式化定理證明要求模型在多個步驟中保持邏輯嚴謹性，以生成正確的數學證明。

在這種背景下，研究團隊提出了一個全新的框架：SubgoalXL，結合了子目標（subgoal）證明策略與專家學習（expert learning）方法，在 Isabelle 中實現了形式化定理證明的性能突破。

• 論文鏈接：https://www.arxiv.org/abs/2408.11172
• 項目地址：https://github.com/zhaoxlpku/SubgoalXL

SubgoalXL 如何應對挑戰(zhàn)？

SubgoalXL 通過以下兩種關鍵策略來應對形式化定理證明中的挑戰(zhàn)：

1. 子目標證明策略：將證明過程分解為多個子目標，這些子目標構成了解決復雜推理任務的關鍵步驟。通過這種分解，SubgoalXL 在更接近形式化證明的邏輯框架下進行推理，使得生成的證明過程更加清晰有序。子目標證明策略有效地緩解了因非形式化與形式化證明之間的不一致性導致的學習瓶頸，增強了模型在形式化環(huán)境中的表現。

2. 專家學習框架：通過一個由形式化陳述生成器、子目標生成器和形式化證明生成器組成的迭代優(yōu)化框架，SubgoalXL 能夠在每個迭代過程中從經驗數據中學習，調整各個組件的參數，使得模型在多步驟推理中的準確性和有效性不斷提升。該框架利用概率建模和梯度估計技術，確保在每個迭代中從最優(yōu)分布中采樣數據，最大化模型的學習效率和推理能力。

方法概述

SubgoalXL 的方法核心在于子目標證明策略和專家學習框架的結合。

子目標證明策略 (圖一左)：我們首先手動創(chuàng)建了一組用于上下文學習的演示示例，然后使用這些示例指導模型生成子目標證明訓練數據。具體來說，我們從 miniF2F-valid 中選擇了部分問題，并手動構建了每個問題的已驗證形式化證明，作為初始輸入。通過 GPT-4o 生成子目標證明，該過程確保了：1) 子目標證明由自回歸模型生成；2) 生成的證明風格一致，降低了模型的學習負擔；3) 每個子目標與 Isabelle 中的形式化中間目標相對應。這種方法保證了非形式化證明與形式化證明之間的更高一致性，有效提升了形式化定理證明的質量。

專家學習框架 (圖一右)：該框架由三個核心模塊組成： 

• 形式化陳述生成器（Formal Statement Generator）：生成與非形式化陳述相對應的形式化陳述。
• 子目標生成器（Subgoal Generator）：根據非形式化和形式化陳述，生成與形式化證明結構相匹配的子目標序列。
• 形式化證明生成器（Formal Proof Generator）：在給定的子目標序列下，生成完整的形式化證明。

在每個迭代過程中，SubgoalXL 根據先前生成的陳述和證明樣本進行參數優(yōu)化。專家學習框架使用概率建模和梯度估計技術，對各模塊進行迭代優(yōu)化，以從最佳分布中采樣數據。這種方法確保了模型在處理新的證明任務時能夠保持高精度和穩(wěn)健性。

圖 1：左：非形式化陳述、非形式化證明、形式化陳述、形式化證明和子目標證明的示例。右：基于子目標的專家學習框架概覽?？s寫：“Stat.” 表示 “陳述”，“F.” 表示 “形式化”，“P.” 表示 “后驗”。每次迭代從最優(yōu)分布中采樣子目標證明、形式化陳述和形式化證明。

實驗結果

我們在標準 miniF2F 數據集上對 SubgoalXL 進行了全面的評估，結果表明其在 Isabelle 環(huán)境下達到了新的最優(yōu)性能：

主實驗結果：SubgoalXL 在 miniF2F-valid 數據集上的通過率達到了 61.9%，在 miniF2F-test 數據集上達到了 56.1%。這一表現超過了多種現有的基線方法，包括 Thor、DSP、Subgoal-Prover、LEGO-Prover 以及 Lyra 等，展示了顯著的性能提升（見表 1）。

表 1：miniF2F 數據集上的性能。標記為?的方法在證明搜索過程中部分或全部使用了人工編寫的非形式化證明。加粗數字表示獲得的最高性能。

迭代提升分析：在逐步迭代的過程中，SubgoalXL 表現出明顯的性能增長。模型在 miniF2F-valid 數據集上的通過率從初始的 58.2% 逐步提升至 61.9%，在 miniF2F-test 數據集上從 51.2% 提升至 56.1%。這些結果表明，通過逐步優(yōu)化和專家學習框架的迭代，模型在每次迭代中都能實現穩(wěn)定的性能提升。

圖 2：miniF2F 數據集中不同迭代次數下的通過率比較。

子目標證明對比分析：實驗顯示，SubgoalXL 使用的子目標證明方法在處理復雜證明任務時表現優(yōu)于人類編寫的非形式化證明。尤其在復雜問題上，子目標證明策略顯著提高了證明的精確性和可靠性（見圖 3）。

圖 3：子目標證明與非形式化證明的案例對比。左側示例為子目標證明的成功嘗試，右側兩個示例為非形式化證明的失敗嘗試。

結論與未來展望

SubgoalXL 的成功展示了大語言模型在形式化定理證明任務中的巨大潛力，并為未來研究指明了方向。我們相信，通過進一步優(yōu)化框架、拓展數據集和應用場景，大語言模型將在數學和科學領域帶來更深遠的影響。