Imitation Learning Increases Automated Theorem Prover Efficiency by 46%

Using graph neural networks and imitation learning on connection-tableau construction, researchers developed policies that solve up to 46% more problems on M2k and TPTP benchmarks than leanCoP. These learned policies reach proofs in an order of magnitude fewer steps by replacing symbolic backtracking with neural-driven decisions.