Imitation Learning for Connection-Tableau Construction | AI Research

Automated theorem provers construct proofs by making a series of choices, such as which logical rules to apply and when to backtrack. The paper "Imitation Learning for Connection-Tableau Construction" by Fredrik Rømming, Mantas Bakšys, Martin S. Fixman, and Sean B. Holden proposes a framework that treats this construction process as a policy acting within a formal transition system. By separating the logical rules of the calculus from the procedural choices of the search, the authors enable the use of machine learning to guide the prover’s decision-making.

A New Framework for Proof Construction

The authors model the construction of clausal connection tableaux as a transition system where states represent partial proof objects and actions represent logical edits, such as extending a branch or pruning an unsuccessful path. By formalizing the prover this way, the researchers separate the "logical memory" (the current state of the proof) from the "control memory" (the search strategy, such as stacks or depth bounds). This allows the prover to use a graph neural network to score potential proof edits, with the network learning from structure that transfers across different problems.

Learning from Expert Proofs

To train the system, the researchers use imitation learning. They collect successful proofs found by a behavior policy and replay them to generate demonstrations. During this process, the system discards failed search attempts and focuses only on the sequence of actions that led to a closed tableau. This creates a dataset of optimal "expert" moves. The authors employ a method called Proof Aggregation (PA), where the policy is iteratively retrained on the proofs it discovers itself, allowing the model to adapt to the states it visits during its own search.

Performance and Efficiency

The researchers evaluated their learned policies on the M2k, MPTP2078-bushy, and TPTP v9.2.1 datasets. Within a fixed step budget, the learned policies solved up to 46% more problems than the baseline leanCoP prover. Furthermore, the learned approach reached proofs in an order of magnitude fewer steps than the traditional symbolic backtracking methods. The study also measured how performance changed as search scaffolding was removed, transitioning from full symbolic backtracking to a system driven entirely by the neural network.

Considerations for Implementation

The authors note that connection-tableau construction is not inherently "proof confluent," meaning that a commitment to one logical rule may require backtracking later, even if a different choice could have led to a proof. While the transition system is reversible—allowing the prover to undo any edit—the efficiency of the search depends on the policy's ability to navigate these choices. Because the system relies on imitation learning, it is limited by the availability of successful proof paths; if the policy wanders into states not present in any known proof, it lacks explicit guidance, which the authors attempt to mitigate through iterative retraining.