# A Deep Reinforcement Learning Approach to First-Order Logic Theorem Proving

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

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 5 Nov 2019.

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

- [TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning](https://mlsanity.com/paper/2102.09756/) (2021)
- [AI Descartes: Combining Data and Theory for Derivable Scientific Discovery](https://mlsanity.com/paper/2109.01634/) (2021)
- [Deep Explainable Learning with Graph Based Data Assessing and Rule Reasoning](https://mlsanity.com/paper/2211.04693/) (2022)

## Abstract (arXiv)

Automated theorem provers have traditionally relied on manually tuned heuristics to guide how they perform proof search. Deep reinforcement learning has been proposed as a way to obviate the need for such heuristics, however, its deployment in automated theorem proving remains a challenge. In this paper we introduce TRAIL, a system that applies deep reinforcement learning to saturation-based theorem proving. TRAIL leverages (a) a novel neural representation of the state of a theorem prover and (b) a novel characterization of the inference selection process in terms of an attention-based action policy. We show through systematic analysis that these mechanisms allow TRAIL to significantly outperform previous reinforcement-learning-based theorem provers on two benchmark datasets for first-order logic automated theorem proving (proving around 15% more theorems).