Elamur Research⌕
☰
home / papers / 2022 / Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers

Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers

Paper · 2022 · Albert Q. Jiang, Wenda Li, Szymon Tworkowski et al.

Summary

Language-model provers for interactive theorem provers (ITPs) are weak at premise selection, which means finding the few useful lemmas in libraries holding hundreds of thousands of facts. A model cannot memorise that many facts, and listing candidate premises in the prompt quickly goes past its context length. Thor hands this job to hammers. A hammer sends the goal to external automated theorem provers (ATPs) and keeps only the premises their proofs actually use. To build the training data, the authors run Sledgehammer on every proof state in the training proofs. Wherever it succeeds, the target proof step is replaced with a special <hammer> token. The language model learns when to output this token, and during proof search the token triggers a real Sledgehammer call. The authors built Thor for Isabelle and tested it on PISA and MiniF2F. On PISA it raised the language model's success rate from 39.0% to 57.0%. On MiniF2F it reached 29.9%, slightly above an expert-iteration system, while using much less compute. The result shows that combining neural and symbolic provers is cheap and effective, and the method can be ported to any ITP that has a hammer.

Key points

  • The motivating measurement: only 1.9% of model-generated steps that cite premises moved the proof forward, compared with 28.2% of steps that cite none.
  • On PISA, Thor solved 57.0% of problems, up from 39.0%, and 8.2% of problems could be solved neither by the language model alone nor by Sledgehammer alone.
  • On MiniF2F (test set), Thor raised the base language model from 24.2% to 29.9%, compared with 29.6% for expert iteration (Polu et al., 2022). The authors estimate that matching that expert-iteration setup in Isabelle would take about 100 human hours of formalisation and 500 TPU hours.
  • The protocol should carry over to other ITPs with hammers, such as HOL(y)Hammer for HOL Light and CoqHammer for Coq, but it was tested only on Isabelle.
  • Thor can only use premise-selection tools that produce valid proof steps directly, so ranking methods like SInE or search tools like SErAPIS cannot be plugged in. Expert iteration or proof artifact co-training could be added on top of Thor.

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🎓Stanford UniversityStanford · United States506 works · 330,053 citations🎓University of CambridgeCambridge · United Kingdom256 works · 123,373 citations🎓University of WarsawWarsaw · Poland8 works · 575 citations🏛️Polish Academy of SciencesWarsaw · Poland12 works · 599 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 2Research subjects and languages the work is about.Language models & pretraining · 3,894 worksReasoning · 1,685 works

Cite

Cite as Albert Q. Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzygóźdź, Piotr Miłoś, Yuhuai Wu and Mateja Jamnik. 2022. Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers. arXiv:2205.10893.

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

@misc{jiang2022thor,
  title = {{Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers}},
  author = {Albert Q. Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzygóźdź, Piotr Miłoś, Yuhuai Wu and Mateja Jamnik},
  year = {2022},
  doi = {10.48550/arxiv.2205.10893},
  eprint = {2205.10893},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2205.10893}
}

References

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

  1. Jeremy Avigad, Kevin Donnelly, David Gray, and Paul Raff. A formally verified proof of the prime number theorem. ACM Transactions on Computational Logic (TOCL), 9(1):2–es, 2007. find
  2. Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, and Josef Urban. Hammering towards QED. J. Formaliz. Reason., 9(1):101–148, 2016. doi: 10.6092/issn.1972-5787/4593. URL https://doi.org/10.6092/issn.1972-5787/4593. ↗
  3. Stephen A Cook. The complexity of theorem-proving procedures. In Proceedings of the third annual ACM symposium on Theory of computing, pages 151–158, 1971. find
  4. Lukasz Czajka and Cezary Kaliszyk. Hammer for coq: Automation for dependent type theory. J. Autom. Reason., 61(1-4):423–453, 2018. doi: 10.1007/s10817-018-9458-4. URL https://doi.org/10.1007/s10817-018-9458-4. ↗
  5. Martin Davis, George Logemann, and Donald Loveland. A machine program for theorem-proving. Communications of the ACM, 5(7):394–397, 1962. find
  6. Leo Gao, Stella Biderman, Sid Black, Laurence Golding, Travis Hoppe, Charles Foster, Jason Phang, Horace He, Anish Thite, Noa Nabeshima, Shawn Presser, and Connor Leahy. The pile: An 800gb dataset of diverse text for language modeling, 2021. URL https://arxiv.org/abs/ 2101.00027. ↗
  7. Thibault Gauthier and Cezary Kaliszyk. Premise selection and external provers for HOL4. In Xavier Leroy and Alwen Tiu, editors, Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015, pages 49–57. find
  8. ACM, 2015. doi: 10.1145/2676724.2693173. URL https://doi.org/10.1145/2676724.2693173. — [doi:10.1145/2676724.2693173](https://doi.org/10.1145/2676724.2693173) ↗
  9. Herbert L Gelernter. Realization of a geometry theorem proving machine. In IFIP congress, pages 273–281, 1959. find
  10. 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, et al. A machine-checked proof of the odd order theorem. In International conference on interactive theorem proving, pages 163–179. Spring… find
  11. Georges Gonthier et al. Formal proof–the four-color theorem. Notices of the AMS, 55(11):1382–1393, 2008. find
  12. Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W. Ayers, and Stanislas Polu. Proof artifact co-training for theorem proving with language models. CoRR, abs/2102.06203, 2021. URL https://arxiv.org/abs/2102.06203. ↗
  13. Kryštof Hoder and Andrei Voronkov. Sine qua non for large theory reasoning. In International Conference on Automated Deduction, pages 299–314. Springer, 2011. find
  14. Geoffrey Irving, Christian Szegedy, Alexander A Alemi, Niklas Eén, François Chollet, and Josef Urban. Deepmath-deep sequence models for premise selection. Advances in neural information processing systems, 29, 2016. — DeepMath - Deep Sequence Models for Premise Selection
  15. Albert Q. Jiang, Wenda Li, Jesse Michael Han, and Yuhuai Wu. Lisa: Language models of isabelle proofs. 6th Conference on Artificial Intelligence and Theorem Proving, 2021. find
  16. Cezary Kaliszyk and Josef Urban. Hol(y)hammer: Online ATP service for HOL light. Math. Comput. Sci., 9(1):5–22, 2015. doi: 10.1007/s11786-014-0182-0. URL https://doi.org/10.1007/ s11786-014-0182-0. find
  17. Cezary Kaliszyk, François Chollet, and Christian Szegedy. Holstep: A machine learning dataset for higher-order logic theorem proving. arXiv preprint arXiv:1703.00426, 2017. find
  18. Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, et al. sel4: Formal verification of an os kernel. In Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles, pages 207–… find
  19. 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, Automated Reasoning - 6th International Joint Conference, IJCAR 20… find
  20. Springer, 2012. doi: 10.1007/978-3-642-31365-3\\_30. URL https://doi.org/10.1007/978-3-642-31365-3_30. — [doi:10.1007/978-3-642-31365-3\\_30](https://doi.org/10.1007/978-3-642-31365-3_30) ↗
  21. Wenda Li, Lei Yu, Yuhuai Wu, and Lawrence C. Paulson. Isarstep: a benchmark for high-level mathematical reasoning. In 9th International Conference on Learning Representations, ICLR 2021, Virtual Event, Austria, May 3-7, 2021. find
  22. OpenReview.net, 2021. URL https://openreview.net/ forum?id=Pzj6fzU6wkj. ↗
  23. Jia Meng and Lawrence C. Paulson. Translating higher-order clauses to first-order clauses. J. Autom. Reason., 40(1):35–60, 2008. doi: 10.1007/s10817-007-9085-y. URL https://doi.org/10. 1007/s10817-007-9085-y. — [doi:10.1007/s10817-007-9085-y](https://doi.org/10.1007/s10817-007-9085-y) find
  24. Olga Ohrimenko, Peter J Stuckey, and Michael Codish. Propagation via lazy clause generation. Constraints, 14(3):357–391, 2009. find
  25. Lawrence C. Paulson. Three years of experience with sledgehammer, a practical link between automatic and interactive theorem provers. In Renate A. Schmidt, Stephan Schulz, and Boris Konev, editors, Proceedings of the 2nd Workshop on Practical Aspects of Automated Reasoning, PAAR-2010, Edinburgh, Sco… find
  26. EasyChair, 2010. doi: 10.29007/tnfd. URL https://doi.org/10.29007/tnfd. ↗
  27. Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. CoRR, abs/2009.03393, 2020. URL https://arxiv.org/abs/2009.03393. ↗
  28. Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever. Formal mathematics statement curriculum learning. CoRR, abs/2202.01344, 2022. URL https://arxiv.org/abs/2202.01344. ↗
  29. Alec Radford, Jeffrey Wu, Rewon Child, David Luan, Dario Amodei, Ilya Sutskever, et al. Language models are unsupervised multitask learners. OpenAI blog, 1(8):9, 2019. find
  30. Peter Scholze. Liquid tensor experiment. Experimental Mathematics, 0(0):1–6, 2021. doi: 10.1080/ 10586458.2021.1926016. URL https://doi.org/10.1080/10586458.2021.1926016. — [doi:10.1080/10586458.2021.1926016](https://doi.org/10.1080/10586458.2021.1926016) ↗
  31. David Silver, Thomas Hubert, Julian Schrittwieser, Ioannis Antonoglou, Matthew Lai, Arthur Guez, Marc Lanctot, Laurent Sifre, Dharshan Kumaran, Thore Graepel, Timothy P. Lillicrap, Karen Simonyan, and Demis Hassabis. Mastering chess and shogi by self-play with a general reinforcement learning algori… — Mastering chess and shogi by self-play with a general reinforcement learning algorithm
  32. Yiannos Stathopoulos, Angeliki Koutsoukou-Argyraki, and LC Paulson. Serapis: A concept-oriented search engine for the isabelle libraries based on natural language. In Online proceedings of the Isabelle Workshop, 2020. find
  33. Jianlin Su, Yu Lu, Shengfeng Pan, Bo Wen, and Yunfeng Liu. Roformer: Enhanced transformer with rotary position embedding, 2021. URL https://arxiv.org/abs/2104.09864. ↗
  34. Geoff Sutcliffe and Yury Puzis. SRASS - A semantic relevance axiom selection system. In Frank Pfenning, editor, Automated Deduction - CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007, Proceedings, volume 4603 of Lecture Notes in Computer Science, pages… find
  35. Springer, 2007. doi: 10.1007/978-3-540-73595-3\\_20. URL https://doi.org/10.1007/978-3-540-73595-3_20. — [doi:10.1007/978-3-540-73595-3\\_20](https://doi.org/10.1007/978-3-540-73595-3_20) ↗
  36. Geoff Sutcliffe, Josef Urban, and Stephan Schulz, editors. Proceedings of the CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories, Bremen, Germany, 17th July 2007, volume 257 of CEUR Workshop Proceedings, 2007. CEUR-WS.org. URL http://ceur-ws.org/Vol-257. ↗
  37. Alfred Tarski. Truth and proof. Scientific American, 220(6):63–77, 1969. find
  38. Josef Urban. Malarea: a metasystem for automated reasoning in large theories. In ESARLT, 2007. find
  39. Josef Urban, Geoff Sutcliffe, Petr Pudlák, and Jirí Vyskocil. Malarea SG1- machine learner for automated reasoning with semantic guidance. In Alessandro Armando, Peter Baumgartner, and Gilles Dowek, editors, Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, Augu… find
  40. Springer, 2008. doi: 10.1007/978-3-540-71070-7\\_37. URL https://doi.org/10.1007/978-3-540-71070-7_37. — [doi:10.1007/978-3-540-71070-7\\_37](https://doi.org/10.1007/978-3-540-71070-7_37) ↗
  41. Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N. Gomez, Lukasz Kaiser, and Illia Polosukhin. Attention is all you need, 2017. URL https://arxiv.org/abs/ 1706.03762. ↗
  42. Ben Wang and Aran Komatsuzaki. GPT-J-6B: A 6 Billion Parameter Autoregressive Language Model. https://github.com/kingoflolz/mesh-transformer-jax, May 2021. ↗
  43. Mingzhe Wang, Yihe Tang, Jian Wang, and Jia Deng. Premise selection for theorem proving by deep graph embedding. Advances in neural information processing systems, 30, 2017. find
  44. Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. minif2f: a cross-system benchmark for formal olympiad-level mathematics. In International Conference on Learning Representations, 2022. URL https://openreview.net/forum?id=9ZPegFuFTFv. ↗

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/jiang-2022-thor-wielding-hammers-integrate-language/