用模仿学习训练神经网络，自动构建命题演算证明表，效率远超传统方法。
Imitation Learning for Connection-Tableau Construction
- 将证明构造视为状态化策略，用图神经网络学习跨问题的证明编辑评分
- 在固定步数内，解决比leanCoP多46%的问题，且所需步数少一个数量级
- 适合对自动化推理、形式证明生成感兴趣的研究者
自动化定理证明器按步骤构建证明，每一步决定添加或删除内容。本文将其建模为由形式演算诱导的状态转移系统中的策略，确保每一步都合乎逻辑：针对子句连接表，leanCoP式的搜索与plCoP/rlCoP式的规划统一为单一接口上的状态化策略，使策略学习方法可直接应用。我们为策略配备图神经网络，基于已找到的证明进行模仿学习，评估其在逐步移除搜索辅助（从完整符号回溯到仅由网络驱动）时的表现。在固定步数预算下，针对M2k、MPTP2078-bushy和TPTP v9.2.1数据集，学习得到的策略比leanCoP多解决46%的问题，并在数量级更少的步骤内完成证明。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。