Gym-saturation: an OpenAI Gym environment for saturation provers
Abstract
`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.
Keywords
Cite
@article{arxiv.2203.04699,
title = {Gym-saturation: an OpenAI Gym environment for saturation provers},
author = {Boris Shminke},
journal= {arXiv preprint arXiv:2203.04699},
year = {2022}
}
Comments
6 pages, 1 figure