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

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

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

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

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

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

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

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

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

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

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

方法概述

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

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

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

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

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

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

實(shí)驗(yàn)結(jié)果

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

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

表 1：miniF2F 數(shù)據(jù)集上的性能。標(biāo)記為?的方法在證明搜索過程中部分或全部使用了人工編寫的非形式化證明。加粗?jǐn)?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í)框架的迭代，模型在每次迭代中都能實(shí)現(xiàn)穩(wěn)定的性能提升。

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

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

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

結(jié)論與未來展望

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