Imitation Learning for Connection-Tableau Construction

📄 arXiv: 2608.26009v1 📥 PDF

作者: Fredrik Rømming, Mantas Bakšys, Martin S. Fixman, Sean B. Holden

分类: cs.AI, cs.LG, cs.LO

发布日期: 2026-08-26

备注: 9 pages. Code: https://github.com/fredrrom/connections

💡 一句话要点

提出模仿学习方法以构建连接表格

🎯 匹配领域: 支柱二：RL算法与架构 (RL & Architecture)

关键词: 自动定理证明 模仿学习 图神经网络 状态策略 形式演算

📋 核心要点

  1. 现有的定理证明方法在选择步骤时缺乏有效的策略，导致效率低下。
  2. 论文提出通过模仿学习结合图神经网络，构建状态策略以优化证明过程。
  3. 实验结果表明，学习的策略在多个基准上比传统方法提高了46%的问题解决率，并显著减少了步骤数。

📝 摘要（中文）

本论文提出了一种自动定理证明器的构建方法，该方法通过逐步选择添加或移除步骤来生成证明。我们将这一构建过程视为在由形式演算诱导的状态转移系统中进行的策略选择。对于子句连接表格，leanCoP风格的搜索和plCoP/rlCoP风格的规划成为在一个接口上的有状态策略，直接应用策略学习方法。我们为这些策略配备了图神经网络，以评分来自不同问题的结构化证明编辑，通过模仿学习训练，并测量在去除搜索支架后性能的保持情况。在固定步骤预算下，学习的策略在M2k、MPTP2078-bushy和TPTP v9.2.1上解决的问题数量比leanCoP多出46%，并且在更少的步骤内达成证明。

🔬 方法详解

问题定义：本论文旨在解决现有定理证明器在构建证明时效率低下的问题，尤其是在选择添加或移除步骤时缺乏有效策略的挑战。

核心思路：论文的核心思路是将定理证明的构建过程视为在状态转移系统中进行的策略选择，通过模仿学习来训练策略，以提高证明的效率和准确性。

技术框架：整体架构包括一个图神经网络模块，该模块负责评分证明编辑，并通过模仿学习从已找到的证明中进行训练。整个流程从全符号回溯到仅由网络驱动的策略，逐步去除搜索支架。

关键创新：最重要的技术创新在于将图神经网络与模仿学习结合，形成了一种新的状态策略，能够有效地在不同问题间转移学习，显著提升了证明效率。

关键设计：在设计中，关键参数包括图神经网络的结构和损失函数的选择，确保网络能够有效地捕捉到证明编辑的结构特征，并在训练过程中优化策略性能。

🖼️ 关键图片

img_0
img_1
img_2

📊 实验亮点

实验结果显示，学习的策略在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.