gym-saturation#
gym-saturation
is a collection of Gymnasium environments for reinforcement
learning (RL) agents guiding saturation-style automated theorem
provers (ATPs) based on the given clause algorithm.
There are two environments in gym-saturation
following the same
API: SaturationEnv:
VampireEnv
— for Vampire prover, and IProverEnv
— for iProver.
gym-saturation
can be interesting for RL practitioners willing to
apply their experience to theorem proving without coding all the
logic-related stuff themselves.
In particular, ATPs serving as gym-saturation
backends
incapsulate parsing the input formal language (usually, one of the
TPTP (Thousands of Problems for Theorem
Provers) library), transforming the input formulae to the clausal
normal form, and logic
inference using rules such as resolution and
superposition.
How to Install#
Attention
If you want to use VampireEnv
you should have a
Vampire binary on your machine. For example, download the
latest release.
To use IProverEnv
, please download a stable iProver
release or build it from this commit.
The best way to install this package is to use pip
:
pip install gym-saturation
Another option is to use conda
:
conda install -c conda-forge gym-saturation
One can also run it in a Docker container (pre-packed with
vampire
and iproveropt
binaries):
docker build -t gym-saturation https://github.com/inpefess/gym-saturation.git
docker run -it --rm -p 8888:8888 gym-saturation jupyter-lab --ip=0.0.0.0 --port=8888
How to use#
One can use gym-saturation
environments as any other Gymnasium environment:
import gym_saturation
import gymnasium
env = gymnasium.make("Vampire-v0") # or "iProver-v0"
# skip this line to use the default problem
env.set_task("a-TPTP-problem-filename")
observation, info = env.reset()
terminated, truncated = False, False
while not (terminated or truncated):
# apply policy (a random action here)
action = env.action_space.sample()
observation, reward, terminated, truncated, info = env.step(action)
env.close()
Or have a look at the basic tutorial.
For a bit more comprehensive experiments, please see this project.
More Documentation#
More documentation can be found here.
How to Contribute#
Please follow the contribution guide while adhering to the code of conduct.
How to Cite#
If you are writing a research paper and want to cite gym-saturation
, please use the following DOI.