Project proposal: A modular reinforcement learning based automated theorem prover

TL;DR

This paper proposes a modular reinforcement learning framework for automated theorem proving, integrating deductive systems, proof state representations, and training algorithms, with a focus on building a competitive prover.

Contribution

It introduces a Vampire-based environment for reinforcement learning in theorem proving and demonstrates a prototype using existing RL frameworks.

Findings

Developed a Vampire-based environment for RL in theorem proving

Integrated the environment with OpenAI Gym and Ray RLlib

Laid out plans for advancing towards a competitive 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 $\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.