Reinforcement Learning of Theorem Proving

By Cezary Kaliszyk, Josef Urban, Henryk Michalewski, M. Olsák. 2018

161 citations recorded by the source corpus.

We introduce a theorem proving algorithm that uses practically no domain heuristics for guiding its connection-style proof search. Instead, it runs many Monte-Carlo simulations guided by reinforcement learning from previous proof attempts. We produce several versions of the prover, parameterized by different learning and guiding algorithms. The strongest version of the system is trained on a large corpus of mathematical problems and evaluated on previously unseen problems. The trained system solves within the same number of inferences over 40% more problems than a baseline prover, which is an unusually high improvement in this hard AI domain. To our knowledge this is the first time reinforcement learning has been convincingly applied to solving general mathematical problems on a large scale.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Reinforcement Learning

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 Reinforcement Learning

Citations in the corpus

Solving Quantitative Reasoning Problems with Language Models (2022, background): “Work on automation of proof assistants and automated theorem provers such as E [26], leanCoP [27], and Vampire [28] has substantially benefited from integration with machine learning methods [29, 30, 31, 32, 33].”
HOList: An Environment for Machine Learning of Higher-Order Theorem Proving (extended version) (2019, methodology): “[25] demonstrated the viability of reinforcement learning with XGBoost and LIBLINEAR [26] on hand engineered features in first order logic context using leanCoP [27] on Mizar mathematical library [13].”
Fast and Slow Enigmas and Parental Guidance (2021, background): “With the recent advent of statistical machine learning (ML), a number of knowledge-based ATP-guiding methods have been created [3,10,11,17].”
INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving (2020, methodology): “Their performances have been improved by machine learning [30, 3, 12, 21, 33, 24, 15].”
Learning dynamic polynomial proofs (2019, unknown): “Recent works have also studied machine learning strategies for automated theorem proving [BLR + 19, HDSS18, KUMO18, GKU + 18].”
An Experimental Study of Formula Embeddings for Automated Theorem Proving in First-Order Logic (2020, background): “2) Best iteration completion performance (Kaliszyk et al. 2018): the ratio of problems solved at the best performing iteration.”
Learning to Reason in Large Theories without Imitation (2019, background): “There are a few automated theorem provers that based on reinforcement learning: Whalen [2016], Kaliszyk et al. [2018] and Zombori et al. [2019], but premise selection tends to be done by ad-hoc, hand engineered mechanisms.”
Learning to Prove Theorems via Interacting with Proof Assistants (2019, methodology): “The proof search has been significantly improved by machine learning (Irving et al., 2016; Wang et al., 2017; Urban et al., 2011; Bridge et al., 2014; Loos et al., 2017; Kaliszyk et al., 2018; Rocktäschel & Riedel, 2017).”
Learning to Prove Theorems by Learning to Generate Theorems (2020, methodology): “Kaliszyk et al. (2018); Bansal et al. (2019a;b) use reinforcement learning to train provers with only human-written theorems but not proofs.”