Sep, 2023
gym-饱和：用于饱和证明器的体育馆环境（系统描述）
gym-saturation: Gymnasium environments for saturation provers (System
description)
TL;DR这项工作描述了之前发布的Python软件包gym-saturation的新版本：这是一个基于给定子句算法和强化学习的OpenAI Gym环境集合。我们提供了两种不同求解器（Vampire和iProver）的使用示例，并将证明状态表示与强化学习分离，并提供了使用已知的ast2vec Python代码嵌入模型作为一阶逻辑表示的示例。此外，我们还展示了环境包装器如何将求解器转化为类似多臂赌博机问题的问题。我们使用Ray RLlib实现了两种强化学习算法（Thompson抽样和Proximal Policy Optimization），以展示我们软件包新版本的实验易用性。