---
title: "ENIGMA: Efficient Learning-based Inference Guiding Machine"
description: "The authors present this as the first practical learning-based internal guidance for a… 97.6% accuracy. 24 references, cited by 13 papers here."
authors: ["Jan Jakubův", "Josef Urban"]
year: 2017
venue: "arXiv:1701.06532"
source: "https://arxiv.org/abs/1701.06532"
doi: "10.48550/arxiv.1701.06532"
arxiv: "1701.06532"
licence: "arXiv — non-exclusive licence to distribute"
licence_url: "https://arxiv.org/licenses/nonexclusive-distrib/1.0/license.html"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/jakubuv-2017-enigma-efficient-learning-based-inference/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/jakubuv-2017-enigma-efficient-learning-based-inference/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2017](https://md.research.elamur.ai/free/en/papers/2017/page/4/) / ENIGMA: Efficient Learning-based Inference Guiding Machine

# ENIGMA: Efficient Learning-based Inference Guiding Machine

**Authors:** [Jan Jakubův](https://md.research.elamur.ai/free/en/authors/jan-jakubuv/) and [Josef Urban](https://md.research.elamur.ai/free/en/authors/josef-urban/) · **Year:** 2017 · **Venue:** [arXiv:1701.06532](https://md.research.elamur.ai/free/en/venues/lecture-notes-in-computer-science/) ([Lecture notes in computer science 2017](https://md.research.elamur.ai/free/en/venues/lecture-notes-in-computer-science/2017/)) · **Publisher:** [Springer Science+Business Media](https://md.research.elamur.ai/free/en/publishers/springer-science-business-media/) · **Licence:** [arXiv — non-exclusive licence to distribute](https://arxiv.org/licenses/nonexclusive-distrib/1.0/license.html)

**Links:** [Publisher's page](https://arxiv.org/abs/1701.06532) · [PDF](https://arxiv.org/pdf/1701.06532v1) · [DOI 10.48550/arxiv.1701.06532](https://doi.org/10.48550/arxiv.1701.06532) · [arXiv 1701.06532](https://arxiv.org/abs/1701.06532) · [OpenAlex](https://openalex.org/W2581202535)

**Citations:** 54 citations (OpenAlex, 2026-10-14) · [13](https://md.research.elamur.ai/free/en/papers/jakubuv-2017-enigma-efficient-learning-based-inference/cited-by/) in our library, of the 149,439 papers whose bibliographies we read

## Summary
Saturation-based provers such as E must constantly decide which generated clause to process next (given clause selection). Their hand-designed heuristics for this choice fall well short of human mathematical intuition. ENIGMA learns this choice from earlier proof searches. In each successful run, selected clauses that appear in the final proof are labelled positive, and the remaining selected clauses negative. Each clause is encoded as a count vector of length-3 term walks through its literal trees, with variables and Skolem symbols replaced by placeholder symbols. A linear L2-SVM from LIBLINEAR is trained on these vectors. Its prediction, plus a clause-length term scaled by γ, forms a new clause weight function inside E that can run alone or alongside an existing strategy. Training takes seconds, and evaluation costs roughly ten microseconds per clause. On the 200 CASC 2016 AIM competition problems, ENIGMA strategies raised the count from 22 (baseline strategy S0) to 52, and to 57 after boosting positive examples. Vampire solved 47. The authors present this as the first practical learning-based internal guidance for a state-of-the-art ATP.

## Key points
- Pipeline: proof-derived positive/negative clauses → term-walk features → LIBLINEAR L2-SVM classifier → weight function in the E prover.
- Classifier M1 was trained on proofs of 337 solved training problems (6821 positive, 219,012 negative examples) in about 7 s. It reached 97.6% accuracy on the training data.
- With a 180 s limit, the best single strategy (S0 combined with the classifier, frequency 30, γ = 0.2) solved 41 of 200 AIM problems, compared with 22 for S0 alone. Three strategies together solved 52, versus 47 for Vampire given 3×180 s.
- Repeating positive examples ten times produced M2. Its overall accuracy fell (93% vs. 98%), but accuracy on positives rose from 12.5% to 81.8%. M2 added 5 more problems, for 57 in total.
- In total, ENIGMA proved 16 problems that Vampire did not solve. Proposed future work includes learning during the proof search and richer features and learners.

*Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.*

## Institutions

- [Czech Technical University in Prague](https://md.research.elamur.ai/free/en/universities/czech-technical-university-in-prague/) — University, Prague, Czechia · 16 works · 930 citations

📚 Shelves (3): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 19,503 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 18,805 works · [🧮 Computational Theory and Mathematics](https://md.research.elamur.ai/free/en/shelves/computer-science/computational-theory-and-mathematics/) · 496 works

🧭 Topics (1): [🧮 Reasoning](https://md.research.elamur.ai/free/en/topics/reasoning/) · 1,948 works

## Cite

Cite as: Jan Jakubův and Josef Urban. 2017. ENIGMA: Efficient Learning-based Inference Guiding Machine. arXiv:1701.06532.

The paper itself, not this page. BibTeX from the library's record of the work.

```bibtex
@misc{jakubuv2017enigma,
  title = {{ENIGMA: Efficient Learning-based Inference Guiding Machine}},
  author = {Jan Jakubův and Josef Urban},
  year = {2017},
  doi = {10.48550/arxiv.1701.06532},
  eprint = {1701.06532},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.1701.06532}
}
```

- [← previous A Characterization Study of Arabic Twitter Data with a Benchmarking for State-of-the-Art Opinion Mining Models](https://md.research.elamur.ai/free/en/papers/baly-2017-characterization-study-arabic-twitter-data/)
- [next → Learning to Explain Non-Standard English Words and Phrases](https://md.research.elamur.ai/free/en/papers/ni-2017-learning-explain-non-standard-english/)
- [↑ back to papers of 2017](https://md.research.elamur.ai/free/en/papers/2017/page/4/)

## References

24 references, 3 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

1. J. C. Blanchette, D. Greenaway, C. Kaliszyk, D. Kühlwein, and J. Urban. A learning-based fact selector for Isabelle/HOL. J. Autom. Reasoning, 57(3):219–244, 2016. [find](https://scholar.google.com/scholar?q=J%2E+C%2E+Blanchette%2C+D%2E+Greenaway%2C+C%2E+Kaliszyk%2C+D%2E+Ku%CC%88hlwein%2C+and+J%2E+Urban%2E+A+learning%2Dbased+fact+selector+for+Isabelle%2FHOL%2E+J%2E+Autom%2E+Reasoning%2C+57%283%29%3A219%E2%80%93244%2C+2016%2E)
2. J. C. Blanchette, C. Kaliszyk, L. C. Paulson, and J. Urban. [Hammering towards QED](https://md.research.elamur.ai/free/en/papers/blanchette-2016-hammering-qed/). J. Formalized Reasoning, 9(1):101–148, 2016.
3. B. E. Boser, I. Guyon, and V. Vapnik. A training algorithm for optimal margin classifiers. In COLT, pages 144–152. ACM, 1992. [find](https://scholar.google.com/scholar?q=B%2E+E%2E+Boser%2C+I%2E+Guyon%2C+and+V%2E+Vapnik%2E+A+training+algorithm+for+optimal+margin+classifiers%2E+In+COLT%2C+pages+144%E2%80%93152%2E+ACM%2C+1992%2E)
4. R. Fan, K. Chang, C. Hsieh, X. Wang, and C. Lin. LIBLINEAR: A library for large linear classification. Journal of Machine Learning Research, 9:1871–1874, 2008. [find](https://scholar.google.com/scholar?q=R%2E+Fan%2C+K%2E+Chang%2C+C%2E+Hsieh%2C+X%2E+Wang%2C+and+C%2E+Lin%2E+LIBLINEAR%3A+A+library+for+large+linear+classification%2E+Journal+of+Machine+Learning+Research%2C+9%3A1871%E2%80%931874%2C+2008%2E)
5. M. Färber, C. Kaliszyk, and J. Urban. Monte Carlo connection prover. CoRR, abs/1611.05990, 2016. 5 In an initial experiment, a simple nearest-neighbor selection of training problems for the learning further decreases the solving times and proves one more AIM problem unsolved by Prover9. — [arXiv:1611.05990](https://arxiv.org/abs/1611.05990) [find](https://scholar.google.com/scholar?q=M%2E+Fa%CC%88rber%2C+C%2E+Kaliszyk%2C+and+J%2E+Urban%2E+Monte+Carlo+connection+prover%2E+CoRR%2C+abs%2F1611%2E05990%2C+2016%2E+5+In+an+initial+experiment%2C+a+simple+nearest%2Dneighbor+selection+of+training+problems+for+the+learning+)
6. G. Gottlob, G. Sutcliffe, and A. Voronkov, editors. Global Conference on Artificial Intelligence, GCAI 2015, Tbilisi, Georgia, October 16-19, 2015, volume 36 of EPiC Series in Computing. EasyChair, 2015. [find](https://scholar.google.com/scholar?q=G%2E+Gottlob%2C+G%2E+Sutcliffe%2C+and+A%2E+Voronkov%2C+editors%2E+Global+Conference+on+Artificial+Intelligence%2C+GCAI+2015%2C+Tbilisi%2C+Georgia%2C+October+16%2D19%2C+2015%2C+volume+36+of+EPiC+Series+in+Computing%2E+EasyChair%2C+20)
7. T. Gransden, N. Walkinshaw, and R. Raman. SEPIA: search for proofs using inferred automata. In Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings, pages 246–255, 2015. [find](https://scholar.google.com/scholar?q=T%2E+Gransden%2C+N%2E+Walkinshaw%2C+and+R%2E+Raman%2E+SEPIA%3A+search+for+proofs+using+inferred+automata%2E+In+Automated+Deduction+%2D+CADE%2D25+%2D+25th+International+Conference+on+Automated+Deduction%2C+Berlin%2C+Germany%2C+Au)
8. C. Hsieh, K. Chang, C. Lin, S. S. Keerthi, and S. Sundararajan. A dual coordinate descent method for large-scale linear SVM. In ICML, volume 307 of ACM International Conference Proceeding Series, pages 408–415. ACM, 2008. [find](https://scholar.google.com/scholar?q=C%2E+Hsieh%2C+K%2E+Chang%2C+C%2E+Lin%2C+S%2E+S%2E+Keerthi%2C+and+S%2E+Sundararajan%2E+A+dual+coordinate+descent+method+for+large%2Dscale+linear+SVM%2E+In+ICML%2C+volume+307+of+ACM+International+Conference+Proceeding+Series%2C+page)
9. J. Jakubuv and J. Urban. BliStrTune: hierarchical invention of theorem proving strategies. In Y. Bertot and V. Vafeiadis, editors, Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017, pages 43–52. ACM, 2017. [find](https://scholar.google.com/scholar?q=J%2E+Jakubuv+and+J%2E+Urban%2E+BliStrTune%3A+hierarchical+invention+of+theorem+proving+strategies%2E+In+Y%2E+Bertot+and+V%2E+Vafeiadis%2C+editors%2C+Proceedings+of+the+6th+ACM+SIGPLAN+Conference+on+Certified+Programs+a)
10. C. Kaliszyk and J. Urban. [Learning-assisted automated reasoning with Flyspeck](https://md.research.elamur.ai/free/en/papers/kaliszyk-2012-learning-assisted-automated-reasoning-flyspeck/). J. Autom. Reasoning, 53(2):173–213, 2014.
11. C. Kaliszyk and J. Urban. FEMaLeCoP: Fairly efficient machine learning connection prover. In M. Davis, A. Fehnker, A. McIver, and A. Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proce… [find](https://scholar.google.com/scholar?q=C%2E+Kaliszyk+and+J%2E+Urban%2E+FEMaLeCoP%3A+Fairly+efficient+machine+learning+connection+prover%2E+In+M%2E+Davis%2C+A%2E+Fehnker%2C+A%2E+McIver%2C+and+A%2E+Voronkov%2C+editors%2C+Logic+for+Programming%2C+Artificial+Intelligence%2C+)
12. C. Kaliszyk and J. Urban. [MizAR 40 for Mizar 40](https://md.research.elamur.ai/free/en/papers/kaliszyk-2013-mizar-40-mizar-40/). J. Autom. Reasoning, 55(3):245–256, 2015.
13. C. Kaliszyk, J. Urban, and J. Vyskočil. Machine learner for automated reasoning 0.4 and 0.5. CoRR, abs/1402.2359, 2014. Accepted to PAAR’14. — [arXiv:1402.2359](https://arxiv.org/abs/1402.2359) [find](https://scholar.google.com/scholar?q=C%2E+Kaliszyk%2C+J%2E+Urban%2C+and+J%2E+Vyskoc%CC%8Cil%2E+Machine+learner+for+automated+reasoning+0%2E4+and+0%2E5%2E+CoRR%2C+abs%2F1402%2E2359%2C+2014%2E+Accepted+to+PAAR%E2%80%9914%2E+%E2%80%94+%5BarXiv%3A1402%2E2359%5D%28https%3A%2F%2Farxiv%2Eorg%2Fabs%2F1402%2E2359%29)
14. C. Kaliszyk, J. Urban, and J. Vyskočil. Efficient semantic features for automated reasoning over large theories. In Q. Yang and M. Wooldridge, editors, IJCAI’15, pages 3084–3090. AAAI Press, 2015. [find](https://scholar.google.com/scholar?q=C%2E+Kaliszyk%2C+J%2E+Urban%2C+and+J%2E+Vyskoc%CC%8Cil%2E+Efficient+semantic+features+for+automated+reasoning+over+large+theories%2E+In+Q%2E+Yang+and+M%2E+Wooldridge%2C+editors%2C+IJCAI%E2%80%9915%2C+pages+3084%E2%80%933090%2E+AAAI+Press%2C+2015%2E)
15. L. Kovács and A. Voronkov. First-order theorem proving and Vampire. In N. Sharygina and H. Veith, editors, CAV, volume 8044 of LNCS, pages 1–35. Springer, 2013. [find](https://scholar.google.com/scholar?q=L%2E+Kova%CC%81cs+and+A%2E+Voronkov%2E+First%2Dorder+theorem+proving+and+Vampire%2E+In+N%2E+Sharygina+and+H%2E+Veith%2C+editors%2C+CAV%2C+volume+8044+of+LNCS%2C+pages+1%E2%80%9335%2E+Springer%2C+2013%2E)
16. D. Kühlwein and J. Urban. MaLeS: A framework for automatic tuning of automated theorem provers. J. Autom. Reasoning, 55(2):91–116, 2015. [find](https://scholar.google.com/scholar?q=D%2E+Ku%CC%88hlwein+and+J%2E+Urban%2E+MaLeS%3A+A+framework+for+automatic+tuning+of+automated+theorem+provers%2E+J%2E+Autom%2E+Reasoning%2C+55%282%29%3A91%E2%80%93116%2C+2015%2E)
17. C. Lin, R. C. Weng, and S. S. Keerthi. Trust region newton method for logistic regression. Journal of Machine Learning Research, 9:627–650, 2008. [find](https://scholar.google.com/scholar?q=C%2E+Lin%2C+R%2E+C%2E+Weng%2C+and+S%2E+S%2E+Keerthi%2E+Trust+region+newton+method+for+logistic+regression%2E+Journal+of+Machine+Learning+Research%2C+9%3A627%E2%80%93650%2C+2008%2E)
18. J. Otten and W. Bibel. leanCoP: lean connection-based theorem proving. J. Symb. Comput., 36(1-2):139–161, 2003. [find](https://scholar.google.com/scholar?q=J%2E+Otten+and+W%2E+Bibel%2E+leanCoP%3A+lean+connection%2Dbased+theorem+proving%2E+J%2E+Symb%2E+Comput%2E%2C+36%281%2D2%29%3A139%E2%80%93161%2C+2003%2E)
19. S. Schäfer and S. Schulz. Breeding theorem proving heuristics with genetic algorithms. In Gottlob et al. [6], pages 263–274. [find](https://scholar.google.com/scholar?q=S%2E+Scha%CC%88fer+and+S%2E+Schulz%2E+Breeding+theorem+proving+heuristics+with+genetic+algorithms%2E+In+Gottlob+et+al%2E+%5B6%5D%2C+pages+263%E2%80%93274%2E)
20. S. Schulz. E - A Brainiac Theorem Prover. AI Commun., 15(2-3):111–126, 2002. [find](https://scholar.google.com/scholar?q=S%2E+Schulz%2E+E+%2D+A+Brainiac+Theorem+Prover%2E+AI+Commun%2E%2C+15%282%2D3%29%3A111%E2%80%93126%2C+2002%2E)
21. G. Sutcliffe. The 8th IJCAR automated theorem proving system competition - CASC-J8. AI Commun., 29(5):607–619, 2016. [find](https://scholar.google.com/scholar?q=G%2E+Sutcliffe%2E+The+8th+IJCAR+automated+theorem+proving+system+competition+%2D+CASC%2DJ8%2E+AI+Commun%2E%2C+29%285%29%3A607%E2%80%93619%2C+2016%2E)
22. J. Urban. BliStr: The Blind Strategymaker. In Gottlob et al. [6], pages 312–319. [find](https://scholar.google.com/scholar?q=J%2E+Urban%2E+BliStr%3A+The+Blind+Strategymaker%2E+In+Gottlob+et+al%2E+%5B6%5D%2C+pages+312%E2%80%93319%2E)
23. J. Urban, G. Sutcliffe, P. Pudlák, and J. Vyskočil. MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance. In A. Armando, P. Baumgartner, and G. Dowek, editors, IJCAR, volume 5195 of LNCS, pages 441–456. Springer, 2008. [find](https://scholar.google.com/scholar?q=J%2E+Urban%2C+G%2E+Sutcliffe%2C+P%2E+Pudla%CC%81k%2C+and+J%2E+Vyskoc%CC%8Cil%2E+MaLARea+SG1+%2D+Machine+Learner+for+Automated+Reasoning+with+Semantic+Guidance%2E+In+A%2E+Armando%2C+P%2E+Baumgartner%2C+and+G%2E+Dowek%2C+editors%2C+IJCAR%2C+volume+)
24. J. Urban, J. Vyskočil, and P. Štěpánek. MaLeCoP: Machine learning connection prover. In K. Brünnler and G. Metcalfe, editors, TABLEAUX, volume 6793 of LNCS, pages 263–277. Springer, 2011. [find](https://scholar.google.com/scholar?q=J%2E+Urban%2C+J%2E+Vyskoc%CC%8Cil%2C+and+P%2E+S%CC%8Cte%CC%8Cpa%CC%81nek%2E+MaLeCoP%3A+Machine+learning+connection+prover%2E+In+K%2E+Bru%CC%88nnler+and+G%2E+Metcalfe%2C+editors%2C+TABLEAUX%2C+volume+6793+of+LNCS%2C+pages+263%E2%80%93277%2E+Springer%2C+2011%2E)

*Updated 3 November 2026*