# Learning to Guide a Saturation-Based Theorem Prover

arXiv: https://arxiv.org/abs/2106.03906 · HTML: https://mlsanity.com/paper/2106.03906/

## Key facts

- Cited by 15 papers in the map (data through 14 Oct 2026).
- Builds on 30 of its 78 references that are in the map.
- First posted on arXiv 7 Jun 2021.

## Builds on (most cited first, 30 of 30)

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [Deep Residual Learning for Image Recognition](https://mlsanity.com/paper/1512.03385/) (2015)
- [Semi-Supervised Classification with Graph Convolutional Networks](https://mlsanity.com/paper/1609.02907/) (2016)
- [Inductive Representation Learning on Large Graphs](https://mlsanity.com/paper/1706.02216/) (2017)
- [Layer Normalization](https://mlsanity.com/paper/1607.06450/) (2016)
- [Modeling Relational Data with Graph Convolutional Networks](https://mlsanity.com/paper/1703.06103/) (2017)
- [Effective Approaches to Attention-based Neural Machine Translation](https://mlsanity.com/paper/1508.04025/) (2015)
- [Mastering Chess and Shogi by Self-Play with a General Reinforcement Learning Algorithm](https://mlsanity.com/paper/1712.01815/) (2017)
- [Learning a SAT Solver from Single-Bit Supervision](https://mlsanity.com/paper/1802.03685/) (2018)
- [DeepMath - Deep Sequence Models for Premise Selection](https://mlsanity.com/paper/1606.04442/) (2016)
- [Directed Acyclic Graph Neural Networks](https://mlsanity.com/paper/2101.07965/) (2021)
- [Reinforcement Learning of Theorem Proving](https://mlsanity.com/paper/1805.07563/) (2018)
- [Graph Representations for Higher-Order Logic and Theorem Proving](https://mlsanity.com/paper/1905.10006/) (2019)
- [Video Paragraph Captioning Using Hierarchical Recurrent Neural Networks](https://mlsanity.com/paper/1510.07712/) (2015)
- [Deep Network Guided Proof Search](https://mlsanity.com/paper/1701.06972/) (2017)
- [Premise Selection for Theorem Proving by Deep Graph Embedding](https://mlsanity.com/paper/1709.09994/) (2017)
- [Learning to Reason in Large Theories without Imitation](https://mlsanity.com/paper/1905.10501/) (2019)
- [ENIGMA: Efficient Learning-based Inference Guiding Machine](https://mlsanity.com/paper/1701.06532/) (2017)
- [ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E](https://mlsanity.com/paper/1903.03182/) (2019)
- [MizAR 40 for Mizar 40](https://mlsanity.com/paper/1310.2805/) (2013)
- [Property Invariant Embedding for Automated Reasoning](https://mlsanity.com/paper/1911.12073/) (2019)
- [Hammering Mizar by Learning Clause Guidance](https://mlsanity.com/paper/1904.01677/) (2019)
- [Improving Graph Neural Network Representations of Logical Formulae with Subgraph Pooling](https://mlsanity.com/paper/1911.06904/) (2019)
- [HOList: An Environment for Machine Learning of Higher-Order Theorem Proving](https://mlsanity.com/paper/1904.03241/) (2019)
- [Learning to Prove from Synthetic Theorems](https://mlsanity.com/paper/2006.11259/) (2020)
- [Stateful Premise Selection by Recurrent Neural Networks](https://mlsanity.com/paper/2004.08212/) (2020)
- [Towards Finding Longer Proofs](https://mlsanity.com/paper/1905.13100/) (2019)
- [Automated Theorem Proving in Intuitionistic Propositional Logic by Deep Reinforcement Learning](https://mlsanity.com/paper/1811.00796/) (2018)
- [Prolog Technology Reinforcement Learning Prover](https://mlsanity.com/paper/2004.06997/) (2020)
- [Certified Connection Tableaux Proofs for HOL Light and TPTP](https://mlsanity.com/paper/1410.5476/) (2014)

## Built on by (most cited first, 15 of 15)

- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [Proving Theorems using Incremental Learning and Hindsight Experience Replay](https://mlsanity.com/paper/2112.10664/) (2021)
- [Abstract Visual Reasoning: An Algebraic Approach for Solving Raven's Progressive Matrices](https://mlsanity.com/paper/2303.11730/) (2023)
- [Finding Increasingly Large Extremal Graphs with AlphaZero and Tabu Search](https://mlsanity.com/paper/2311.03583/) (2023)
- [An Ensemble Approach for Automated Theorem Proving Based on Efficient Name Invariant Graph Neural Representations](https://mlsanity.com/paper/2305.08676/) (2023)
- [Gym-saturation: an OpenAI Gym environment for saturation provers](https://mlsanity.com/paper/2203.04699/) (2022)
- [Application of AI to formal methods - an analysis of current trends](https://mlsanity.com/paper/2411.14870/) (2024)
- [gym-saturation: Gymnasium environments for saturation provers (System description)](https://mlsanity.com/paper/2309.09022/) (2023)
- [Three Pathways to Neurosymbolic Reinforcement Learning with Interpretable Model and Policy Networks](https://mlsanity.com/paper/2402.05307/) (2024)
- [Hierarchical Attention Generates Better Proofs](https://mlsanity.com/paper/2504.19188/) (2025)
- [Foundation of Intelligence: Review of Math Word Problems from Human Cognition Perspective](https://mlsanity.com/paper/2510.21999/) (2025)
- [From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier](https://mlsanity.com/paper/2607.07779/) (2026)
- [Efficient Neural Clause-Selection Reinforcement](https://mlsanity.com/paper/2503.07792/) (2025)
- [When GNNs Met a Word Equations Solver: Learning to Rank Equations (Extended Technical Report)](https://mlsanity.com/paper/2506.23784/) (2025)
- [An Automated Theorem Generator with Theoretical Foundation Based on Rectangular Standard Contradiction](https://mlsanity.com/paper/2511.04092/) (2025)

## Abstract (arXiv)

Traditional automated theorem provers have relied on manually tuned heuristics to guide how they perform proof search. Recently, however, there has been a surge of interest in the design of learning mechanisms that can be integrated into theorem provers to improve their performance automatically. In this work, we introduce TRAIL, a deep learning-based approach to theorem proving that characterizes core elements of saturation-based theorem proving within a neural framework. TRAIL leverages (a) an effective graph neural network for representing logical formulas, (b) a novel neural representation of the state of a saturation-based theorem prover in terms of processed clauses and available actions, and (c) a novel representation of the inference selection process as an attention-based action policy. We show through a systematic analysis that these components allow TRAIL to significantly outperform previous reinforcement learning-based theorem provers on two standard benchmark datasets (up to 36% more theorems proved). In addition, to the best of our knowledge, TRAIL is the first reinforcement learning-based approach to exceed the performance of a state-of-the-art traditional theorem prover on a standard theorem proving benchmark (solving up to 17% more problems).