11
1

Project proposal: A modular reinforcement learning based automated theorem prover

Abstract

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 gym-saturation\texttt{gym-saturation} package of OpenAI Gym environments for saturation provers. We demonstrate a prototype of using gym-saturation\texttt{gym-saturation} together with a popular reinforcement learning framework (Ray RLlib\texttt{RLlib}). Finally, we discuss our plans for completing this work in progress to a competitive automated theorem prover.

View on arXiv
Comments on this paper