摘要

我们介绍了一种适用于高阶逻辑的环境、基准测试和基于深度学习的自动定理证明器。高阶交互式定理证明器能够形式化任意数学理论，因此为深度学习提供了一个有趣且开放性的挑战。我们提供了一个基于HOL Light定理证明器的开源框架，该框架可用作强化学习环境。HOL Light涵盖了微积分和开普勒猜想的形式证明等基本数学定理，从中我们推导出一个用于自动推理的具有挑战性的基准测试。此外，我们还介绍了一种由深度强化学习驱动的自动定理证明器——DeepHOL，在这一基准测试中取得了初步的良好结果。