# gym-saturation: Gymnasium environments for saturation provers (System description)

arXiv: https://arxiv.org/abs/2309.09022 · HTML: https://mlsanity.com/paper/2309.09022/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 15 of its 40 references that are in the map.
- First posted on arXiv 16 Sep 2023.

## Builds on (most cited first, 15 of 15)

- [Language Models are Few-Shot Learners](https://mlsanity.com/paper/2005.14165/) (2020)
- [PyTorch: An Imperative Style, High-Performance Deep Learning Library](https://mlsanity.com/paper/1912.01703/) (2019)
- [LLaMA: Open and Efficient Foundation Language Models](https://mlsanity.com/paper/2302.13971/) (2023)
- [OpenAI Gym](https://mlsanity.com/paper/1606.01540/) (2016)
- [Meta-World: A Benchmark and Evaluation for Multi-Task and Meta Reinforcement Learning](https://mlsanity.com/paper/1910.10897/) (2019)
- [code2vec: Learning Distributed Representations of Code](https://mlsanity.com/paper/1803.09473/) (2018)
- [Property Invariant Embedding for Automated Reasoning](https://mlsanity.com/paper/1911.12073/) (2019)
- [Learning to Guide a Saturation-Based Theorem Prover](https://mlsanity.com/paper/2106.03906/) (2021)
- [Towards Finding Longer Proofs](https://mlsanity.com/paper/1905.13100/) (2019)
- [Recursive Tree Grammar Autoencoders](https://mlsanity.com/paper/2012.02097/) (2020)
- [A Study of Continuous Vector Representationsfor Theorem Proving](https://mlsanity.com/paper/2101.09142/) (2021)
- [Certified Connection Tableaux Proofs for HOL Light and TPTP](https://mlsanity.com/paper/1410.5476/) (2014)
- [Gym-saturation: an OpenAI Gym environment for saturation provers](https://mlsanity.com/paper/2203.04699/) (2022)
- [Interactive Visualization of Saturation Attempts in Vampire](https://mlsanity.com/paper/2001.04100/) (2020)
- [Project proposal: A modular reinforcement learning based automated theorem prover](https://mlsanity.com/paper/2209.02562/) (2022)

## Built on by (most cited first, 1 of 1)

- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)

## Abstract (arXiv)

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.