mlsanityData to 7 Oct 2026

ENIGMA: Efficient Learning-based Inference Guiding Machine

arXiv 1701.06532 ↗First posted 23 Jan 2017cs.LO cs.AI cs.LGcited by 26

Not on the map. Why?

Abstract (arXiv)

ENIGMA is a learning-based method for guiding given clause selection in saturation-based theorem provers. Clauses from many proof searches are classified as positive and negative based on their participation in the proofs. An efficient classification model is trained on this data, using fast feature-based characterization of the clauses . The learned model is then tightly linked with the core prover and used as a basis of a new parameterized evaluation heuristic that provides fast ranking of all generated clauses. The approach is evaluated on the E prover and the CASC 2016 AIM benchmark, showing a large increase of E's performance.

Key facts. Cited by 26 papers in the map (data through 7 Oct 2026). First posted on arXiv 23 Jan 2017.

Builds on

No reference list yet.

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2021: 8; 2022: 2; 2023: 6; 2024: 5; 2025: 3; 2026: 2.

26 papers.

Sort:

By area:

  1. 2021Proof Artifact Co-training for Theorem Proving with Language Modelscited by 130
  2. 2024A Survey on Deep Learning for Theorem Provingcited by 55
  3. 2021Learning to Guide a Saturation-Based Theorem Provercited by 15
  4. 2024Graph2Tac: Online Representation Learning of Formal Math Conceptscited by 15
  5. 2021Proving Theorems using Incremental Learning and Hindsight Experience Replaycited by 13
  6. 2021Vampire With a Brain Is a Good ITP Hammercited by 10
  7. 2023Machine-Learned Premise Selection for Leancited by 10
  8. 2021The Role of Entropy in Guiding a Connection Provercited by 8
  9. 2021Fast and Slow Enigmas and Parental Guidancecited by 8
  10. 2022The Isabelle ENIGMAcited by 8
  11. 2021Learning Theorem Proving Componentscited by 7
  12. 2024Learning Guided Automated Reasoning: A Brief Surveycited by 7
14 more
  1. 2023CoProver: A Recommender System for Proof Constructioncited by 5
  2. 2023Lemmas: Generation, Selection, Applicationcited by 3
  3. 2023Reinforcement Learning and Data-Generation for Syntax-Guided Synthesiscited by 3
  4. 2021Improving ENIGMA-Style Clause Selection While Learning From Historycited by 1
  5. 2022Project proposal: A modular reinforcement learning based automated theorem provercited by 1
  6. 2024Solving Hard Mizar Problems with Instantiation and Strategy Inventioncited by 1
  7. 2025Extended Triangular Method: A Generalized Algorithm for Contradiction Separation Based Automated Deductioncited by 1
  8. 2023Safety without alignmentcited by 0
  9. 2023Translating SUMO-K to Higher-Order Set Theorycited by 0
  10. 2024Machine Learning for Quantifier Selection in cvc5cited by 0
  11. 2025Efficient Neural Clause-Selection Reinforcementcited by 0
  12. 2025Partial Label Learning for Automated Theorem Provingcited by 0
  13. 2026Twitch: Learning Abstractions for Equational Theorem Provingcited by 0
  14. 2026High Quality Embeddings for Horn Logic Reasoningcited by 0