mlsanityData to 7 Oct 2026

The Isabelle ENIGMA

arXiv 2205.01981 ↗First posted 4 May 2022cs.AI cs.LG cs.LOcited by 8

Not on the map. Why?

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.

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

Builds on

21 of 54 references.

References · 21

  1. 2019Optuna: A Next-generation Hyperparameter Optimization Frameworkcited by 2,455
  2. 2016DeepMath - Deep Sequence Models for Premise Selectioncited by 80
  3. 2018Reinforcement Learning of Theorem Provingcited by 69
  4. 2018TacticToe: Learning to Prove with Tacticscited by 43
  5. 2017ENIGMA: Efficient Learning-based Inference Guiding Machinecited by 26
  6. 2020ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description)cited by 26
  7. 2019ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for Ecited by 24
  8. 2013MizAR 40 for Mizar 40cited by 23
  9. 2020The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coqcited by 23
  10. 2019Property Invariant Embedding for Automated Reasoningcited by 22
  11. 2019Hammering Mizar by Learning Clause Guidancecited by 20
  12. 2018ATPboost: Learning Premise Selection in Binary Setting with ATP Feedbackcited by 12
9 more
  1. 2020Stateful Premise Selection by Recurrent Neural Networkscited by 11
  2. 2021The Role of Entropy in Guiding a Connection Provercited by 8
  3. 2021Fast and Slow Enigmas and Parental Guidancecited by 8
  4. 2016A Proof Strategy Language and Proof Script Generation for Isabelle/HOLcited by 5
  5. 2016BliStrTune: Hierarchical Invention of Theorem Proving Strategiescited by 5
  6. 2019ENIGMAWatch: ProofWatch Meets ENIGMAcited by 5
  7. 2020Make E Smart Againcited by 4
  8. 2016Encoding Monomorphic and Polymorphic Typescited by 2
  9. 2019GRUNGE: A Grand Unified ATP Challengecited by 2

Built on by

Cited by year

Citing papers per year: 2023: 3; 2024: 5.

8 papers.

  1. 2024A Survey on Deep Learning for Theorem Provingcited by 55
  2. 2023Magnushammer: A Transformer-Based Approach to Premise Selectioncited by 50
  3. 2024Graph2Tac: Online Representation Learning of Formal Math Conceptscited by 15
  4. 2023MizAR 60 for Mizar 50cited by 6
  5. 2024Application of AI to formal methods - an analysis of current trendscited by 2
  6. 2024Solving Hard Mizar Problems with Instantiation and Strategy Inventioncited by 1
  7. 2023Graph Neural Networks For Mapping Variables Between Programs -- Extended Versioncited by 0
  8. 2024Machine Learning for Quantifier Selection in cvc5cited by 0