Elamur Research⌕
☰
home / papers / 2017 / HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving

HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving

Paper · 2017 · Cezary Kaliszyk, François Chollet and Christian Szegedy

Summary

Formal proofs checked by interactive theorem provers (ITPs) contain enormous numbers of intermediate logical steps. Most of these steps come from hand-crafted search heuristics rather than learned guidance. The authors argue that deep learning may now be ready to improve automated reasoning, and they release HolStep, a public benchmark dataset (BSD license) for this purpose.

HolStep was extracted from proof traces of HOL Light, covering its multivariate analysis library and the formal Kepler conjecture (Flyspeck) development. Every kernel-level inference was logged. Each proof step was then labelled as either used in the final proof or derived but ultimately unnecessary. Each example includes the target conjecture, its dependencies, a human-readable printout, and a compact tokenization. In that tokenization, type information is erased and bound variables are encoded as de Bruijn indices.

The paper defines several learning tasks, centred on classifying whether a step is useful, with or without the conjecture as context. It benchmarks logistic regression, CNN and RNN baselines on these tasks. The authors report that the results look promising. The dataset is intended to work like ImageNet, giving the field a shared testbed for ML-guided proof search.

Key points

  • The dataset has 2,013,046 training and 196,030 test examples from about 11,400 non-trivial proofs (9,999 training and 1,411 test conjectures). The classes are exactly balanced, with 1,104,538 positive and 1,104,538 negative steps.
  • Examples are grouped by proof, so conjectures in the training and test splits are generally disjoint.
  • In the custom tokenization, only partial applications are marked, which removes parentheses for over 90% of applications. Top-level universal quantifiers are dropped, and free variables are renamed canonically.
  • Proposed tasks include:
    • unconditioned and conjecture-conditioned step-usefulness classification;
    • premise selection;
    • predicting human-named statements or the source conjecture;
    • generating intermediate steps or lemmas.
  • The data, format description, generation scripts and baseline code are available at cl-informatik.uibk.ac.at/cek/holstep/.

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

🏢GoogleMountain View · United States533 works · 443,885 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, François Chollet and Christian Szegedy. 2017. HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving. arXiv:1703.00426.

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

@misc{kaliszyk2017holstep,
  title = {{HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving}},
  author = {Cezary Kaliszyk, François Chollet and Christian Szegedy},
  year = {2017},
  doi = {10.48550/arxiv.1703.00426},
  eprint = {1703.00426},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.1703.00426}
}

References

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

  1. Martín Abadi, Ashish Agarwal, Paul Barham, Eugene Brevdo, Zhifeng Chen, Craig Citro, Greg S. Corrado, Andy Davis, Jeffrey Dean, Matthieu Devin, Sanjay Ghemawat, Ian Goodfellow, Andrew Harp, Geoffrey Irving, Michael Isard, Yangqing Jia, Rafal Jozefowicz, Lukasz Kaiser, Manjunath Kudlur, Josh Levenber… find
  2. 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. doi: 10.1007/s10817-013-9286-5.
  3. Alex A. Alemi, François Chollet, 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 (eds.), Advances in Neural Information Processing Systems (NIPS 2016),… — DeepMath - Deep Sequence Models for Premise Selection
  4. David Aspinall and Cezary Kaliszyk. What’s in a theorem name? In Jasmin Christian Blanchette and Stephan Merz (eds.), Interactive Theorem Proving (ITP 2016), volume 9807 of LNCS, pp. 459–465. find
  5. Franz Baader and Tobias Nipkow. Term rewriting and all that. Cambridge University Press, 1998. ISBN 978-0-521-45520-6. find
  6. Jasmin C. Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, and Josef Urban. Hammering towards QED. J. Formalized Reasoning, 9(1):101–148, 2016. ISSN 1972-5787. doi: 10.6092/issn.1972-5787/4593. — [doi:10.6092/issn.1972-5787/4593](https://doi.org/10.6092/issn.1972-5787/4593) find
  7. Jasmin Christian Blanchette, Maximilian P. L. Haslbeck, Daniel Matichuk, and Tobias Nipkow. Mining the Archive of Formal Proofs. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge (eds.), Intelligent Computer Mathematics (CICM 2015), volume 9150 of LNCS, pp. 3–17. find
  8. James P. Bridge, Sean B. Holden, and Lawrence C. Paulson. Machine learning for first-order theorem proving - learning to select a good heuristic. J. Autom. Reasoning, 53(2):141–172, 2014. doi: 10.1007/s10817-014-9301-5. — [doi:10.1007/s10817-014-9301-5](https://doi.org/10.1007/s10817-014-9301-5) find
  9. Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zel-dovich. Using crash Hoare logic for certifying the FSCQ file system. In Ajay Gulati and Hakim Weatherspoon (eds.), USENIX 2016. find
  10. USENIX Association, 2016. find
  11. François Chollet. Keras. https://github.com/fchollet/keras, 2015. ↗
  12. Alonzo Church. A formulation of the simple theory of types. J. Symb. Log., 5(2):56–68, 1940. doi: 10.2307/2266170. URL http://dx.doi.org/10.2307/2266170. ↗
  13. J. Deng, W. Dong, R. Socher, L.-J. Li, K. Li, and L. Fei-Fei. ImageNet: A Large-Scale Hierarchical Image Database. In CVPR09, 2009. find
  14. Hazel Duncan. The Use of Data-Mining for the Automatic Formation of Tactics. PhD thesis, University of Edinburgh, 2007. find
  15. Michael Färber and Chad E. Brown. Internal guidance for Satallax. In Nicola Olivetti and Ashish Tiwari (eds.), International Joint Conference on Automated Reasoning (IJCAR 2016), volume 9706 of LNCS, pp. 349–361. find
  16. Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O’Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, and Laurent Théry. A machine-checked proof of the odd order theorem. In Sandr… find
  17. Michael J. C. Gordon, Robin Milner, and Christopher P. Wadsworth. Edinburgh LCF, volume 78 of Lecture Notes in Computer Science. Springer, 1979. ISBN 3-540-09724-4. doi: 10.1007/3-540-09724-4. URL http://dx.doi.org/10.1007/3-540-09724-4. — [doi:10.1007/3-540-09724-4](https://doi.org/10.1007/3-540-09724-4) ↗
  18. Adam Grabowski, Artur Kornilowicz, and Adam Naumowicz. Mizar in a nutshell. J. Formalized Reasoning, 3(2):153–245, 2010. doi: 10.6092/issn.1972-5787/1980. — [doi:10.6092/issn.1972-5787/1980](https://doi.org/10.6092/issn.1972-5787/1980) find
  19. Thomas 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
  20. Thomas C. Hales, Mark Adams, Gertrud Bauer, Dat Tat Dang, John Harrison, Truong Le Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Thang Tat Nguyen, Truong Quang Nguyen, Tobias Nipkow, Steven Obua, Joseph Pleso, Jason Rute, Alexey Solovyev, An Hoai Thi Ta, Trung Nam Tran, Diep Thi Trieu, Jos… — A formal proof of the Kepler conjecture
  21. John Harrison. HOL Light: An overview. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel (eds.), Theorem Proving in Higher Order Logics (TPHOLs 2009), volume 5674 of LNCS, pp. 60–66. find
  22. John Harrison. The HOL Light theory of Euclidean space. J. Autom. Reasoning, 50(2):173–190, 2013. doi: 10.1007/s10817-012-9250-9. — [doi:10.1007/s10817-012-9250-9](https://doi.org/10.1007/s10817-012-9250-9) find
  23. John Harrison, Josef Urban, and Freek Wiedijk. History of interactive theorem proving. In Jörg Siekmann (ed.), Handbook of the History of Logic vol. 9 (Computational Logic), pp. 135–214. Elsevier, 2014.
  24. R. Hindley. The principal type-scheme of an object in combinatory logic. Transactions of the american mathematical society, 146:29–60, 1969. ISSN 0002-9947. find
  25. Sepp Hochreiter and Jürgen Schmidhuber. Long short-term memory. Neural computation, 9(8): 1735–1780, 1997. find
  26. Kryštof Hoder and Andrei Voronkov. Sine qua non for large theory reasoning. In Nikolaj Bjørner and Viorica Sofronie-Stokkermans (eds.), CADE-23, volume 6803 of LNAI, pp. 299–314. Springer, 2011. find
  27. Joe Hurd. First-order proof tactics in higher-order logic theorem provers. In Myla Archer, Ben Di Vito, and César Muñoz (eds.), Design and Application of Strategies/Tactics in Higher Order Logics (STRATA 2003), number NASA/CP-2003-212448 in NASA Technical Reports, pp. 56–68, September 2003. URL http… find
  28. Joe Hurd. The OpenTheory standard theory library. In Mihaela Gheorghiu Bobaru, Klaus Havelund, Gerard J. Holzmann, and Rajeev Joshi (eds.), NASA Formal Methods (NFM 2011), volume 6617 of LNCS, pp. 177–191. find
  29. Cezary Kaliszyk and Alexander Krauss. Scalable LCF-style proof translation. In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie (eds.), Interactive Theorem Proving (ITP 2013), volume 7998 of LNCS, pp. 51–66. find
  30. Cezary Kaliszyk and Josef Urban. Learning-assisted automated reasoning with Flyspeck. J. Autom. Reasoning, 53(2):173–213, 2014. doi: 10.1007/s10817-014-9303-3.
  31. Cezary Kaliszyk and Josef Urban. FEMaLeCoP: Fairly efficient machine learning connection prover. In Martin Davis, Ansgar Fehnker, Annabelle McIver, and Andrei Voronkov (eds.), 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2015), volume 9450 of L… find
  32. Cezary Kaliszyk and Josef Urban. Learning-assisted theorem proving with millions of lemmas. J. Symbolic Computation, 69:109–128, 2015b. doi: 10.1016/j.jsc.2014.09.032. — [doi:10.1016/j.jsc.2014.09.032](https://doi.org/10.1016/j.jsc.2014.09.032) find
  33. Cezary Kaliszyk, Josef Urban, and Jiří Vyskočil. Learning to parse on aligned corpora. In Christian Urban and Xingyuan Zhang (eds.), Proc. 6h Conference on Interactive Theorem Proving (ITP’15), volume 9236 of LNCS, pp. 227–233. Springer-Verlag, 2015. doi: 10.1007/978-3-319-22102-1_15. — [doi:10.1007/978-3-319-22102-1_15](https://doi.org/10.1007/978-3-319-22102-1_15) find
  34. Gerwin Klein, June Andronick, Kevin Elphinstone, Toby C. Murray, Thomas Sewell, Rafal Kolanski, and Gernot Heiser. Comprehensive formal verification of an OS microkernel. ACM Trans. Comput. Syst., 32(1):2, 2014. find
  35. Laura Kovács and Andrei Voronkov. First-order theorem proving and Vampire. In Natasha Sharygina and Helmut Veith (eds.), Computer-Aided Verification (CAV 2013), volume 8044 of LNCS, pp. 1–35. find
  36. Daniel Kühlwein and Josef Urban. MaLeS: A framework for automatic tuning of automated theorem provers. J. Autom. Reasoning, 55(2):91–116, 2015. doi: 10.1007/s10817-015-9329-1. — [doi:10.1007/s10817-015-9329-1](https://doi.org/10.1007/s10817-015-9329-1) find
  37. Xavier Leroy. Formal verification of a realistic compiler. Commun. ACM, 52(7):107–115, 2009. find
  38. Steven Obua and Sebastian Skalberg. Importing HOL into Isabelle/HOL. In Ulrich Furbach and Natarajan Shankar (eds.), International Joint Conference on Automated Reasoning (IJCAR 2006), volume 4130 of LNCS, pp. 298–302. find
  39. Lawrence C. Paulson. A generic tableau prover and its integration with Isabelle. J. Universal Computer Science, 5(3):73–87, 1999. find
  40. Stephan Schulz. System description: E 1.8. In Kenneth L. McMillan, Aart Middeldorp, and Andrei Voronkov (eds.), Logic for Programming, Artificial Intelligence (LPAR 2013), volume 8312 of LNCS, pp. 735–743. find
  41. David Silver, Aja Huang, Christopher J. Maddison, Arthur Guez, Laurent Sifre, George van den Driessche, Julian Schrittwieser, Ioannis Antonoglou, Veda Panneershelvam, Marc Lanctot, Sander Dieleman, Dominik Grewe, John Nham, Nal Kalchbrenner, Ilya Sutskever, Timothy Lillicrap, Madeleine Leach, Koray… find
  42. Richard Socher, Danqi Chen, Christopher D. Manning, and Andrew Y. Ng. Reasoning with neural tensor networks for knowledge base completion. In Advances in Neural Information Processing Systems 26: 27th Annual Conference on Neural Information Processing Systems 2013. Proceedings., pp. 926–934, 2013a.…
  43. Richard Socher, Alex Perelygin, Jean Wu, Jason Chuang, Christopher D. Manning, Andrew Y. Ng, and Christopher Potts. Recursive deep models for semantic compositionality over a sentiment treebank. In Proceedings of the 2013 Conference on Empirical Methods in Natural Language Processing, pp. 1631–1642,…
  44. Sainbayar Sukhbaatar, Jason Weston, Rob Fergus, et al. End-to-end memory networks. In Advances in Neural Information Processing Systems, pp. 2431–2439, 2015. find
  45. Geoff Sutcliffe. The CADE ATP system competition - CASC. AI Magazine, 37(2):99–101, 2016. find
  46. Josef Urban, Jiří Vyskočil, and Petr Štěpánek. MaLeCoP: Machine learning connection prover. In Kai Brünnler and George Metcalfe (eds.), TABLEAUX 2011, volume 6793 of LNCS. find
  47. Yonghui Wu, Mike Schuster, Zhifeng Chen, Quoc V. Le, Mohammad Norouzi, Wolfgang Macherey, Maxim Krikun, Yuan Cao, Qin Gao, Klaus Macherey, Jeff Klingner, Apurva Shah, Melvin Johnson, Xiaobing Liu, Lukasz Kaiser, Stephan Gouws, Yoshikiyo Kato, Taku Kudo, Hideto Kazawa, Keith Stevens, George Kurian, N… find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/kaliszyk-2017-holstep-machine-learning-dataset-higher/