# The Isabelle ENIGMA

arXiv: https://arxiv.org/abs/2205.01981 · HTML: https://mlsanity.com/paper/2205.01981/

## Key facts

- Cited by 8 papers in the map (data through 14 Oct 2026).
- Builds on 21 of its 54 references that are in the map.
- First posted on arXiv 4 May 2022.

## Builds on (most cited first, 21 of 21)

- [Optuna: A Next-generation Hyperparameter Optimization Framework](https://mlsanity.com/paper/1907.10902/) (2019)
- [DeepMath - Deep Sequence Models for Premise Selection](https://mlsanity.com/paper/1606.04442/) (2016)
- [Reinforcement Learning of Theorem Proving](https://mlsanity.com/paper/1805.07563/) (2018)
- [TacticToe: Learning to Prove with Tactics](https://mlsanity.com/paper/1804.00596/) (2018)
- [ENIGMA: Efficient Learning-based Inference Guiding Machine](https://mlsanity.com/paper/1701.06532/) (2017)
- [ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description)](https://mlsanity.com/paper/2002.05406/) (2020)
- [ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E](https://mlsanity.com/paper/1903.03182/) (2019)
- [The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coq](https://mlsanity.com/paper/2008.00120/) (2020)
- [MizAR 40 for Mizar 40](https://mlsanity.com/paper/1310.2805/) (2013)
- [Property Invariant Embedding for Automated Reasoning](https://mlsanity.com/paper/1911.12073/) (2019)
- [Hammering Mizar by Learning Clause Guidance](https://mlsanity.com/paper/1904.01677/) (2019)
- [ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback](https://mlsanity.com/paper/1802.03375/) (2018)
- [Stateful Premise Selection by Recurrent Neural Networks](https://mlsanity.com/paper/2004.08212/) (2020)
- [The Role of Entropy in Guiding a Connection Prover](https://mlsanity.com/paper/2105.14706/) (2021)
- [Fast and Slow Enigmas and Parental Guidance](https://mlsanity.com/paper/2107.06750/) (2021)
- [A Proof Strategy Language and Proof Script Generation for Isabelle/HOL](https://mlsanity.com/paper/1606.02941/) (2016)
- [BliStrTune: Hierarchical Invention of Theorem Proving Strategies](https://mlsanity.com/paper/1611.08733/) (2016)
- [ENIGMAWatch: ProofWatch Meets ENIGMA](https://mlsanity.com/paper/1905.09565/) (2019)
- [Make E Smart Again](https://mlsanity.com/paper/2004.08858/) (2020)
- [Encoding Monomorphic and Polymorphic Types](https://mlsanity.com/paper/1609.08916/) (2016)
- [GRUNGE: A Grand Unified ATP Challenge](https://mlsanity.com/paper/1903.02539/) (2019)

## Built on by (most cited first, 8 of 8)

- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [Magnushammer: A Transformer-Based Approach to Premise Selection](https://mlsanity.com/paper/2303.04488/) (2023)
- [Graph2Tac: Online Representation Learning of Formal Math Concepts](https://mlsanity.com/paper/2401.02949/) (2024)
- [MizAR 60 for Mizar 50](https://mlsanity.com/paper/2303.06686/) (2023)
- [Application of AI to formal methods - an analysis of current trends](https://mlsanity.com/paper/2411.14870/) (2024)
- [Solving Hard Mizar Problems with Instantiation and Strategy Invention](https://mlsanity.com/paper/2406.17762/) (2024)
- [Graph Neural Networks For Mapping Variables Between Programs -- Extended Version](https://mlsanity.com/paper/2307.13014/) (2023)
- [Machine Learning for Quantifier Selection in cvc5](https://mlsanity.com/paper/2408.14338/) (2024)

## Abstract (arXiv)

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.