Download PDFOpen PDF in browser

Automated Theorem Proving, Fast and Slow

EasyChair Preprint no. 4433

13 pagesDate: October 20, 2020

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: asynchronous-policy, Connection tableaux, heuristic search, learned-guidance, Mizar, proof search

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
@Booklet{EasyChair:4433,
  author = {Michael Rawson and Giles Reger},
  title = {Automated Theorem Proving, Fast and Slow},
  howpublished = {EasyChair Preprint no. 4433},

  year = {EasyChair, 2020}}
Download PDFOpen PDF in browser