饱和度证明者的 OpenAI Gym 环境
项目描述
运动饱和度
gym-saturation是OpenAI Gym环境的集合，用于强化学习 (RL) 代理努力证明定理。目前，仅支持用TPTP 库形式语言以分句范式 (CNF)编写的定理gym-saturation 实现了“给定子句”算法（类似于 Vampire和E Prover中使用的算法）。
在gym-saturation中有两个环境：SaturationEnv 和VampireEnv。SaturationEnv是一个用 Python 编写的饱和度证明器，灵感来自PyRes。VampireEnv是最近的吸血鬼二进制文件的 Python 包装器，可用于 使用 RL引导吸血鬼。
与典型的自动定理证明器 (ATP) 的单体架构相比，gym-saturation为不同的代理提供了自己选择子句并根据他们的经验进行训练的机会。结合特定的代理，健身饱和度可以作为 ATP 发挥作用。
对于愿意将他们的经验应用于定理证明而无需自己编写所有逻辑相关内容的 RL 从业者来说， gym-saturation可能会很有趣。它对于想要创建 RL 授权的 ATP 的自动推理研究人员也很有用。
如何安装
安装这个包的最好方法是使用pip：
pip install gym-saturation另一种选择是使用conda：
conda install -c conda-forge gym-saturation也可以在 Docker 容器中运行它（使用预打包的 吸血鬼二进制文件）：
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如何使用
import gym_saturation
import gym
import os
env = gym.make(
"GymSaturation-v0", problem_list=["..."]
)
observation = env.reset()
observation, reward, done, info = env.step(action)如何贡献
欢迎请求请求。开始：
git clone https://github.com/inpefess/gym-saturation
cd gym-saturation
# activate python virtual environment with Python 3.7+
pip install -U pip
pip install -U setuptools wheel poetry
poetry install
# recommended but not necessary
pre-commit install
# install vampire binary
wget https://github.com/vprover/vampire/releases/download/v4.7/vampire4.7.zip -O vampire.zip
unzip vampire.zip
# then use vampire_z3_rel_static_HEAD_6295 as an argument or put in $PATH这个包中的所有测试都是 doctests。可以使用以下命令运行它们：
pytest --doctest-modules gym-saturation要在创建拉取请求之前检查代码质量，可以运行脚本local-build.sh。创建 PR 后，它在本地执行与 CI 管道几乎相同的操作。
报告软件问题或问题
欢迎在跟踪器上提出问题和错误报告。
更多文档
更多文档可以在 这里找到。
