License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2022.16
URN: urn:nbn:de:0030-drops-167253
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16725/
Go to the corresponding LIPIcs Volume Portal

Goertzel, Zarathustra A. ; Jakubův, Jan ; Kaliszyk, Cezary ; Olšák, Miroslav ; Piepenbrock, Jelle ; Urban, Josef

The Isabelle ENIGMA

pdf-format:
LIPIcs-ITP-2022-16.pdf (0.8 MB)

Abstract

We significantly improve the performance of the E automated theorem prover on the Isabelle Sledgehammer problems by combining learning and theorem proving in several ways. In particular, we develop targeted versions of the ENIGMA guidance for the Isabelle problems, targeted versions of neural premise selection, and targeted strategies for E. The methods are trained in several iterations over hundreds of thousands untyped and typed first-order problems extracted from Isabelle. Our final best single-strategy ENIGMA and premise selection system improves the best previous version of E by 25.3% in 15 seconds, outperforming also all other previous ATP and SMT systems.

BibTeX - Entry

@InProceedings{goertzel_et_al:LIPIcs.ITP.2022.16,
  author =	{Goertzel, Zarathustra A. and Jakub\r{u}v, Jan and Kaliszyk, Cezary and Ol\v{s}\'{a}k, Miroslav and Piepenbrock, Jelle and Urban, Josef},
  title =	{{The Isabelle ENIGMA}},
  booktitle =	{13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages =	{16:1--16:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-252-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{237},
  editor =	{Andronick, June and de Moura, Leonardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2022/16725},
  URN =		{urn:nbn:de:0030-drops-167253},
  doi =		{10.4230/LIPIcs.ITP.2022.16},
  annote =	{Keywords: E Prover, ENIGMA, Premise Selection, Isabelle/Sledgehammer}
}

Keywords: E Prover, ENIGMA, Premise Selection, Isabelle/Sledgehammer
Collection: 13th International Conference on Interactive Theorem Proving (ITP 2022)
Issue Date: 2022
Date of publication: 03.08.2022
Supplementary Material: Dataset: https://github.com/ai4reason/isa_enigma_paper

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI