Source-linked AI summary
Imitation Learning for Connection-Tableau Construction
Fredrik Rømming, Mantas Bakšys, Martin S. Fixman, Sean B. Holden
TL;DR
Connection-tableau provers must control non-confluent proof construction, where admissible choices can require later undoing. The paper casts construction as policy learning over calculus-induced transition systems, trains policies by replaying found proofs, and reports that learned policies solve up to 46% more problems than leanCoP while some reach proofs in an order of magnitude fewer steps.
Problem
Clausal connection-tableau construction has sound local rules but non-confluent control choices, motivating learned procedures that transfer across problems.
Method
The paper models tableau edits as actions in a calculus-induced transition system and trains stateful graph-neural-network policies by imitation from replayed proof trajectories.
Results
Up to 46% more problems are solved than by leanCoP within a fixed step budget, while policy behavior trades proof retention against shorter searches as scaffolding is removed.
Takeaways & Limitations
Separating calculus-valid edits from procedural control enables direct comparison of search and planning policies under a common interface.
Takeaways & Limitations
Proof-only supervision omits undo actions and labels only successful proof paths, leaving states outside those paths unsupervised.
Abstract
from arXiv · showhide
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.
Introduction
The paper reframes proof-procedure control as policy learning over calculus-induced transition systems, focusing on the non-confluent construction choices of clausal connection tableaux. It learns across problems from proof trajectories and evaluates policies as search scaffolding is removed.
- Introduction: Proof calculi fix sound steps, while procedures choose which admissible steps to try, retain, or undo.The framework models the calculus as a transition system and the procedure as a policy within it.
- Introduction: Proof replay labels intermediate proof objects with their next edit, enabling imitation learning across problems and zero-shot evaluation on unseen problems.Newly found proofs are iteratively added to training, while coverage and retention are measured as search scaffolding is removed.
- Introduction: Clausal connection tableaux use one compact tableau rather than a growing set of derived clauses, but admissible choices can make later closure impossible.This loss of proof confluence makes exploration equivalent to modifying the tableau.
- Introduction: Existing connection provers implement different policies for organizing construction choices, from Prolog-style depth-first backtracking to learned alternative ordering.leanCoP uses fixed depth-first, program-order choices, while later variants explore control more freely.
Preliminaries
The preliminaries define stateful policy learning and clausal connection tableaux, including their proof objects, closure condition, local operations, and admissibility constraints. These definitions provide the formal vocabulary for treating tableau construction as controlled proof search.
- Transition Systems, Policies, and Demonstrations: A stateful policy chooses enabled actions from the current state and updates memory that summarizes the trajectory seen so far.Bundling action choice and memory update yields a memoryless policy over the augmented state.
- Transition Systems, Policies, and Demonstrations: Behavioral cloning fits a policy to demonstrated trajectory actions, using state alone for memoryless policies or state plus memory for stateful policies.Imitation learning supplies local action labels rather than delayed reward credit assignment.
- Connection Tableaux: A connection tableau is a finite rooted tree whose branches are closed when they contain complementary literals under a substitution.An unclosed leaf is an open goal, and its active path contains the branch’s ancestor literals.
- Connection Tableaux: The calculus provides start, extension, reduction, and factorization operations for constructing or closing tableau goals.Factorization reuses a solved node, while extension and reduction require a substitution making the goal complementary to a selected literal.
- Connection Tableaux: Regularity removes rule applications that would create two equal same-polarity literals on a branch under the produced substitution.The definitions specify admissible local operations but not the order in which goals or rule instances are tried.
Connection-Tableau Construction as Control
The paper models tableau construction as edits to annotated partial tableaux, with admissibility determined by the calculus and control choices delegated to the policy. This separation preserves soundness while leaving completeness and backtracking behavior to the policy or proof procedure.
- Connection-Tableau Construction as Control: The transition system P(M) uses annotated partial tableaux as states, tableau edits as actions, an empty initial tableau, and closed tableaux as goals.States carry the current rigid substitution and proof-object annotations such as rule applications, parent links, and factorization sources.
- Connection-Tableau Construction as Control: An edit appends an applicable calculus rule or prunes a rule application, with pruning removing dependent applications and resetting introduced constraints.Because substitution is global, dependencies can extend beyond the pruned subtree.
- Connection-Tableau Construction as Control: The tableau determines valid actions through open goals, active paths, substitutions, and rule annotations, while search-stack and frontier information belongs to policy memory.Depth bounds, cuts, failed alternatives, and planning statistics are control memory rather than logical state.
- Connection-Tableau Construction as Control: Any policy acting only through the transition function produces valid partial tableaux, and any terminal goal state is a checkable closed tableau.Completeness instead depends on whether the policy explores reachable proofs fairly enough under its bounds and pruning refinements.
- Connection-Tableau Construction as Control: Figure 3 illustrates that the tableau state and matrix determine enabled edits, including regularity-based exclusion of an otherwise possible extension.In the example, the open ¬P goal closes by reduction against its ancestor P because another extension would duplicate a same-polarity literal.
Learning from Proof-Trajectory Replay
The paper learns proof-construction policies from replayed successful proofs, retaining only proof-producing edits rather than failed search. Proof aggregation expands supervision toward states visited by the current policy, while replay can fail when a target policy cannot expose the demonstrated action.
- Proof-Trajectory Replay: Replay converts found closed tableaux into target-policy trajectories by extracting and reapplying their proof-producing rule applications.Memory updates are replayed when the target policy is stateful.
- Proof-Trajectory Replay: Replay fails when a recovered proof action is unavailable under the target policy’s enabled-action or memory constraints.A growing depth bound may prevent replaying a proof that closes a deep branch first.
- Proof-Trajectory Replay: Replayed demonstrations retain only successful proof actions, removing failed branches, undo actions, and other wasted search effort from the behavior-policy trace.The resulting trajectory is treated as the successful subset of the behavior run rather than the full demonstrator trajectory.
- Proof Cloning: Proof cloning trains by supervised action prediction on replayed proof trajectories using a negative-log-likelihood cross-entropy loss.The dataset consists of replayed proof trajectories, and training decomposes trajectories into per-decision terms.
- Proof Aggregation: Proof aggregation retrains on proofs found by the current policy, reducing behavioral-cloning distribution shift while leaving unsolved and off-proof states unlabeled.Because the expert labels only successful paths, the available supervision remains bounded.
Implementation
The implementation instantiates strategies as policies acting in transition systems fixed by matrix options, with learned policies scoring admissible edits using graph representations of tableau states.
- Prover Infrastructure: Strategies pair a policy type with matrix options and policy options, where matrix options determine the matrix and its transition system.The policy options determine how the policy is built and behaves.
- Prover Infrastructure: The implementation retains input clause and literal order and provides unrestricted-stack and iterative-deepening memory updates for reproducing leanCoP-family search stepwise.Udfs maintains ordered untried actions and undo edits, while Uid adds an iterative-deepening bound.
- Learned Policies: Learned policies replace leanCoP’s first-action head with scores over candidate edits, using increasingly restrictive action sets for πmarkov, πdfs, and πid.Each learned strategy substitutes one of these policy types for πleanCoP.
- Learned Policies: The policy distribution is a softmax over available actions and is fitted with cross-entropy proof cloning, with separate models for each memory-dependent prediction problem.The normalization set differs by memory, so the three policy types define different prediction problems.
- Scorer: The scorer is a graph neural network over a typed graph whose syntax nodes encode shared term structure and occurrence nodes mark proof positions.The matrix subgraph is encoded once per problem, while goal nodes and their relations vary during search.
- Scorer: Hash-consing and type-only node features make the encoding invariant to signature renaming, so scoring does not depend on training-corpus symbol names.Identical ground structures share nodes, while variables derive identity from their edges.
Evaluation
The evaluation isolates learned policy choices within a fixed calculus and interface, testing coverage, proof retention, and step efficiency across corpora, profiles, and training regimes. Learned policies improve coverage broadly, while action-space freedom trades retention for shorter searches and scorer fitting recovers much of that loss.
- Setup: The evaluation fixes the calculus, transition interface, and option profile while varying only the policy, avoiding confounding learned choices with different prover designs.Tests cover M2k, MPTP2078-bushy, and TPTP v9.2.1, with five leanCoP profiles and five proof-aggregation iterations.
- Coverage: A learned policy beats the baseline in every corpus and option-profile row, while πdfs and πid are strongest overall.πmarkov is inconsistent and falls below the baseline in several rows.
- Early stopping: Under early stopping, widening the action space trades retention for shorter searches: πmarkov is fastest but loses the most proofs, whereas πid retains nearly all baseline proofs at the highest step cost.πdfs finds the most proofs and the most new ones, with step counts closer to the baseline than πid.
- Action-space tradeoff: Coverage peaks at an intermediate action-space setting because successful proof trajectories omit undo edits, leaving policies untrained to decide when to backtrack.πdfs preserves omitted backtracking, whereas πmarkov does not; search traces would provide that signal.
- Training to convergence: The largest retention improvement reduces πmarkov’s lost proofs from 27 to 1 and πdfs’s from 12 to 3, while πmarkov keeps its order-of-magnitude step advantage.Step counts otherwise barely move; πdfs rises from 21.7 to 26.6 because it newly finds longer proofs.
- Training to convergence: Training to convergence adds +34 solved problems to πmarkov and +33 to πdfs, but only +5 to πid.The ordering indicates how much each policy’s behavior rests on learning rather than imposed search.
- Aggregation: After five aggregation iterations, converged policies clear the baseline from the first iteration and then level off.Remaining unsolved problems lie outside gathered-proof patterns or beyond the step budget.
Conclusion
The paper frames connection-tableau construction as zero-shot multi-task policy learning over calculus-valid transitions. Proof aggregation trains a graph-neural-network policy from replayed proofs, yielding policy-dependent gains in coverage and step efficiency while exposing a retention tradeoff that scorer fitting largely recovers.
- Conclusion: The framework separates calculus-controlled soundness from procedure-controlled proof-step choices, enabling policy learning across connection-tableau problems.Existing search and planning procedures become stateful policies over the induced transition system.
- Conclusion: Proof cloning and aggregation train a graph-neural-network policy from inference-step labels obtained by replaying found proofs.The transition system admits only calculus-valid edits, leaving soundness with the system.
- Conclusion: πdfs solves up to 46% more problems than the baseline, πmarkov reaches proofs in an order of magnitude fewer steps, and πid retains nearly every baseline proof.These differences reflect the policies’ imposed search structure within a fixed step budget across three benchmarks.
- Conclusion: Under early stopping, less imposed structure buys shorter proofs at the cost of retention, while fitting the scorer largely recovers retention.The conclusion summarizes a policy-dependent tradeoff rather than a single uniformly best behavior.