The Isabelle Enigma
Zar Goerzel, Jan Jakubův, Cezary Kaliszyk, Mirek Olšák, Jelle Piepenbroek, Josef Urban13th International Conference on Interactive Theorem Proving, ITP 2022, pp. 16:1—16:21, 2022.
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
@inproceedings{zgjjckmojpju-itp22,
author = {Zar Goerzel and Jan Jakubuv and Cezary Kaliszyk and Mirek Olsak and Jelle Piepenbroek and Josef Urban},
booktitle = {13th International Conference on Interactive Theorem Proving, {ITP} 2022},
doi = {10.4230/LIPIcs.ITP.2022.16},
editor = {June Andronick and Leonardo de Moura},
pages = {16:1--16:21},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik},
series = {LIPIcs},
title = {The Isabelle Enigma},
url = {https://doi.org/10.4230/LIPIcs.ITP.2022.16},
volume = {237},
year = {2022}
}