Tacq - Rocq 的上下文感知戰術推薦

Tacq - Rocq 的上下文感知戰術推薦

Tacq - Context Aware Tactic Recommendation for Rocq

https://hal.science/hal-05428141v1/file/jfla2026-final55.pdf

盡管大型語言模型（LLMs）在利用證明助手進行形式化數學方面取得了令人矚目的最新成果，但當前最先進的研究主要集中在數學競賽問題上，而這些問題通常涉及簡單且已被充分理解的概念。不幸的是，這與當前形式化數學的實際實踐相去甚遠——在實際工作中，專家必須在龐大的引理庫中導航，并處理復雜的構造。

本文聚焦于 Rocq 中的“下一步戰術推薦”（next tactic recommendation）問題。一個關鍵挑戰在于：當證明依賴于包含大量依賴項的大型庫、且廣泛使用專門符號（notations）時，如何向模型提供足夠的上下文信息，使其能夠理解當前的證明目標。我們提出了一種工具，可以從當前目標中提取符號和依賴關系，并用自然語言文檔字符串（docstrings）對其進行注釋。我們證明，這種增強后的上下文能夠提升當前最先進模型在具有挑戰性的 MathComp 庫上生成有效戰術（tactics）的能力。

1 引言

在過去一年中，利用大型語言模型進行數學推理引發了激烈競爭。2025年7月，DeepMind 的 Gemini 和 OpenAI 的實驗性模型均在 2025 年國際數學奧林匹克競賽（IMO）中取得了金牌成績 [Deea, Ope]。這些突破利用了 LLM 的自然語言能力來生成非形式化證明，這些證明可由人類專家（如 IMO 評委）驗證。

然而，一旦超出奧賽的六道題目，驗證此類證明就變得極其困難。因此，其他研究團隊轉而專注于形式化證明的專用模型，其中 LLM 生成可由交互式定理證明器（如 Lean [YSG+23]、Rocq [YD19] 或 Isabelle/HOL [FRRB23]）自動驗證的證明腳本。

這一形式化方法由 DeepMind 的 AlphaProof [AAt] 首創，該系統在 2024 年奧賽中使用 Lean 達到銀牌水平，展現出巨大潛力。2025 年 7 月，字節跳動的 SeedProver [CGH+25] 在 2025 年奧賽中復現了 AlphaProof 的性能，而 Harmonic 的 Aristotle [ABD+25] 則借助 Lean（以及一個專門的幾何問題求解器）達到了金牌水平。

這些近期模型遵循三階段流程：

1. 在混合了形式化證明與自然語言推理的數據集上對預訓練 LLM 進行微調 [XGS+24, WUL+25, DM25]；
2. 通過強化學習或專家迭代（expert iteration）[WHZ+24, LTL+25, XXY+25] 循環，在無監督情況下嘗試證明新定理，以改進模型 [XRS+25, CGH+25, ABD+25]；
3. 在推理階段，將訓練好的模型與搜索算法（如 pass@k、束搜索 [XXY+25] 或蒙特卡洛樹搜索 [XRS+25, ABD+25]）結合，構建智能體（即針對特定任務的 AI 驅動程序），從而利用來自證明助手的反饋。

遺憾的是，這些模型不僅在訓練其數千億參數時需要巨大的計算資源，在推理階段同樣耗費巨大——智能體通常需要嘗試成千上萬次才能找到一個有效證明。

本文聚焦于一個更專門的任務：在 MathComp 庫中為 Rocq 提供“下一步戰術推薦”。在證明過程中，模型需根據當前目標預測下一個戰術。雖然從技術上講，這比完整的證明發現更簡單，但我們認為，此類工具對于幫助人類用戶和基于 LLM 的智能體導航復雜證明（尤其是當這些證明依賴于或貢獻于大型現有庫時）具有重要價值。

戰術推薦的一個關鍵問題是如何向模型提供足夠上下文，使其理解當前目標。先前的工作包括前提檢索（premise retrieval）技術，用于在提示中加入可能有用的引理和定義 [YD19, YSG+23, BOR+24, TTW+24, TSC+25]。然而，據我們所知，現有工作并未考慮符號（notations）——即用于使復雜項更簡潔、更易理解的語法快捷方式。這類專門符號在 MathComp 中極為普遍。另一個難點在于，LLM 主要是在自然語言數據集上訓練的，而 MathComp 中關于其定理、引理和符號的自然語言解釋卻非常稀少。

本文的主要貢獻如下：— 一種可自動從目標中提取 Rocq 依賴項和符號的工具；— LLM4Docq：一個基于 LLM 的智能體，可利用專家反饋半自動地為 MathComp 元素添加自然語言文檔字符串；— Tacq：一個基于 LLM 的智能體，利用依賴項、符號及其文檔字符串，根據當前目標推薦下一步戰術；— 在 MathComp 庫中隨機抽取的一組證明目標上對 Tacq 進行評估。

2 Tacq：概述

圖1展示了我們的戰術推薦智能體 Tacq 的整體架構。給定當前的證明目標，Tacq 會檢索相關的依賴項和符號定義，并關聯由 LLM4Docq 生成的相應自然語言文檔字符串（docstrings）。隨后，Tacq 將所有這些信息整合起來，用于提示一個大型語言模型（LLM）生成下一步戰術，該戰術可由 Rocq 解釋器執行，從而推進到下一個證明目標。接下來，我們簡要描述各個組成部分。

依賴項（Dependencies）。為了與 Rocq 交互，我們使用 Pétanque [TBAL24]——一個輕量級環境，其基于 Flèche [CAI]，后者是 Rocq 的增量式文檔管理器，可直接訪問證明狀態和戰術引擎。我們對 Pétanque 進行了擴展，使其能夠獲取 Rocq 的抽象語法樹（AST）。然后，我們可以分析當前目標的 AST，從中提取依賴項。例如，圖1列出了當前目標所涉及的五個依賴項。

符號（Notations）。MathComp 經常使用專門的符號，這些符號模仿標準數學慣例，為復雜操作提供直觀的語法，對于理解證明目標至關重要。然而，Rocq 解釋器在處理時會將這些符號替換為其定義，而不會保留原始的符號語法。本文中，我們增強了 Pétanque，使其能夠通過攔截 Rocq 解釋器中的符號解析過程，提取當前目標中使用的符號。例如，在圖1中，我們可以看到當前目標使用了三個非顯而易見的符號。

自然語言文檔字符串（Natural language docstrings）。盡管大型語言模型在訓練期間很少接觸 MathComp，但當前最先進的模型在自然語言推理方面表現卓越。為了給當前目標提供語義上下文，我們將每個依賴項和符號都關聯上一段自然語言文檔字符串。為此，我們提出了 LLM4Docq——一個基于 LLM 的智能體，它通過半自動流程結合專家反饋，為 MathComp 元素提出并優化文檔字符串。

本文其余部分組織如下：第3節介紹我們如何利用 Rocq 解釋器提取當前目標的依賴項和符號；第4節介紹 LLM4Docq，并說明我們如何為 MathComp 元素生成文檔字符串；第5節在 MathComp 庫上對 Tacq 進行評估，使用了多種不同規模的模型（包括閉源和開源模型），并進行了消融研究，以衡量提示中每個組件的影響。

3 Rocq 上下文：依賴項與符號

本節介紹我們如何利用 Pétanque 環境從當前目標中提取依賴項和符號。圖2展示了我們方法的示意圖。

我們并未直接從整個目標中提取信息，而是采用“逐假設分解”策略——即將每個假設和結論分別轉換為獨立的定義，以便單獨檢查。這一選擇是受第3.2節所述限制所驅動的。這樣我們可以分別處理每個組件，使提取過程對單個假設中的錯誤更具魯棒性。

3.1 依賴項

所謂“依賴項”，是指出現在目標中、但既不是符號（notation），也未在目標內部定義的 Rocq 對象。這類對象包括先前定義的引理、定義、不動點（fixpoints）和歸納類型，但不包括已在目標中明確列出的假設。依賴項提供了關于用于定義目標的對象的重要上下文信息。

雖然 Pétanque 已支持執行命令、獲取目標和搜索定義，但我們對其進行了擴展，使其也能獲取 Rocq 的抽象語法樹（AST），然后我們通過分析 AST 提取對象名稱。接著，我們過濾掉不需要的名稱（例如其他假設，或已在目標其他位置出現的依賴項），僅保留真正的依賴項名稱。最后，我們使用 Locate 和 About 命令檢索這些依賴項對應的類型。

3.2 符號

符號為復雜操作提供直觀的語法表達，對于理解目標至關重要。相比依賴項，提取符號的過程出人意料地困難。在 Rocq 中，符號由解釋器處理，并依賴于當前作用域（scope）。AST 中僅包含符號的字符串表示形式，若無當前作用域信息，則這些符號含義模糊。例如，在 MathComp 中，“_ + _”這個符號就有8種不同實例。因此，我們需要對 Rocq 解釋器進行改造，以在正確的作用域內攔截符號的解析過程。

改造 Rocq 解釋器。為了執行 Rocq 代碼或“文言表達式”（vernacular expressions），解釋器會在類型推斷前的“內部化”（internalization）階段解析符號、作用域和隱式參數。隨后，符號立即被其定義替換，原始語法也隨之丟失。為此，我們在符號被丟棄之前，對 Rocq 解釋器進行改造，使其在內部化階段攔截符號。

圖3展示了我們為提取符號而修改 Rocq 解釋器的一個（非常）簡化的版本。1 在原始代碼（左側），主入口函數是 interp（第18行），它遞歸遍歷項的 AST。文言表達式由 translate_vernac 函數（第14行）解釋。我們只從 Rocq 定義中提取符號，因此重點關注 VernacDefinition 構造器（第15行）。隨后，internalize 函數通過調用 intern_notation 函數（第9行）處理符號：該函數識別符號（第4行，interp_notation），并將其替換為其定義（第5行，instantiate_notation_constr）。

在我們的補丁代碼（右側），intern_notation 函數不僅返回符號的實例化結果，還同時返回符號本身（第5行）；我們向 intern 函數傳入一個累加器（第7–11行），用于收集所有符號。因此，internalize 函數除了原有輸出外，還會返回一個符號列表。之后，我們再使用 Locate 命令檢索這些符號的定義。

局限性。部分符號被標記為“僅用于解析”（parsing only）。用戶可以書寫這些符號，但在打印出的目標中不會顯示，我們也無法提取它們。例如，在 MathComp 中，“_ = _ :> ”用于指定等式兩邊成員的類型，但我們在目標中只能看到“ = _”。幸運的是，這種限制僅影響 MathComp 中極小一部分假設。我們“逐假設分解”方法的一個關鍵優勢在于，我們可以安全忽略這些異常情況，繼續處理目標的其余部分。

4 LLM4Docq：自然語言文檔字符串

MathComp 包含數萬個定義、引理和符號，但其中只有極少數附帶人類可讀的解釋。這種文檔缺失對人類用戶和自動化智能體都構成了重大障礙：對人類而言，這使得庫難以導航；對基于 LLM 的智能體而言，則導致許多符號缺乏語義基礎（semantic grounding）。然而，鑒于當前庫的規模，讓 MathComp 開發者手動為所有代碼添加文檔字符串幾乎是不可能的任務。

為解決這一問題，我們引入了 LLM4Docq（在 2025 年 Rocqshop 會議 [SVC25] 上首次提出）——一個基于 LLM 的智能體，通過半自動流程并結合專家參與（experts-in-the-loop），為定義、引理和符號生成并優化簡短的自然語言文檔字符串。我們利用 LLM4Docq 構建了一個包含所有 MathComp 對象文檔字符串的數據庫。Tacq 隨后可利用該數據庫，將依賴項和符號與其對應的文檔字符串關聯起來，從而為預測下一步戰術提供語義上下文。

4.1 專家參與的生成流程

LLM4Docq 采用一種迭代流程（如圖4所示），在自動生成與專家評審之間交替進行。其目標是以最小的人工投入，產出一套全面且高質量的文檔字符串集合。LLM4Docq 的實時進展及審閱者列表可在 https://github.com/LLM4Rocq/LLM4Docq 查看。

自動生成。我們使用當前最先進的 LLM（Gemini 2.5 Pro [Deeb]）為每個源文件中的每個對象生成文檔字符串。對于每個文件，提示（prompt）包含以下三部分：

1. 文件的原始內容；
2. 由 MathComp 專家精心設計的通用指令提示，并附有幾個高質量文檔字符串示例，用于上下文學習（in-context learning）；
3. 一個針對該文件的特定提示，該提示將在每次迭代中由專家更新。

專家反饋。在每次迭代中，MathComp 專家通過協作式標注界面審閱一部分自動生成的文檔字符串。每個候選文檔字符串可被標記為“可接受”（Acceptable）、“需改進”（Needs Improvement）或“錯誤”（Incorrect）。如適用，評審者會提供評論、建議或修正版本。圖5展示了兩個專家反饋的示例。

重新生成。我們并非手動修正所有文檔字符串，而是在收集到足夠多的專家反饋后，利用這些反饋優化 LLM 的提示內容。針對文件特定提示的典型調整包括：增加正負樣本示例，以及澄清數學術語的使用。通用指令提示也可根據反復出現的錯誤進行補充修正。隨后，我們啟動新一輪迭代，重新生成所有尚未被審閱的文檔字符串。該循環持續重復，直至不滿意文檔字符串的比例穩定在目標閾值以下。

4.2 進展與成果

覆蓋范圍。截至本文撰寫時，LLM4Docq 已完成對 MathComp 庫的兩輪完整迭代，覆蓋了所有顯式編寫的定義、引理和符號。總計已有超過 20,000 個對象被自動標注了文檔字符串。下一版本還將涵蓋由 Hierarchy Builder (HB) 隱式生成的元素。

專家評審情況。通過標注界面，MathComp 專家已審閱了 600 條文檔字符串。其中，82% 被判定為“可接受”，15.2% “需改進”，僅 3% 被認為“錯誤”。在“需改進”類別中，多數問題涉及風格或精確性方面：32% 的文檔字符串被認為過于冗長，48% 存在措辭或術語不一致的問題，20% 缺乏精確性或遺漏關鍵細節。

我們收集了這些反饋，并用于生成 LLM4Docq 的第二版（即當前版本）。由此構建的數據庫目前已全面覆蓋 MathComp，其用途不僅限于 Tacq。該數據庫已被用于微調一個雙向模型——在源文件上下文基礎上，建立文檔字符串與形式化語句之間的映射關系。我們的最終目標是：一旦文檔字符串達到社區認可的質量標準，便將其正式添加進 MathComp 庫中。

5 評估

本節中，我們在 MathComp 庫中隨機抽取的一組證明目標上對 Tacq 進行評估，使用了多種不同規模的模型（包括閉源和開源模型），并進行了消融研究，以衡量提示中每個組件的影響。

5.1 通用方法論

為評估上下文信息對戰術預測的影響，我們在四種不同的提示配置下對每個 LLM 進行評估，這些配置提供不同程度的上下文：

• G：基線場景，僅提供當前目標。
• G + D + L：僅添加依賴項及其文檔字符串（docstrings）。
• G + D & N：添加依賴項和符號（notations），但不包含文檔字符串。
• G + D & N + L：同時添加依賴項、符號以及它們的文檔字符串。

在所有配置中，任務保持一致：給定當前目標及相應上下文，預測最可能的下一步戰術。為衡量模型性能，我們檢驗所預測的戰術是否能通過類型檢查（type-check）。因此，該評估測試的是模型生成語法正確且可應用的戰術的能力。

Pass@k。對于每個模型和每種提示配置，我們計算 k ∈ { 1 , 4 , 8 , 32 }
時的 pass@k 指標。遵循標準做法 [CTJ+21]，pass@k 表示在 k k 個生成樣本中至少有一個正確的概率。我們使用無偏估計量（unbiased estimator）來估算 pass@k：

其中 n n 是每個問題生成的樣本總數（滿足）， c c 是這 n n 個樣本中正確的樣本數量。內層項表示在無放回抽樣的情況下，從 k k 個樣本中至少有一個正確的概率，然后對測試集中所有問題取平均。對于每個模型，所展示的 pass@k 結果中最大的 k k 值，即表示該模型在每個戰術預測任務中生成的樣本總數。對于嚴格小于該最大值的 k k，其 pass@k 結果使用公式 (1) 中的估計量進行計算。

測試集構建。我們通過從 MathComp 庫中的定理中采樣證明步驟來構建測試集。對于每個選定的定理，我們隨機選擇一個證明步驟位置，并提取對應的證明狀態，包括目標、其依賴項與符號，以及來自 LLM4Docq 的文檔字符串。這一過程生成了一組多樣化的戰術預測任務，充分反映了 MathComp 證明目標的復雜性及其對符號的高度依賴。

5.2 結果

表1展示了所有被評估模型在不同提示配置下的 pass@k 結果。
出于成本控制的考慮，專有模型 GPT-4o 和 Claude Sonnet 4 的結果僅計算至 pass@8。

表1中的結果表明，引入額外的上下文信息通常能提升模型性能，盡管提升幅度因模型系列和規模而異。對于 GPT-4o，每次在提示中增加新信息都帶來了顯著收益，取得了整體最佳的改進效果。這一趨勢在 Claude Sonnet 4 和 Qwen3 32B 上則不那么一致，但這兩個模型仍從提示增強中獲益。

正如預期，所有模型和配置均展現出測試時的擴展規律（test-time scaling law）：增加生成樣本數量始終能帶來更好的性能。重要的是，上下文增強所帶來的改進在所有 pass@k 值下均持續存在，這表明預測質量得到了普遍提升。

針對參數量從 4B 到 32B 的 Qwen3 模型的實驗表明，只有最大規模的模型能從額外信息中受益。我們認為，較小的模型缺乏足夠的容量來有效利用附加上下文。不過，Qwen3 系列模型經過專門的數學與編程任務訓練 [YLY+25]，這或許解釋了它們整體上在 Rocq 任務中表現尚可的原因。

消融研究。本工作的一個創新點是將符號（notations）納入上下文。為驗證符號的影響，我們進行了消融研究，比較僅包含依賴項及其文檔字符串的上下文（G + D + L）與同時包含依賴項和符號及其文檔字符串的上下文（G + D & N + L）。結果表明，在大多數情況下，加入符號及其文檔字符串能夠提升性能，從而驗證了我們方法的有效性。

其他指標。我們也考察了其他評估指標。為判斷 LLM 是否生成了有意義的戰術，我們檢查了所生成的戰術是否改變了當前目標。為判斷 LLM 是否將證明引向正確方向，我們檢查了應用所生成戰術后是否得到與應用參考戰術（reference tactic）相同的目標狀態。然而，這些更精細的指標由于結果始終趨于極端而未能得出明確結論：盡管在幾乎所有情況下目標狀態都被修改了，但幾乎從未出現過與應用參考戰術后所得目標狀態一致的情況。

6 相關工作與結論

近期基于大型語言模型（LLM）的定理證明進展大致可分為兩類方法：

• 步驟級證明器（step-level provers）[PHZ+22, WHZ+24, XXY+25]：通過與證明助手進行細粒度交互，逐步生成證明；
• 整證生成模型（whole-proof generation models）[XRS+25, DM25]：試圖一次性生成完整證明。

步驟級證明器能持續獲得定理證明器的反饋，但通常需要復雜的支撐基礎設施，且其操作粒度過細，不利于高層次的數學推理。整證生成模型雖避免了這些限制，但傳統上缺乏交互式精調能力。

最近，該領域逐漸趨向于混合方法，結合兩種范式的優點。例如，通過擴展的思維鏈（chain-of-thought）推理增強整證模型 [WUL+25, RSS+25, LTL+25]，其性能已優于純步驟級生成方法。更近期的工作 [CGH+25, VVS+25] 通過將通用 LLM 的非形式化推理能力與專用符號證明器相結合，在研究生水平的數學問題上取得了更強的結果。例如，[CSL+25] 實現了一個三階段神經符號流水線——草稿（自然語言子目標）、概要（自動形式化）和證明（符號搜索）——該方法建立在 [XXY+25] 的步驟級證明器基礎之上。

然而，上述幾乎所有工作都針對 Lean 證明助手。本文則為 Rocq 開發了類似的基礎設施，特別聚焦于前提檢索（premise retrieval）和符號提取（notation retrieval）。盡管前提檢索——即在提示中加入可能相關的引理和定義——已在先前研究中有所探索 [YD19, YSG+23, BOR+24, TTW+24, TSC+25]，但據我們所知，尚無現有方法處理符號的提取與解釋。這一空白在 MathComp 等庫中尤為關鍵，因為其中廣泛使用專門符號，而這些符號對理解證明狀態至關重要。對于新項目而言，顯式提供符號定義更為關鍵，因為 LLM 在此缺乏先驗知識。

本研究表明，通過在提示中加入定義信息和符號，通常能提升戰術生成的性能，尤其對大型閉源模型和中等規模的開源模型效果顯著。然而，較小的模型在增強提示下表現有限，甚至性能下降，表明它們缺乏有效處理額外上下文的能力，反而將這些信息視為噪聲。

本工作仍在持續推進中，但目前已促成三個已合并的拉取請求（pull requests），分別提交至 Rocq、rocq-lsp 和 Pytanque 項目。未來的研究將把我們這種單步提示驅動的方法與采用多步搜索策略的完整證明合成方法（如 ProofWala [TTDC25]、COPRA [TTW+24] 和 Hilbert [VVS+25] 中實現的方法）進行比較，以更深入地理解：在實現功能正確性方面，提示工程（prompt engineering）與基于搜索的探索（search-based exploration）各自貢獻如何。

原文鏈接：https://hal.science/hal-05428141v1/file/jfla2026-final55.pdf