Tacq - Rocq 的上下文感知戰(zhàn)術(shù)推薦

Tacq - Context Aware Tactic Recommendation for Rocq

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

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

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

1 引言

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

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

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

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

1. 在混合了形式化證明與自然語言推理的數(shù)據(jù)集上對預(yù)訓(xùn)練 LLM 進行微調(diào) [XGS+24, WUL+25, DM25]；
2. 通過強化學(xué)習(xí)或?qū)＜业╡xpert iteration）[WHZ+24, LTL+25, XXY+25] 循環(huán)，在無監(jiān)督情況下嘗試證明新定理，以改進模型 [XRS+25, CGH+25, ABD+25]；
3. 在推理階段，將訓(xùn)練好的模型與搜索算法（如 pass@k、束搜索 [XXY+25] 或蒙特卡洛樹搜索 [XRS+25, ABD+25]）結(jié)合，構(gòu)建智能體（即針對特定任務(wù)的 AI 驅(qū)動程序），從而利用來自證明助手的反饋。

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

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

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

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

2 Tacq：概述

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

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

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

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

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

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

本節(jié)介紹我們?nèi)绾卫?Pétanque 環(huán)境從當(dāng)前目標(biāo)中提取依賴項和符號。圖2展示了我們方法的示意圖。

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

3.1 依賴項

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

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

3.2 符號

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

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

圖3展示了我們?yōu)樘崛》柖薷?Rocq 解釋器的一個（非常）簡化的版本。1 在原始代碼（左側(cè)），主入口函數(shù)是 interp（第18行），它遞歸遍歷項的 AST。文言表達式由 translate_vernac 函數(shù)（第14行）解釋。我們只從 Rocq 定義中提取符號，因此重點關(guān)注 VernacDefinition 構(gòu)造器（第15行）。隨后，internalize 函數(shù)通過調(diào)用 intern_notation 函數(shù)（第9行）處理符號：該函數(shù)識別符號（第4行，interp_notation），并將其替換為其定義（第5行，instantiate_notation_constr）。

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

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

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

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

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

4.1 專家參與的生成流程

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

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

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

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

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

4.2 進展與成果

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

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

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

5 評估

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

5.1 通用方法論

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

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

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

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

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

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

5.2 結(jié)果

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

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

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

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

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

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

6 相關(guān)工作與結(jié)論

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

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

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

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

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

本研究表明，通過在提示中加入定義信息和符號，通常能提升戰(zhàn)術(shù)生成的性能，尤其對大型閉源模型和中等規(guī)模的開源模型效果顯著。然而，較小的模型在增強提示下表現(xiàn)有限，甚至性能下降，表明它們?nèi)狈τ行幚眍~外上下文的能力，反而將這些信息視為噪聲。

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

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