gym-saturation: an OpenAI Gym environment for saturation provers
Boris Shminke · The Journal of Open Source Software · 2022
gym-saturation is an OpenAI Gym (Brockman et al., 2016) 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 (Sutcliffe, 2017) in clausal normal form (CNF) are supported.gym-saturation implements the 'given clause' algorithm (similar to the one used in Vampire (Kovács & Voronkov, 2013) and E Prover (Schulz et al., 2019)).Being written in Python, gym-saturation was inspired by PyRes (Schulz & Pease, 2020).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.