Elamur Research⌕
☰
home / papers / 2013 / HOL(y)Hammer: Online ATP Service for HOL Light

HOL(y)Hammer: Online ATP Service for HOL Light

Paper · 2013 · Cezary Kaliszyk and Josef Urban

Summary

Interactive proof assistants such as HOL Light require users to locate relevant library lemmas and assemble proofs by hand. This becomes costly in very large developments like Flyspeck. The authors turn their earlier offline experiments on large-theory automated reasoning into HOL(y)Hammer, a public online service. Users can submit a conjecture, or upload and update a whole HOL Light project.

For each query, the service extracts symbol-, subterm- and type-based features. Premise selectors trained on all previous proofs then rank useful lemmas, using sparse naive Bayes from SNoW and a distance-weighted k-NN. The top-ranked premises are translated into ATP formats and passed to provers such as Vampire, E and Z3. Successful proofs are minimized and rebuilt as HOL Light tactics. Native decision procedures run alongside in parallel.

Offline evaluation showed that 47% of Flyspeck toplevel theorems can be proved automatically in 30 seconds. The service also offers Emacs, web and command-line front ends and a local installation option. It is a practical step toward a reasoning assistant for formal mathematics, comparable in spirit to Wolfram Alpha.

Key points

  • The server has 48 CPUs and runs 7 AI/ATP combinations plus 4 decision procedures per query. Counting individual prover strategies, this amounts to roughly 70 attempts per query.
  • Preloaded libraries include Flyspeck, Multivariate Analysis and Complex Analysis. Users can upload new projects, and content encoding plus checkpointing let earlier proof knowledge be reused across versions.
  • The June 2012 Flyspeck version has 14,185 theorems, about 30.000 features per extraction method and 16,082 labels.
    • Push-button success rose from 39% to 47%, using 14 CPUs for 30 seconds each.
    • Training takes about 1 s for k-NN and 6–25 s for naive Bayes.
  • The local installation uses naive Bayes on HOL Light proof dependencies and runs Vampire, Eprover and Z3 with three-fold parallelism.
  • Planned future work includes:
    • git-based project updates,
    • secure and private uploads,
    • using the system as a semantic layer for parsing informal mathematical texts.

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. HOL(y)Hammer: Online ATP Service for HOL Light. arXiv:1309.4962.

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

@misc{kaliszyk2013hol,
  title = {{HOL(y)Hammer: Online ATP Service for HOL Light}},
  author = {Cezary Kaliszyk and Josef Urban},
  year = {2013},
  doi = {10.48550/arxiv.1309.4962},
  eprint = {1309.4962},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.1309.4962}
}

References

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

  1. Behzad Akbarpour and Lawrence C. Paulson. MetiTarski: An automatic theorem prover for real-valued special functions. J. Autom. Reasoning, 44(3):175–205, 2010. find
  2. Jesse Alama, Kasper Brink, Lionel Mamane, and Josef Urban. Large formal wikis: Issues and solutions. In James H. Davenport, William M. Farmer, Josef Urban, and Florian Rabe, editors, Calculemus/MKM, volume 6824 of LNCS, pages 133–148. Springer, 2011. find
  3. Jasmin Christian Blanchette, Sascha Böhme, Andrei Popescu, and Nicholas Smallbone. Encoding Monomorphic and Polymorphic Types. In TACAS, 2013. To appear, http://www21.in.tum.de/˜blanchet/enc_types_paper.pdf. ↗
  4. Jasmin Christian Blanchette and Andrei Paskevich. TFF1: The TPTP typed first-order form with rank-1 polymorphism. Available online at http://www21.in.tum.de/˜blanchet/tff1spec.pdf. ↗
  5. Andy Carlson, Chad Cumby, Jeff Rosen, and Dan Roth. The SNoW Learning Architecture. Technical Report UIUCDCS-R-99-2101, UIUC Computer Science Department, 5 1999. find
  6. 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
  7. Sahibsingh A. Dudani. The distance-weighted k-nearest-neighbor rule. Systems, Man and Cybernetics, IEEE Transactions on, SMC-6(4):325–327, 1976. find
  8. Ulrich Furbach and Natarajan Shankar, editors. Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, volume 4130 of LNCS. Springer, 2006. find
  9. Allen Van Gelder and Geoff Sutcliffe. Extending the TPTP language to higher-order logic with automated parser generation. In Furbach and Shankar [8], pages 156–161. find
  10. 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
  11. 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
  12. John Harrison. Optimizing Proof Search in Model Elimination. In M. McRobbie and J.K. Slaney, editors, Proceedings of the 13th International Conference on Automated Deduction, number 1104 in LNAI, pages 313–327. Springer-Verlag, 1996. find
  13. 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
  14. Cezary Kaliszyk and Alexander Krauss. Scalable LCF-style proof translation. Accepted to ITP 2013, http://cl-informatik.uibk.ac.at/˜cek/import.pdf. ↗
  15. Cezary Kaliszyk and Josef Urban. Learning-assisted automated reasoning with Flyspeck. CoRR, abs/1211.7012, 2012.
  16. 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
  17. 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
  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. Jia Meng and Lawrence C. Paulson. Translating higher-order clauses to first-order clauses. J. Autom. Reasoning, 40(1):35–60, 2008. find
  20. Lawrence C. Paulson and Jasmin Blanchette. Three years of experience with Sledgehammer, a practical link between automated and interactive theorem provers. In 8th IWIL, 2010. Invited talk. find
  21. Lawrence C. Paulson and Kong Woei Susanto. Source-level proof reconstruction for interactive theorem proving. In Klaus Schneider and Jens Brandt, editors, TPHOLs, volume 4732 of LNCS, pages 232–245. Springer, 2007. find
  22. Andrew Pitts. The HOL logic. In M. J. C. Gordon and T. F. Melham, editors, Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, 1993. find
  23. Alexandre Riazanov and Andrei Voronkov. The design and implementation of VAMPIRE. AI Commun., 15(2-3):91–110, 2002. find
  24. Stephan Schulz. E - A Brainiac Theorem Prover. AI Commun., 15(2-3):111–126, 2002. find
  25. Geoff Sutcliffe, Stephan Schulz, Koen Claessen, and Allen Van Gelder. Using the TPTP language for writing derivations and finite interpretations. In Furbach and Shankar [8], pages 67–81. find
  26. Carst Tankink, Cezary Kaliszyk, Josef Urban, and Herman Geuvers. Formal mathematics on display: A wiki for Flyspeck. 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 152–167… find
  27. Josef Urban. MoMM - fast interreduction and retrieval in large libraries of formalized mathematics. International Journal on Artificial Intelligence Tools, 15(1):109–130, 2006. find
  28. 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
  29. Josef Urban. Content-based encoding of mathematical and code libraries. In Christoph Lange and Josef Urban, editors, Proceedings of the ITP 2011 Workshop on Mathematical Wikis (MathWikis), number 767 in CEUR Workshop Proceedings, pages 49–53, Aachen, 2011. find
  30. Josef Urban. Parallelizing Mizar. CoRR, abs/1206.0141, 2012. — [arXiv:1206.0141](https://arxiv.org/abs/1206.0141) find
  31. Josef Urban. BliStr: The Blind Strategymaker. CoRR, abs/1301.2683, 2013. — [arXiv:1301.2683](https://arxiv.org/abs/1301.2683) find
  32. Josef Urban, Piotr Rudnicki, and Geoff Sutcliffe. ATP and presentation service for Mizar formalizations. J. Autom. Reasoning, 50:229–241, 2013. find
  33. Josef Urban and Geoff Sutcliffe. Automated reasoning and presentation support for formalizing mathematics in Mizar. In Serge Autexier, Jacques Calmet, David Delahaye, Patrick D. F. Ion, Laurence Rideau, Renaud Rioboo, and Alan P. Sexton, editors, AISC/MKM/Calculemus, volume 6167 of LNCS, pages 132–… find
  34. 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
  35. 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. find
  36. Vernor Vinge. A Fire Upon the Deep. Tor Books, 1992. find
  37. Lee Worden. WorkingWiki: a MediaWiki-based platform for collaborative research. In Christoph Lange and Josef Urban, editors, ITP Workshop on Mathematical Wikis (MathWikis), number 767 in CEUR Workshop Proceedings, pages 63–73, Aachen, 2011. Cezary Kaliszyk University of Innsbruck, Austria Josef Urba… find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/kaliszyk-2013-hol-y-hammer-online-atp/