The Isabelle ENIGMA

TL;DR

This paper enhances the E theorem prover's performance on Isabelle Sledgehammer problems by integrating learning-based guidance, premise selection, and strategies, achieving a 25.3% improvement over previous methods.

Contribution

It introduces targeted ENIGMA guidance, neural premise selection, and strategies specifically optimized for Isabelle problems, advancing automated theorem proving techniques.

Findings

25.3% performance improvement over previous E system

Outperforms all previous ATP and SMT systems on Isabelle problems

Effective integration of learning and theorem proving methods

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.