知识卡片：连接Tableau构造的模仿学习

一句话结论：将自动定理证明中的逐步证明构建建模为形式演算转移系统上的策略，并用图神经网络进行模仿学习，可在固定步数预算下显著提升连接Tableau证明器的求解能力：比 leanCoP 最多多解决 46% 的问题，且达到证明所需步数少一个数量级。

事件概述或研究问题：自动定理证明器如何选择下一步在证明中添加或删除什么？本文提出将证明构造视为一个策略，作用在由形式演算诱导的转移系统上；形式演算保证了哪些步骤是合法的（sound）。针对子句连接Tableau，研究将 leanCoP 风格搜索与 plCoP/rlCoP 风格规划统一为同一接口上的有状态策略，从而使策略学习方法可直接应用。

方法/产品要点：

• 证明构造被建模为形式演算转移系统上的策略，每一步对证明状态进行编辑（添加/删除）。
• 对于子句连接Tableau，leanCoP 风格搜索和 plCoP/rlCoP 风格规划被统一为一种有状态策略接口。
• 使用图神经网络对证明编辑进行评分，利用跨问题迁移的结构信息。
• 通过模仿学习，从已经找到的证明中训练策略。
• 评估时逐步移除搜索脚手架，从完整符号回溯一直过渡到仅由网络驱动策略的极端情况。

主要结果或产业意义：在 M2k、MPTP2078-bushy 和 TPTP v9.2.1 基准上，固定步数预算内，学习策略比 leanCoP 解决多达 46% 更多的问题；找到证明所用的步数减少一个数量级。这表明将机器学习与经典连接Tableau搜索相结合，能带来显著的效率提升。

为什么重要：传统自动定理证明依赖人工设计的搜索启发式，本文展示了如何用图神经网络策略从已发现的证明中学习可迁移的步骤选择能力。其增量在于：把搜索和规划统一为可学习的策略接口，并通过模仿学习直接驱动证明构造，而不需要改变底层形式演算的合法性保证。

局限与不确定性：

• 摘要未给出模型参数规模、训练数据规模、训练/推理时间成本，这些信息待核实。
• “多解决 46%”的结果限定在固定步数预算内，未说明完整搜索或时间受限场景下的表现。
• 纯网络驱动（无符号回溯）策略在更广泛问题上的泛化能力尚不清楚。
• 具体实现细节、超参数和复现信息需查阅全文，PDF 内容待核实。

可用于图书/PPT/简报的角度：

• 以“AI 如何一步步构造数学证明”为例，说明将证明过程转化为策略学习任务的新思路。
• 用图神经网络为证明步骤打分，可以类比为“为数学家推荐下一步该做什么”。
• 核心数据对比（多解 46%、步数降低一个数量级）适合作为学习型符号推理潜力的例证。

原始材料：

• 英文标题：Imitation Learning for Connection-Tableau Construction
• 英文关键词：imitation learning, connection tableaux, automated theorem proving, graph neural networks, leanCoP
• arXiv ID：2608.26009v1
• 作者：Fredrik Rømming, Mantas Bakšys, Martin S. Fixman, Sean B. Holden
• 提交/更新：2026-08-26T16:53:25Z
• 分类：cs.AI（另含 cs.LG, cs.LO）
• 来源 URL：https://arxiv.org/abs/2608.26009v1