形式化定理證明新突破：SubgoalXL框架讓大模型在Isabelle中性能暴漲

09月27日 12:05 新浪網 news-china-auto-hilite

AIxiv專欄是機器之心發佈學術、技術內容的欄目。過去數年，機器之心AIxiv專欄接收報導了2000多篇內容，覆蓋全球各大高校與企業的頂級實驗室，有效促進了學術交流與傳播。如果您有優秀的工作想要分享，歡迎投稿或者聯繫報導。投稿郵箱：liyazhou@jiqizhixin.com；zhaoyunfeng@jiqizhixin.com

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

背景介紹：形式化定理證明的新挑戰

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

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

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

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

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

SubgoalXL 如何應對挑戰？

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

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

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

方法概述

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

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

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

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

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

圖 1：左：非形式化陳述、非形式化證明、形式化陳述、形式化證明和子目標證明的示例。右：基於子目標的專家學習框架概覽。縮寫：「Stat.」表示「陳述」，「F.」表示「形式化」，「P.」表示「後驗」。每次迭代從最優分佈中采樣子目標證明、形式化陳述和形式化證明。

實驗結果

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

主實驗結果：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%。這些結果表明，通過逐步優化和專家學習框架的迭代，模型在每次迭代中都能實現穩定的性能提升。