# Project proposal: A modular reinforcement learning based automated theorem prover

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 19 of its 35 references that are in the map.
- First posted on arXiv 6 Sep 2022.

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

- [Proximal Policy Optimization Algorithms](https://mlsanity.com/paper/1707.06347/) (2017)
- [IMPALA: Scalable Distributed Deep-RL with Importance Weighted Actor-Learner Architectures](https://mlsanity.com/paper/1802.01561/) (2018)
- [Rainbow: Combining Improvements in Deep Reinforcement Learning](https://mlsanity.com/paper/1710.02298/) (2017)
- [Deep Reinforcement Learning that Matters](https://mlsanity.com/paper/1709.06560/) (2017)
- [Distributed Prioritized Experience Replay](https://mlsanity.com/paper/1803.00933/) (2018)
- [code2vec: Learning Distributed Representations of Code](https://mlsanity.com/paper/1803.09473/) (2018)
- [Formal Mathematics Statement Curriculum Learning](https://mlsanity.com/paper/2202.01344/) (2022)
- [Learning to Prove Theorems via Interacting with Proof Assistants](https://mlsanity.com/paper/1905.09381/) (2019)
- [Reinforcement Learning of Theorem Proving](https://mlsanity.com/paper/1805.07563/) (2018)
- [RLlib: Abstractions for Distributed Reinforcement Learning](https://mlsanity.com/paper/1712.09381/) (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)
- [Towards Finding Longer Proofs](https://mlsanity.com/paper/1905.13100/) (2019)
- [TensorFlow Agents: Efficient Batched Reinforcement Learning in TensorFlow](https://mlsanity.com/paper/1709.02878/) (2017)
- [Recursive Tree Grammar Autoencoders](https://mlsanity.com/paper/2012.02097/) (2020)
- [A Study of Continuous Vector Representationsfor Theorem Proving](https://mlsanity.com/paper/2101.09142/) (2021)
- [Certified Connection Tableaux Proofs for HOL Light and TPTP](https://mlsanity.com/paper/1410.5476/) (2014)
- [Catalyst.RL: A Distributed Framework for Reproducible RL Research](https://mlsanity.com/paper/1903.00027/) (2019)
- [Gym-saturation: an OpenAI Gym environment for saturation provers](https://mlsanity.com/paper/2203.04699/) (2022)

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

- [gym-saturation: Gymnasium environments for saturation provers (System description)](https://mlsanity.com/paper/2309.09022/) (2023)

## Abstract (arXiv)

We propose to build a reinforcement learning prover of independent components: a deductive system (an environment), the proof state representation (how an agent sees the environment), and an agent training algorithm. To that purpose, we contribute an additional Vampire-based environment to textttgym-saturation package of OpenAI Gym environments for saturation provers. We demonstrate a prototype of using textttgym-saturation together with a popular reinforcement learning framework (Ray textttRLlib). Finally, we discuss our plans for completing this work in progress to a competitive automated theorem prover.