论文标题
项目建议：基于模块化的基于学习的自动化定理供体
Project proposal: A modular reinforcement learning based automated theorem prover
论文作者
论文摘要
我们建议建立一个独立组件的强化学习谚语：演绎系统（环境），证明状态表示（代理如何看待环境）和代理培训算法。为此，我们为$ \ texttt {Gym-Saturation} $ of Openai Gym Anvironments的$ \ texttt {Gym-Saturation} $ texttt贡献了一个基于吸血鬼的环境。我们演示了使用$ \ texttt {健身房饱和} $的原型，以及流行的增强学习框架（ray $ \ texttt {rllib} $）。最后，我们讨论了完成这项工作中的计划，以进行具有竞争性自动定理供体。
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.
