Elamur Research⌕
☰
home / papers / 2021 / Proof Artifact Co-training for Theorem Proving with Language Models

Proof Artifact Co-training for Theorem Proving with Language Models

Paper · 2021 · Jesse Michael Han, Jason Rute, Yuhuai Wu et al.

Summary

Neural theorem provers for big formal libraries don't have much training data. Human-written proofs take a lot of work to produce, so large Transformer models overfit fast and stop improving as they get bigger. The authors propose PACT (Proof Artifact Co-Training) to get more data. Lean's kernel stores every proof as a low-level proof term. PACT walks through those terms and generates a large set of self-supervised tasks: predicting the next lemma, filling in masked subterms, classifying which premises and local hypotheses are used, and similar. A decoder-only Transformer is trained on these tasks together with the usual objective of predicting the next tactic from human proofs. They also release LeanStep, a set of datasets plus an environment for Lean 3 and mathlib that supports supervised training, proof-search evaluation and reinforcement learning. Co-training with PACT raises the share of held-out theorems the model proves from 32% to 48%, and combining it with WebMath pre-training works best. The approach also carries over to newly added mathlib theorems, and the proofs it found were merged into mathlib.

Key points

  • On held-out mathlib test theorems, the proof success rate rises from 32% (tactic data only) to 48% with PACT co-training.
  • LeanStep is described as the first tactic proof dataset for Lean. It pairs human tactic steps with kernel-level proof terms taken from Lean core and mathlib, which had over 46,000 lemmas at the time.
  • On several thousand theorems added to mathlib after the data was extracted, some of them using new definitions, the prover reaches 37%.
  • WebMath pre-training followed by PACT co-training gives the lowest validation loss and the highest proving rate. Fine-tuning on the full mix (mix1 + mix2 + tactic) took about 1.5K A100 GPU-hours.
  • Over a third of the proofs the model found are shorter than the human versions. This led to dozens of mathlib commits co-authored by GPT-f, with proof terms up to 12× smaller.

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🎓Carnegie Mellon UniversityPittsburgh · United States598 works · 191,226 citations🏢IBMArmonk · United States154 works · 72,606 citations🎓University of PittsburghPittsburgh · United States65 works · 23,401 citations🏢OpenAISan Francisco · United States23 works · 27,874 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 Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W. Ayers and Stanislas Polu. 2021. Proof Artifact Co-training for Theorem Proving with Language Models. arXiv:2102.06203.

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

@misc{han2021proof,
  title = {{Proof Artifact Co-training for Theorem Proving with Language Models}},
  author = {Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W. Ayers and Stanislas Polu},
  year = {2021},
  doi = {10.48550/arxiv.2102.06203},
  eprint = {2102.06203},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2102.06203}
}

References

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

  1. Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, and Christian Szegedy. Learning to reason in large theories without imitation. CoRR, abs/1905.10501, 2019a. URL http://arxiv.org/abs/ 1905.10501. ↗
  2. Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, Christian Szegedy, and Stewart Wilcox. Holist: An environment for machine learning of higher order logic theorem proving. In Kamalika Chaudhuri and Ruslan Salakhutdinov (eds.), Proceedings of the 36th International Conference on Machine Learning, ICML 2… — HOList: An Environment for Machine Learning of Higher-Order Theorem Proving
  3. PMLR, 2019b. URL http://proceedings.mlr.press/v97/bansal19a.html. ↗
  4. Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, Christian Szegedy, and Stewart Wilcox. Holist: An environment for machine learning of higher-order theorem proving (extended version). CoRR, abs/1904.03241, 2019c. URL http://arxiv.org/abs/1904.03241. ↗
  5. Lasse Blaauwbroek, Josef Urban, and Herman Geuvers. The tactician - A seamless, interactive tactic learner and prover for coq. In Christoph Benzmüller and Bruce R. Miller (eds.), Intelligent Computer Mathematics - 13th International Conference, CICM 2020, Bertinoro, Italy, July 26-31, 2020, Proceedi… find
  6. Springer, 2020. doi: 10.1007/978-3-030-53518-6\\_17. URL https://doi.org/10.1007/ 978-3-030-53518-6_17. — [doi:10.1007/978-3-030-53518-6\\_17](https://doi.org/10.1007/978-3-030-53518-6_17) find
  7. Tom B. Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, Sandhini Agarwal, Ariel Herbert-Voss, Gretchen Krueger, Tom Henighan, Rewon Child, Aditya Ramesh, Daniel M. Ziegler, Jeffrey Wu, Clemens Winter,… — Language Models are Few-Shot Learners
  8. Kevin Buzzard, Johan Commelin, and Patrick Massot. Formalising perfectoid spaces. In Jasmin Blanchette and Catalin Hritcu (eds.), Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020, pp. 299–312. find
  9. ACM, 2020. doi: 10.1145/3372885.3373830. URL https://doi.org/10.1145/3372885.3373830. ↗
  10. Kevin Buzzard, Chris Hughes, Kenny Lau, Amelia Livingston, Ramon Fernández Mir, and Scott Morrison. Schemes in lean. Experimental Mathematics, 0(0):1–9, 2021. doi: 10.1080/10586458. 2021.1983489. URL https://doi.org/10.1080/10586458.2021.1983489. — [doi:10.1080/10586458](https://doi.org/10.1080/10586458) ↗
  11. François Charton, Amaury Hayat, and Guillaume Lample. Learning advanced mathematical computations from examples. In 9th International Conference on Learning Representations, ICLR 2021, Virtual Event, Austria, May 3-7, 2021. find
  12. OpenReview.net, 2021. URL https://openreview.net/forum?id=-gfhS00XfKj. ↗
  13. Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The lean theorem prover (system description). In Amy P. Felty and Aart Middeldorp (eds.), Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7,… find
  14. Springer, 2015. doi: 10.1007/978-3-319-21401-6\\_26. URL https://doi.org/10.1007/978-3-319-21401-6_26. — [doi:10.1007/978-3-319-21401-6\\_26](https://doi.org/10.1007/978-3-319-21401-6_26) ↗
  15. Alexey Dosovitskiy, Lucas Beyer, Alexander Kolesnikov, Dirk Weissenborn, Xiaohua Zhai, Thomas Unterthiner, Mostafa Dehghani, Matthias Minderer, Georg Heigold, Sylvain Gelly, Jakob Uszkoreit, and Neil Houlsby. An image is worth 16x16 words: Transformers for image recognition at scale. In 9th Internat…
  16. OpenReview.net, 2021. URL https://openreview.net/forum?id= YicbFdNTTy. ↗
  17. Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, and Leonardo de Moura. A metapro-gramming framework for formal verification. Proc. ACM Program. Lang., 1(ICFP):34:1–34:29, 2017. doi: 10.1145/3110278. URL https://doi.org/10.1145/3110278. — [doi:10.1145/3110278](https://doi.org/10.1145/3110278) ↗
  18. M. Ganesalingam and W. T. Gowers. A fully automatic theorem prover with human-style output. J. Autom. Reason., 58(2):253–291, 2017. doi: 10.1007/s10817-016-9377-1. URL https://doi.org/10.1007/s10817-016-9377-1. — [doi:10.1007/s10817-016-9377-1](https://doi.org/10.1007/s10817-016-9377-1) ↗
  19. Thibault Gauthier and Cezary Kaliszyk. Sharing HOL4 and HOL light proof knowledge. In Martin Davis, Ansgar Fehnker, Annabelle McIver, and Andrei Voronkov (eds.), Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2… find
  20. Springer, 2015. doi: 10.1007/978-3-662-48899-7\\_26. URL https://doi.org/ 10.1007/978-3-662-48899-7_26. — [doi:10.1007/978-3-662-48899-7\\_26](https://doi.org/10.1007/978-3-662-48899-7_26) find
  21. Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, and Michael Norrish. Tactictoe: Learning to prove with tactics. J. Autom. Reason., 65(2):257–286, 2021. doi: 10.1007/ s10817-020-09580-x. URL https://doi.org/10.1007/s10817-020-09580-x. ↗
  22. Christopher Hahn, Frederik Schmitt, Jens U. Kreber, Markus Norman Rabe, and Bernd Finkbeiner. Teaching temporal logics to neural networks. In 9th International Conference on Learning Representations, ICLR 2021, Virtual Event, Austria, May 3-7, 2021. find
  23. OpenReview.net, 2021. URL https://openreview.net/forum?id=dOcQK-f4byz. ↗
  24. Jesse Michael Han and Floris van Doorn. A formal proof of the independence of the continuum hypothesis. In Jasmin Blanchette and Catalin Hritcu (eds.), Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020, p… find
  25. ACM, 2020. doi: 10.1145/3372885.3373826. URL https://doi.org/10.1145/3372885.3373826. — [doi:10.1145/3372885.3373826](https://doi.org/10.1145/3372885.3373826) ↗
  26. Tom Henighan, Jared Kaplan, Mor Katz, Mark Chen, Christopher Hesse, Jacob Jackson, Heewoo Jun, Tom B. Brown, Prafulla Dhariwal, Scott Gray, Chris Hallacy, Benjamin Mann, Alec Radford, Aditya Ramesh, Nick Ryder, Daniel M. Ziegler, John Schulman, Dario Amodei, and Sam McCandlish. Scaling laws for auto… — Scaling Laws for Autoregressive Generative Modeling
  27. Daniel Huang, Prafulla Dhariwal, Dawn Song, and Ilya Sutskever. Gamepad: A learning environment for theorem proving. In 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019. find
  28. OpenReview.net, 2019. URL https://openreview.net/forum?id=r1xwKoR9Y7. ↗
  29. Cezary Kaliszyk and Josef Urban. Mizar 40 for mizar 40. J. Autom. Reason., 55(3):245– 256, 2015a. doi: 10.1007/s10817-015-9330-8. URL https://doi.org/10.1007/ s10817-015-9330-8. find
  30. Cezary Kaliszyk and Josef Urban. Learning-assisted theorem proving with millions of lemmas. J. Symb. Comput., 69:109–128, 2015b. doi: 10.1016/j.jsc.2014.09.032. URL https://doi.org/ 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
  31. Cezary Kaliszyk, Josef Urban, and Jirí Vyskocil. Lemmatization for stronger reasoning in large theories. In Carsten Lutz and Silvio Ranise (eds.), Frontiers of Combining Systems - 10th International Symposium, FroCoS 2015, Wroclaw, Poland, September 21-24, 2015. Proceedings, volume 9322 of Lecture N… find
  32. Springer, 2015. doi: 10.1007/ 978-3-319-24246-0\\_21. URL https://doi.org/10.1007/978-3-319-24246-0_ 21. — [doi:10.1007/978-3-319-24246-0_](https://doi.org/10.1007/978-3-319-24246-0_) ↗
  33. Cezary Kaliszyk, François Chollet, and Christian Szegedy. Holstep: A machine learning dataset for higher-order logic theorem proving. In 5th International Conference on Learning Representations, ICLR 2017, Toulon, France, April 24-26, 2017, Conference Track Proceedings. find
  34. OpenReview.net, 2017. URL https://openreview.net/forum?id=ryuxYmvel. ↗
  35. Jared Kaplan, Sam McCandlish, Tom Henighan, Tom B. Brown, Benjamin Chess, Rewon Child, Scott Gray, Alec Radford, Jeffrey Wu, and Dario Amodei. Scaling laws for neural language models. CoRR, abs/2001.08361, 2020. URL https://arxiv.org/abs/2001.08361. ↗
  36. Guillaume Lample and François Charton. Deep learning for symbolic mathematics. In 8th International Conference on Learning Representations, ICLR 2020, Addis Ababa, Ethiopia, April 26-30, 2020.
  37. OpenReview.net, 2020. URL https://openreview.net/forum?id= S1eZYeHFDS. ↗
  38. Wenda Li, Lei Yu, Yuhuai Wu, and Lawrence C. Paulson. Isarstep: a benchmark for high-level mathematical reasoning. In International Conference on Learning Representations, 2021. URL https://openreview.net/forum?id=Pzj6fzU6wkj. mathlib. The lean mathematical library. In Jasmin Blanchette and Catalin… ↗
  39. ACM, 2020. doi: 10.1145/3372885. 3373824. URL https://doi.org/10.1145/3372885.3373824. — [doi:10.1145/3372885](https://doi.org/10.1145/3372885) ↗
  40. Pengyu Nie, Karl Palmskog, Junyi Jessy Li, and Milos Gligoric. Deep generation of coq lemma names using elaborated terms. In Nicolas Peltier and Viorica Sofronie-Stokkermans (eds.), Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Par… find
  41. Springer, 2020. doi: 10.1007/978-3-030-51054-1\\_6. URL https://doi.org/10.1007/ 978-3-030-51054-1_6. — [doi:10.1007/978-3-030-51054-1\\_6](https://doi.org/10.1007/978-3-030-51054-1_6) find
  42. Myle Ott, Sergey Edunov, Alexei Baevski, Angela Fan, Sam Gross, Nathan Ng, David Grangier, and Michael Auli. fairseq: A fast, extensible toolkit for sequence modeling. In Waleed Ammar, Annie Louis, and Nasrin Mostafazadeh (eds.), Proceedings of the 2019 Conference of the North American Chapter of th…
  43. Aditya Paliwal, Sarah M. Loos, Markus N. Rabe, Kshitij Bansal, and Christian Szegedy. Graph representations for higher-order logic and theorem proving. In The Thirty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2020, The Thirty-Second Innovative Applications of Artificial Intelligence Con… find
  44. AAAI Press, 2020. URL https://aaai.org/ojs/index.php/AAAI/article/view/5689. ↗
  45. Frank Pfenning and Christine Paulin-Mohring. Inductively defined types in the calculus of constructions. In Michael G. Main, Austin Melton, Michael W. Mislove, and David A. Schmidt (eds.), Mathematical Foundations of Programming Semantics, 5th International Conference, Tulane University, New Orleans… find
  46. Springer, 1989. doi: 10.1007/BFb0040259. URL https://doi.org/10.1007/BFb0040259. — [doi:10.1007/bfb0040259](https://doi.org/10.1007/bfb0040259) ↗
  47. Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. CoRR, abs/2009.03393, 2020. URL https://arxiv.org/abs/2009.03393. ↗
  48. Markus Norman Rabe, Dennis Lee, Kshitij Bansal, and Christian Szegedy. Mathematical reasoning via self-supervised skip-tree training. In 9th International Conference on Learning Representations, ICLR 2021, Virtual Event, Austria, May 3-7, 2021. find
  49. OpenReview.net, 2021. URL https://openreview.net/forum?id=YmqAnY0CMEy. ↗
  50. Alec Radford, Jong Wook Kim, Chris Hallacy, Aditya Ramesh, Gabriel Goh, Sandhini Agarwal, Girish Sastry, Amanda Askell, Pamela Mishkin, Jack Clark, Gretchen Krueger, and Ilya Sutskever. Learning transferable visual models from natural language supervision. In Marina Meila and Tong Zhang (eds.), Proc…
  51. PMLR, 2021. URL http://proceedings.mlr.press/v139/ radford21a.html. ↗
  52. Alex Sanchez-Stern, Yousef Alhessi, Lawrence K. Saul, and Sorin Lerner. Generating correctness proofs with neural networks. In Koushik Sen and Mayur Naik (eds.), Proceedings of the 4th ACM SIGPLAN International Workshop on Machine Learning and Programming Languages, MAPL@PLDI 2020, London, UK, June… find
  53. ACM, 2020. doi: 10.1145/3394450. 3397466. URL https://doi.org/10.1145/3394450.3397466. — [doi:10.1145/3394450](https://doi.org/10.1145/3394450) ↗
  54. Peter Scholze. Liquid tensor experiment. https://xenaproject.wordpress.com/ 2020/12/05/liquid-tensor-experiment/, 2020. Formalization available at https://github.com/leanprover-community/lean-liquid. ↗
  55. Josef Urban and Jan Jakubuv. First neural conjecturing datasets and experiments. In Christoph Benzmüller and Bruce R. Miller (eds.), Intelligent Computer Mathematics - 13th International Conference, CICM 2020, Bertinoro, Italy, July 26-31, 2020, Proceedings, volume 12236 of Lecture Notes in Computer… find
  56. Springer, 2020. doi: 10.1007/978-3-030-53518-6\\_24. URL https://doi.org/10.1007/978-3-030-53518-6_24. — [doi:10.1007/978-3-030-53518-6\\_24](https://doi.org/10.1007/978-3-030-53518-6_24) ↗
  57. Mingzhe Wang and Jia Deng. Learning to prove theorems by learning to generate theorems. In Hugo Larochelle, Marc’Aurelio Ranzato, Raia Hadsell, Maria-Florina Balcan, and Hsuan-Tien Lin (eds.), Advances in Neural Information Processing Systems 33: Annual Conference on Neural Information Processing Sy… find
  58. Qingxiang Wang, Cezary Kaliszyk, and Josef Urban. First experiments with neural translation of informal to formal mathematics. In Florian Rabe, William M. Farmer, Grant O. Passmore, and Abdou Youssef (eds.), Intelligent Computer Mathematics - 11th International Conference, CICM 2018, Hagenberg, Aust… find
  59. Springer, 2018. doi: 10.1007/978-3-319-96812-4\\_22. URL https://doi.org/10.1007/978-3-319-96812-4_22. — [doi:10.1007/978-3-319-96812-4\\_22](https://doi.org/10.1007/978-3-319-96812-4_22) ↗
  60. Qingxiang Wang, Chad E. Brown, Cezary Kaliszyk, and Josef Urban. Exploration of neural machine translation in autoformalization of mathematics in mizar. In Jasmin Blanchette and Catalin Hritcu (eds.), Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2… find
  61. ACM, 2020. doi: 10.1145/3372885.3373827. URL https://doi.org/10.1145/3372885.3373827. ↗
  62. Daniel Whalen. Holophrasm: a neural automated theorem prover for higher-order logic. CoRR, abs/1608.02644, 2016. URL http://arxiv.org/abs/1608.02644. ↗
  63. Freek Wiedijk. The De Bruijn factor, 2000. URL http://www.cs.ru.nl/F.Wiedijk/ factor/factor.pdf. ↗
  64. Minchao Wu, Michael Norrish, Christian Walder, and Amir Dezfouli. Tacticzero: Learning to prove theorems from scratch with deep reinforcement learning. In A. Beygelzimer, Y. Dauphin, P. Liang, and J. Wortman Vaughan (eds.), Advances in Neural Information Processing Systems, 2021a. URL https://openre… find
  65. Yuhuai Wu, Markus N. Rabe, Wenda Li, Jimmy Ba, Roger B. Grosse, and Christian Szegedy. LIME: learning inductive bias for primitives of mathematical reasoning. In Marina Meila and Tong Zhang (eds.), Proceedings of the 38th International Conference on Machine Learning, ICML 2021, 18-24 July 2021, Virt… find
  66. PMLR, 2021b. URL http://proceedings.mlr.press/v139/wu21c.html. ↗
  67. Kaiyu Yang and Jia Deng. Learning to prove theorems via interacting with proof assistants. In Kamalika Chaudhuri and Ruslan Salakhutdinov (eds.), Proceedings of the 36th International Conference on Machine Learning, ICML 2019, 9-15 June 2019, Long Beach, California, USA, volume 97 of Proceedings of…
  68. PMLR, 2019. URL http://proceedings.mlr.press/v97/yang19a.html. ↗

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/han-2021-proof-artifact-co-training-theorem/