Project proposal: A modular reinforcement learning based automated theorem prover
This work addresses automated theorem proving for AI researchers, but it is incremental as it builds on existing tools and frameworks.
The authors propose building a modular reinforcement learning-based automated theorem prover by integrating a Vampire-based environment into the gym-saturation package and demonstrating a prototype with Ray RLlib, with plans to develop it into a competitive system.
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 $\texttt{gym-saturation}$ package of OpenAI Gym environments for saturation provers. We demonstrate a prototype of using $\texttt{gym-saturation}$ together with a popular reinforcement learning framework (Ray $\texttt{RLlib}$). Finally, we discuss our plans for completing this work in progress to a competitive automated theorem prover.