HOList: An Environment for Machine Learning of Higher-Order Theorem Proving (extended version)

By Kshitij Bansal, Sarah M. Loos, Markus Norman Rabe, Christian Szegedy, Stewart Wilcox. 2019

59 citations recorded by the source corpus.

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.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, LLM Agents & Tool Use

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computational Theory and Mathematics

In LLM Agents & Tool Use

Citations in the corpus

Measuring Mathematical Problem Solving With the MATH Dataset (2021, methodology): “Bansal et al. (2019) introduce the HOList benchmark for automated theorem proving, which uses a formal language to enable automatic evaluation.”
Mathematical Reasoning via Self-supervised Skip-tree Training (2020, methodology): “To make this measurable, we added the provable statements to the theorem database, and ran the reinforcement learning experiments of the DeepHOL theorem prover [Bansal et al., 2019] to measure how many of the statements were used as premises.”
Language Modeling for Formal Mathematics (2020, methodology): “To make this measurable, we added the provable statements to the theorem database, and ran the reinforcement learning experiments of the DeepHOL theorem prover [Bansal et al., 2019] to measure how many of the statements were used as premises.”
Proof Artifact Co-training for Theorem Proving with Language Models (2021, methodology): “In the setting of HOL Light, and under the assumption of a hardcoded ﬁnite action space of tactics, Bansal et al. (2019a) in conjunction with supervised seed data was able to achieve up to 70% proof success rate on the HOList theorem proving task.”
Improving Graph Neural Network Representations of Logical Formulae with Subgraph Pooling (2019, methodology): “Another approach [19] represented formulae as DAGs with shared subexpressions and used Message-Passing GNNs to generate neural embeddings that could be used to guide theorem proving on a higher-order logic benchmark introduced in [10].”
Learning to Prove Theorems via Interacting with Proof Assistants (2019, methodology): “Compared to prior work that chooses tactics from a fixed set (Huang et al., 2019; Gransden et al., 2015; Gauthier et al., 2018; Bansal et al., 2019), we generate tactics dynamically in the form of abstract syntax trees (ASTs) and synthesize arguments using the available premises during runtime.”
Learning to Reason in Large Theories without Imitation (2019, methodology): “Our baseline solution is the DeepHOL theorem prover as given in Bansal et al. [2019]. They give two related approaches: one is based on pure imitation learning and another employs a combination of imitation learning and reinforcement learning.”
Teaching Temporal Logics to Neural Networks (2020, background): “, 2018; Selsam & Bjørner, 2019) or predicting individual proof steps (Loos et al., 2017; Gauthier et al., 2018; Bansal et al., 2019; Huang et al., 2018).”
Large Language Models for Mathematical Reasoning: Progresses and Challenges (2024, background): “In a similar vein, the HOList benchmark (Bansal et al., 2019), with its comprehensive array of theorem statements from various corpora, sets a sequential proving challenge for ATP systems, where each theorem must be proved using only the lemmas preceding it.”
NaturalProofs: Mathematical Theorem Proving in Natural Language (2021, methodology): “[3] developed the HOList benchmark based on the HOL Light theorem prover, while”