Imitation Learning for Connection-Tableau Construction

Noosaga Placements

• Artificial Intelligencesubfield90%
  The paper addresses automated theorem proving, a core AI problem, and integrates learning with symbolic reasoning.
  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.
• Reinforcement Learningframework80%
  The paper frames proof construction as a policy in a transition system, which is a reinforcement learning perspective, and uses imitation learning (a subfield of RL) to train the policy.
  We cast this construction as a policy acting in a transition systemtrain it by imitation learning from found proofs
• Machine Learningsubfield85%
  The core method is imitation learning (proof cloning) with a graph neural network, which are machine learning techniques.
  train it by imitation learning from found proofsProof cloning (PC) trains on D by supervised action prediction
• Symbolic AIframework75%
  The work is situated within symbolic AI, as it deals with formal calculi and proof systems, but extends them with learning.
  for clausal connection tableauxThe calculus is stated over the resulting matrix M
• Instance-Based Learningframework70%
  The paper uses a graph neural network, which is a deep learning model, to score proof edits.
  We equip such policies with a graph neural network that scores proof edits
• Planning And Searchsubfield70%
  The paper deals with proof search as a planning problem, framing search strategies as policies over a transition system.
  leanCoP-style search and plCoP/rlCoP-style planning then become stateful policies over one interfaceWe zoom out and consider search a part of learnable policy
• Supervised Learningframework70%
  The training method is supervised learning on demonstrated actions (proof cloning), which is a form of supervised learning.
  Proof cloning (PC) trains on D by supervised action prediction
• Knowledge Representation Reasoningsubfield60%
  The work is grounded in formal logic and proof calculi, which are part of knowledge representation and reasoning.
  for clausal connection tableauxThe calculus is stated over the resulting matrix M
• Deep Learningsubfield60%
  The policy uses a graph neural network, a deep learning model, to score proof edits.
  We equip such policies with a graph neural network that scores proof edits
• Plan-Space Planningframework50%
  The paper discusses planning in the context of proof search, but does not use plan-space planning directly.
  plCoP/rlCoP-style planning then become stateful policies over one interface

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.

Paper Context