# Gym-saturation: an OpenAI Gym environment for saturation provers

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

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 6 of its 17 references that are in the map.
- First posted on arXiv 9 Mar 2022.

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

- [OpenAI Gym](https://mlsanity.com/paper/1606.01540/) (2016)
- [Graph Representations for Higher-Order Logic and Theorem Proving](https://mlsanity.com/paper/1905.10006/) (2019)
- [GamePad: A Learning Environment for Theorem Proving](https://mlsanity.com/paper/1806.00608/) (2018)
- [Learning to Reason in Large Theories without Imitation](https://mlsanity.com/paper/1905.10501/) (2019)
- [ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description)](https://mlsanity.com/paper/2002.05406/) (2020)
- [Learning to Guide a Saturation-Based Theorem Prover](https://mlsanity.com/paper/2106.03906/) (2021)

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

- [Application of AI to formal methods - an analysis of current trends](https://mlsanity.com/paper/2411.14870/) (2024)
- [Project proposal: A modular reinforcement learning based automated theorem prover](https://mlsanity.com/paper/2209.02562/) (2022)
- [gym-saturation: Gymnasium environments for saturation provers (System description)](https://mlsanity.com/paper/2309.09022/) (2023)

## Abstract (arXiv)

`gym-saturation` is an OpenAI Gym environment for reinforcement learning (RL) agents capable of proving theorems. Currently, only theorems written in a formal language of the Thousands of Problems for Theorem Provers (TPTP) library in clausal normal form (CNF) are supported. `gym-saturation` implements the 'given clause' algorithm (similar to the one used in Vampire and E Prover). Being written in Python, `gym-saturation` was inspired by PyRes. In contrast to the monolithic architecture of a typical Automated Theorem Prover (ATP), `gym-saturation` gives different agents opportunities to select clauses themselves and train from their experience. Combined with a particular agent, `gym-saturation` can work as an ATP. Even with a non trained agent based on heuristics, `gym-saturation` can find refutations for 688 (of 8257) CNF problems from TPTP v7.5.0.