Elamur Research
☰
home / papers / 2022 / Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs

Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs

Written for the Research library (claude-opus-5-5) from the paper text. Original — arxiv.org/pdf/2210.12283v3

Summary

Formal proofs that a proof assistant can check are expensive to write, so there is little training data for neural provers. Informal mathematics written in natural language and LaTeX is plentiful, but no one has used it to guide a formal prover. The authors propose Draft, Sketch, and Prove (DSP), a pipeline with three stages. First, an informal proof is obtained, either written by a human or generated by Minerva. Second, a large language model (Codex), prompted with a few examples, turns that proof into an Isabelle "proof sketch": the high-level steps become intermediate conjectures, and the low-level justifications are left open. Third, an off-the-shelf automated prover fills in each open gap. The authors evaluate DSP on miniF2F, using a new set of informal statements and proofs they curated and aligned with its formal problems. DSP nearly doubles the share of competition problems the automated prover can close. This matters because it shows that informal human or model-written reasoning can steer formal search, and every final result is still checked by the kernel.

Key points

  • On the miniF2F test set, the automated-prover baseline solves 20.9% of problems. DSP raises this to 38.9% with Minerva-drafted proofs and to 39.3% with human-written proofs.
  • Resource: the authors release informal statements and human proofs that are manually aligned with the formal miniF2F statements in Isabelle.
  • Earlier neural provers use small models (<1B parameters) with heavy search. DSP instead makes few calls to very large few-shot models (up to 175B parameters).
  • To help the model map informal steps to formal ones, the sketch examples in the prompt carry informal proof fragments as comments next to each formal step.
  • Three ablations show that each part helps: drafting informal proofs, annotating sketches with informal fragments, and using automated provers to close the open conjectures. The sketches can also fix small errors in Minerva's reasoning, for example by starting induction from n = 0.

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: Mathematics & statistics

Cited by

150 papers of our library cite it (of the 140673 whose bibliographies we read); 14 of them have a page here, 136 not yet.

Cite

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

@misc{jiang2022draft,
  title = {{Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs}},
  author = {Jiang, Albert Q. and Welleck, Sean and Zhou, Jin Peng and Li, Wenda and Liu, Jiacheng and Jamnik, Mateja and Lacroix, Timothée and Wu, Yuhuai and Lample, Guillaume},
  year = {2022},
  doi = {10.48550/arxiv.2210.12283},
  eprint = {2210.12283},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2210.12283}
}

References

46 references, 9 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… find
  3. PMLR, 2019b. URL http://proceedings. mlr.press/v97/bansal19a.html. find
  4. Bruno Barras, Samuel Boutin, Cristina Cornes, Judicaël Courant, Jean-Christophe Filliatre, Eduardo Gimenez, Hugo Herbelin, Gerard Huet, Cesar Munoz, Chetan Murthy, et al. The Coq proof assistant reference manual: Version 6.1. PhD thesis, Inria, 1997. find
  5. 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,… find
  6. Nicholas Carlini, Daphne Ippolito, Matthew Jagielski, Katherine Lee, Florian Tramèr, and Chiyuan Zhang. Quantifying memorization across neural language models. CoRR, abs/2202.07646, 2022. URL https://arxiv.org/abs/2202.07646. ↗
  7. Mark Chen, Jerry Tworek, Heewoo Jun, Qiming Yuan, Henrique Ponde, Jared Kaplan, Harrison Edwards, Yura Burda, Nicholas Joseph, Greg Brockman, Alex Ray, Raul Puri, Gretchen Krueger, Michael Petrov, Heidy Khlaaf, Girish Sastry, Pamela Mishkin, Brooke Chan, Scott Gray, Nick Ryder, Mikhail Pavlov, Aleth… find our card
  8. Aakanksha Chowdhery, Sharan Narang, Jacob Devlin, Maarten Bosma, Gaurav Mishra, Adam Roberts, Paul Barham, Hyung Won Chung, Charles Sutton, Sebastian Gehrmann, Parker Schuh, Kensen Shi, Sasha Tsvyashchenko, Joshua Maynez, Abhishek Rao, Parker Barnes, Yi Tay, Noam Shazeer, Vinodkumar Prabhakaran, Emi… find
  9. Jia Deng, Wei Dong, Richard Socher, Li-Jia Li, Kai Li, and Li Fei-Fei. Imagenet: A large-scale hierarchical image database. In 2009 IEEE conference on computer vision and pattern recognition, pp. 248–255. find
  10. Iddo Drori, Sarah Zhang, Reece Shuttleworth, Leonard Tang, Albert Lu, Elizabeth Ke, Kevin Liu, Linda Chen, Sunny Tran, Newman Cheng, et al. A neural network solves, explains, and generates university math problems by program synthesis and few-shot learning at human level. Proceedings of the National… find
  11. Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, and Michael Norrish. Tactictoe: learning to prove with tactics. Journal of Automated Reasoning, 65(2):257–286, 2021. 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. In The Tenth International Conference on Learning Representations, ICLR 2022, Virtual Event, April 25-29, 2022. find
  13. OpenReview.net, 2022. URL https://openreview.net/forum?id=rpxJc9j04U. ↗
  14. Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. Measuring mathematical problem solving with the math dataset. NeurIPS, 2021. find our card
  15. Ari Holtzman, Jan Buys, Li Du, Maxwell Forbes, and Yejin Choi. The curious case of neural text degeneration. arXiv preprint arXiv:1904.09751, 2019. find
  16. Albert Q. Jiang, Wenda Li, Jesse Michael Han, and Yuhuai Wu. LISA: Language models of Isabelle proofs. In 6th Conference on Artificial Intelligence and Theorem Proving, 2021. find
  17. Albert Q. Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzygózdz, Piotr Milos, Yuhuai Wu, and Mateja Jamnik. Thor: Wielding hammers to integrate language models and automated theorem provers. CoRR, abs/2205.10893, 2022. doi: 10.48550/arXiv.2205.10893. URL https://doi.org/10.48550/… find
  18. Guillaume Lample and François Charton. Deep learning for symbolic mathematics. In International Conference on Learning Representations, 2020. URL https://openreview.net/forum? id=S1eZYeHFDS. ↗
  19. Guillaume Lample, Marie-Anne Lachaux, Thibaut Lavril, Xavier Martinet, Amaury Hayat, Gabriel Ebner, Aurélien Rodriguez, and Timothée Lacroix. Hypertree proof search for neural theorem proving. CoRR, abs/2205.11491, 2022. doi: 10.48550/arXiv.2205.11491. URL https://doi. org/10.48550/arXiv.2205.1149… find our card
  20. Aitor Lewkowycz, Anders Andreassen, David Dohan, Ethan Dyer, Henryk Michalewski, Vinay V. Ramasesh, Ambrose Slone, Cem Anil, Imanol Schlag, Theo Gutman-Solo, Yuhuai Wu, Behnam Neyshabur, Guy Gur-Ari, and Vedant Misra. Solving quantitative reasoning problems with language models. CoRR, abs/2206.14858… find our card
  21. Yujia Li, David H. Choi, Junyoung Chung, Nate Kushman, Julian Schrittwieser, Rémi Leblond, Tom Eccles, James Keeling, Felix Gimeno, Agustin Dal Lago, Thomas Hubert, Peter Choy, Cyprien de Masson d’Autume, Igor Babuschkin, Xinyun Chen, Po-Sen Huang, Johannes Welbl, Sven Gowal, Alexey Cherepanov, Jam… find our card
  22. Norman D. Megill and David A. Wheeler. Metamath: A Computer Language for Mathematical Proofs. Lulu Press, Morrisville, North Carolina, 2019. http://us.metamath.org/downloads/metamath.pdf. ↗
  23. Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The lean theorem prover (system description). In International Conference on Automated Deduction, pp. 378–388. Springer, 2015. find
  24. Lawrence C. Paulson. Isabelle - A Generic Theorem Prover (with a contribution by T. Nipkow), volume 828 of Lecture Notes in Computer Science. Springer, 1994. ISBN 3-540-58244-4. doi: 10.1007/BFb0030541. URL https://doi.org/10.1007/BFb0030541. — [doi:10.1007/bfb0030541](https://doi.org/10.1007/bfb0030541) ↗
  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 (eds.), Proceedings of the 2nd Workshop on Practical Aspects of Automated Reasoning, PAAR-2010, Edinburgh, Scotl… 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. ↗ our card
  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. ↗ our card
  29. David Silver, Thomas Hubert, Julian Schrittwieser, Ioannis Antonoglou, Matthew Lai, Arthur Guez, Marc Lanctot, Laurent Sifre, Dharshan Kumaran, Thore Graepel, et al. A general reinforcement learning algorithm that masters chess, shogi, and go through self-play. Science, 362(6419): 1140–1144, 2018. find
  30. Ilya Sutskever, Oriol Vinyals, and Quoc V Le. Sequence to sequence learning with neural networks. Advances in neural information processing systems, 27, 2014. find
  31. Donald Syme. DECLARE: A prototype declarative proof system for higher order logic. Citeseer, 1997. find
  32. Christian Szegedy. A promising path towards autoformalization and general artificial intelligence. 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 Lectur… find
  33. Springer, 2020. doi: 10.1007/978-3-030-53518-6\\ 1. URL https://doi.org/10.1007/978-3-030-53518-6\_1. — [doi:10.1007/978-3-030-53518-6\](https://doi.org/10.1007/978-3-030-53518-6\) ↗
  34. Trieu H. Trinh and Quoc V. Le. A simple method for commonsense reasoning. CoRR, abs/1806.02847, 2018. URL http://arxiv.org/abs/1806.02847. ↗
  35. 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
  36. ACM, 2020. doi: 10.1145/3372885.3373827. URL https://doi.org/10.1145/3372885.3373827. ↗
  37. Sean Welleck, Jiacheng Liu, Ronan Le Bras, Hannaneh Hajishirzi, Yejin Choi, and Kyunghyun Cho. Naturalproofs: Mathematical theorem proving in natural language. In Thirty-fifth Conference on Neural Information Processing Systems Datasets and Benchmarks Track (Round 1), 2021. URL https://openreview.ne… ↗
  38. Sean Welleck, Jiacheng Liu, Ximing Lu, Hannaneh Hajishirzi, and Yejin Choi. Naturalprover: Grounded mathematical proof generation with language models. CoRR, abs/2205.12910, 2022. doi: 10.48550/arXiv.2205.12910. URL https://doi.org/10.48550/arXiv.2205.12910. ↗
  39. Freek Wiedijk. Formal proof sketches. In Stefano Berardi, Mario Coppo, and Ferruccio Damiani (eds.), Types for Proofs and Programs, International Workshop, TYPES 2003, Torino, Italy, April 30 - May 4, 2003, Revised Selected Papers, volume 3085 of Lecture Notes in Computer Science, pp. 378–393. find
  40. Springer, 2003. doi: 10.1007/978-3-540-24849-1\\ 24. URL https: //doi.org/10.1007/978-3-540-24849-1\_24. — [doi:10.1007/978-3-540-24849-1\](https://doi.org/10.1007/978-3-540-24849-1\) find
  41. Freek Wiedijk. Formal proof – getting started. Notices of the American Mathematical Society, 55: 1408–1414, 2008. find
  42. Yuhuai Wu, Albert Jiang, Jimmy Ba, and Roger Baker Grosse. INT: An inequality benchmark for evaluating generalization in theorem proving. In International Conference on Learning Representations, 2021. URL https://openreview.net/forum?id=O6LPudowNQm. ↗
  43. Yuhuai Wu, Albert Q. Jiang, Wenda Li, Markus N. Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models. CoRR, abs/2205.12615, 2022. doi: 10.48550/arXiv.2205.12615. URL https://doi.org/10.48550/arXiv.2205.12615. ↗ our card
  44. Kaiyu Yang and Jia Deng. Learning to prove theorems via interacting with proof assistants. In International Conference on Machine Learning (ICML), 2019. find
  45. Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. miniF2F: a cross-system benchmark for formal olympiad-level mathematics. In The Tenth International Conference on Learning Representations, ICLR 2022, Virtual Event, April 25-29, 2022. find our card
  46. OpenReview.net, 2022. URL https://openreview.net/forum?id=9ZPegFuFTFv. ↗