Elamur Research⌕
☰
home / papers / 2019 / HOList: An Environment for Machine Learning of Higher-Order Theorem Proving

HOList: An Environment for Machine Learning of Higher-Order Theorem Proving

Paper · 2019 · Kshitij Bansal, Sarah M. Loos, Markus N. Rabe et al.

Summary

Learning-based theorem proving has lacked a shared, large-scale benchmark. Existing proof assistants use incompatible logical foundations, and earlier datasets were either small or scored only with proxy metrics. HOList fills this gap. It is an open-source environment built on the HOL Light interactive prover, packaged as a Docker image and controlled through a Python API, so agents can search for proofs as in reinforcement learning. The authors added logging of the human-written proofs, faster startup for distributed search, and an independent proof checker, so a proof found through the API does not have to be trusted blindly. The benchmark comes from HOL Light's core library, its complex-analysis library and the Flyspeck formalization of the Kepler conjecture. To show the setup is usable, they built DeepHOL, a neural prover. It first imitates human proofs, then improves through reinforcement learning, picking a tactic and ranking premises for each goal. On the complex-analysis validation set, its best version proved 38.9% of theorems. The resource gives higher-order automated reasoning a reproducible yardstick based on how many theorems a system actually proves.

Key points

  • The benchmark covers about 2,200 definitions and 29,462 theorems across three corpora (core, complex, flyspeck), with over 1 million proof states. The Coq-based GamePad has only 1,602 theorems.
  • DeepHOL uses WaveNet-style encoders to choose among 41 tactics and to rank theorem arguments (premises). The deeper variant has about 47M parameters.
  • On the 3,225-theorem complex validation set, the scores were:
    • ASM_MESON_TAC baselines: 6.1% (no arguments) and 9.2% (with argument selection)
    • Supervised WaveNet models: 27.6–32.65%
    • Reinforcement-learning loops: 36.3–38.9%
  • In each reinforcement-learning round, the system tries 2,000 training theorems spread over 1,000 cores, with limits of 100 proof states and 300 s per attempt. Together, all loops proved 58.0% of the training set (5,919 of 10,199 theorems).
  • Code and tools are released at deephol.org, including proof export/import and a separate checker that replays found proofs inside HOL Light.

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 States492 works · 440,463 citations

 Fields, topics and concepts

📚 Shelves 2The field of science this work belongs to (OpenAlex fields).Computer Science · 18,614 worksArtificial Intelligence · 17,965 works

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

Cite

Cite as Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, Christian Szegedy and Stewart Wilcox. 2019. HOList: An Environment for Machine Learning of Higher-Order Theorem Proving. arXiv:1904.03241.

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

@misc{bansal2019holist,
  title = {{HOList: An Environment for Machine Learning of Higher-Order Theorem Proving}},
  author = {Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, Christian Szegedy and Stewart Wilcox},
  year = {2019},
  doi = {10.48550/arxiv.1904.03241},
  eprint = {1904.03241},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.1904.03241}
}

References

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

  1. Vassil Panayotov, Guoguo Chen, Daniel Povey, and Sanjeev Khudanpur. Librispeech: an asr corpus based on public domain audio books. In Acoustics, Speech and Signal Processing (ICASSP), 2015 IEEE International Conference on, pages 5206–5210. IEEE, 2015. find
  2. James Bennett, Stan Lanning, et al. The netflix prize. In Proceedings of KDD cup and workshop, volume 2007, page 35. New York, NY, USA, 2007. find
  3. Jia Deng, Wei Dong, Richard Socher, Li-Jia Li, Kai Li, and Li Fei-Fei. Imagenet: A large-scale hierarchical image database. In Computer Vision and Pattern Recognition, 2009. CVPR 2009. IEEE Conference on, pages 248–255. Ieee, 2009. find
  4. Tsung-Yi Lin, Michael Maire, Serge Belongie, James Hays, Pietro Perona, Deva Ramanan, Piotr Dollár, and C Lawrence Zitnick. Microsoft coco: Common objects in context. In European conference on computer vision, pages 740–755. Springer, 2014.
  5. Ondrej Bojar, Christian Buck, Christian Federmann, Barry Haddow, Philipp Koehn, Johannes Leveling, Christof Monz, Pavel Pecina, Matt Post, Herve Saint-Amand, et al. Findings of the 2014 workshop on statistical machine translation. In Proceedings of the ninth workshop on statistical machine translati…
  6. Pranav Rajpurkar, Jian Zhang, Konstantin Lopyrev, and Percy Liang. Squad: 100,000+ questions for machine comprehension of text. arXiv preprint arXiv:1606.05250, 2016.
  7. Thomas Hales, Mark Adams, Gertrud Bauer, Tat Dat Dang, John Harrison, Hoang Le Truong, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Tat Thang Nguyen, et al. A formal proof of the kepler conjecture. In Forum of Mathematics, Pi, volume 5. Cambridge University Press, 2017. find
  8. Josef Urban, Geoff Sutcliffe, Petr Pudlák, and Jiří Vyskočil. [21] Daniel Whalen. Holophrasm: a neural automated the-Malarea sg1-machine learner for automated reasoning with orem prover for higher-order logic. arXiv preprint semantic guidance. In International Joint Conference on arXiv:1608.02644,… find
  9. Thibault Gauthier, Cezary Kaliszyk, and Josef Urban. Tactictoe: Learning to reason with hol4 tactics. In LPAR-21. [23] Sarah Loos, Geoffrey Irving, Christian Szegedy, and 21st International Conference on Logic for Programming, Cezary Kaliszyk. Deep network guided proof search. arXiv Artificial Intel…
  10. Daniel Huang, Prafulla Dhariwal, Dawn Song, and Ilya Holstep: A machine learning dataset for higher-order logic Sutskever. Gamepad: A learning environment for theorem theorem proving. arXiv preprint arXiv:1703.00426, 2017. proving. arXiv preprint arXiv:1806.00608, 2018. [25] Cezary Kaliszyk, Josef U… find
  11. Konrad Slind and Michael Norrish. A brief overview of arXiv preprint arXiv:1805.07563, 2018. hol4. In International Conference on Theorem Proving in Higher Order Logics, pages 28–32. Springer, 2008. [26] Rong-En Fan, Kai-Wei Chang, Cho-Jui Hsieh, Xiang-Rui Wang, and Chih-Jen Lin. Liblinear: A librar… find
  12. Yves Bertot and Pierre Castéran. Interactive theorem prov-linear classification. Journal of machine learning research, ing and program development: Coq’Art: the calculus of 9(Aug):1871–1874, 2008. inductive constructions. Springer Science & Business Media, 2013. [27] Jens Otten and Wolfgang Bibel. l… find
  13. Mizar. The Mizar Mathematical Library. URL http: 161, 2003. //mizar.org. Accessed: 2018/01/18. [28] Stephan Schulz. Learning search control knowledge find
  14. Makarius Wenzel, Lawrence C. Paulson, and Tobias Nip-for equational deduction, volume 230 of DISKI. Infix kow. The isabelle framework. In Otmane Aït Mohamed, Akademische Verlagsgesellschaft, 2000. ISBN 978-3-César A. Muñoz, and Sofiène Tahar, editors, Theorem Prov-89838-230-4. ing in Higher Order Lo… find
  15. Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris machine learning connection prover. In International Con-Van Doorn, and Jakob von Raumer. The lean theorem ference on Automated Reasoning with Analytic Tableaux prover (system description). In International Conference and Related Methods, pages 2… find
  16. Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June vadze, Josef Urban, and Tom Heskes. Overview and eval-Andronick, David Cock, Philip Derrin, Dhammika Elka-uation of premise selection techniques for large theory duwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, mathematics. In International… — [doi:10.1145/1629575.1629596](https://doi.org/10.1145/1629575.1629596) find
  17. Cezary Kaliszyk and Josef Urban. Learning-assisted au-Theorem Proving, pages 35–50. Springer, 2013. tomated reasoning with flyspeck. Journal of Automated [34] Jesse Alama, Tom Heskes, Daniel Kühlwein, Evgeni Tsivt-Reasoning, 53(2):173–213, 2014. sivadze, and Josef Urban. Premise selection for mathe- find
  18. Cezary Kaliszyk and Josef Urban. Initial experiments with matics by corpus analysis and kernel methods. Journal of external provers and premise selection on hol light corpora. Automated Reasoning, 52(2):191–213, 2014. 2012. [35] James P. Bridge, Sean B. Holden, and Lawrence C. Paulson. find
  19. Alexander A Alemi, François Chollet, Geoffrey Irv-Machine learning for first-order theorem proving. J. Autom. ing, Niklas Eén, Christian Szegedy, and Josef Urban. Reasoning, pages 1–32, 2014. ISSN 0168-7433. doi: 10. Deepmath-deep sequence models for premise selection. 1007/s10817-014-9301-5. URL ht…
  20. Stephan Schulz. E - A Brainiac Theorem Prover. AI learner for automated reasoning 0.4 and 0.5. arXiv preprint Commun., 15(2-3):111–126, 2002. arXiv:1402.2359, 2014. [37] Cezary Kaliszyk, Lionel Mamane, and Josef Urban. Machine learning of coq proof guidance: First experiments. arXiv preprint arXiv:1… find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/bansal-2019-holist-environment-machine-learning-higher/