论文标题
健身房饱和：用于饱和掠夺者的OpenAI健身环境
Gym-saturation: an OpenAI Gym environment for saturation provers
论文作者
论文摘要
“健身房饱和度”是一种能够证明定理的开放式健身环境（RL）特工。当前，仅支持以clausal正常形式（CNF）的数千个问题（TPTP）库的形式语言编写的定理。 “健身房饱和”实现了“给定子句”算法（类似于吸血鬼和e供诗人中使用的算法）。 “体育饱和”是用Python写的，受到Pyres的启发。与典型的自动定理鄙视（ATP）的整体建筑相反，“健身房饱和”为不同的代理商提供了选择自己的条款本身并从经验中进行训练的机会。结合特定的特工，“健身房饱和”可以作为ATP工作。即使有了基于启发式方法的未训练的代理，“健身房饱和”也可以从TPTP v7.5.0中找到688（8257）CNF问题的反驳。
`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.
