# Proving Theorems using Incremental Learning and Hindsight Experience Replay

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

## Key facts

- Cited by 13 papers in the map (data through 14 Oct 2026).
- Builds on 22 of its 48 references that are in the map.
- First posted on arXiv 20 Dec 2021.

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

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [Adam: A Method for Stochastic Optimization](https://mlsanity.com/paper/1412.6980/) (2014)
- [Hindsight Experience Replay](https://mlsanity.com/paper/1707.01495/) (2017)
- [A Generalization of Transformer Networks to Graphs](https://mlsanity.com/paper/2012.09699/) (2020)
- [In-Datacenter Performance Analysis of a Tensor Processing Unit](https://mlsanity.com/paper/1704.04760/) (2017)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [Reinforcement Learning of Theorem Proving](https://mlsanity.com/paper/1805.07563/) (2018)
- [Deep Network Guided Proof Search](https://mlsanity.com/paper/1701.06972/) (2017)
- [TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning](https://mlsanity.com/paper/2102.09756/) (2021)
- [ENIGMA: Efficient Learning-based Inference Guiding Machine](https://mlsanity.com/paper/1701.06532/) (2017)
- [ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description)](https://mlsanity.com/paper/2002.05406/) (2020)
- [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)
- [Hammering Mizar by Learning Clause Guidance](https://mlsanity.com/paper/1904.01677/) (2019)
- [Policy-Guided Heuristic Search with Guarantees](https://mlsanity.com/paper/2103.11505/) (2021)
- [Learning to Guide a Saturation-Based Theorem Prover](https://mlsanity.com/paper/2106.03906/) (2021)
- [Learning to Prove from Synthetic Theorems](https://mlsanity.com/paper/2006.11259/) (2020)
- [Training a First-Order Theorem Prover from Synthetic Data](https://mlsanity.com/paper/2103.03798/) (2021)
- [Prolog Technology Reinforcement Learning Prover](https://mlsanity.com/paper/2004.06997/) (2020)
- [Learning-assisted Theorem Proving with Millions of Lemmas](https://mlsanity.com/paper/1402.3578/) (2014)
- [Make E Smart Again](https://mlsanity.com/paper/2004.08858/) (2020)
- [Iterative Budgeted Exponential Search](https://mlsanity.com/paper/1907.13062/) (2019)

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

- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving](https://mlsanity.com/paper/2502.00212/) (2025)
- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [CodeIt: Self-Improving Language Models with Prioritized Hindsight Replay](https://mlsanity.com/paper/2402.04858/) (2024)
- [Proposing and solving olympiad geometry with guided tree search](https://mlsanity.com/paper/2412.10673/) (2024)
- [Shape of Thought: When Distribution Matters More than Correctness in Reasoning Tasks](https://mlsanity.com/paper/2512.22255/) (2025)
- [REFACTOR: Learning to Extract Theorems from Proofs](https://mlsanity.com/paper/2402.17032/) (2024)
- [Finding Increasingly Large Extremal Graphs with AlphaZero and Tabu Search](https://mlsanity.com/paper/2311.03583/) (2023)
- [Learning Guided Automated Reasoning: A Brief Survey](https://mlsanity.com/paper/2403.04017/) (2024)
- [An Ensemble Approach for Automated Theorem Proving Based on Efficient Name Invariant Graph Neural Representations](https://mlsanity.com/paper/2305.08676/) (2023)
- [Application of AI to formal methods - an analysis of current trends](https://mlsanity.com/paper/2411.14870/) (2024)
- [Theoretical Barriers in Bellman-Based Reinforcement Learning](https://mlsanity.com/paper/2502.11968/) (2025)
- [Architecture-driven Shift: towards a lightweight selector for capturing the trends of logit shift](https://mlsanity.com/paper/2605.27469/) (2026)

## Abstract (arXiv)

Traditional automated theorem provers for first-order logic depend on speed-optimized search and many handcrafted heuristics that are designed to work best over a wide range of domains. Machine learning approaches in literature either depend on these traditional provers to bootstrap themselves or fall short on reaching comparable performance. In this paper, we propose a general incremental learning algorithm for training domain specific provers for first-order logic without equality, based only on a basic given-clause algorithm, but using a learned clause-scoring function. Clauses are represented as graphs and presented to transformer networks with spectral features. To address the sparsity and the initial lack of training data as well as the lack of a natural curriculum, we adapt hindsight experience replay to theorem proving, so as to be able to learn even when no proof can be found. We show that provers trained this way can match and sometimes surpass state-of-the-art traditional provers on the TPTP dataset in terms of both quantity and quality of the proofs.