Imitation Learning for Connection-Tableau Construction· 连接表构建的模仿学习
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,
使用图神经网络和模仿学习优化定理证明的连接表构建政策。
- 核心方法
- 将连接表构建视为状态转换系统中的策略，利用图神经网络评估证明步骤，并通过模仿学习从已发现的证明中训练策略。
- 适合谁读
- 研究者、工程师
- 要解决的问题
- 自动定理证明器在构建证明时需要高效地选择添加和移除的步骤，现有方法存在搜索效率低下和泛化能力不足的问题。
- 关键实验
- 在M2k、MPTP2078-bushy和TPTP v9.2.1数据集上进行了实验，展示了在逐步移除搜索支持情况下的性能保持情况。
- 主要贡献
- 提出了一个基于图神经网络的策略学习方法，可以在不同的问题上泛化，并减少对符号回溯搜索的依赖。
- 意义与局限
- 该方法提高了自动定理证明器的效率和泛化能力，但其效果可能受限于训练数据的质量和多样性。