# Imitation Learning for Connection-Tableau Construction

arXiv: https://arxiv.org/abs/2608.26009 · HTML: https://mlsanity.com/paper/2608.26009/

## Key facts

- No citing papers in the map yet (data through 14 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.

## Placed in

- Offline RL and imitation learning from data / [Imitation learning methods](https://mlsanity.com/offlinerl/imitation-learning-methods/)

## Builds on (most cited first, 6 of 6)

- [How Powerful are Graph Neural Networks?](https://mlsanity.com/paper/1810.00826/) (2018)
- [Modeling Relational Data with Graph Convolutional Networks](https://mlsanity.com/paper/1703.06103/) (2017)
- [An Algorithmic Perspective on Imitation Learning](https://mlsanity.com/paper/1811.06711/) (2018)
- [Reinforcement Learning of Theorem Proving](https://mlsanity.com/paper/1805.07563/) (2018)
- [Property Invariant Embedding for Automated Reasoning](https://mlsanity.com/paper/1911.12073/) (2019)
- [A Curiously Effective Backtracking Strategy for Connection Tableaux](https://mlsanity.com/paper/2106.13722/) (2021)

## 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.