项目提案：基于模块化强化学习的自动定理证明器

我们提议构建一个由独立组件构成的强化学习证明器：演绎系统（环境）、证明状态表示（智能体感知环境的方式）以及智能体训练算法。为此，我们向 OpenAI Gym 的饱和证明器环境包 $\texttt{gym-saturation}$ 贡献了一个额外的基于 Vampire 的环境。我们展示了将 $\texttt{gym-saturation}$ 与流行的强化学习框架（Ray $\texttt{RLlib}$）结合使用的原型。最后，我们讨论了将这项进行中的工作完善为具有竞争力的自动定理证明器的计划。