发表机构
University of Cambridge（剑桥大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
该研究将连接表构造建模为迁移系统中的策略，结合模仿学习与图神经网络训练策略，在多个基准上较leanCoP提升了定理证明的问题解决率并大幅减少步数。
AI 中文摘要
自动定理证明器逐步构建证明，在每一步选择添加和移除的内容。我们将这种构造视为在形式演算诱导的迁移系统中执行的策略，该演算确定哪些步骤是合理的：对于子句连接表，leanCoP式搜索与plCoP/rlCoP式规划随后成为单个接口上的有状态策略，策略学习方法可直接应用。我们为这类策略配备图神经网络，该网络根据跨问题可迁移的结构对证明编辑进行评分，通过从已找到的证明中进行模仿学习来训练该网络，并测量当移除搜索支撑时性能的保持情况，从完整的符号回溯到仅由网络驱动的策略。在M2k、MPTP2078-bushy和TPTP v9.2.1的固定步数预算内，学习到的策略比leanCoP多解决多达46%的问题，且达到证明所需的步数减少了一个数量级。
英文摘要
An automated theorem prover builds a proof step by step, choosing at each point what to add and what to remove. We cast this construction as a policy acting in a transition system induced by a formal calculus, which fixes which steps are sound: for clausal connection tableaux, leanCoP-style search and plCoP/rlCoP-style planning then become stateful policies over one interface, and policy-learning methods apply directly. We equip such policies with a graph neural network that scores proof edits from structure that transfers across problems, train it by imitation learning from found proofs, and measure how performance holds as we remove search scaffolding, from full symbolic backtracking to a policy the network drives alone. Within a fixed step budget on M2k, MPTP2078-bushy, and TPTP v9.2.1, learned policies solve up to 46% more problems than leanCoP, and reach proofs in an order of magnitude fewer steps.
Comments9 pages. Code: https://github.com/fredrrom/connections
