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

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

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

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

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

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

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

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

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

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

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

方法概述

SubgoalXL 的方法核心在于子目標證明策略和專家學(xué)習(xí)框架的結(jié)合。

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

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

• 形式化陳述生成器（Formal Statement Generator）：生成與非形式化陳述相對應(yīng)的形式化陳述。
• 子目標生成器（Subgoal Generator）：根據(jù)非形式化和形式化陳述，生成與形式化證明結(jié)構(gòu)相匹配的子目標序列。
• 形式化證明生成器（Formal Proof Generator）：在給定的子目標序列下，生成完整的形式化證明。

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

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

實驗結(jié)果

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

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

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

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

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

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

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

結(jié)論與未來展望

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