Imitation Learning for Connection-Tableau Construction

AI summary

Overview

Research area: Automated theorem proving, specifically clausal connection tableaux, combined with imitation learning and graph neural networks.

Technical level: Advanced. The paper assumes familiarity with first-order logic, proof calculi, reinforcement/imitation learning, and graph neural networks, though its central idea — treating proof search as a learnable policy — is conceptually simple.

Scope in one sentence: The paper recasts connection-tableau proof construction as a policy acting in a calculus-induced transition system, trains a graph neural network by imitation from successfully found proofs, and measures how much performance survives as symbolic search scaffolding is progressively removed, on M2k, MPTP2078-bushy, and TPTP v9.2.1.

What This Paper Is About

Automated theorem provers build proofs step by step, and the order in which they add or undo proof steps strongly affects whether they succeed — especially in connection tableaux, where the construction is not proof confluent, so a bad early choice can make a proof unreachable even when other choices would have worked. The authors ask whether these procedural control choices can be learned across problems rather than hand-designed.

Their goal is a single framework in which existing provers such as leanCoP, plCoP, and rlCoP are all just different stateful policies over the same interface, so that general policy-learning methods can be applied, and then to test how well a learned policy performs when the classical search machinery (stacks, depth bounds, cuts) is removed.

Key Contributions

1. A transition-system formulation of connection-tableau construction. The formal calculus induces the transition system (fixing which edits are sound); the proof procedure becomes a policy within it. Any policy acting only through the transition function is sound by construction, and undo edits make the state graph reversible.

2. Proof cloning and proof aggregation as imitation learning for provers. Replaying a found closed tableau yields an optimal expert trajectory automatically, stripped of the failed search that surrounded it. Proof cloning is supervised action prediction on these trajectories; proof aggregation is the DAgger-style iterative variant that retrains on proofs the current policy itself finds.

3. A symbol-independent, type-aware graph neural network scorer. A typed graph over syntax nodes (terms, variables, symbols) and occurrence nodes (clauses, literals, goals) with relations including membership, connection, instance, parent, and path, using relational graph convolutions. Symbol identity is excluded, so the encoding is invariant to signature renaming; the matrix subgraph is encoded once per problem and reused.

4. A controlled evaluation that isolates the learned component. Calculus, transition interface, and option profile are held fixed while only the policy varies, across five leanCoP option profiles and three corpora, plus an ablation over three learned policies with progressively more restrictive action spaces.

Main Findings

• Learned policies beat the baseline in every row of the coverage table. Across M2k, MPTP, and TPTP and all five option profiles (default, conj, cut, cut,comp(7), def,scut), at least one learned policy solves more problems than leanCoP. The abstract states learned policies solve up to 46% more problems than leanCoP; the largest relative gain in Table 2 is M2k with the conj profile, 474 to 694.

• The strongest policies are π_dfs and π_id. They take roughly half the rows each. π_markov is inconsistent and falls below the baseline in several rows (for example M2k cut at 583 versus 602, and TPTP conj at 861 versus 999).

• Order-of-magnitude step reductions. At the cut,comp(7) profile on MPTP, π_markov reaches proofs in 11.9 average transition steps versus 188.4 for leanCoP (early stopping), while π_dfs uses 21.7 and π_id uses 158.7.

• A retention versus speed tradeoff driven by action-space width. On MPTP cut,comp(7) under early stopping, π_markov finds 51 new proofs but loses 27; π_dfs finds 94 new and loses 12; π_id finds 60 new and loses 1. Coverage peaks in the middle of this range.

• Proof-only supervision leaves undo behaviour untrained. Proof trajectories contain the successful path alone, so undo edits never appear as labels and a policy that must decide when to backtrack is never trained for it. The authors note that training on search traces rather than proofs alone would supply that signal.

• Most of the retention penalty is scorer error, not intrinsic to a wide action space. Retraining to convergence on MPTP (100% training accuracy or a 200-epoch cap, mean training accuracy rising from 0.975 to 0.995) raises π_markov to 339 solved with 59 new and only 1 lost, and π_dfs to 396 solved with 118 new and 3 lost, while π_markov keeps its order-of-magnitude step advantage (11.3).

• Training to convergence helps policies that rely on learning most. It is worth +34 solved problems to π_markov and +33 to π_dfs, but only +5 to π_id. The authors read this as measuring how much of a policy's behaviour rests on learning rather than imposed search.

• Coverage levels off after the first aggregation iteration. Figure 4 shows all three converged policies clearing the baseline from the first iteration and then plateauing at cut,comp(7) on MPTP, with remaining unsolved problems outside the patterns covered by gathered proofs or beyond the step budget.

• Cost of newly found proofs. π_dfs's average steps rise from 21.7 to 26.6 because of the longer proofs it newly finds; of the 65 problems it gains, all but one previously exhausted the step or time budget.

Methodology in Plain English

The authors write down a formal calculus for clausal connection tableaux — a compact tree-shaped proof object grown by four operations (start, extension, reduction, factorization), with a rigid substitution applied globally and a regularity side condition. From this calculus they build a state space whose states are partial tableaux annotated with the substitution, and whose actions are tableau edits: either append a rule application to an open goal, or prune an existing one. This keeps the transition system "logically honest" — it carries only the tableau, no control memory — while all the bookkeeping that real provers use (search stacks, depth bounds, cuts, planning statistics) is pushed into the policy.

They then show that leanCoP-style search is a stateful policy with a depth-first memory (U_dfs, plus an iterative-deepening bound U_id) that takes the first action in its ordered list, and that options like conj, cut, scut, and comp(I) are simply policy options. They verify stepwise equivalence of their implementation to leanCoP 2.1, ileanCoP 1.2, and MleanCoP 1.3.

Training data comes from found proofs. A closed tableau found by any behaviour policy is replayed from the empty tableau under the target policy, labelling each intermediate state with the next construction action. This discards all the failed search and leaves the trajectory of an optimal expert. Proof cloning fits the policy by maximum likelihood (cross-entropy) on these labels; proof aggregation runs this in a loop, using the current policy as the next round's behaviour policy and adding newly found closed tableaux to the pool, so the training distribution follows states the policy actually visits.

The scorer is a relational graph neural network over a typed graph. Messages are aggregated by a mean within each directed relation and summed across relations, then nodes are updated with a residual around a type-specific self-transform and layer norm. A candidate edit is scored from its type embedding plus the embeddings of its source and target nodes (with a learned null embedding for backtracks). Because message flow is directional, matrix embeddings are computed once and reused; only goal nodes are re-encoded as the tableau grows, and trajectories from one problem share a single matrix encoding within a training batch.

Three learned policies are trained separately because they define different prediction problems over different action sets: π_markov over all of A(s), π_dfs with the stack memory, and π_id with the stack plus iterative-deepening bound. Evaluation is deterministic (argmax), and a problem counts as solved only when a closed tableau is reached; Satisfiable/CounterSatisfiable outcomes give no replay signal.

Hyperparameters came from a one-axis-at-a-time star search on M2k cut,comp(7): width 64, Adam at learning rate 10^-3, batch size 64, trained until five epochs passed with no improvement. The network depth L = 4 was chosen via a Weisfeiler–Leman analysis of an M2k training set. Runs use a budget of 1,000 transition steps and a 120-second wall-clock guard on one Intel Xeon Platinum core under a 3 GB memory limit.

Why This Matters

The paper is a step toward making proof search learnable in a way that is not tied to any one prover's implementation. Because the calculus fixes soundness and the policy only chooses among valid edits, different provers become variants of the same object, and improvements to the learning component can in principle be transferred between them. The coverage results suggest that a graph neural network can replace substantial hand-tuned search control without sacrificing soundness.

Real-world applications:

• Formal verification of software and hardware, where provers must discharge many similar proof obligations and a policy trained across a library could generalize to new ones.
• Formal mathematics and large proof libraries (the Mizar-derived M2k and MPTP corpora are exactly this setting), where proofs found on some problems should help solve others.
• SMT and interactive theorem prover backends, where learned control could cut the time spent on search heuristics.
• Sequential decision-making under non-confluent search more broadly, since the transition-system framing applies to any calculus whose construction steps are non-confluent but reversible.

Industry relevance: the work targets the practical bottleneck in automated reasoning deployments — not the soundness of the calculus, but the cost of search control. An order-of-magnitude reduction in transition steps (11.9 versus 188.4 average on MPTP cut,comp(7)) is directly relevant to compute budgets, and the explicit step budget of 1,000 transitions gives an implementation-independent measure of effort. The authors are careful to state that this is not yet a competition-winning prover and that they do not compare against other connection provers or saturation systems.

Future Directions

• Train on search traces rather than proofs alone. The authors identify this as the missing signal: because trajectories contain only the successful path, undo edits never appear as labels, so policies are never taught when to backtrack. Supplying search traces would target the retention-versus-shortness tradeoff directly.

• Extend and compare beyond a fixed option profile. The evaluation deliberately holds calculus and interface fixed and does not compare against other connection provers or saturation systems, so the learned component's contribution is isolated but its competitiveness is untested. The implementation already supports intuitionistic and modal (QMF) problems over constant, cumulative, and varying domains, while the reported evaluation is classical first-order throughout.

• Abolish the remaining scaffolding entirely. The stated aim is to measure performance as search scaffolding is removed, from full symbolic backtracking to a policy the network drives alone. π_markov, with no memory at all, is the widest action space but still the weakest on retention before convergence — an open question is whether better supervision makes the scaffold-free policy competitive.

• Address the supervision ceiling and the lack of validation. The expert labels only the proof's own path, so unsolved problems yield no labels and off-path states stay unlabeled, bounding what the policy can learn; the paper also reports no held-out validation set, with generalization measured as transfer to unsolved problems and a plateau in coverage after the first aggregation iteration.

Target Audience

Researchers and graduate students in automated theorem proving, automated reasoning, and neuro-symbolic AI; practitioners of imitation learning interested in a domain where expert demonstrations can be recovered exactly from found solutions; and engineers working on proof search backends who want a concrete recipe for replacing hand-tuned search control with a learned scorer. Readers without background in proof calculi or graph neural networks will find the framing accessible but the formalism dense.

Authors’ abstract

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.