有大脑的 Vampire 是一把优秀的 ITP 锤
人工智能
2021-05-12 v2
摘要
Vampire 长期以来是最强的一阶自动定理证明器，被广泛用于 Mizar、Isabelle、HOL 和 Coq 等 ITP 中的锤式证明自动化。在本工作中，我们通过以高效神经引导增强其饱和过程，显著提升了 Vampire 在整个 Mizar 库上锤击的性能。特别地，我们采用一种近期提出的递归神经网络，仅基于生成子句的推导历史对其进行分类。与以往基于子句逻辑内容的神经方法相比，我们的架构使单个子句的评估耗时大幅减少。所得系统展现出良好的学习能力，并在 Mizar 库上超越了当前最优性能，同时证明了许多相关 ENIGMA 系统在类似锤击评估中无法证明的定理。
引用
@article{arxiv.2102.03529,
title = {Vampire With a Brain Is a Good ITP Hammer},
author = {Martin Suda},
journal= {arXiv preprint arXiv:2102.03529},
year = {2021}
}
备注
14.5 pages excluding references