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

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

145 citations recorded by the source corpus.

Subfields: Natural Language Processing, 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 Natural Language Processing

In LLM Agents & Tool Use

Citations in the corpus

Generative Language Modeling for Automated Theorem Proving (2020, methodology): “Deep learning applied to automated theorem-proving HOList [30] proposes a formal environment based on HOL Light.”
Autoformalization with Large Language Models (2022, methodology): “Newly found correct proofs can then be used as the new training data to improve the neural prover [7, 35, 36].”
HyperTree Proof Search for Neural Theorem Proving (2022, background): “DeepHOL [20] focuses on the HOL-Light environment [21].”
Learning to Prove Theorems by Learning to Generate Theorems (2020, methodology): “Task setup We use the standard theorem proving setup in prior work (Irving et al., 2016; Bansal et al., 2019a).”
IsarStep: a Benchmark for High-level Mathematical Reasoning (2021, methodology): “(2020) pretrain a masked language models on proofs mined from the HOList dataset (Bansal et al., 2019) and apply the pretrained models to the downstream tasks of type inference and predicting conjectures.”
A Survey of Deep Learning for Mathematical Reasoning (2022, unknown): “WaveNet has been applied to theorem proving (Loos et al., 2017; Bansal et al., 2019), due to its ability to address longitudinal time-series data.”
Baldur: Whole-Proof Generation and Repair with Large Language Models (2023, methodology): “Neural theorem provers rely on diverse neural architectures, such as Wavenet [5, 92], graph neural networks [69], short long-term memory models [22], and language models with the transformer architecture [31, 73].”
Modelling High-Level Mathematical Reasoning in Mechanised Declarative Proofs (2020, methodology): “The declarative feature (i.e. focusing on intermediate propositions) was then incorporated into other systems including HOL Light [51], Isabelle [50], and Coq [15].”
Mathematical Reasoning via Self-supervised Skip-tree Training (2020, methodology): “We start from the HOList dataset introduced by Bansal et al. [2019]. The complete dataset includes 29465 theorems and their proofs.”
MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics (2021, methodology): “While we report baseline results on miniF2F using GPT-f , a language model based on GPT-3 which has been ﬁnetuned for theorem proving, language models are not a mandatory approach for Olympiad problems and this assumption is not reﬂected in miniF2F , preserving the generality and widespread applicab”
LeanDojo: Theorem Proving with Retrieval-Augmented Language Models (2023, background): “Existing tools and datasets can be divided by proof assistants: Coq has GamePad [51], CoqGym [9], and PRISM [52]; Isabelle has IsarStep [53] and PISA [15]; HOL Light has HOList [54] and HoLStep [55], and Lean has LeanStep [16] and lean-gym [19].”
Improving Graph Neural Network Representations of Logical Formulae with Subgraph Pooling (2019, methodology): “lar domains (Alama et al.,2014; Irving et al.,2016). At present, there has been a rising interest in developing neural approaches for both the tasks of premise selection and proof step classiﬁcation (Bansal et al., 2019;Kaliszyk et al.,2017;Loos et al.,2017); however, the complex and structured natu”
INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving (2020, methodology): “There have been relatively fewer works [1, 9, 11, 37] on learning-assisted ITP.”
Reasoning with Transformer-based Models: Deep Learning, but Shallow Reasoning (2021, background): “Other mathematical theorem proving datasets in the same spirit are HOList [Bansal et al., 2019] and MetaMathStep [Polu and Sutskever, 2020].”
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.”