2019ICML 2019

CoqGym: 通过与证明助手交互学习定理证明

Learning to Prove Theorems via Interacting with Proof Assistants

Princeton 团队构建了大规模定理证明数据集 CoqGym（71K 人工证明，123 个 Coq 项目），并提出 ASTactic 模型，通过 TreeLSTM 编码 + GRU 解码生成 tactic AST，将定理证明成功率从 4.9% 提升至 30.0%（结合 hammer），首次将 AST 生成引入交互式定理证明。

Kaiyu Yang, Jia Deng

AI解读定理证明形式化验证神经符号

项目概览

论文: Learning to Prove Theorems via Interacting with Proof Assistants (ICML 2019)

作者: Kaiyu Yang, Jia Deng (Princeton University)

项目地址: github.com/princeton-vl/CoqGym

论文链接: arXiv:1905.09381

传统自动定理证明器（ATP）采用归结反演（resolution refutation），将定理转化为一阶子句的合取范式（CNF），通过归结规则不断生成新子句直到空子句出现。这种方式虽具通用性，但 CNF 表示往往冗长且不可读，难以利用人类数学推理中的高层次抽象。交互式定理证明（ITP）则更接近人类思维方式：用户通过输入一系列 tactic（策略）来完成证明，tactic 捕获了归纳、化简等高层次证明技术。

CoqGym 的核心洞察在于：人类专家已在 Coq 中积累了大量 ITP 代码，这些代码为训练机器学习系统提供了丰富的监督信号。该项目同时贡献了一个大规模数据集和一个新的 tactic 生成方法。

核心贡献

1. CoqGym 数据集

CoqGym 是当时最大规模的 ITP 数据集，包含：

统计项	数值
人工编写证明	71K (70,856)
Coq 项目数	123
Coq 源文件	3,061
训练集证明	43,844
验证集证明	13,875
测试集证明	13,137
每证明平均目标数	8.7
每证明平均步数	9.1
每环境平均前提数	10,350.3
每局部上下文平均前提数	5.6
每 tactic 平均 token 数	2.0
Tactic AST 平均高度	1.9

数据集按项目划分训练/验证/测试集，确保测试证明不来自训练项目中的同一项目，从而衡量跨领域泛化能力。

合成证明（Synthetic Proofs）：CoqGym 创新性地从人工证明的中间目标生成短证明。具体方法是将中间目标视为新定理，将其兄弟子目标转化为前提（通过 generalize dependent 处理变量依赖），然后截取原始证明树的子树作为合成证明：

合成证明长度	数量
1 步	159,761
2 步	109,602
3 步	79,967
4 步	61,126

这些短证明更适合学习，因为人工证明往往过长过复杂。

2. ASTactic 模型

ASTactic 是一个 encoder-decoder 架构的深度学习模型，首次将基于学习的 AST 生成应用于交互式定理证明。

与先前工作的关键区别：此前的方法（SEPIA、TacticToe、GamePad、HOList）均从固定集合中选择 tactic，无法生成训练数据中未见过的 tactic。ASTactic 则动态生成 tactic 的完整 AST，理论输出空间无限大。

编码器：TreeLSTM

输入包括当前目标（goal）、局部上下文（local context）和环境中最多 10 个前提（premises），均为 Coq 术语的 AST 形式。编码器使用 child-sum TreeLSTM 对每棵 AST 进行编码：

(\mathbf{c}, \mathbf{h}) = f_{\text{update}}(\mathbf{n}, \{(\mathbf{c}_i, \mathbf{h}_i)\})

其中 $\mathbf{n}$ 是节点符号的 one-hot 编码， $\mathbf{c}_i, \mathbf{h}_i$ 是子节点的状态。整棵树由根节点隐状态 $\mathbf{h}_{\text{root}}$ 表示，并附加 3 维 one-hot 向量标识其类型（目标/环境前提/局部前提）。所有嵌入维度为 256。

解码器：GRU + CFG

解码器遵循 Yin & Neubig (2017) 的方法，按深度优先顺序逐步生长 tactic AST。在每个非终止节点，从上下文无关文法（CFG）中选择产生式规则；在终止节点，生成对应 tactic 参数的 token。

GRU 隐状态更新：

\mathbf{s}_t = f_{\text{GRU}}(\mathbf{s}_{t-1}, [\mathbf{a}_{t-1} : \mathbf{p}_t : \mathbf{n}_t : \mathbf{g} : \mathbf{u}_t])

其中 $\mathbf{a}_{t-1}$ 是前一步的产生式规则嵌入， $\mathbf{p}_t$ 是父节点状态与产生式规则的拼接， $\mathbf{n}_t$ 是当前节点符号， $\mathbf{g}$ 是目标嵌入， $\mathbf{u}_t$ 是通过注意力机制加权求和的前提：

w_i = f_{\text{att}}(\mathbf{s}_{t-1} : \mathbf{r}_i), \quad \mathbf{u}_t = \sum_i w_i \mathbf{r}_i

产生式规则概率：

\mathbf{p}_t = \text{softmax}(\mathbf{W}_R \cdot f(\mathbf{s}_t))

参数合成

tactic 参数被分为不同类别，各有不同处理方式：

Premises（如 apply H 中的 H）：通过注意力分数的 softmax 从所有可用前提中选择
Integers（如 constructor 2）：4-way 分类器（数据中绝大多数为 1-4）
Quantified variables（如 induction n 中的 n）：从目标中全称量词变量随机选取

Tactic 空间

输出空间由一个 CFG 定义，包含 40+ 种 tactic 类型（intro, apply, rewrite, induction, destruct, simpl, assumption, ring 等）。仅生成原子 tactic（排除 tac1; tac2 复合形式），当需要 Coq 术语参数时约束为标识符。

训练与推理

训练：190K 人工证明步骤，teacher forcing，RMSProp（lr=3e-5, weight decay=1e-6），5 epochs，单块 GTX 1080
推理：beam search（k=20）生成 top-20 tactic，DFS 搜索完整证明（depth limit=50, max 300 tactics, 10 分钟超时），重复状态检测剪枝

实验结果

在 CoqGym 的 13,137 个测试定理上评估全自动化定理证明：

方法	成功率
`trivial`	2.4%
`auto`	2.9%
`intuition`	4.4%
`easy`	4.9%
`hammer` (默认 20s)	17.8%
`hammer` (扩展 10min)	24.8%
ASTactic	12.2%
ASTactic + hammer	30.0%

关键发现：

ASTactic 显著超越 Coq 内置自动 tactic：12.2% vs <4.9%，证明了学习方法的有效性
与 hammer 互补：ASTactic + hammer 达到 30.0%，比单独使用 hammer（24.8%）提升 5.2 个百分点，说明 ASTactic 能证明 hammer 无法处理的定理
Beam width 优化点为 20：成功率随 beam width 增长到 20（12.2%）后下降（25 时为 11.7%），可能因模型在不理想分支中困太久
生成证明偏短：平均 6.0 步 vs 人工证明 12.5 步，表明长证明对模型更具挑战性
有时生成更短证明：部分情况下 ASTactic 调用决策过程（如 ring）以更少步骤完成证明

项目工程实现

数据格式

CoqGym 的数据以 JSON + LMDB 的形式存储：

data/: 每个 .json 文件对应一个 Coq .v 源文件，包含 vernac_cmds（Coq 命令列表）、proofs（人工证明）、synthetic_proofs（合成证明）
sexp_cache/: LMDB 数据库，将 JSON 中的哈希码映射到 S-expression
projs_split.json: 训练/验证/测试集划分

每个证明包含 env_delta（环境增量，相对于前一证明的变化）、steps（证明步骤）、goals（目标字典）和 proof_tree（证明树）。

核心组件

组件	功能
`serapi.py`	SerAPI 接口，与 Coq 交互
`eval_env.py`	证明交互环境
`gallina.py`	Coq 术语 S-expression 解析器
`check_proofs.py`	检查 Coq 文件并定位证明
`extract_proof.py`	从 Coq 代码提取证明
`ASTactic/`	模型代码（训练、评估）

依赖工具链

Coq: 证明助手（修改版，暴露内部接口）
SerAPI: Coq 的机器友好序列化接口
CoqHammer: hammer 自动化系统（调用 Z3, CVC4, Vampire, E Prover）
OPAM: OCaml 包管理器（4.07.1+flambda）
PyTorch: 深度学习框架

项目提供 Docker 镜像简化部署，包含预提取数据集和预训练模型。

启示与思考

对形式化验证的启示：ASTactic 证明了深度学习可以在高层次推理任务中生成有效策略。虽然 12.2% 的成功率看似不高，但考虑到 Coq 定理证明的难度（测试集涵盖 123 个不同领域的项目），以及模型几乎无人工工程（vs hammer 调用 4 个经过多年开发的 ATP 系统），这一结果具有重要意义。与 hammer 结合后 30.0% 的成功率表明，学习方法与传统 ATP 方法具有强互补性。

AST 生成的创新性：将 tactic 视为程序而非分类标签，是本文最重要的方法论贡献。通过 CFG 定义输出空间，ASTactic 可以生成训练数据中未出现过的 tactic 组合，突破了先前工作"从固定集合选择"的局限。这一思路对后续的 LeanDojo、ReProver 等工作产生了深远影响。

局限性：

仅编码 10 个前提：模型无法从完整的 10,000+ 前提中选择相关信息，这是明显的瓶颈。论文将前提选择留作未来工作，后来被 ReProver (ICLR 2023) 通过检索增强解决
简化 tactic 空间：排除了复合 tactic 和用户自定义 tactic，限制了适用范围
长证明困难：生成证明平均仅 6 步，远短于人工证明的 12.5 步
无强化学习：仅使用监督学习，未利用 CoqGym 提供的交互环境进行 RL 训练

历史意义：CoqGym 是机器学习辅助定理证明领域的里程碑工作之一。它首次在大规模、多领域的 Coq 数据上验证了学习方法的有效性，为后续的 HOList (Bansal et al., 2019)、LeanDojo (Yang et al., 2023)、AlphaProof 等工作奠定了基础。作者 Kaiyu Yang 后来持续推动这一方向，参与了 LeanDojo、ReProver 和 LeanCopilot 等重要项目。

参考链接

论文: arXiv:1905.09381
代码: github.com/princeton-vl/CoqGym
数据集: Zenodo DOI:10.5281/zenodo.8101883
预训练模型: HuggingFace: kaiyuy/ASTactic
PMLR: proceedings.mlr.press/v97/yang19a.html
作者主页: yangky11.github.io

研究