# ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description)

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

## Key facts

- Cited by 26 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 13 Feb 2020.

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

- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [Graph2Tac: Online Representation Learning of Formal Math Concepts](https://mlsanity.com/paper/2401.02949/) (2024)
- [Proving Theorems using Incremental Learning and Hindsight Experience Replay](https://mlsanity.com/paper/2112.10664/) (2021)
- [Vampire With a Brain Is a Good ITP Hammer](https://mlsanity.com/paper/2102.03529/) (2021)
- [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)
- [The Isabelle ENIGMA](https://mlsanity.com/paper/2205.01981/) (2022)
- [Learning Theorem Proving Components](https://mlsanity.com/paper/2107.10034/) (2021)
- [Learning Guided Automated Reasoning: A Brief Survey](https://mlsanity.com/paper/2403.04017/) (2024)
- [MizAR 60 for Mizar 50](https://mlsanity.com/paper/2303.06686/) (2023)
- [Learning from Lukasiewicz and Meredith: Investigations into Proof Structures (Extended Version)](https://mlsanity.com/paper/2104.13645/) (2021)
- [An Ensemble Approach for Automated Theorem Proving Based on Efficient Name Invariant Graph Neural Representations](https://mlsanity.com/paper/2305.08676/) (2023)
- [Gym-saturation: an OpenAI Gym environment for saturation provers](https://mlsanity.com/paper/2203.04699/) (2022)
- [Machine Learning Meets The Herbrand Universe](https://mlsanity.com/paper/2210.03590/) (2022)
- [Learning to solve geometric construction problems from images](https://mlsanity.com/paper/2106.14195/) (2021)
- [Investigations into Proof Structures](https://mlsanity.com/paper/2304.12827/) (2023)
- [Application of AI to formal methods - an analysis of current trends](https://mlsanity.com/paper/2411.14870/) (2024)
- [Improving ENIGMA-Style Clause Selection While Learning From History](https://mlsanity.com/paper/2102.13564/) (2021)
- [Adversarial Learning to Reason in an Arbitrary Logic](https://mlsanity.com/paper/2204.02737/) (2022)
- [Guiding Word Equation Solving using Graph Neural Networks (Extended Technical Report)](https://mlsanity.com/paper/2411.15194/) (2024)
- [Feynman on Artificial Intelligence and Machine Learning, with Updates](https://mlsanity.com/paper/2209.00083/) (2022)
- [Translating SUMO-K to Higher-Order Set Theory](https://mlsanity.com/paper/2305.07903/) (2023)
- [Machine Learning for Quantifier Selection in cvc5](https://mlsanity.com/paper/2408.14338/) (2024)
- [Learning Rules Explaining Interactive Theorem Proving Tactic Prediction](https://mlsanity.com/paper/2411.01188/) (2024)
- [Efficient Neural Clause-Selection Reinforcement](https://mlsanity.com/paper/2503.07792/) (2025)
- [When GNNs Met a Word Equations Solver: Learning to Rank Equations (Extended Technical Report)](https://mlsanity.com/paper/2506.23784/) (2025)

## Abstract (arXiv)

We describe an implementation of gradient boosting and neural guidance of saturation-style automated theorem provers that does not depend on consistent symbol names across problems. For the gradient-boosting guidance, we manually create abstracted features by considering arity-based encodings of formulas. For the neural guidance, we use symbol-independent graph neural networks (GNNs) and their embedding of the terms and clauses. The two methods are efficiently implemented in the E prover and its ENIGMA learning-guided framework. To provide competitive real-time performance of the GNNs, we have developed a new context-based approach to evaluation of generated clauses in E. Clauses are evaluated jointly in larger batches and with respect to a large number of already selected clauses (context) by the GNN that estimates their collectively most useful subset in several rounds of message passing. This means that approximative inference rounds done by the GNN are efficiently interleaved with precise symbolic inference rounds done inside E. The methods are evaluated on the MPTP large-theory benchmark and shown to achieve comparable real-time performance to state-of-the-art symbol-based methods. The methods also show high complementarity, solving a large number of hard Mizar problems.