Elamur Research⌕
☰
home / papers / 2020 / ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description)

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

Paper · 2020 · Jan Jakubův, Karel Chvalovský, Miroslav Olšák et al.

Summary

Learned guidance for saturation-style provers usually relies on symbol names. Such guidance cannot carry over to problems or libraries that use different names. This system description adds two name-agnostic clause classifiers to the ENIGMA framework of the E prover. Under either classifier, consistently renaming all symbols in a problem leaves the search unchanged. The first classifier uses gradient-boosted decision trees (XGBoost and LightGBM). Its features replace each symbol with a token that records only whether it is a function or predicate and its arity. These features are extended with variable and symbol statistics and 22 problem-level features. The second classifier is a symbol-independent graph neural network that works on a hypergraph of clauses, symbols and terms. It runs fast enough because generated clauses are scored in batches against a context of already selected clauses. Both models were trained iteratively on the MPTP large-theory benchmark and more than doubled the problems solved by the baseline strategy within 10 s. Together they solved many Mizar40 problems no earlier method had cracked. This makes cross-library transfer of learned proving skills more realistic.

Key points

  • Baseline vs. learned models (10 s per problem): the unguided strategy solves 14,966 problems. The best GBDT (D2, LightGBM) reaches 24,347 (+62.7%), and the best GNN (N2) reaches 23,262 (+55.4%).
  • GNN vs. GBDT: GNNs score higher test accuracy and lead in the first iteration, but the GBDTs overtake them in later rounds. LightGBM trained about 10× faster than XGBoost (40 min vs. 7 h).
  • Complementarity: GNNs are notably complementary to each other and to GBDTs. A GNN strategy adds 2,045 solutions to the best GBDT strategy.
  • Union of all twenty strategies (≤200 s): about 29.1k problems solved, including 2,109 hard Mizar40 problems. For comparison, Vampire solves 27,842 problems in 300 s.
  • Status of the work: this is reported as the first tight integration of symbol-independent features and GNNs into E with competitive real-time results. The anonymous GBDTs even beat the authors' earlier symbol-dependent versions.

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

🎓Universität InnsbruckInnsbruck · Austria23 works · 1,475 citations🎓Czech Technical University in PraguePrague · Czechia16 works · 930 citations🎓University of WarsawWarsaw · Poland14 works · 774 citations

 Fields, topics and concepts

📚 Shelves 3The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksComputational Theory and Mathematics · 496 works

Cite

Cite as Jan Jakubův, Karel Chvalovský, Miroslav Olšák, Bartosz Piotrowski, Martin Suda and Josef Urban. 2020. ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description). arXiv:2002.05406.

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.48550/arxiv.2002.05406 · arXiv 2002.05406

@misc{jakubuv2020enigma,
  title = {{ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description)}},
  author = {Jan Jakubův, Karel Chvalovský, Miroslav Olšák, Bartosz Piotrowski, Martin Suda and Josef Urban},
  year = {2020},
  doi = {10.48550/arxiv.2002.05406},
  eprint = {2002.05406},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2002.05406}
}

References

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

  1. Martı́n Abadi, Ashish Agarwal, Paul Barham, Eugene Brevdo, Zhifeng Chen, Craig Citro, Greg S. Corrado, Andy Davis, Jeffrey Dean, Matthieu Devin, Sanjay Ghemawat, Ian Goodfellow, Andrew Harp, Geoffrey Irving, Michael Isard, Yangqing Jia, Rafal Jozefowicz, Lukasz Kaiser, Manjunath Kudlur, Josh Levenbe… find
  2. Jasmin Christian Blanchette, David Greenaway, Cezary Kaliszyk, Daniel Kühlwein, and Josef Urban. A learning-based fact selector for Isabelle/HOL. J. Autom. Reasoning, 57(3):219–244, 2016. find
  3. Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, and Josef Urban. Hammering towards QED. J. Formalized Reasoning, 9(1):101–148, 2016.
  4. Tianqi Chen and Carlos Guestrin. XGBoost: A scalable tree boosting system. In Proceedings of the 22nd ACM SIGKDD International Conference on Knowledge Discovery and Data Mining, KDD ’16, pages 785–794, New York, NY, USA, 2016. ACM. find
  5. Karel Chvalovský, Jan Jakubuv, Martin Suda, and Josef Urban. ENIGMA-NG: efficient neural and gradient-boosted inference guidance for E. In Pascal Fontaine, editor, Automated Deduction - CADE 27 - 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings, v…
  6. Lukasz Czajka and Cezary Kaliszyk. Hammer for Coq: Automation for dependent type theory. J. Autom. Reasoning, 61(1-4):423–453, 2018. find
  7. Rong-En Fan, Kai-Wei Chang, Cho-Jui Hsieh, Xiang-Rui Wang, and Chih-Jen Lin. Liblinear: A library for large linear classification. J. Mach. Learn. Res., 9:1871– 1874, June 2008. find
  8. Thibault Gauthier and Cezary Kaliszyk. Premise selection and external provers for HOL4. In Xavier Leroy and Alwen Tiu, editors, Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015, pages 49–57. ACM, 2015. find
  9. Thibault Gauthier and Cezary Kaliszyk. Sharing HOL4 and HOL light proof knowledge. In Martin Davis, Ansgar Fehnker, Annabelle McIver, and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28,… find
  10. Thibault Gauthier and Cezary Kaliszyk. Aligning concepts across proof assistant libraries. J. Symb. Comput., 90:89–123, 2019. find
  11. Thibault Gauthier, Cezary Kaliszyk, and Josef Urban. Initial experiments with statistical conjecturing over large formal corpora. In Andrea Kohlhase, Paul Libbrecht, Bruce R. Miller, Adam Naumowicz, Walther Neuper, Pedro Quaresma, Frank Wm. Tompa, and Martin Suda, editors, Joint Proceedings of the F… find
  12. Zarathustra Goertzel, Jan Jakubův, and Josef Urban. ENIGMAWatch: ProofWatch meets ENIGMA. In Serenella Cerrito and Andrei Popescu, editors, Automated Reasoning with Analytic Tableaux and Related Methods, pages 374–388, Cham, 2019. Springer International Publishing. find
  13. Jan Jakubuv and Josef Urban. ENIGMA: efficient learning-based inference guiding machine. In Herman Geuvers, Matthew England, Osman Hasan, Florian Rabe, and Olaf Teschke, editors, Intelligent Computer Mathematics - 10th International Conference, CICM 2017, Edinburgh, UK, July 17-21, 2017, Proceedings…
  14. Jan Jakubuv and Josef Urban. Enhancing ENIGMA given clause guidance. In Florian Rabe, William M. Farmer, Grant O. Passmore, and Abdou Youssef, editors, Intelligent Computer Mathematics - 11th International Conference, CICM 2018, Hagenberg, Austria, August 13-17, 2018, Proceedings, volume 11006 of Le… find
  15. Jan Jakubuv and Josef Urban. Hammering Mizar by learning clause guidance. In John Harrison, John O’Leary, and Andrew Tolmach, editors, 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA, volume 141 of LIPIcs, pages 34:1–34:8. Schloss Dagst… find
  16. Cezary Kaliszyk and Josef Urban. Learning-assisted automated reasoning with Flyspeck. J. Autom. Reasoning, 53(2):173–213, 2014.
  17. Cezary Kaliszyk and Josef Urban. HOL(y)Hammer: Online ATP service for HOL Light. Mathematics in Computer Science, 9(1):5–22, 2015.
  18. Cezary Kaliszyk and Josef Urban. MizAR 40 for Mizar 40. J. Autom. Reasoning, 55(3):245–256, 2015.
  19. Guolin Ke, Qi Meng, Thomas Finley, Taifeng Wang, Wei Chen, Weidong Ma, Qiwei Ye, and Tie-Yan Liu. Lightgbm: A highly efficient gradient boosting decision tree. In NIPS, pages 3146–3154, 2017. find
  20. Laura Kovács and Andrei Voronkov. First-order theorem proving and Vampire. In Natasha Sharygina and Helmut Veith, editors, CAV, volume 8044 of LNCS, pages 1–35. Springer, 2013. find
  21. Miroslav Olsák, Cezary Kaliszyk, and Josef Urban. Property invariant embedding for automated reasoning. CoRR, abs/1911.12073, 2019.
  22. Ross A. Overbeek. A new class of automated theorem-proving algorithms. J. ACM, 21(2):191–200, April 1974. find
  23. Stephan Schulz. Learning search control knowledge for equational deduction, volume 230 of DISKI. Infix Akademische Verlagsgesellschaft, 2000. find
  24. Stephan Schulz. Learning search control knowledge for equational theorem proving. In Franz Baader, Gerhard Brewka, and Thomas Eiter, editors, KI 2001: Advances in Artificial Intelligence, Joint German/Austrian Conference on AI, Vienna, Austria, September 19-21, 2001, Proceedings, volume 2174 of Lect… find
  25. Stephan Schulz. E - A Brainiac Theorem Prover. AI Commun., 15(2-3):111–126, 2002. find
  26. Stephan Schulz. Fingerprint Indexing for Paramodulation and Rewriting. In Bernhard Gramlich, Ulrike Sattler, and Dale Miller, editors, Proc. of the 6st IJCAR, Manchester, volume 7364 of LNAI, pages 477–483. Springer, 2012. find
  27. Stephan Schulz. Simple and efficient clause subsumption with feature vector indexing. In Automated Reasoning and Mathematics, volume 7788 of Lecture Notes in Computer Science, pages 45–67. Springer, 2013. find
  28. Josef Urban. MPTP 0.2: Design, implementation, and initial experiments. J. Autom. Reasoning, 37(1-2):21–43, 2006. find
  29. Josef Urban, Geoff Sutcliffe, Petr Pudlák, and Jiřı́ Vyskočil. MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance. In Alessandro Armando, Peter Baumgartner, and Gilles Dowek, editors, IJCAR, volume 5195 of LNCS, pages 441–456. Springer, 2008. find
  30. Robert Veroff. Using hints to increase the effectiveness of an automated reasoning program: Case studies. J. Autom. Reasoning, 16(3):223–239, 1996. find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/jakubuv-2020-enigma-anonymous-symbol-independent-inference/