Elamur Research⌕
☰
home / papers / 2012 / Learning-Assisted Automated Reasoning with Flyspeck

Learning-Assisted Automated Reasoning with Flyspeck

Paper · 2012 · Cezary Kaliszyk and Josef Urban

Summary

The paper addresses the lack of a "hammer" for HOL Light: a tool that automatically proves a new goal by choosing relevant lemmas from a large library and handing them to external automated theorem provers (ATPs). The authors use the Flyspeck formalization of the Kepler Conjecture, together with the HOL Light library parts it depends on, as their corpus. They built sound translations of HOL Light's polymorphic higher-order logic into several TPTP formats and exported proof dependency data. That data trains premise-selection learners, such as k-nearest neighbor, using formula features in which variables are replaced by their HOL types. The evaluation imitates the library's historical growth, so each theorem may use only earlier theorems and proofs. A carefully chosen parallel mix of premise selectors and ATPs proves 39% of the Flyspeck theorems fully automatically within 30 seconds. The resulting system is also offered as an online service. The work matters because it brings HOL Light and Flyspeck into large-theory AI/ATP research and gives mathematicians a practical push-button proving aid.

Key points

  • Translations: HOL Light formulas are translated into untyped first-order (FOF), polymorphic typed first-order (TFF1) and typed higher-order (THF) formats. Re-proving experiments used 17 different ATP/SMT systems.
  • Push-button results: In the push-button setting, 39% of the 14,185 theorems were proved in 30 s of real time on a 14-CPU workstation. The best single method proved only 24.1% in 30 s and 26.8% in 300 s.
  • Other success rates:
    • When the original HOL Light dependencies are supplied, 7 parallel ATP methods re-prove 50% of the theorems.
    • All tried methods combined reach 56%.
  • Method search: 435 premise-selector/ATP combinations were tested to find the most complementary mix. The mix included SInE strategies in E and Vampire, a MaLARea-style loop interleaving ATP runs with learning, and proof minimization.
  • Proof quality: Learning-advised ATPs sometimes produced simpler or substantially different proofs than the originals and exposed duplicate theorems in the library. For comparison, a similar push-button evaluation on the Mizar library (MML) reached about 18%.

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 · Netherlands21 works · 1,796 citations🎓Universität InnsbruckInnsbruck · Austria10 works · 876 citations

 Fields, topics and concepts

📚 Shelves 3The field of science this work belongs to (OpenAlex fields).Computer Science · 18,614 worksArtificial Intelligence · 17,965 worksComputational Theory and Mathematics · 321 works

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

💡 Concepts 1Key ideas and methods explained on our concept pages.Lemma · 24 works

Cite

Cite as Cezary Kaliszyk and Josef Urban. 2012. Learning-Assisted Automated Reasoning with Flyspeck. arXiv:1211.7012 (J. Automated Reasoninig 54(1): 99, 2014).

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.1007/s10817-014-9303-3 · arXiv 1211.7012

@misc{kaliszyk2012learning,
  title = {{Learning-Assisted Automated Reasoning with Flyspeck}},
  author = {Cezary Kaliszyk and Josef Urban},
  year = {2012},
  doi = {10.1007/s10817-014-9303-3},
  eprint = {1211.7012},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.1007/s10817-014-9303-3}
}

References

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

  1. Mark Adams. Introducing HOL Zero - (extended abstract). In Komei Fukuda, Joris van der Hoeven, Michael Joswig, and Nobuki Takayama, editors, ICMS, volume 6327 of LNCS, pages 142–143. Springer, 2010. find
  2. 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
  3. 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
  4. 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. find
  5. Jesse Alama, Daniel Kühlwein, and Josef Urban. Automated and Human Proofs in General Mathematics: An Initial Comparison. In Bjørner and Voronkov [11], pages 37–45. find
  6. Alessandro Armando, Peter Baumgartner, and Gilles Dowek, editors. Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings, volume 5195 of LNCS. Springer, 2008. find
  7. Michael Beeson. Automatic derivation of the irrationality of e. J. Symb. Comput., 32(4):333–349, 2001. find
  8. Johan G. F. Belinfante. On computer-assisted proofs in ordinal number theory. J. Autom. Reasoning, 22(2):341–378, 1999. find
  9. Christoph Benzmüller, Lawrence C. Paulson, Frank Theiss, and Arnaud Fietzke. LEO-II - a cooperative automatic theorem prover for classical higher-order logic (system description). In Armando et al. [6], pages 162–170. find
  10. Nikolaj Bjørner and Viorica Sofronie-Stokkermans, editors. Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroc law, Poland, July 31 - August 5, 2011. Proceedings, volume 6803 of LNCS. Springer, 2011. find
  11. Nikolaj Bjørner and Andrei Voronkov, editors. Logic for Programming, Artificial Intelligence, and Reasoning - 18th International Conference, LPAR-18, Mérida, Venezuela, March 11-15, 2012. Proceedings, volume 7180 of LNCS. Springer, 2012. find
  12. Jasmin Christian Blanchette. Automatic Proofs and Refutations for Higher-Order Logic. PhD thesis, Fakultät für Informatik, Technische Universität München, 2012. http://www21.in.tum.de/~blanchet/phdthesis.pdf. ↗
  13. Jasmin Christian Blanchette, Sascha Böhme, and Lawrence C. Paulson. Extending Sledgehammer with SMT solvers. In Bjørner and Sofronie-Stokkermans [10], pages 116–130. find
  14. Jasmin Christian Blanchette, Sascha Böhme, Andrei Popescu, and Nicholas Smallbone. Encoding monomorphic and polymorphic types. In Nir Piterman and Scott A. Smolka, editors, TACAS, volume 7795 of Lecture Notes in Computer Science, pages 493–507. Springer, 2013. find
  15. Jasmin Christian Blanchette, Lukas Bulwahn, and Tobias Nipkow. Automatic proof and disproof in Isabelle/HOL. In Cesare Tinelli and Viorica Sofronie-Stokkermans, editors, FroCoS, volume 6989 of LNCS, pages 12–27. Springer, 2011. find
  16. Jasmin Christian Blanchette and Andrei Paskevich. TFF1: The TPTP typed first-order form with rank-1 polymorphism. In Maria Paola Bonacina, editor, CADE, volume 7898 of Lecture Notes in Computer Science, pages 414–420. Springer, 2013. find
  17. Jasmin Christian Blanchette, Andrei Popescu, Daniel Wand, and Christoph Weidenbach. More SPASS with Isabelle - superposition with hard sorts and configurable simplification. In Lennart Beringer and Amy P. Felty, editors, ITP, volume 7406 of LNCS, pages 345–360. Springer, 2012. find
  18. Sascha Böhme and Tobias Nipkow. Sledgehammer: Judgement Day. In Jürgen Giesl and Reiner Hähnle, editors, IJCAR, volume 6173 of LNCS, pages 107–121. Springer, 2010. find
  19. Chad E. Brown. Satallax: An automatic higher-order prover. In Gramlich et al. [29], pages 111–117. find
  20. 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
  21. Alonzo Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56–68, 1940. find
  22. Ingo Dahn. Interpretation of a Mizar-like logic in first-order logic. In Ricardo Caferra and Gernot Salzer, editors, FTP (LNCS Selection), volume 1761 of LNCS, pages 137–151. Springer, 1998. find
  23. Ingo Dahn and Christoph Wernhard. First order proof problems extracted from an article in the MIZAR Mathematical Library. In Maria Paola Bonacina and Ulrich Furbach, editors, Int. Workshop on First-Order Theorem Proving (FTP’97), RISC-Linz Report Series No. 97-50, pages 58–62. Johannes Kepler Univer… find
  24. 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
  25. Jean-Christophe Filliâtre and Claude Marché. The Why/Krakatoa/Caduceus platform for deductive program verification. In Werner Damm and Holger Hermanns, editors, CAV, volume 4590 of LNCS, pages 173–177. Springer, 2007. find
  26. 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
  27. Allen Van Gelder and Geoff Sutcliffe. Extending the TPTP language to higher-order logic with automated parser generation. In Furbach and Shankar [26], pages 156–161. find
  28. Michael R. Genesereth and Richard E. Fikes. Knowledge Interchange Format, Version 3.0 Reference Manual. Technical Report Logic-92-1, Computer Science Department, Stanford University, 1992. find
  29. Bernhard Gramlich, Dale Miller, and Uli Sattler, editors. Automated Reasoning - 6th International Joint Conference, IJCAR 2012, Manchester, UK, June 26-29, 2012. Proceedings, volume 7364 of LNCS. Springer, 2012. find
  30. Reiner Hähnle, Manfred Kerber, and Christoph Weidenbach. Common syntax of the DFGSchwerpunktprogramm deduction. Technical Report TR 10/96, Fakultät für Informatik, Universität Karlsruhe, Karlsruhe, Germany, 1996. find
  31. Thomas C. Hales. Introduction to the Flyspeck project. In Thierry Coquand, Henri Lombardi, and Marie-Françoise Roy, editors, Mathematics, Algorithms, Proofs, number 05021 in Dagstuhl Seminar Proceedings, pages 1–11, Dagstuhl, Germany, 2006. Internationales Begegnungs- und Forschungszentrum für Inf… find
  32. Thomas C. Hales. Mathematics in the age of the Turing machine. Lecture Notes in Logic, 2012. to appear; http://www.math.pitt.edu/~thales/papers/turing.pdf. ↗
  33. Thomas C. Hales, John Harrison, Sean McLaughlin, Tobias Nipkow, Steven Obua, and Roland Zumkeller. A revision of the proof of the Kepler Conjecture. Discrete & Computational Geometry, 44(1):1–34, 2010. find
  34. 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
  35. John Harrison. A Mizar mode for HOL. In Joakim von Wright, Jim Grundy, and John Harrison, editors, TPHOLs, volume 1125 of LNCS, pages 203–220. Springer, 1996. find
  36. 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
  37. R. Hindley. The principal type-scheme of an object in combinatory logic. Transactions of the American Mathematical Society, 146:29–60, 1969. find
  38. Krystof Hoder and Andrei Voronkov. Sine qua non for large theory reasoning. In Bjørner and Sofronie-Stokkermans [10], pages 299–314. find
  39. Joe Hurd. Integrating Gandalf and HOL. In Yves Bertot, Gilles Dowek, André Hirschowitz, C. Paulin, and Laurent Théry, editors, TPHOLs, volume 1690 of LNCS, pages 311–322. Springer, 1999. find
  40. Joe Hurd. An LCF-style interface between HOL and first-order logic. In Andrei Voronkov, editor, CADE, volume 2392 of Lecture Notes in Computer Science, pages 134–138. Springer, 2002. find
  41. Joe Hurd. First-order proof tactics in higher-order logic theorem provers. In Myla Archer, Ben Di Vito, and César Muñoz, editors, Design and Application of Strategies/Tactics in Higher Order Logics (STRATA 2003), number NASA/CP-2003-212448 in NASA Technical Reports, pages 56–68, September 2003. find
  42. Cezary Kaliszyk. Web interfaces for proof assistants. Electr. Notes Theor. Comput. Sci., 174(2):49–61, 2007. find
  43. Cezary Kaliszyk and Alexander Krauss. Scalable LCF-style proof translation. In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors, Proc. of the 4th International Conference on Interactive Theorem Proving (ITP’13), volume 7998 of LNCS, pages 51–66. Springer Verlag, 2013. find
  44. Cezary Kaliszyk and Josef Urban. Initial experiments with external provers and premise selection on HOL Light corpora. In Pascal Fontaine, Renate A. Schmidt, and Stephan Schulz, editors, PAAR-2012, volume 21 of EPiC Series, pages 72–81. EasyChair, 2013. find
  45. Johannes Kepler. Strena seu de nive sexangula. Frankfurt: Gottfried. Tampach, 1611. find
  46. Laura Kovács and Andrei Voronkov. First-order theorem proving and Vampire. In Natasha Sharygina and Helmut Veith, editors, CAV, volume 8044 of Lecture Notes in Computer Science, pages 1–35. Springer, 2013. find
  47. 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
  48. 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 Gramlich et al. [29], pages 378–392. find
  49. Donald W. Loveland. Mechanical theorem proving by model elimination. Journal of the ACM, 15(2):236–251, April 1968. find
  50. Donald W. Loveland. Automated Theorem Proving: A Logical Basis. North-Holland, Amsterdam, 1978. find
  51. David A. McAllester. Ontic: a knowledge representation system for mathematics. MIT Press, Cambridge, MA, USA, 1989. find
  52. William McCune. Prover9 and Mace4. http://www.cs.unm.edu/~mccune/prover9/, 2005– 2010. ↗
  53. William McCune and Olga Shumsky Matlin. Ivy: A Preprocessor and Proof Checker for First-Order Logic. In M. Kaufmann, P. Manolios, and J. Strother Moore, editors, Computer-Aided Reasoning: ACL2 Case Studies, number 4 in Advances in Formal Methods, pages 265–282. Kluwer Academic Publishers, 2000. find
  54. William McCune and Larry Wos. Otter: The CADE-13 Competition Incarnations. Journal of Automated Reasoning, 18(2):211–220, 1997. find
  55. Andreas Meier. System description: Tramp: Transformation of machine-found proofs into nd-proofs at the assertion level. In David A. McAllester, editor, CADE, volume 1831 of LNCS, pages 460–464. Springer, 2000. find
  56. Jia Meng and Lawrence C. Paulson. Translating higher-order clauses to first-order clauses. J. Autom. Reasoning, 40(1):35–60, 2008. find
  57. Steven Obua and Sebastian Skalberg. Importing hol into Isabelle/HOL. In Furbach and Shankar [26], pages 298–302. find
  58. Lawrence C. Paulson. A generic tableau prover and its integration with Isabelle. J. UCS, 5(3):73–87, 1999. find
  59. 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
  60. 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
  61. Adam Pease and Geoff Sutcliffe. First order reasoning on a large ontology. In Geoff Sutcliffe, Josef Urban, and Stephan Schulz, editors, ESARLT, volume 257 of CEUR Workshop Proceedings. CEUR-WS.org, 2007. find
  62. 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
  63. Henri Poincaré. The foundations of science: Science and hypothesis, The value of science, Science and method. The Science Press, New York, 1913. find
  64. Virgile Prevosto and Uwe Waldmann. SPASS+T. In G. Sutcliffe, R. Schmidt, and S. Schulz, editors, ESCoR 2006, volume 192 of CEUR, pages 18–33, 2006. find
  65. Art Quaife. Automated Development of Fundamental Mathematical Theories. Kluwer Academic Publishers, 1992. find
  66. Piotr Rudnicki and Andrzej Trybulec. On the integrity of a repository of formalized mathematics. In Andrea Asperti, Bruno Buchberger, and James H. Davenport, editors, MKM, volume 2594 of LNCS, pages 162–174. Springer, 2003. find
  67. Stephan Schulz. E - A Brainiac Theorem Prover. AI Commun., 15(2-3):111–126, 2002. find
  68. Konrad Slind, Michael J. C. Gordon, Richard J. Boulton, and Alan Bundy. System description: An interface between CLAM and HOL. In Claude Kirchner and Hélène Kirchner, editors, CADE, volume 1421 of LNCS, pages 134–138. Springer, 1998. find
  69. Geoff Sutcliffe and Christoph Benzmüller. Automated Reasoning in Higher-Order Logic using the TPTP THF Infrastructure. Journal of Formalized Reasoning, 3(1):1–27, 2010. find
  70. Geoff Sutcliffe, Stephan Schulz, Koen Claessen, and Peter Baumgartner. The TPTP typed first-order form with arithmetic. In Bjørner and Voronkov [11], pages 406–419. find
  71. Geoff Sutcliffe, Stephan Schulz, Koen Claessen, and Allen Van Gelder. Using the TPTP language for writing derivations and finite interpretations. In Furbach and Shankar [26], pages 67–81. find
  72. Josef Urban. Translating Mizar for first order theorem provers. In MKM, volume 2594 of LNCS, pages 203–215. Springer, 2003. find
  73. Josef Urban. MPTP - Motivation, Implementation, First Experiments. Journal of Automated Reasoning, 33(3-4):319–339, 2004. find
  74. Josef Urban. MoMM - fast interreduction and retrieval in large libraries of formalized mathematics. Int. J. on Artificial Intelligence Tools, 15(1):109–130, 2006. find
  75. Josef Urban. MPTP 0.2: Design, implementation, and initial experiments. J. Autom. Reasoning, 37(1-2):21–43, 2006. find
  76. 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
  77. Josef Urban. BliStr: The Blind Strategymaker. CoRR, abs/1301.2683, 2014. Accepted to PAAR’14. — [arXiv:1301.2683](https://arxiv.org/abs/1301.2683) find
  78. Josef Urban, Piotr Rudnicki, and Geoff Sutcliffe. ATP and presentation service for Mizar formalizations. J. Autom. Reasoning, 50:229–241, 2013. find
  79. 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, AIS-C/MKM/Calculemus, volume 6167 of LNCS, pages 132–… find
  80. Josef Urban, Geoff Sutcliffe, Petr Pudlák, and Jiřı́ Vyskočil. MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance. In Armando et al. [6], pages 441–456. find
  81. 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
  82. 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
  83. Larry Wall. Programming Perl. O’Reilly & Associates, Inc., Sebastopol, CA, USA, 3rd edition, 2000. find
  84. Christoph Weidenbach, Bijan Afshordel, Uwe Brahm, Christian Cohrs, Thorsten Engel, Enno Keen, Christian Theobalt, and Dalibor Topić. System description: SPASS version 1.0.0. In Automated Deduction - CADE-16, volume 1632 of LNCS, pages 378–382. Springer Berlin Heidelberg, 1999. find
  85. Christoph Weidenbach, Dilyana Dimova, Arnaud Fietzke, Rohit Kumar, Martin Suda, and Patrick Wischnewski. SPASS Version 3.5. In Renate A. Schmidt, editor, CADE, volume 5663 of LNCS, pages 140–145. Springer, 2009. find
  86. Freek Wiedijk. Estimating the cost of a standard library for a mathematical proof checker. http://www.cs.ru.nl/~freek/notes/mathstdlib2.pdf, 2001. ↗
  87. Freek Wiedijk. A synthesis of the procedural and declarative styles of interactive theorem proving. Logical Methods in Computer Science, 8(1), 2012. find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/kaliszyk-2012-learning-assisted-automated-reasoning-flyspeck/