Gym-saturation：一个面向饱和证明器的 OpenAI Gym 环境
人工智能
2022-03-10 v1
摘要
gym-saturation 是一个供能够证明定理的强化学习 (RL) 智能体使用的 OpenAI Gym 环境。目前仅支持以 Thousands of Problems for Theorem Provers (TPTP) 库中从句范式 (CNF) 形式化语言书写的定理。gym-saturation 实现了“给定从句”算法（类似于 Vampire 和 E Prover 中所用）。用 Python 编写的 gym-saturation 受 PyRes 启发。与典型自动定理证明器 (ATP) 的整体式架构不同，gym-saturation 赋予不同智能体自行选择从句并从经验中训练的机会。结合特定智能体，gym-saturation 可作为 ATP 工作。即使使用基于启发式但未训练的智能体，gym-saturation 也能为来自 TPTP v7.5.0 的 8257 个 CNF 问题中的 688 个找到反驳。
引用
@article{arxiv.2203.04699,
title = {Gym-saturation: an OpenAI Gym environment for saturation provers},
author = {Boris Shminke},
journal= {arXiv preprint arXiv:2203.04699},
year = {2022}
}
备注
6 pages, 1 figure