Automated Theorem Proving, Fast and Slow

EasyChair Preprint 4433, version 3

Abstract

State-of-the-art automated theorem provers explore large search spaces with carefully-engineered routines, but do not learn from past experience as human mathematicians can. Unfortunately, machine-learned heuristics for theorem proving are typically either fast or accurate, not both. Therefore, systems must make a tradeoff between the quality of heuristic guidance and the reduction in inference rate required to use it. We present a system that is completely insulated from heuristic overhead, allowing the use of even deep neural networks with no measurable reduction in inference rate. Given 10 seconds to find proofs in a corpus of mathematics, the system improves from 64% to 70% when trained on its own proofs.

Keyphrases: Connection tableaux, Mizar, asynchronous-policy, heuristic search, learned-guidance, proof search

@booklet{EasyChair:4433,
  author    = {Michael Rawson and Giles Reger},
  title     = {Automated Theorem Proving, Fast and Slow},
  howpublished = {EasyChair Preprint 4433},
  year      = {EasyChair, 2021}}