🤖 AI

When Agda met Vampire

本文提出了一种将依赖类型证明助手 Agda 与经典一阶逻辑自动定理证明器 Vampire 集成的方法，通过构建两者间基于等式 Horn 子句的可靠翻译桥梁，成功将 Vampire 生成的经典证明转化为 Agda 可验证的构造性证明项，从而以较小的工程代价显著提升了复杂数学定理（如含单位根的域性质）的自动化证明效率。

原作者： Artjoms Šinkarovs, Michael Rawson

发布于 2026-02-24

📖 1 分钟阅读☕ 轻松阅读

CC BY 4.0

原作者： Artjoms Šinkarovs, Michael Rawson

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

这篇文章讲述了一个有趣的“跨界合作”故事：让两个性格迥异、语言不通的数学证明专家（Agda 和 Vampire）联手工作，从而极大地减轻了程序员和数学家的负担。

我们可以把这篇论文的核心思想想象成**“给一位严谨的工匠（Agda）配了一位不知疲倦的搬运工（Vampire）”**。

1. 主角介绍：两个性格迥异的专家

Agda（严谨的工匠）：
- 身份： 一个依赖类型证明助手。你可以把它想象成一位极度挑剔、追求完美的建筑大师。
- 特点： 他坚持“构造主义”（Constructive Logic）。这意味着，如果你想让他相信“有一把钥匙能打开这扇门”，他不仅要求你证明门是开的，还要求你亲手把钥匙造出来给他看。如果只说“肯定有钥匙”，他是不会接受的。
- 痛点： 虽然他的建筑（软件/证明）绝对安全、无懈可击，但他干活太慢了。很多简单重复的砌砖工作（比如证明两个东西长得一样），都要他亲力亲为，非常累人。
Vampire（不知疲倦的搬运工）：
- 身份： 一个自动定理证明器（ATP）。你可以把它想象成一位反应极快、力大无穷但有点“粗线条”的搬运工。
- 特点： 他信奉“经典逻辑”。只要逻辑上通顺，他就能瞬间算出“肯定有钥匙”，甚至能告诉你钥匙在哪。他不需要你亲手造钥匙，只要结果对就行。
- 痛点： 他太“粗线条”了。他给出的答案（证明过程）往往是一堆混乱的推导步骤，Agda 这位严谨的大师根本看不懂，也不接受这种“没亲手造钥匙”的证明。

2. 遇到的难题：语言不通，互不信任

过去，让这两个家伙合作很难：

Agda 说：“你的证明太粗俗了，我不信。”
Vampire 说：“你的要求太繁琐了，我懒得一步步造给你看。”
如果强行合作，要么需要把 Agda 改得面目全非（风险大），要么需要给 Vampire 穿上复杂的防护服（成本高）。

3. 破局之道：寻找“最大公约数”

作者们想出了一个聪明的办法：不要试图让他们完全理解对方，而是找一个双方都能听懂的“通用方言”。

发现共同语言： 他们发现，虽然 Agda 和 Vampire 的大语言体系不同，但有一小部分简单的等式逻辑（Horn 子句），是双方都能轻松理解的。
- 这就好比：虽然一个是说“中文”的，一个是说“英文”的，但他们都会简单的“数学公式”（比如 $A+B=C$ ）。
工作流程（三步骤）：
1. 翻译（Agda -> Vampire）： 当 Agda 遇到一个繁琐的“砌砖”任务时，它利用自己的“反射”功能（就像照镜子），把这个任务翻译成 Vampire 能听懂的“数学公式方言”，然后扔给 Vampire。
2. 搬运（Vampire 干活）： Vampire 瞬间计算出结果，并给出一堆推导步骤，大喊：“搞定！门开了！”
3. 重构（Vampire -> Agda）： 这是最关键的一步。作者写了一个小小的**“翻译官”（用 Prolog 语言写的脚本）**。这个翻译官把 Vampire 那堆混乱的推导步骤，重新“翻译”回 Agda 能看懂的“亲手造钥匙”的过程。
  - 比喻： 就像搬运工说“我推倒了墙”，翻译官就把它重写成“我按照图纸，一块砖一块砖地拆掉了墙，这是每一块砖的编号”。

4. 实际效果：从“两天”到“一眨眼”

为了测试这个方法，作者们拿了一个真实的难题：复数域中“单位根”的性质证明。

以前： 一位专业的 Agda 程序员，需要整整两天时间，手动编写代码来证明这些性质。
现在： 系统自动完成。Agda 把任务扔给 Vampire，Vampire 瞬间算出，翻译官瞬间重构。整个过程不到一秒钟。

5. 核心意义：轻量级的“锤子”

在计算机科学界，这种系统被称为"Hammer"（锤子），意思是能一锤定音解决难题。

以前的锤子： 很重，需要把整个房子（证明系统）拆了重装。
这篇论文的锤子： 轻量级。它不需要改动 Agda 的核心，也不需要改动 Vampire 的核心。它只是站在中间，做一个聪明的“翻译官”和“中间人”。

总结

这篇论文告诉我们：
不需要把两个性格迥异的专家强行融合成一个新物种。只要找到他们都能理解的简单规则，并派一个聪明的翻译官在中间协调，就能让严谨的工匠享受搬运工的高效，同时保证最终成果依然完美无缺。

这不仅让写代码和做数学证明变得更快，也为未来让各种智能工具更好地协作提供了新思路。

这篇论文《When Agda met Vampire》（当 Agda 遇见 Vampire）由南安普顿大学的 Artjoms Šinkarovs 和 Michael Rawson 撰写，提出了一种将依赖类型证明助手（Agda）与自动定理证明器（Vampire）进行轻量级集成的方法。该方法旨在解决依赖类型系统中自动化证明不足的问题，同时保持构造性逻辑的正确性保证。

以下是该论文的详细技术总结：

1. 研究背景与问题 (Problem)

依赖类型证明助手的局限性：像 Agda、Lean 和 Rocq 这样的依赖类型证明助手基于构造性类型理论（如 Martin-Löf 类型论），通过 Curry-Howard 对应关系将定理视为类型。虽然这提供了极高的正确性保证，但用户经常需要手动完成繁琐的证明义务（proof obligations），特别是那些涉及等式推理或简单代数性质的证明。
自动化的困境：
- 内部策略：证明助手内部的自动化策略（Tactics）通常较弱，难以处理复杂的逻辑推理。
- 外部集成挑战：现有的“重锤”（Hammer）系统（如 Isabelle 的 Sledgehammer）通常依赖于经典逻辑的自动定理证明器（ATP）。然而，ATP（如 Vampire）基于经典一阶逻辑，而 Agda 基于构造性依赖类型理论。两者在逻辑基础（排中律、空域假设等）和术语/公式的区分上存在根本性差异。直接集成会导致信任问题（ATP 生成的证明不可信）或无法将经典证明转化为构造性证明项。
核心难点：如何在保持 Agda 核心信任不变的前提下，利用强大的经典 ATP 来辅助 Agda 完成证明，并将 ATP 的“黑盒”证明转化为 Agda 可验证的构造性证明项。

2. 方法论 (Methodology)

作者提出了一种轻量级、基于反射（Reflection）的往返翻译（Round-trip Translation）方案，核心思想是限制在两个系统都能理解的表达性片段（主要是等式 Horn 子句）上进行交互。

A. 核心观察

Horn 子句片段：许多 Agda 中的有用前提和目标可以表示为 $\forall \bar{x}. R_1 \to R_2 \to \dots \to R_n$ 的形式，其中 $R_i$ 是原子类型。这对应于一阶逻辑中的 Horn 子句片段。
构造性有效性：Vampire 的核心推理规则（如超归结 Superposition）在 Horn 子句上是构造性有效的。虽然 Vampire 使用反证法（Refutation）和经典逻辑预处理，但其推导过程本身可以转化为构造性证明。
Friedman 变换的变体：通过将目标 $G$ 从 $\bot$ （假）替换为 $G \to G$ （重言式），可以将 Vampire 的反证证明（ $\Gamma, \neg G \vdash \bot$ ）机械地转化为构造性证明（ $\Gamma \vdash G$ ）。

B. 工作流程

Agda 到 Vampire 的翻译（导出）：
- 利用 Agda 的反射机制（Reflection），无需修改 Agda 内核。
- 定义宏（kty, kdata, kfun, kthm, kgoal）将 Agda 的定义（数据类型、函数、定理、目标）提取并转换为 SMT-LIB 格式。
- 限制条件：仅支持无参数的归纳数据类型、非依赖类型的函数、以及 Horn 形式的命题（主要是命题相等性）。
- 生成的 SMT-LIB 代码包含公理和待证目标的否定形式。
调用 Vampire：
- 将生成的 SMT-LIB 输入发送给 Vampire。
- 使用 CASC 竞赛的预设策略集（Portfolio）运行 Vampire，利用其强大的超归结演算（Superposition Calculus）寻找证明。
- Vampire 输出 TSTP 格式的证明序列（一系列推理步骤）。
证明转换与重构（导入）：
- 证明变换：在重构之前，对 Vampire 的证明进行机械变换。将证明根节点的目标子句 $G \to \bot$ 替换为 $G \to G$ ，并将证明中所有涉及 $\bot$ 的前提替换为 $G$ 。这使得整个证明从“反证”变为“直接证明”。
- Prolog 引擎：使用 Prolog 编写了一个紧凑的重构引擎（少于 500 行代码）。
  - Prolog 读取 TSTP 证明。
  - 利用 Prolog 原生的回溯搜索和变量重命名机制，将 Vampire 的推理步骤（如 Resolution, Factoring, Superposition）映射为 Agda 的证明项（Proof Terms）。
  - 处理等式对称性、空域（Empty Domains）等边缘情况（若无法确定域非空，则留空给用户填充）。
- 类型检查：生成的 Agda 证明项最终由 Agda 的类型检查器进行验证，确保其完全符合构造性逻辑。

3. 关键贡献 (Key Contributions)

轻量级集成架构：提出了一种无需修改 Agda 或 Vampire 内核的集成方案。利用 Agda 的反射和 Prolog 的搜索能力，实现了“即插即用”的自动化。
Horn 子句片段的桥梁：识别并形式化了依赖类型理论与经典一阶逻辑之间的等式 Horn 子句公共片段，证明了该片段在两个方向上的翻译是保真且构造性有效的。
基于 Prolog 的证明重构：创新性地使用 Prolog 作为中间层来重构 ATP 证明。相比修改 ATP 输出或调用另一个认证 ATP，这种方法在变量处理和推理规则匹配上更加自然、简洁且高效。
Friedman 变换的实用化：展示了如何在实际工具链中应用类似 Friedman 变换的技术，将经典反证证明转化为构造性证明，而无需复杂的逻辑转换理论。

4. 实验结果 (Results)

案例研究：作者在形式化**快速傅里叶变换（FFT）**算法时应用了该系统。具体任务是验证一个带有单位根（roots of unity）的复数域表示是否满足特定的代数性质（如环公理和单位根性质）。
性能对比：
- 人工证明：一位专业的 Agda 开发人员完成该证明（涉及 12 个定理）耗时约 2 天。
- 自动证明：使用该系统，所有 12 个定理在 不到一秒 的时间内被自动证明。
- 证明规模：生成的 Agda 证明项虽然冗长（部分证明约 300 行代码），但完全由 Agda 类型检查器验证通过。
鲁棒性：系统成功处理了包含归纳数据类型、等式推理和复杂代数结构的证明，且未出现重构失败的情况。

5. 意义与未来工作 (Significance & Future Work)

实践意义：显著降低了依赖类型系统中繁琐证明义务的开发成本，使得形式化验证更具实用性。
通用性：该方法不特定于 Agda 或 Vampire。任何支持反射提取的依赖类型证明助手（如 Lean, Idris）和任何基于超归结或类似演算的 ATP（如 E, Zipperposition）均可采用此架构。
未来方向：
- 扩展逻辑片段：从 Horn 子句扩展到完整的子句逻辑（Full Clausal Logic），利用双重否定翻译处理更复杂的类型。
- 支持更丰富的 Agda 特性：处理参数化类型、索引族（Indexed Families）和证明相关类型（Proof-relevant types）。
- 证明美化：优化生成的证明项，使其更接近人类编写的风格，减少冗长性。
- 前提选择（Premise Selection）：引入类似 Sledgehammer 的前提选择机制，自动筛选最相关的公理，减少输入规模。

总结

这篇论文展示了一种巧妙且实用的方法，通过限制在 Horn 子句片段并利用反射和 Prolog，成功弥合了构造性依赖类型理论与经典自动定理证明之间的鸿沟。它不仅解决了 Agda 自动化不足的问题，也为其他依赖类型证明助手集成外部 ATP 提供了一条低侵入、高可信的技术路线。