Elamur Research⌕
☰
home / papers / 2013 / MizAR 40 for Mizar 40

MizAR 40 for Mizar 40

Paper · 2013 · Cezary Kaliszyk and Josef Urban

Summary

The paper asks how much of the Mizar Mathematical Library (MML) can be proved fully automatically by learning-guided ATP systems that scale to the whole library rather than to small benchmarks. Building on their earlier Flyspeck/HOL Light work, the authors translate MML 4.181.1147 into TPTP with MPTP. They then train fast premise-selection methods on proof dependencies taken from earlier proofs, using only chronologically preceding proofs. The selected premises are passed to the Vampire, E and Z3 provers. Training data are improved over several MaLARea-style rounds: better selectors yield new proofs, and those proofs become fresh training data. The best result comes from running 14 complementary method/prover combinations in parallel for 30 seconds on a 14-CPU machine, which proves 40.6% of the roughly 58,000 top-level theorems with no user help. Training on the full library takes only 1–3 seconds, so the methods could be deployed in the online MizAR service. This makes automated assistance practical for Mizar users and lowers the barrier to formalizing mathematics.

Key points

  • The corpus is MML 4.181.1147: 57,897 theorems and top-level lemmas, plus about 90,000 other formulas (about 150,000 in total). It is translated via MPTP, and the provers are Vampire 3.0, Z3 4.0 and E 1.8 run with the Epar strategies.
  • Six iterative passes increased the number of ATP-proved theorems used for training from 27,842 (48%) to 32,165 (55.6%). Combining human and learned premise selection eventually proved 32,557 theorems (56.2%).
  • The premise selectors include:
    • naive Bayes (nb, nb_idf);
    • distance-weighted k-NN with IDF weighting;
    • k-NN on an LSI-reduced feature space built with gensim (800, 3200 and 6,400 topics);
    • recursive dependency weighting (geo_1_F, geo_r_F);
    • rank-combination ensembles, of which comb_min and comb_geo worked best.
  • Formulas are described by MaLARea-style syntactic features (symbols, terms, subterms), mostly with all variables renamed to a single variable.
  • In MizAR, the selectors are retrained for each query on the whole MML plus the submitted article. To better handle proof-local lemmas, local constants are also generalized to variables when extracting features.

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

🎓Radboud University NijmegenNijmegen · Netherlands26 works · 2,125 citations🎓Universität InnsbruckInnsbruck · Austria23 works · 1,475 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

🧭 Topics 1Research subjects and languages the work is about.Reasoning · 1,948 works

Cite

Cite as Cezary Kaliszyk and Josef Urban. 2013. MizAR 40 for Mizar 40. arXiv:1310.2805 (J. Automated Reasoning 55(3): 245-256 (2015)).

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.1007/s10817-015-9330-8 · arXiv 1310.2805

@misc{kaliszyk2013mizar,
  title = {{MizAR 40 for Mizar 40}},
  author = {Cezary Kaliszyk and Josef Urban},
  year = {2013},
  doi = {10.1007/s10817-015-9330-8},
  eprint = {1310.2805},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.1007/s10817-015-9330-8}
}

References

33 references, 4 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. Journal of Automated Reasoning, 2013. http://dx.doi.org/10.1007/s10817-013-9286-5. ↗
  2. Jesse Alama, Daniel Kühlwein, and Josef Urban. Automated and Human Proofs in General Mathematics: An Initial Comparison. In Nikolaj Bjørner and Andrei Voronkov, editors, LPAR, volume 7180 of LNCS, pages 37–45. Springer, 2012. find
  3. Leonardo Mendonça de Moura and Nikolaj Bjørner. Z3: An Efficient SMT Solver. In C. R. Ramakrishnan and Jakob Rehof, editors, TACAS, volume 4963 of LNCS, pages 337–340. Springer, 2008. find
  4. Scott C. Deerwester, Susan T. Dumais, Thomas K. Landauer, George W. Furnas, and Richard A. Harshman. Indexing by Latent Semantic Analysis. JASIS, 41(6):391–407, 1990. find
  5. Sahibsingh A. Dudani. The distance-weighted k-nearest-neighbor rule. Systems, Man and Cybernetics, IEEE Transactions on, SMC-6(4):325–327, 1976. find
  6. Adam Grabowski, Artur Korni lowicz, and Adam Naumowicz. Mizar in a nutshell. Journal of Formalized Reasoning, 3(2):153–245, 2010. find
  7. Thomas C. Hales. Introduction to the Flyspeck project. In Thierry Coquand, Henri Lombardi, and Marie-Françoise Roy, editors, Mathematics, Algorithms, Proofs, volume 05021 of Dagstuhl Seminar Proceedings. Internationales Begegnungs- und Forschungszentrum für Informatik (IBFI), Schloss Dagstuhl, Ger… find
  8. John Harrison. HOL Light: A tutorial introduction. In Mandayam K. Srivas and Albert John Camilleri, editors, FMCAD, volume 1166 of LNCS, pages 265–269. Springer, 1996. find
  9. Krystof Hoder and Andrei Voronkov. Sine qua non for large theory reasoning. In Nikolaj Bjørner and Viorica Sofronie-Stokkermans, editors, CADE, volume 6803 of LNCS, pages 299–314. Springer, 2011. find
  10. Karen Sprck Jones. A statistical interpretation of term specificity and its application in retrieval. Journal of Documentation, 28:11–21, 1972. find
  11. Cezary Kaliszyk and Josef Urban. Learning-assisted automated reasoning with Flyspeck. CoRR, abs/1211.7012, 2012.
  12. Cezary Kaliszyk and Josef Urban. Automated reasoning service for HOL Light. In Jacques Carette, David Aspinall, Christoph Lange, Petr Sojka, and Wolfgang Windsteiger, editors, MKM/Calculemus/DML, volume 7961 of Lecture Notes in Computer Science, pages 120– 135. Springer, 2013. find
  13. Cezary Kaliszyk and Josef Urban. HOL(y)Hammer: Online ATP service for HOL Light. CoRR, abs/1309.4962, 2013.
  14. Cezary Kaliszyk and Josef Urban. PRocH: Proof reconstruction for HOL Light. In Maria Paola Bonacina, editor, CADE, volume 7898 of Lecture Notes in Computer Science, pages 267–274. Springer, 2013. find
  15. Cezary Kaliszyk and Josef Urban. Stronger automation for Flyspeck by feature weighting and strategy evolution. In Jasmin Christian Blanchette and Josef Urban, editors, PxTP 2013, volume 14 of EPiC Series, pages 87–95. EasyChair, 2013. find
  16. 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
  17. Daniel Kühlwein, Jasmin Christian Blanchette, Cezary Kaliszyk, and Josef Urban. MaSh: Machine learning for Sledgehammer. In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors, ITP, volume 7998 of Lecture Notes in Computer Science, pages 35–50. Springer, 2013. find
  18. 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
  19. Radim Řehůřek and Petr Sojka. Software framework for topic modelling with large corpora. In Proceedings of the LREC 2010 Workshop on New Challenges for NLP Frameworks, pages 45–50, Valletta, Malta, May 2010. ELRA. find
  20. Alexandre Riazanov and Andrei Voronkov. The design and implementation of VAMPIRE. AI Commun., 15(2-3):91–110, 2002. find
  21. Robert E. Schapire. The strength of weak learnability. Machine Learning, 5:197–227, 1990. find
  22. Stephan Schulz. E - A Brainiac Theorem Prover. AI Commun., 15(2-3):111–126, 2002. find
  23. John Shawe-Taylor and Nello Cristianini. Kernel Methods for Pattern Analysis. Cambridge University Press, New York, NY, USA, 2004. find
  24. Steffen Juilf Smolka and Jasmin Christian Blanchette. Robust, semi-intelligible isabelle proofs from atp proofs. In Jasmin Christian Blanchette and Josef Urban, editors, PxTP 2013, volume 14 of EPiC Series, pages 117–132. EasyChair, 2013. find
  25. Josef Urban. Translating Mizar for first order theorem provers. In MKM, volume 2594 of LNCS, pages 203–215. Springer, 2003. find
  26. Josef Urban. MPTP - Motivation, Implementation, First Experiments. Journal of Automated Reasoning, 33(3-4):319–339, 2004. find
  27. Josef Urban. MPTP 0.2: Design, implementation, and initial experiments. J. Autom. Reasoning, 37(1-2):21–43, 2006. find
  28. Josef Urban. MaLARea: a metasystem for automated reasoning in large theories. In Geoff Sutcliffe, Josef Urban, and Stephan Schulz, editors, ESARLT, volume 257 of CEUR Workshop Proceedings. CEUR-WS.org, 2007.
  29. Josef Urban. An Overview of Methods for Large-Theory Automated Theorem Proving (Invited Paper). In Peter Höfner, Annabelle McIver, and Georg Struth, editors, ATE Workshop, volume 760 of CEUR Workshop Proceedings, pages 3–8. CEUR-WS.org, 2011. find
  30. Josef Urban. BliStr: The Blind Strategymaker. CoRR, abs/1301.2683, 2013. — [arXiv:1301.2683](https://arxiv.org/abs/1301.2683) find
  31. Josef Urban, Piotr Rudnicki, and Geoff Sutcliffe. ATP and presentation service for Mizar formalizations. J. Autom. Reasoning, 50:229–241, 2013. find
  32. 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
  33. Josef Urban and Jiřı́ Vyskočil. Theorem proving in large formal mathematics as an emerging AI field. In Maria Paola Bonacina and Mark E. Stickel, editors, Automated Reasoning and Mathematics: Essays in Memory of William McCune, volume 7788 of LNAI, pages 240–257. Springer, 2013. find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/kaliszyk-2013-mizar-40-mizar-40/