Elamur Research⌕
☰
home / papers / 2016 / Holophrasm: a neural Automated Theorem Prover for higher-order logic

Holophrasm: a neural Automated Theorem Prover for higher-order logic

Paper · 2016 · Daniel Whalen

Summary

Holophrasm is a fully automatic prover for higher-order logic that avoids hand-engineered features. It works in the Metamath language, where each proof step applies a known theorem through substitution and turns that theorem's hypotheses into new subgoals, so proofs naturally form trees. The system grows partial proof trees with a variant of the UCT bandit algorithm, guided by three neural networks:

  • a relevance network that ranks candidate theorems,
  • a generative sequence-to-sequence model (GRU with attention and beam search) that proposes expressions for unconstrained variables, an otherwise infinite action space,
  • a payoff network that estimates how provable a subgoal is.

Training data come from expanding the proofs in Metamath's set.mm module into individual steps. On held-out theorems, the prover proves 14.3% overall and 45.1% of those from the early part of the database. The results are below state of the art and not directly comparable to Mizar benchmarks. Still, the author presents Holophrasm as the first effective complete prover without hand-crafted features, which suggests that deep learning combined with tree search is a viable path for theorem proving.

Key points

  • Data: set.mm propositions split into 21,786 train, 2711 validation and 2720 test. These expand to about 1.2M training proof steps, and 426k of those steps involve unconstrained variables and are used for the generative network.
  • The relevance network reaches 55.3% top-1, 72.8% top-5 and 87.4% top-20 accuracy when choosing among viable theorems.
  • The generative network has a test perplexity of 2.08 over 1083 tokens. It produces fully correct substitutions in 39.1%, 51.3% and 57.5% of cases at beam widths 1, 5 and 20.
  • The payoff network classifies subgoals with 77.6% accuracy, compared with a 62.1% all-negative baseline.
  • Each test theorem gets at most 10,000 search passes or 5 minutes. The system proves 388 of 2720 test theorems, and successful proofs need a median of only 17 passes.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 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 Daniel Whalen. 2016. Holophrasm: a neural Automated Theorem Prover for higher-order logic. arXiv:1608.02644.

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

@misc{whalen2016holophrasm,
  title = {{Holophrasm: a neural Automated Theorem Prover for higher-order logic}},
  author = {Daniel Whalen},
  year = {2016},
  doi = {10.48550/arxiv.1608.02644},
  eprint = {1608.02644},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.1608.02644}
}

References

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

  1. Norman Megill. Metamath: A computer language for pure mathematics. 1997. find
  2. Roman Matuszewski and Piotr Rudnicki. Mizar: the first 30 years. Mechanized mathematics and its applications, 4(1):3–24, 2005. find
  3. Thomas C Hales. Introduction to the Flyspeck project. In Dagstuhl Seminar Proceedings. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2006. find
  4. Mauro Jaskelioff and Stephan Merz. Proving the correctness of Disk Paxos. Archive of Formal Proofs, June 2005. ISSN 2150-914x. http://isa-afp.org/entries/DiskPaxos.shtml, Formal proof development. ↗
  5. The Coq development team. The Coq proof assistant reference manual. INRIA, 2012. URL http://coq.inria.fr. Version 8.4. ↗
  6. John Harrison. HOL Light: a tutorial introduction. In International Conference on Formal Methods in Computer-Aided Design, pages 265–269. Springer, 1996. find
  7. Cezary Kaliszyk and Josef Urban. MizAR 40 for Mizar 40. Journal of Automated Reasoning, 55(3): 245–256, 2015.
  8. 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, 52(2):191–213, 2014.
  9. 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 International Joint Conference on Automated Reasoning, pages 378–392. Springer, 2012. find
  10. Daniel Kühlwein, Jasmin Christian Blanchette, Cezary Kaliszyk, and Josef Urban. Mash: machine learning for Sledgehammer. In Interactive Theorem Proving, pages 35–50. Springer, 2013. find
  11. Alex A Alemi, Francois Chollet, Geoffrey Irving, Christian Szegedy, and Josef Urban. DeepMath-Deep sequence models for premise selection. arXiv preprint arXiv:1606.04442, 2016.
  12. Levente Kocsis and Csaba Szepesvári. Bandit based Monte-Carlo planning. In Machine Learning: ECML 2006, pages 282–293. Springer, 2006. find
  13. Ilya Sutskever, Oriol Vinyals, and Quoc V Le. Sequence to sequence learning with neural networks. In Advances in neural information processing systems, pages 3104–3112, 2014.
  14. Chris J Maddison, Aja Huang, Ilya Sutskever, and David Silver. Move evaluation in Go using deep convolutional neural networks. arXiv preprint arXiv:1412.6564, 2014. — [arXiv:1412.6564](https://arxiv.org/abs/1412.6564) find
  15. David Silver, Aja Huang, Chris J Maddison, Arthur Guez, Laurent Sifre, George Van Den Driessche, Julian Schrittwieser, Ioannis Antonoglou, Veda Panneershelvam, Marc Lanctot, et al. Mastering the game of Go with deep neural networks and tree search. Nature, 529(7587):484–489, 2016. find
  16. Minh-Thang Luong, Hieu Pham, and Christopher D Manning. Effective approaches to attention-based neural machine translation. arXiv preprint arXiv:1508.04025, 2015.
  17. Xavier Glorot and Yoshua Bengio. Understanding the difficulty of training deep feedforward neural networks. In Aistats, volume 9, pages 249–256, 2010. find
  18. Diederik Kingma and Jimmy Ba. arXiv:1412.6980, 2014. Adam: A method for stochastic optimization. arXiv preprint

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/whalen-2016-holophrasm-neural-automated-theorem-prover/