连接表演算构造的模仿学习

自动定理证明器逐步构建证明，在每一步选择要添加和要移除的内容。我们将这一构造表示为在由形式演算诱导的转移系统中起作用的策略，该演算规定哪些步骤是正确的：对于子句连接表演算，leanCoP 风格的搜索和 plCoP/rlCoP 风格的规划于是变成了在同一接口上的有状态策略，策略学习方法可以直接应用。我们为这类策略配备一个图神经网络，利用可在不同问题间迁移的结构来为证明编辑打分；再用已找到的证明进行模仿学习训练，并考察当我们移除搜索脚手架时性能如何保持，从完整的符号回溯到仅由网络驱动的策略。在 M2k、MPTP2078-bushy 和 TPTP v9.2.1 上，在固定步数预算内，学习得到的策略比 leanCoP 多解决最多 46% 的问题，并且能以少一个数量级的步数找到证明。