Search papers, labs, and topics across Lattice.
This paper presents a novel approach to automated theorem proving by framing the construction of clausal connection tableaux as a policy in a transition system, allowing for the application of policy-learning methods. By integrating a graph neural network that evaluates proof edits based on transferable structural information, the authors employ imitation learning to enhance the performance of these policies. The results show that their learned policies outperform the leanCoP system, solving up to 46% more problems and achieving proofs with significantly fewer steps within a fixed budget across multiple benchmarks.
Imitation learning enables automated theorem provers to solve 46% more problems while drastically reducing proof steps compared to traditional methods.
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.
