论文标题
Prolog Technology增强学习供款者
Prolog Technology Reinforcement Learning Prover
论文作者
论文摘要
我们为实验提供了一个强化学习工具包，并在连接计算中证明了自动定理。该工具包的核心是一种紧凑且易于扩展的称为PLCOP的自动定理供体。 PLCOP建立在LeanCop Prolog实现的基础上，并在RLCOP系统中添加了学习引导的蒙特卡洛树搜索。其他组件包括PLCOP和机器学习者的Python接口，以及一个验证PLCOP证明有效性的外部证明检查器。该工具包在两个基准上进行了评估，我们通过两种添加性证明了它的可扩展性：（1）指导扩展到还原步骤，（2）标准的LeanCop微积分通过重写步骤及其学习的指导扩展。我们认为，序言设置适合组合统计和符号学习方法。完整的工具包已公开发布。
We present a reinforcement learning toolkit for experiments with guiding automated theorem proving in the connection calculus. The core of the toolkit is a compact and easy to extend Prolog-based automated theorem prover called plCoP. plCoP builds on the leanCoP Prolog implementation and adds learning-guided Monte-Carlo Tree Search as done in the rlCoP system. Other components include a Python interface to plCoP and machine learners, and an external proof checker that verifies the validity of plCoP proofs. The toolkit is evaluated on two benchmarks and we demonstrate its extendability by two additions: (1) guidance is extended to reduction steps and (2) the standard leanCoP calculus is extended with rewrite steps and their learned guidance. We argue that the Prolog setting is suitable for combining statistical and symbolic learning methods. The complete toolkit is publicly released.
