Imitation Learning for Connection-Tableau Construction
On the map: Offline RL and imitation learning from data → Imitation learning methods
Abstract (arXiv)
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.
Key facts. No citing papers in the map yet (data through 7 Oct 2026). Placed in Imitation learning methods, one of 13 directions in Offline RL and imitation learning from data. Builds on 6 of its 29 references that are in the map. First posted on arXiv 26 Aug 2026.
Builds on
6 of 29 references.
Closest ancestors · 1
Same direction, newest first
Other references · 5
- 2018How Powerful are Graph Neural Networks?cited by 4,355
- 2017Modeling Relational Data with Graph Convolutional Networkscited by 1,684
- 2018Reinforcement Learning of Theorem Provingcited by 69
- 2019Property Invariant Embedding for Automated Reasoningcited by 22
- 2021A Curiously Effective Backtracking Strategy for Connection Tableauxcited by 1
Built on by
Not cited yet.
Similar, not cited
Close in wording, no citation either way
- 2021Proof Artifact Co-training for Theorem Proving with Language Models
- 2026Direct Optimization of Generators for Search in Automated Theorem Proving
- 2025DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition
- 2025Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving
- 2026FormalRewardBench: A Benchmark for Formal Theorem Proving Reward Models
- 2026Exponential Sample Complexity Separation between Flat and Hierarchical Agentic Theorem Provers
- 2025StepFun-Prover Preview: Let's Think and Verify Step by Step
- 2025CriticLean: Critic-Guided Reinforcement Learning for Mathematical Formalization