Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Reinforcement Learning of Theorem Proving

Cezary Kaliszyk, Josef Urban, Henryk Michalewski, Mirek Olšák

TL;DR

This work addresses automated theorem proving by replacing hand-crafted proof-search heuristics with reinforcement learning guided Monte-Carlo planning in a bare connection-based prover. By training on a large corpus and evaluating on unseen problems, the authors show that policy and value learning can substantially improve proof search efficiency, achieving over 40% more solved problems than a strong baseline within the same inference budget. The approach integrates Monte-Carlo Tree Search with learned priors and state evaluations, using engineered features and fast linear/boosting learners to maintain practical runtime. The Miz40 evaluation demonstrates strong generalization and highlights the potential of RL-driven proof search for mathematics and formal verification, with significant performance gains and new solvable theorems beyond traditional systems.

Abstract

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.

Reinforcement Learning of Theorem Proving

TL;DR

This work addresses automated theorem proving by replacing hand-crafted proof-search heuristics with reinforcement learning guided Monte-Carlo planning in a bare connection-based prover. By training on a large corpus and evaluating on unseen problems, the authors show that policy and value learning can substantially improve proof search efficiency, achieving over 40% more solved problems than a strong baseline within the same inference budget. The approach integrates Monte-Carlo Tree Search with learned priors and state evaluations, using engineered features and fast linear/boosting learners to maintain practical runtime. The Miz40 evaluation demonstrates strong generalization and highlights the potential of RL-driven proof search for mathematics and formal verification, with significant performance gains and new solvable theorems beyond traditional systems.

Abstract

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.

Paper Structure

This paper contains 18 sections, 1 equation, 2 figures, 8 tables.

Table of Contents

  1. Introduction
  2. The Game of Connection Based Theorem Proving
  3. The Bare Prover
  4. Guidance
  5. Monte-Carlo Guidance
  6. Policy Learning and Guidance
  7. Value Learning and Guidance
  8. Features
  9. Learners and Their Integration
  10. Experimental Results
  11. Performance without Learning
  12. Reinforcement Learning of Policy Only
  13. Reinforcement Learning of Value Only
  14. Reinforcement Learning of Policy and Value
  15. Evaluation on the Whole Miz40 Dataset
  16. ...and 3 more sections

Figures (2)

  • Figure 1: Closed connection tableau for a set of clauses (adapted from Letz et al. Letz1994ControlledIO).
  • Figure 2: The MCTS tree for the WAYBEL_0:28 problem at the moment when the proof is found. For each node we display the predicted probability $p$, the number of visits $n$ and the average reward $r=w/n$. For the (thicker) nodes leading to the proof the corresponding local proof goals are presented on the right.