Elamur Research⌕
☰
home / papers / 2019 / ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E

ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E

Paper · 2019 · Karel Chvalovský, Jan Jakubův, Martin Suda et al.

Summary

The paper tackles given-clause selection in saturation-based first-order provers, specifically E. Choosing which clause to process next largely determines whether a proof is found. ENIGMA previously guided this choice with fast linear classifiers (LIBLINEAR) over handcrafted clause features: vertical, horizontal, symbol, length and conjecture features. The authors add two stronger learners. The first is gradient-boosted decision trees on the same features. The second is recursive neural networks trained end-to-end, which need no manual feature design.

Training data come from successful proof runs. Clauses that appear in the final proof are labelled positive, and other processed clauses are labelled negative. A learned model can either drive clause selection alone (S ⊙ M) or share selection roughly evenly with the original strategy (S ⊕ M).

Neural evaluation is expensive. The authors offset this by caching results along E's shared term structures. On a large benchmark, the tree models beat the linear ones. The neural model, though far slower, already outperforms the linear model when it drives selection alone. The authors present this as the first practically convincing use of boosted and neural guidance in saturation-style provers.

Key points

  • Three learners are compared inside E's clause selection: linear (M lin), gradient-boosted trees (M tree) and recursive neural network (M nn). Each is combined with a baseline strategy S using ⊙ (model only) or ⊕ (model mixed with S).
  • Evaluation speed relative to S, measured as generated clauses on problems where every run timed out: linear about 60 %, trees about 40 %, neural about 6–7 %. Caching roughly doubles neural speed, from 3.6 % to 7.1 % for S ⊕ M nn.
  • Despite running about ten times slower within a 10 s limit, S ⊙ M nn proves more problems than S ⊙ M lin. Most configurations also need fewer given-clause iterations than S to reach a proof.
  • Feature hashing was tested with hash bases from 32k down to 1k, against 31,675 distinct training features. Without hashing, M tree solves 1231 problems (⊙) and 1256 (⊕); at 1k it still solves 1215 and 1232. M lin drops from 1115/1210 to 938/1119.
  • Hashing models perform comparably to unhashed ones down to 25 % of the original dimension. Training accuracy rises at small bases while prover performance slightly falls, which the authors attribute to collisions.

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 PraguePrague · Czechia16 works · 930 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 Karel Chvalovský, Jan Jakubův, Martin Suda and Josef Urban. 2019. ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E. arXiv:1903.03182.

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

@misc{chvalovsky2019enigma,
  title = {{ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E}},
  author = {Karel Chvalovský, Jan Jakubův, Martin Suda and Josef Urban},
  year = {2019},
  doi = {10.48550/arxiv.1903.03182},
  eprint = {1903.03182},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.1903.03182}
}

References

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

  1. Jesse Alama, Tom Heskes, Daniel Kühlwein, Evgeni Tsivtsivadze, and Josef Urban. Premise selection for mathematics by corpus analysis and kernel methods. J. Autom. Reasoning, 52(2):191–213, 2014.
  2. Alexander A. Alemi, François Chollet, Niklas Eén, Geoffrey Irving, Christian Szegedy, and Josef Urban. DeepMath - deep sequence models for premise selection. In Daniel D. Lee, Masashi Sugiyama, Ulrike V. Luxburg, Isabelle Guyon, and Roman Garnett, editors, Advances in Neural Information Processing…
  3. Grzegorz Bancerek, Czeslaw Bylinski, Adam Grabowski, Artur Kornilowicz, Roman Matuszewski, Adam Naumowicz, Karol Pak, and Josef Urban. Mizar: State-of-the-art and beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics -… find
  4. 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
  5. Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, and Josef Urban. Hammering towards QED. J. Formalized Reasoning, 9(1):101–148, 2016.
  6. Tianqi Chen and Carlos Guestrin. Xgboost: A scalable tree boosting system. In KDD, pages 785–794. ACM, 2016. 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. Journal of Machine Learning Research, 9:1871–1874, 2008. find
  8. Michael Färber, Cezary Kaliszyk, and Josef Urban. Monte Carlo tableau proof search. In Leonardo de Moura, editor, Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings, volume 10395 of Lecture Notes in Computer Scien… find
  9. Thibault Gauthier and Cezary Kaliszyk. Premise selection and external provers for HOL4. In Certified Programs and Proofs (CPP’15), LNCS. Springer, 2015. http://dx.doi.org/10.1145/2676724.2693173. — [doi:10.1145/2676724.2693173](https://doi.org/10.1145/2676724.2693173) ↗
  10. Zarathustra Goertzel, Jan Jakubův, Stephan Schulz, and Josef Urban. ProofWatch: Watchlist guidance for large theories in E. In Jeremy Avigad and Assia Mahboubi, editors, Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018,… find
  11. Zarathustra Goertzel, Jan Jakubuv, and Josef Urban. ProofWatch meets ENIGMA: First experiments. In Gilles Barthe, Konstantin Korovin, Stephan Schulz, Martin Suda, Geoff Sutcliffe, and Margus Veanes, editors, LPAR-22 Workshop and Short Paper Proceedings, volume 9 of Kalpa Publications in Computing, p… find
  12. Georg Gottlob, Geoff Sutcliffe, and Andrei 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
  13. Sepp Hochreiter and Jrgen Schmidhuber. Long short-term memory. Neural computation, 9:1735–80, 12 1997. find
  14. Jan Jakubův 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, Proceeding…
  15. Jan Jakubův 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 L… find
  16. Jan Jakubův and Josef Urban. Hierarchical invention of theorem proving strategies. AI Commun., 31(3):237–250, 2018. find
  17. Jan Jakubuv and Josef Urban. BliStrTune: hierarchical invention of theorem proving strategies. In Yves Bertot and Viktor 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
  18. Armand Joulin, Edouard Grave, Piotr Bojanowski, and Tomas Mikolov. Bag of tricks for efficient text classification. In Proceedings of the 15th Conference of the European Chapter of the Association for Computational Linguistics: Volume 2, Short Papers, pages 427–431. Association for Computational Lin… find
  19. Cezary Kaliszyk and Josef Urban. Learning-assisted automated reasoning with Flyspeck. J. Autom. Reasoning, 53(2):173–213, 2014.
  20. Cezary Kaliszyk and Josef Urban. FEMaLeCoP: Fairly efficient machine learning connection prover. 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, N… find
  21. Cezary Kaliszyk, Josef Urban, Henryk Michalewski, and Miroslav Olsák. Reinforcement learning of theorem proving. In Samy Bengio, Hanna M. Wallach, Hugo Larochelle, Kristen Grauman, Nicolò Cesa-Bianchi, and Roman Garnett, editors, Advances in Neural Information Processing Systems 31: Annual Confere…
  22. Cezary Kaliszyk, Josef Urban, and Jirı́ Vyskocil. Efficient semantic features for automated reasoning over large theories. In IJCAI, pages 3084–3090. AAAI Press, 2015. find
  23. 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
  24. Daniel Kuehlwein and Josef Urban. Learning from multiple proofs: First experiments. In Pascal Fontaine, Renate A. Schmidt, and Stephan Schulz, editors, PAAR-2012, volume 21 of EPiC Series, pages 82–94. EasyChair, 2013. find
  25. Daniel Kühlwein, Twan van Laarhoven, Evgeni Tsivtsivadze, Josef Urban, and Tom Heskes. Overview and evaluation of premise selection techniques for large theory mathematics. In Bernhard Gramlich, Dale Miller, and Uli Sattler, editors, IJCAR, volume 7364 of LNCS, pages 378–392. Springer, 2012. find
  26. Sarah M. Loos, Geoffrey Irving, Christian Szegedy, and Cezary Kaliszyk. Deep network guided proof search. In Thomas Eiter and David Sands, editors, LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017, volume 46 of EPi…
  27. William McCune. Otter 2.0. In International Conference on Automated Deduction, pages 663–664. Springer, 1990. find
  28. Jia Meng and Lawrence C. Paulson. Translating higher-order clauses to first-order clauses. J. Autom. Reasoning, 40(1):35–60, 2008. find
  29. Jens Otten and Wolfgang Bibel. leanCoP: lean connection-based theorem proving. J. Symb. Comput., 36(1-2):139–161, 2003. find
  30. Bartosz Piotrowski and Josef Urban. ATPboost: Learning premise selection in binary setting with ATP feedback. In Didier Galmiche, Stephan Schulz, and Roberto Sebastiani, editors, Automated Reasoning - 9th International Joint Conference, IJ-CAR 2018, Held as Part of the Federated Logic Conference, Fl… find
  31. Robi Polikar. Ensemble based systems in decision making. Circuits and Systems Magazine, IEEE, 6(3):21–45, 2006. find
  32. John Alan Robinson and Andrei Voronkov, editors. Handbook of Automated Reasoning (in 2 volumes). Elsevier and MIT Press, 2001. find
  33. Simon Schäfer and Stephan Schulz. Breeding theorem proving heuristics with genetic algorithms. In Gottlob et al. [12], pages 263–274. find
  34. Stephan Schulz. E - A Brainiac Theorem Prover. AI Commun., 15(2-3):111–126, 2002. find
  35. Stephan Schulz and Martin Möhrmann. Performance of clause selection heuristics for saturation-based theorem proving. In Nicola Olivetti and Ashish Tiwari, editors, Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings, volume 97… find
  36. Richard Socher, Brody Huval, Christopher D. Manning, and Andrew Y. Ng. Semantic compositionality through recursive matrix-vector spaces. In Proceedings of the 2012 Joint Conference on Empirical Methods in Natural Language Processing and Computational Natural Language Learning, EMNLP-CoNLL 2012, July…
  37. Josef Urban. MPTP 0.2: Design, implementation, and initial experiments. J. Autom. Reasoning, 37(1-2):21–43, 2006. find
  38. Josef Urban. BliStr: The Blind Strategymaker. In Gottlob et al. [12], pages 312– 319. find
  39. 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
  40. Josef Urban, Jiřı́ Vyskočil, and Petr Štěpánek. MaLeCoP: Machine learning connection prover. In Kai Brünnler and George Metcalfe, editors, TABLEAUX, volume 6793 of LNCS, pages 263–277. Springer, 2011. Strategy S from Experiments in Section 5 A The following E strategy has been used to undertak… find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/chvalovsky-2019-enigma-ng-efficient-neural-gradient/