gym-saturation: Gymnasium environments for saturation provers (System description)
Abstract
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.
Cite
@article{arxiv.2309.09022,
title = {gym-saturation: Gymnasium environments for saturation provers (System description)},
author = {Boris Shminke},
journal= {arXiv preprint arXiv:2309.09022},
year = {2023}
}
Comments
13 pages, 3 figures. This version of the contribution has been accepted for publication, after peer review but is not the Version of Record and does not reflect post-acceptance improvements, or any corrections. The Version of Record is available online at: https://doi.org/10.1007/978-3-031-43513-3_11