A Learning-Based Fact Selector for Isabelle/HOL

J.C. Blanchette, David Greenaway, Cezary Kaliszyk, Daniel Kühlwein, Josef Urban

Research output: Contribution to JournalArticleAcademicpeer-review

Abstract

Sledgehammer integrates automatic theorem provers in the proof assistant Isabelle/HOL. A key component, the fact selector, heuristically ranks the thousands of facts (lemmas, definitions, or axioms) available and selects a subset, based on syntactic similarity to the current proof goal. We introduce MaSh, an alternative that learns from successful proofs. New challenges arose from our “zero click” vision: MaSh integrates seamlessly with the users’ workflow, so that they benefit from machine learning without having to install software, set up servers, or guide the learning. MaSh outperforms the old fact selector on large formalizations.
Original languageEnglish
Pages (from-to)219-244
Number of pages26
JournalJournal of Automated Reasoning
Volume57
Issue number3
DOIs
Publication statusPublished - 1 Oct 2016
Externally publishedYes

Keywords

  • Automatic theorem provers
  • Machine learning
  • Proof assistants
  • Relevance filtering

Fingerprint Dive into the research topics of 'A Learning-Based Fact Selector for Isabelle/HOL'. Together they form a unique fingerprint.

  • Cite this