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