Document Open Access Logo

Hammering Mizar by Learning Clause Guidance (Short Paper)

Authors Jan Jakubův, Josef Urban

PDF
Thumbnail PDF

File

LIPIcs.ITP.2019.34.pdf
  • Filesize: 353 kB
  • 8 pages

Document Identifiers

Author Details

Jan Jakubův
  • Czech Technical University in Prague, Czech Republic
Josef Urban
  • Czech Technical University in Prague, Czech Republic

Funding

Supported by the AI4REASON ERC Consolidator grant number 649043, and by the Czech project AI&Reasoning CZ.02.1.01/0.0/0.0/15\_003/0000466 and the European Regional Development Fund.

Cite As Get BibTex

Jan Jakubův and Josef Urban. Hammering Mizar by Learning Clause Guidance (Short Paper). In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 34:1-34:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.ITP.2019.34

Abstract

We describe a very large improvement of existing hammer-style proof automation over large ITP libraries by combining learning and theorem proving. In particular, we have integrated state-of-the-art machine learners into the E automated theorem prover, and developed methods that allow learning and efficient internal guidance of E over the whole Mizar library. The resulting trained system improves the real-time performance of E on the Mizar library by 70% in a single-strategy setting.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automated reasoning
  • Computing methodologies → Theorem proving algorithms
  • Computing methodologies → Machine learning
Keywords
  • Proof automation
  • ITP hammers
  • Automated theorem proving
  • Machine learning

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  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. URL: https://doi.org/10.1007/s10817-013-9286-5.
  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 Systems 29: Annual Conference on Neural Information Processing Systems 2016, December 5-10, 2016, Barcelona, Spain, pages 2235-2243, 2016. URL: http://papers.nips.cc/paper/6280-deepmath-deep-sequence-models-for-premise-selection.
  3. 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. URL: https://doi.org/10.1007/s10817-016-9362-8.
  4. Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, and Josef Urban. Hammering towards QED. J. Formalized Reasoning, 9(1):101-148, 2016. URL: https://doi.org/10.6092/issn.1972-5787/4593.
  5. Tianqi Chen and Carlos Guestrin. XGBoost: A Scalable Tree Boosting System. In KDD, pages 785-794. ACM, 2016. Google Scholar
  6. Karel Chvalovský, Jan Jakubuv, Martin Suda, and Josef Urban. ENIGMA-NG: efficient neural and gradient-boosted inference guidance for E. CoRR, abs/1903.03182, 2019. URL: http://arxiv.org/abs/1903.03182.
  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. URL: https://doi.org/10.1145/1390681.1442794.
  8. Michael Färber and Cezary Kaliszyk. Random Forests for Premise Selection. In Carsten Lutz and Silvio Ranise, editors, Frontiers of Combining Systems - 10th International Symposium, FroCoS 2015, Wroclaw, Poland, September 21-24, 2015. Proceedings, volume 9322 of Lecture Notes in Computer Science, pages 325-340. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-24246-0_20.
  9. 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 Science, pages 563-579. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-63046-5_34.
  10. Thibault Gauthier, Cezary Kaliszyk, and Josef Urban. TacticToe: Learning to reason with HOL4 tactics. 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 EPiC Series in Computing, pages 125-143. EasyChair, 2017. URL: http://www.easychair.org/publications/paper/340355.
  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, pages 15-22. EasyChair, 2018. URL: https://doi.org/10.29007/z7qx.
  12. Adam Grabowski, Artur Korniłowicz, and Adam Naumowicz. Mizar in a nutshell. J. Formalized Reasoning, 3(2):153-245, 2010. Google Scholar
  13. Thomas Gransden, Neil Walkinshaw, and Rajeev 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. URL: https://doi.org/10.1007/978-3-319-21401-6_16.
  14. Jan Jakubův 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. URL: https://doi.org/10.1145/3018610.3018619.
  15. 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, Proceedings, volume 10383 of Lecture Notes in Computer Science, pages 292-302. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-62075-6_20.
  16. 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 Lecture Notes in Computer Science, pages 118-124. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-96812-4_11.
  17. Cezary Kaliszyk and Josef Urban. Learning-Assisted Automated Reasoning with Flyspeck. J. Autom. Reasoning, 53(2):173-213, 2014. URL: https://doi.org/10.1007/s10817-014-9303-3.
  18. 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, November 24-28, 2015, Proceedings, volume 9450 of Lecture Notes in Computer Science, pages 88-96. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-48899-7_7.
  19. Cezary Kaliszyk and Josef Urban. MizAR 40 for Mizar 40. J. Autom. Reasoning, 55(3):245-256, 2015. URL: https://doi.org/10.1007/s10817-015-9330-8.
  20. 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 Conference on Neural Information Processing Systems 2018, NeurIPS 2018, 3-8 December 2018, Montréal, Canada., pages 8836-8847, 2018. URL: http://papers.nips.cc/paper/8098-reinforcement-learning-of-theorem-proving.
  21. Cezary Kaliszyk, Josef Urban, and Jirí Vyskocil. Efficient Semantic Features for Automated Reasoning over Large Theories. In IJCAI, pages 3084-3090. AAAI Press, 2015. Google Scholar
  22. 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. URL: https://doi.org/10.1007/978-3-642-39799-8_1.
  23. 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 EPiC Series in Computing, pages 85-105. EasyChair, 2017. URL: http://www.easychair.org/publications/paper/340345.
  24. Robi Polikar. Ensemble based systems in decision making. Circuits and Systems Magazine, IEEE, 6(3):21-45, 2006. Google Scholar
  25. Stephan Schulz. E - A Brainiac Theorem Prover. AI Commun., 15(2-3):111-126, 2002. URL: http://iospress.metapress.com/content/n908n94nmvk59v3c/.
  26. Stephan Schulz. System Description: E 1.8. In Kenneth L. McMillan, Aart Middeldorp, and Andrei Voronkov, editors, LPAR, volume 8312 of LNCS, pages 735-743. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-45221-5_49.
  27. Josef Urban. MPTP 0.2: Design, implementation, and initial experiments. J. Autom. Reasoning, 37(1-2):21-43, 2006. URL: https://doi.org/10.1007/s10817-006-9032-3.
  28. Josef Urban, Geoff Sutcliffe, Petr Pudlák, and Jiří Vyskočil. MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance. In IJCAR, pages 441-456, 2008. URL: https://doi.org/10.1007/978-3-540-71070-7_37.
  29. 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. URL: https://doi.org/10.1007/978-3-642-22119-4_21.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact