..
Copyright 2021-2024 Boris Shminke
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
|PyPI version|\ |Anaconda|\ |CircleCI|\ |Documentation Status|\ |codecov|\ |DOI|
gym-saturation
==============
``gym-saturation`` is a collection of `Gymnasium
<https://gymnasium.farama.org/>`__ environments for reinforcement
learning (RL) agents guiding saturation-style automated theorem
provers (ATPs) based on the `given clause algorithm
<https://royalsocietypublishing.org/doi/10.1098/rsta.2018.0034#d3e468>`__.
There are two environments in ``gym-saturation`` following the same
API: `SaturationEnv
<https://gym-saturation.readthedocs.io/en/latest/environments/saturation-env.html>`__:
``VampireEnv`` --- for `Vampire
<https://github.com/vprover/vampire>`__ prover, and ``IProverEnv``
--- for `iProver <https://gitlab.com/korovin/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 <https://tptp.org/>`__ (Thousands of Problems for Theorem
Provers) library), transforming the input formulae to the `clausal
normal form
<https://en.wikipedia.org/wiki/Conjunctive_normal_form>`__, and logic
inference using rules such as `resolution
<https://en.wikipedia.org/wiki/Resolution_(logic)>`__ and
`superposition
<https://en.wikipedia.org/wiki/Superposition_calculus>`__.
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
<https://github.com/vprover/vampire/releases/tag/v4.8casc2023>`__.
To use ``IProverEnv``, please download a stable iProver
`release
<https://gitlab.com/inpefess/iprover/-/releases/2023.07.13>`__ or build it from `this commit <https://gitlab.com/korovin/iprover/-/commit/11831c13057ff984e62c8acb7226288e7092797a>`__.
The best way to install this package is to use ``pip``:
.. code:: sh
pip install gym-saturation
Another option is to use ``conda``:
.. code:: sh
conda install -c conda-forge gym-saturation
One can also run it in a Docker container (pre-packed with
``vampire`` and ``iproveropt`` binaries):
.. code:: sh
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:
.. code:: python
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 <https://gym-saturation.readthedocs.io/en/latest/auto_examples/plot_age_agent.html>`__.
For a bit more comprehensive experiments, please see `this project <https://github.com/inpefess/ray-prover>`__.
More Documentation
==================
More documentation can be found
`here <https://gym-saturation.readthedocs.io/en/latest>`__.
Related Projects
=================
``gym-saturation`` is compatible with RL-frameworks such as `Ray
RLlib <https://docs.ray.io/en/latest/rllib/package_ref/index.html>`__
and can leverage code embeddings such as `CodeBERT
<https://github.com/microsoft/CodeBERT>`__.
Other projects using RL-guidance for ATPs include:
* `TRAIL <https://github.com/IBM/TRAIL>`__
* `FLoP <https://github.com/atpcurr/atpcurr>`__ (see `the paper <https://doi.org/10.1007/978-3-030-86059-2_10>`__ for more details)
* `lazyCoP <https://github.com/MichaelRawson/lazycop>`__ (see `the paper <https://doi.org/10.1007/978-3-030-86059-2_11>`__ for more details)
Other projects not using RL per se, but iterating a supervised
learning procedure instead:
* ENIGMA (several repos, e.g. `this one
<https://gitlab.ciirc.cvut.cz/chvalkar/iprover-gnn-server>`__ for
iProver; see `the paper <https://doi.org/10.29007/tp23>`__ for
others)
* `Deepire <https://github.com/quickbeam123/deepire-paper-supplementary-materials>`__
How to Contribute
=================
Please follow `the contribution guide <https://gym-saturation.readthedocs.io/en/latest/contributing.html>`__ while adhering to `the code of conduct <https://gym-saturation.readthedocs.io/en/latest/code-of-conduct.html>`__.
How to Cite
============
If you are writing a research paper and want to cite ``gym-saturation``, please use the following `DOI <https://doi.org/10.1007/978-3-031-43513-3_11>`__.
.. |PyPI version| image:: https://badge.fury.io/py/gym-saturation.svg
:target: https://badge.fury.io/py/gym-saturation
.. |CircleCI| image:: https://circleci.com/gh/inpefess/gym-saturation.svg?style=svg
:target: https://circleci.com/gh/inpefess/gym-saturation
.. |Documentation Status| image:: https://readthedocs.org/projects/gym-saturation/badge/?version=latest
:target: https://gym-saturation.readthedocs.io/en/latest/?badge=latest
.. |codecov| image:: https://codecov.io/gh/inpefess/gym-saturation/branch/master/graph/badge.svg
:target: https://codecov.io/gh/inpefess/gym-saturation
.. |DOI| image:: https://img.shields.io/badge/DOI-10.1007%2F978--3--031--43513--3__11-blue
:target: https://doi.org/10.1007/978-3-031-43513-3_11
.. |Anaconda| image:: https://anaconda.org/conda-forge/gym-saturation/badges/version.svg
:target: https://anaconda.org/conda-forge/gym-saturation
Raw data
{
"_id": null,
"home_page": "https://github.com/inpefess/gym-saturation",
"name": "gym-saturation",
"maintainer": "",
"docs_url": null,
"requires_python": ">=3.8.1,<3.13",
"maintainer_email": "",
"keywords": "saturation prover,OpenAI Gym,Gymnasium,automated theorem prover",
"author": "Boris Shminke",
"author_email": "boris@shminke.com",
"download_url": "https://files.pythonhosted.org/packages/3b/a5/e376838023e3e6c027d01f3dc3cb35f398d8dd60480942f146173c473622/gym_saturation-0.11.5.tar.gz",
"platform": null,
"description": "..\n Copyright 2021-2024 Boris Shminke\n\n Licensed under the Apache License, Version 2.0 (the \"License\");\n you may not use this file except in compliance with the License.\n You may obtain a copy of the License at\n\n https://www.apache.org/licenses/LICENSE-2.0\n\n Unless required by applicable law or agreed to in writing, software\n distributed under the License is distributed on an \"AS IS\" BASIS,\n WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.\n See the License for the specific language governing permissions and\n limitations under the License.\n\n|PyPI version|\\ |Anaconda|\\ |CircleCI|\\ |Documentation Status|\\ |codecov|\\ |DOI|\n\ngym-saturation\n==============\n\n``gym-saturation`` is a collection of `Gymnasium\n<https://gymnasium.farama.org/>`__ environments for reinforcement\nlearning (RL) agents guiding saturation-style automated theorem\nprovers (ATPs) based on the `given clause algorithm\n<https://royalsocietypublishing.org/doi/10.1098/rsta.2018.0034#d3e468>`__.\n\nThere are two environments in ``gym-saturation`` following the same\nAPI: `SaturationEnv\n<https://gym-saturation.readthedocs.io/en/latest/environments/saturation-env.html>`__:\n``VampireEnv`` --- for `Vampire\n<https://github.com/vprover/vampire>`__ prover, and ``IProverEnv``\n--- for `iProver <https://gitlab.com/korovin/iprover/>`__.\n\n``gym-saturation`` can be interesting for RL practitioners willing to\napply their experience to theorem proving without coding all the\nlogic-related stuff themselves.\n\nIn particular, ATPs serving as ``gym-saturation`` backends\nincapsulate parsing the input formal language (usually, one of the\n`TPTP <https://tptp.org/>`__ (Thousands of Problems for Theorem\nProvers) library), transforming the input formulae to the `clausal\nnormal form\n<https://en.wikipedia.org/wiki/Conjunctive_normal_form>`__, and logic\ninference using rules such as `resolution\n<https://en.wikipedia.org/wiki/Resolution_(logic)>`__ and\n`superposition\n<https://en.wikipedia.org/wiki/Superposition_calculus>`__.\n\nHow to Install\n==============\n\n.. attention:: If you want to use ``VampireEnv`` you should have a\n Vampire binary on your machine. For example, download the\n latest `release\n <https://github.com/vprover/vampire/releases/tag/v4.8casc2023>`__.\n\n To use ``IProverEnv``, please download a stable iProver \n `release\n <https://gitlab.com/inpefess/iprover/-/releases/2023.07.13>`__ or build it from `this commit <https://gitlab.com/korovin/iprover/-/commit/11831c13057ff984e62c8acb7226288e7092797a>`__.\n\nThe best way to install this package is to use ``pip``:\n\n.. code:: sh\n\n pip install gym-saturation\n\nAnother option is to use ``conda``:\n\n.. code:: sh\n\n conda install -c conda-forge gym-saturation\n \nOne can also run it in a Docker container (pre-packed with\n``vampire`` and ``iproveropt`` binaries):\n\n.. code:: sh\n\n docker build -t gym-saturation https://github.com/inpefess/gym-saturation.git\n docker run -it --rm -p 8888:8888 gym-saturation jupyter-lab --ip=0.0.0.0 --port=8888\n\nHow to use\n==========\n\nOne can use ``gym-saturation`` environments as any other Gymnasium environment:\n\n.. code:: python\n\n import gym_saturation\n import gymnasium\n\n env = gymnasium.make(\"Vampire-v0\") # or \"iProver-v0\"\n # skip this line to use the default problem\n env.set_task(\"a-TPTP-problem-filename\")\n observation, info = env.reset()\n terminated, truncated = False, False\n while not (terminated or truncated):\n # apply policy (a random action here)\n action = env.action_space.sample()\n observation, reward, terminated, truncated, info = env.step(action)\n env.close()\n\nOr have a look at the basic `tutorial <https://gym-saturation.readthedocs.io/en/latest/auto_examples/plot_age_agent.html>`__.\n \nFor a bit more comprehensive experiments, please see `this project <https://github.com/inpefess/ray-prover>`__.\n\nMore Documentation\n==================\n\nMore documentation can be found\n`here <https://gym-saturation.readthedocs.io/en/latest>`__.\n\nRelated Projects\n=================\n\n``gym-saturation`` is compatible with RL-frameworks such as `Ray\nRLlib <https://docs.ray.io/en/latest/rllib/package_ref/index.html>`__\nand can leverage code embeddings such as `CodeBERT\n<https://github.com/microsoft/CodeBERT>`__.\n\nOther projects using RL-guidance for ATPs include:\n\n* `TRAIL <https://github.com/IBM/TRAIL>`__\n* `FLoP <https://github.com/atpcurr/atpcurr>`__ (see `the paper <https://doi.org/10.1007/978-3-030-86059-2_10>`__ for more details)\n* `lazyCoP <https://github.com/MichaelRawson/lazycop>`__ (see `the paper <https://doi.org/10.1007/978-3-030-86059-2_11>`__ for more details)\n\nOther projects not using RL per se, but iterating a supervised\nlearning procedure instead:\n\n* ENIGMA (several repos, e.g. `this one\n <https://gitlab.ciirc.cvut.cz/chvalkar/iprover-gnn-server>`__ for\n iProver; see `the paper <https://doi.org/10.29007/tp23>`__ for\n others)\n* `Deepire <https://github.com/quickbeam123/deepire-paper-supplementary-materials>`__\n\nHow to Contribute\n=================\n\nPlease follow `the contribution guide <https://gym-saturation.readthedocs.io/en/latest/contributing.html>`__ while adhering to `the code of conduct <https://gym-saturation.readthedocs.io/en/latest/code-of-conduct.html>`__.\n\nHow to Cite\n============\n\nIf you are writing a research paper and want to cite ``gym-saturation``, please use the following `DOI <https://doi.org/10.1007/978-3-031-43513-3_11>`__.\n\n.. |PyPI version| image:: https://badge.fury.io/py/gym-saturation.svg\n :target: https://badge.fury.io/py/gym-saturation\n.. |CircleCI| image:: https://circleci.com/gh/inpefess/gym-saturation.svg?style=svg\n :target: https://circleci.com/gh/inpefess/gym-saturation\n.. |Documentation Status| image:: https://readthedocs.org/projects/gym-saturation/badge/?version=latest\n :target: https://gym-saturation.readthedocs.io/en/latest/?badge=latest\n.. |codecov| image:: https://codecov.io/gh/inpefess/gym-saturation/branch/master/graph/badge.svg\n :target: https://codecov.io/gh/inpefess/gym-saturation\n.. |DOI| image:: https://img.shields.io/badge/DOI-10.1007%2F978--3--031--43513--3__11-blue\n :target: https://doi.org/10.1007/978-3-031-43513-3_11\n.. |Anaconda| image:: https://anaconda.org/conda-forge/gym-saturation/badges/version.svg\n :target: https://anaconda.org/conda-forge/gym-saturation\n",
"bugtrack_url": null,
"license": "Apache-2.0",
"summary": "Gymnasium environments for saturation provers",
"version": "0.11.5",
"project_urls": {
"Homepage": "https://github.com/inpefess/gym-saturation",
"Repository": "https://github.com/inpefess/gym-saturation"
},
"split_keywords": [
"saturation prover",
"openai gym",
"gymnasium",
"automated theorem prover"
],
"urls": [
{
"comment_text": "",
"digests": {
"blake2b_256": "e571f04f1a2ee35cb4b3ab17ef9540a3404b2c8071c1971c6cb17ac972a2da92",
"md5": "7faed2c55ac603067617b23254226caa",
"sha256": "beb7cdf2a7dea5a56c9f1ad0e361e4f96c8a8ffd62902a48701a943613e1974d"
},
"downloads": -1,
"filename": "gym_saturation-0.11.5-py3-none-any.whl",
"has_sig": false,
"md5_digest": "7faed2c55ac603067617b23254226caa",
"packagetype": "bdist_wheel",
"python_version": "py3",
"requires_python": ">=3.8.1,<3.13",
"size": 35547,
"upload_time": "2024-02-23T19:44:02",
"upload_time_iso_8601": "2024-02-23T19:44:02.133655Z",
"url": "https://files.pythonhosted.org/packages/e5/71/f04f1a2ee35cb4b3ab17ef9540a3404b2c8071c1971c6cb17ac972a2da92/gym_saturation-0.11.5-py3-none-any.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": "",
"digests": {
"blake2b_256": "3ba5e376838023e3e6c027d01f3dc3cb35f398d8dd60480942f146173c473622",
"md5": "744a9e2f49f796c07ea3e60ddb1551ce",
"sha256": "a65d5a4be8f3191806de2d70b84b880d109fe77522d0c81d7bac6c788b60f85d"
},
"downloads": -1,
"filename": "gym_saturation-0.11.5.tar.gz",
"has_sig": false,
"md5_digest": "744a9e2f49f796c07ea3e60ddb1551ce",
"packagetype": "sdist",
"python_version": "source",
"requires_python": ">=3.8.1,<3.13",
"size": 22770,
"upload_time": "2024-02-23T19:44:04",
"upload_time_iso_8601": "2024-02-23T19:44:04.968548Z",
"url": "https://files.pythonhosted.org/packages/3b/a5/e376838023e3e6c027d01f3dc3cb35f398d8dd60480942f146173c473622/gym_saturation-0.11.5.tar.gz",
"yanked": false,
"yanked_reason": null
}
],
"upload_time": "2024-02-23 19:44:04",
"github": true,
"gitlab": false,
"bitbucket": false,
"codeberg": false,
"github_user": "inpefess",
"github_project": "gym-saturation",
"travis_ci": false,
"coveralls": false,
"github_actions": false,
"circle": true,
"lcname": "gym-saturation"
}
JSON
