Gym-saturation: an OpenAI Gym environment for saturation provers

TL;DR

gym-saturation is an OpenAI Gym environment enabling reinforcement learning agents to prove theorems in formal logic, offering a flexible platform that can function as an automated theorem prover with promising initial results.

Contribution

It introduces a novel RL environment for theorem proving based on the TPTP library, allowing agents to select clauses and learn from experience, diverging from traditional monolithic ATP architectures.

Findings

Can find refutations for 688 out of 8257 TPTP problems

Supports theorem proving in CNF form using RL agents

Provides a flexible, trainable environment for automated theorem proving

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.