摘要

人类证明定理时依赖大量的高层次推理和特定问题的洞察力。证明助手提供了一种类似于人类数学推理的形式化方法，将定理表示为高阶逻辑，并将证明表示为高层次的策略。然而，人类专家仍需手动通过在证明助手中输入策略来构建证明。本文研究了利用机器学习自动化与证明助手交互的问题。我们构建了CoqGym，一个大规模的数据集和学习环境，包含来自123个使用Coq证明助手开发的项目中的71000个人类编写的证明。我们开发了ASTactic，一种基于深度学习的模型，该模型生成以抽象语法树（AST）形式表示的策略程序。实验结果表明，经过CoqGym训练的ASTactic能够生成有效的策略，并可用于证明之前自动化方法无法解决的新定理。代码可在https://github.com/princeton-vl/CoqGym 获取。