学习等式定理证明
机器学习
2021-02-11 v1 人工智能
计算机科学中的逻辑
摘要
我们提出分层最短解模仿学习(3SIL)以在深度强化学习(RL)设定下学习等式定理证明。自训练模型在准群理论中顶级开放猜想之一的阿贝尔内映射(AIM)猜想所生成的问题上达到了最先进性能。为开发方法,我们首先使用两个更简单的算术重写任务,它们与 AIM 问题共享树结构证明状态和稀疏奖励。在这些任务上,3SIL 被证明显著优于几种成熟的 RL 和模仿学习方法。最终系统在 AIM 问题上以独立和协作模式进行评估。独立 3SIL 训练系统在 60 秒内证明的定理(70.2%)多于复杂的、手工设计的 Waldmeister 系统(65.5%)。在协作模式下,最终系统与 Prover9 系统结合,在 2 秒内证明了独立 Prover9 在 60 秒内证明的内容。
引用
@article{arxiv.2102.05547,
title = {Learning Equational Theorem Proving},
author = {Jelle Piepenbrock and Tom Heskes and Mikoláš Janota and Josef Urban},
journal= {arXiv preprint arXiv:2102.05547},
year = {2021}
}
备注
17 pages, 4 figures