HOList：一个用于高阶定理证明机器学习的环境
计算机科学中的逻辑
2019-11-05 v3 人工智能
机器学习
摘要
我们提出一个面向高阶逻辑的环境、基准以及深度学习驱动的自动定理证明器。高阶交互式定理证明器能够对任意数学理论进行形式化，从而为深度学习提供了一个有趣的、开放性的挑战。我们提供了一个基于 HOL Light 定理证明器的开源框架，可用作强化学习环境。HOL Light 附带了关于微积分和开普勒猜想形式化证明的广泛基本数学定理，我们从中导出一个用于自动推理的具有挑战性的基准。我们还提出了一个深度学习强化学习驱动的自动定理证明器 DeepHOL，在该基准上取得了强劲的初步结果。
引用
@article{arxiv.1904.03241,
title = {HOList: An Environment for Machine Learning of Higher-Order Theorem Proving},
author = {Kshitij Bansal and Sarah M. Loos and Markus N. Rabe and Christian Szegedy and Stewart Wilcox},
journal= {arXiv preprint arXiv:1904.03241},
year = {2019}
}
备注
Accepted at ICML 2019