HOList: An Environment for Machine Learning of Higher-Order Theorem Proving

TL;DR

This paper introduces HOList, an open-source environment and benchmark for applying deep reinforcement learning to higher-order theorem proving, leveraging HOL Light and demonstrating promising initial results.

Contribution

It provides a novel environment and benchmark for deep learning in higher-order logic theorem proving, along with a deep RL prover, DeepHOL, showing initial success.

Findings

DeepHOL achieves strong initial results on the benchmark.

The environment facilitates reinforcement learning for higher-order logic.

HOL Light covers extensive mathematical theorems, enabling complex reasoning tasks.

Abstract

We present an environment, benchmark, and deep learning driven automated theorem prover for higher-order logic. Higher-order interactive theorem provers enable the formalization of arbitrary mathematical theories and thereby present an interesting, open-ended challenge for deep learning. We provide an open-source framework based on the HOL Light theorem prover that can be used as a reinforcement learning environment. HOL Light comes with a broad coverage of basic mathematical theorems on calculus and the formal proof of the Kepler conjecture, from which we derive a challenging benchmark for automated reasoning. We also present a deep reinforcement learning driven automated theorem prover, DeepHOL, with strong initial results on this benchmark.