Learning to Reason in Large Theories without Imitation

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

45 citations recorded by the source corpus.

In this paper, we demonstrate how to do automated theorem proving in the presence of a large knowledge base of potential premises without learning from human proofs. We suggest an exploration mechanism that mixes in additional premises selected by a tf-idf (term frequency-inverse document frequency) based lookup in a deep reinforcement learning scenario. This helps with exploring and learning which premises are relevant for proving a new theorem. Our experiments show that the theorem prover trained with this exploration mechanism outperforms provers that are trained only on human proofs. It approaches the performance of a prover trained by a combination of imitation and reinforcement learning. We perform multiple experiments to understand the importance of the underlying assumptions that make our exploration approach work, thus explaining our design choices.

Subfields: Artificial Intelligence, Information Systems, Prompting & Reasoning

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 Information Systems

In Prompting & Reasoning

Citations in the corpus

Generative Language Modeling for Automated Theorem Proving (2020, neutral): “They achieve their best performance [31] with a GNN model designed for premise selection and the use of exploration.”
Formal Mathematics Statement Curriculum Learning (2022, background): “…and lem-mas but very few exercises), we hypothesized that if the difﬁculty of this set of statements was made varied enough, expert iteration could potentially leverage it to effectively shift our models’ distribution closer to miniF2F ’s, and in turn, improve their eventual performance on it.”
An Experimental Study of Formula Embeddings for Automated Theorem Proving in First-Order Logic (2020, background): “Since then, there has been a ﬂurry of activity [ Chvalovsk ´ y et al. , 2019; Bansal et al. , 2019; Ol ˇ s ´ ak et al. , 2019; Crouse et al. , 2019b ] surrounding the applicability of neural networks in the ATP domain.”
LeanDojo: Theorem Proving with Retrieval-Augmented Language Models (2023, background): “…dimensions: proof search algorithms for assembling model-generated steps into complete proofs [17, 21]; overcoming data scarcity through reinforcement learning (RL) [17, 19, 36, 37] or synthetic/auxiliary data [16, 38–40]; as well as outsourcing some proof goals to classical provers [18, 41–43].”
Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs (2022, methodology): “To address the scarcity of formal proofs, previous studies have proposed to use synthetic data (Wu et al., 2021), self-supervision (Polu & Sutskever, 2020; Han et al., 2022), or reinforcement learning (Bansal et al., 2019a; Polu et al., 2022) to synthesize additional formal training data.”
MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics (2021, background): “HOList [2, 3, 10] provides an environment as well as a benchmark for HOL Light.”
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.”
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).”