Download PDFOpen PDF in browserCurrent version

Automated Theorem Proving, Fast and Slow

EasyChair Preprint 4433, version 2

Versions: 123history
13 pagesDate: January 25, 2021

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

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 4433},
  year      = {EasyChair, 2021}}
Download PDFOpen PDF in browserCurrent version