Imitation Learning for Connection-Tableau Construction
The paper reports learned theorem-proving policies solving up to 46% more benchmark problems than leanCoP under a fixed step budget.
The authors model connection-tableau proof construction as a policy over sound proof edits. A graph neural network scores those edits, trained by imitation learning from proofs already found. They test how the learned policy holds up as symbolic search support is reduced, including a version driven by the network alone. The reported gains come on M2k, MPTP2078-bushy, and TPTP v9.2.1, with proofs reached in about an order of magnitude fewer steps. ArXiv · AI/CL/LG's note
The authors model connection-tableau proof construction as a policy over sound proof edits. A graph neural network scores those edits, trained by imitation learning from proofs already found. They test how the learned policy holds up as symbolic search support is reduced, including a version driven by the network alone. The reported gains come on M2k, MPTP2078-bushy, and TPTP v9.2.1, with proofs reached in about an order of magnitude fewer steps. ArXiv · AI/CL/LG's note
score 4