Source-linked AI summary
Reinforcement Learning of Theorem Proving
Cezary Kaliszyk, Josef Urban, Henryk Michalewski, Mirek Olšák
TL;DR
Automated theorem provers remain much weaker than trained mathematicians, motivating a system that guides connection-style search with Monte-Carlo simulations and reinforcement learning rather than domain heuristics. Trained on mathematical problems and evaluated on unseen problems, the system solves more than 40% more problems than a baseline at the same inference budget, while future progress depends on stronger learning architectures for mathematical data.
Problem
Current automated theorem provers remain far weaker than trained mathematicians in most research domains, despite using complete calculi and search heuristics.
Method
The paper builds a bare connection-style prover guided by Monte-Carlo search and reinforcement learning from previous proof searches, without human-designed proof-search restrictions or heuristics.
Results
42.1% more testing problems were proved than by mlCoP at the same inference limit on previously unseen data.
Takeaways & Limitations
The results support reinforcement learning as a viable approach for building general problem solvers for mathematics, verification, and hard sciences.
Takeaways & Limitations
The paper identifies suitable learning architectures that capture syntactic and semantic features of mathematical objects as crucial for training stronger systems.
Abstract
from arXiv · showhide
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.
1 Introduction
The paper addresses the weakness of current automated theorem provers by replacing much human-designed search guidance with Monte-Carlo search and reinforcement learning. Its strongest system improves performance on previously unseen mathematical problems after repeated proving-and-learning iterations.
- Motivation: Current automated theorem provers use complete calculi and search heuristics but remain far weaker than trained mathematicians in most research domains.They are already useful for smaller proof obligations in large interactive theorem-proving projects.
- Contribution: The approach removes the requirement that all shorter proof candidates be tried before a longer proof is found.This enables a bare connection-style prover without that traversal restriction.
- Contribution: The bare prover avoids human-designed proof-search restrictions, heuristics, and targeted decision procedures.This contrasts with mainstream ATP research that increasingly adds sophisticated human-designed procedures.
- Method and evaluation: The authors build systems that add Monte-Carlo tree search plus reinforcement learning for policy and value guidance.The systems are evaluated on a large corpus extracted from the Mizar Mathematical Library.
- Result: After ten proving-and-learning iterations, rlCoP solves significantly more previously unseen problems than leanCoP at the same total inference-step budget.The system initially performs much worse than standard leanCoP before surpassing it.
2 The Game of Connection Based Theorem Proving
Connection-based theorem proving converts first-order problems into clause-based refutation search over tableaux. The bare prover removes iterative deepening, uses random unrestricted steps and Monte-Carlo playouts, and relies on learning to avoid unproductive infinite branches.
- Connection tableau setting: First-order formulas are converted to clause normal form, and proof search seeks a refutation showing the axioms plus the negated conjecture are unsatisfiable.A closed connection tableau is a finished proof tree in which every branch contains complementary literals.
- Connection tableau setting: A connection tableau grows by extension steps that unify a goal with a complementary literal from a new clause and reduction steps that close goals against the active path.Extension can split a branch and instantiate tableau variables.
- The Bare Prover: The prover removes iterative deepening and randomly chooses extension or reduction steps, allowing arbitrary depth and making the bare prover trivially incomplete.Without depth bounds, it may repeatedly extend an infinite branch instead of taking an immediately closing clause.
- The Bare Prover: Monte-Carlo playouts are sequences of extension or reduction inferences from a proof state, with visited search-node counts updated after each playout.Playouts may have a fixed length or continue until reaching a previously unexplored search node.
- The Bare Prover: After groups of b playouts, bigsteps select a single inference and make subsequent playouts start from the resulting tableau.This repeats by alternating batches of playouts with selected bigsteps.
- The Bare Prover: Without guidance or heuristics, the bare prover is typically much weaker than standard mlCoP with iterative deepening.Its unguided behavior alternates random batches of playouts with random bigsteps.
3 Guidance
The guidance system combines Monte-Carlo tree search with learned policy and value estimates to guide theorem-proving inferences. It learns from proof states and actions, using sparse engineered features and fast predictive models integrated into the prover.
- Monte-Carlo guidance: rlCoP combines UCT-based Monte-Carlo tree search with learned policy priors and proof-state value estimates.UCT balances exploration and exploitation during playouts, while policy and value models guide inference selection and state evaluation.
- Baseline evaluation: The default non-learned leaf heuristic assigns value 0.95^Go, where Go is the number of open tableau goals.The value decreases exponentially as the number of open goals increases, favoring states closer to closed tableaux.
- Policy guidance: Policy learning represents each decision using features of the proof state and the selected clause-literal inference.Proof-state features come from the current goal, active path, and whole tableau; action features describe the clause and literal used.
- Value guidance: Value learning labels bigstep proof states according to whether the subsequent search finds a proof and predicts their values by regression.Successful proof searches receive positive values, while unsuccessful searches receive zero; the predictor estimates proof-state value during search.
- Features and learners: The system uses sparse features from terms, clauses, goals, and tableaux, with XGBoost selected over LIBLINEAR for final policy and value learning.The feature set includes term walks and abstract tableau or path statistics; the learner choice reflects better observed performance.
- Integration and cost: Guidance is integrated through the OCaml foreign interface, and the resulting inference slowdown is reported as being in low linear factors.The overhead includes prediction plus feature computation and transformation; inference-speed data are averaged over 2003 problems.
4 Experimental Results
The experiments compare bare, heuristic, policy-guided, value-guided, and jointly guided rlCoP variants against mlCoP on M2k and Miz40. Joint policy-and-value learning gives the strongest results, including a 42.1% improvement over mlCoP on previously unseen Miz40 problems.
- Datasets: The evaluation uses M2k and Miz40 first-order problems exported from the Mizar Mathematical Library, including a 90/10 train/test split for Miz40.Miz40 contains 32524 problems; the split uses 29272 training and 3252 previously unseen test problems.
- 4.1 Performance without Learning: Without learning, the bare prover solves about half as many M2k problems as mlCoP, while non-learning rlCoP improves substantially over the bare prover but remains weaker than mlCoP.The comparison uses a 200000-inference limit and UCT with simple goal-counting evaluation.
- 4.2 Reinforcement Learning of Policy Only: Starting with the fourth iteration, policy-only rlCoP outperforms mlCoP even when mlCoP receives a 4 ∗106-inference limit.Policy training uses data from previous iterations to estimate prior action probabilities in later runs.
- 4.3 Reinforcement Learning of Value Only: Value-only learning nearly reaches mlCoP but remains far below policy-only rlCoP on M2k.Each value-learning iteration trains a new predictor on value data from all previous iterations.
- 4.4 Reinforcement Learning of Policy and Value: 1235 problems are proved at the 20th full-learning iteration, 19.4% more than mlCoP with 4 ∗106 inferences, 13.6% more than policy-only rlCoP, and 44.3% more than value-only rlCoP.The first full-learning iteration improves over mlCoP with 200000 inferences by 18.4%, and the second already exceeds the best policy-only result.
- 4.5 Evaluation on the Whole Miz40 Dataset: On previously unseen Miz40 problems, full rlCoP proves 1624 test problems, 42.1% more than mlCoP with the same inference limit.Policy and value learning use only training-set problems; the result is reported as the final comparison on unseen data.
- 4.6 Examples: The trained prover solves 577 test problems that standard mlCoP cannot, although mlCoP solves 96 problems that rlCoP does not.The final performance difference is 481 problems because theorem proving is almost never monotonically better.
5 Related Work
Prior systems used feedback loops or supervised learning to guide fact selection or internal ATP search. This work distinguishes itself by applying reinforcement-style feedback loops to internal connection-tableau proof search.
- Feedback loops: Earlier feedback-loop systems improved high-level selection of relevant facts while treating internal ATP proof search as a black box.These systems reason over large theories but delegate internal search to standard ATP systems.
- Learning-based ATP guidance: Supervised learning had guided internal ATP search in connection-tableau and saturation-style systems, but reinforcement-style feedback loops had not yet been explored in this setting.The paper positions its approach as extending learning-based ATP guidance beyond supervised methods.
6 Conclusion
The work presents a theorem-proving algorithm requiring practically no domain engineering, using Monte-Carlo simulations guided by reinforcement learning, and reports over 40% greater strength than a baseline on new problems. It identifies stronger learning methods and architectures for mathematical data as important future research.
- Over 40% stronger than the baseline, the trained system solves more nontrivial new problems after learning from a large corpus of general mathematical problems.The comparison is measured in terms of solving nontrivial new problems.
- The algorithm uses Monte-Carlo simulations guided by reinforcement learning from previous proof searches, with practically no domain engineering.
- Suitable deep learning architectures that capture syntactic and semantic features of mathematical objects are identified as crucial for stronger reinforcement-learning assistants.