gym-saturation: Gymnasium environments for saturation provers (System
  description)
Boris Shminke
This work describes a new version of a previously published Python package -
gym-saturation: a collection of OpenAI Gym environments for guiding
saturation-style provers based on the given clause algorithm with reinforcement
learning. We contribute usage examples with two different provers: Vampire and
iProver. We also have decoupled the proof state representation from
reinforcement learning per se and provided examples of using a known ast2vec
Python code embedding model as a first-order logic representation. In addition,
we demonstrate how environment wrappers can transform a prover into a problem
similar to a multi-armed bandit. We applied two reinforcement learning
algorithms (Thompson sampling and Proximal policy optimisation) implemented in
Ray RLlib to show the ease of experimentation with the new release of our
package.