mlsanityData to 7 Oct 2026

Project proposal: A modular reinforcement learning based automated theorem prover

arXiv 2209.02562 ↗First posted 6 Sep 2022cs.AIcited by 1

Not on the map. Why?

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.

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

Builds on

19 of 35 references.

References · 19

  1. 2017Proximal Policy Optimization Algorithmscited by 14,441
  2. 2018IMPALA: Scalable Distributed Deep-RL with Importance Weighted Actor-Learner Architecturescited by 866
  3. 2017Rainbow: Combining Improvements in Deep Reinforcement Learningcited by 774
  4. 2017Deep Reinforcement Learning that Matterscited by 727
  5. 2018Distributed Prioritized Experience Replaycited by 260
  6. 2018code2vec: Learning Distributed Representations of Codecited by 249
  7. 2022Formal Mathematics Statement Curriculum Learningcited by 141
  8. 2019Learning to Prove Theorems via Interacting with Proof Assistantscited by 107
  9. 2018Reinforcement Learning of Theorem Provingcited by 69
  10. 2017RLlib: Abstractions for Distributed Reinforcement Learningcited by 53
  11. 2021TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learningcited by 37
  12. 2017ENIGMA: Efficient Learning-based Inference Guiding Machinecited by 26
7 more
  1. 2019Towards Finding Longer Proofscited by 10
  2. 2017TensorFlow Agents: Efficient Batched Reinforcement Learning in TensorFlowcited by 9
  3. 2020Recursive Tree Grammar Autoencoderscited by 5
  4. 2021A Study of Continuous Vector Representationsfor Theorem Provingcited by 4
  5. 2014Certified Connection Tableaux Proofs for HOL Light and TPTPcited by 3
  6. 2019Catalyst.RL: A Distributed Framework for Reproducible RL Researchcited by 3
  7. 2022Gym-saturation: an OpenAI Gym environment for saturation proverscited by 3

Built on by

Cited by year

Citing papers per year: 2023: 1.

1 paper.

  1. 2023gym-saturation: Gymnasium environments for saturation provers (System description)cited by 1