Elamur Research⌕
☰
home / papers / 2022 / NaturalProver: Grounded Mathematical Proof Generation with Language Models

NaturalProver: Grounded Mathematical Proof Generation with Language Models

Paper · 2022 · Sean Welleck, Jiacheng Liu, Ximing Lu et al.

Summary

The paper tackles theorem proving in informal mathematics, where proofs mix prose and LaTeX, a setting that modern generative models had barely explored. The authors define two generation tasks: proposing the next step of a partially written proof, and writing a complete proof. For this they build NaturalProofs-Gen from the ProofWiki-based NaturalProofs benchmark. Proofs are segmented into steps and annotated with mentions of theorems and definitions. Their system, NaturalProver, is a fine-tuned language model that takes the titles of relevant references in its input, either retrieved automatically or supplied by a human. It is also trained to rebuild each reference's content from its title. Optionally, a stepwise beam search favours candidate steps that cover the given references. University mathematics students judged the outputs and preferred NaturalProver over a fine-tuned GPT-3 baseline on both tasks. It proves some theorems that need short proofs, and over 40% of its next-step suggestions were rated correct and useful. The authors call this a first for neural LMs. Long proofs, valid justifications and multi-step symbolic derivations remain weak.

Key points

  • Dataset: NaturalProofs-Gen keeps the NaturalProofs splits of about 12.5k train, 1k validation and 1k test theorem–proof pairs. It adds core sets of 100 dev and 100 test theorems for human evaluation. Proofs cite a pool of roughly 33k theorems and definitions.
  • Training method: The model sees the theorem plus reference titles in its prompt. A joint loss combines proof generation with a reference reconstruction objective, which maps each title to its content.
  • Decoding: Stepwise beam search (and a Stepwise++ variant) samples candidate proof steps, using multiple temperatures in Stepwise++. It ranks them by a weighted mix of reference coverage and log-probability. The method needs only sampled text and its log-probability, so it works through APIs like GPT-3's.
  • Results: NaturalProver outperforms fine-tuned GPT-3 in human evaluation. It can fully prove some theorems requiring 2–6 steps, and more than 40% of its next-step suggestions were rated correct and useful.
  • Resources: The work appeared at NeurIPS 2022, and code and data are available at github.com/wellecks/naturalprover.

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 5The field of science this work belongs to (OpenAlex fields).Computer Science · 18,614 worksArtificial Intelligence · 17,965 worksArts and Humanities · 17,450 worksLanguage and Linguistics · 17,296 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 Sean Welleck, Jiacheng Liu, Ximing Lu, Hannaneh Hajishirzi and Yejin Choi. 2022. NaturalProver: Grounded Mathematical Proof Generation with Language Models. arXiv:2205.12910.

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

@misc{welleck2022naturalprover,
  title = {{NaturalProver: Grounded Mathematical Proof Generation with Language Models}},
  author = {Sean Welleck, Jiacheng Liu, Ximing Lu, Hannaneh Hajishirzi and Yejin Choi},
  year = {2022},
  doi = {10.48550/arxiv.2205.12910},
  eprint = {2205.12910},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2205.12910}
}

References

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

  1. P. Anderson, B. Fernando, M. Johnson, and S. Gould. Guided open vocabulary image captioning with constrained beam search. In Proceedings of the 2017 Conference on Empirical Methods in Natural Language Processing, pages 936–945, Copenhagen, Denmark, Sept. 2017. Association for Computational Linguisti…
  2. J. Austin, A. Odena, M. Nye, M. Bosma, H. Michalewski, D. Dohan, E. Jiang, C. Cai, M. Terry, Q. Le, and C. Sutton. Program synthesis with large language models, 2021.
  3. R. Bommasani, D. A. Hudson, E. Adeli, R. Altman, S. Arora, S. von Arx, M. S. Bernstein, J. Bohg, A. Bosselut, E. Brunskill, E. Brynjolfsson, S. Buch, D. Card, R. Castellon, N. S. Chatterji, A. S. Chen, K. Creel, J. Davis, D. Demszky, C. Donahue, M. Doumbouya, E. Durmus, S. Ermon, J. Etchemendy, K. E… — On the Opportunities and Risks of Foundation Models
  4. K. Bostrom, X. Zhao, S. Chaudhuri, and G. Durrett. Flexible generation of natural language deductions. In Proceedings of the 2021 Conference on Empirical Methods in Natural Language Processing, pages 6266–6278, Online and Punta Cana, Dominican Republic, Nov. 2021. Association for Computational Lingu… find
  5. T. B. Brown, B. Mann, N. Ryder, M. Subbiah, J. Kaplan, P. Dhariwal, A. Neelakantan, P. Shyam, G. Sastry, A. Askell, S. Agarwal, A. Herbert-Voss, G. Krueger, T. J. Henighan, R. Child, A. Ramesh, D. M. Ziegler, J. Wu, C. Winter, C. Hesse, M. Chen, E. Sigler, M. Litwin, S. Gray, B. Chess, J. Clark, C.… — Language Models are Few-Shot Learners
  6. M. Chen, J. Tworek, H. Jun, Q. Yuan, H. P. d. O. Pinto, J. Kaplan, H. Edwards, Y. Burda, N. Joseph, G. Brockman, et al. Evaluating large language models trained on code. arXiv preprint arXiv:2107.03374, 2021.
  7. K. Cobbe, V. Kosaraju, M. Bavarian, M. Chen, H. Jun, L. Kaiser, M. Plappert, J. Tworek, J. Hilton, R. Nakano, C. Hesse, and J. Schulman. Training verifiers to solve math word problems. arXiv preprint arXiv:2110.14168, 2021.
  8. B. Dalvi, P. Jansen, O. Tafjord, Z. Xie, H. Smith, L. Pipatanangkura, and P. Clark. Explaining answers with entailment trees. In Proceedings of the 2021 Conference on Empirical Methods in Natural Language Processing, pages 7358–7370, Online and Punta Cana, Dominican Republic, Nov. 2021. Association…
  9. B. Dalvi, O. Tafjord, and P. Clark. Towards teachable reasoning systems. ArXiv, abs/2204.13074, 2022. find
  10. Davis and Hersh. The mathematical experience. Birkhauser, 1981. find
  11. L. M. de Moura, S. Kong, J. Avigad, F. van Doorn, and J. von Raumer. The lean theorem prover (system description). In A. P. Felty and A. Middeldorp, editors, CADE, volume 9195 of Lecture Notes in Computer Science, pages 378–388. Springer, 2015. ISBN 978-3-319-21400-9. URL http://dblp.uni-trier.de/db… ↗
  12. M. de Villiers. The role and function of proof in Mathematics. Pythagoras, 1990. find
  13. E. Dinan, S. Roller, K. Shuster, A. Fan, M. Auli, and J. Weston. Wizard of wikipedia: Knowledge-powered conversational agents. In International Conference on Learning Representations, 2019. URL https://openreview.net/forum?id=r1l73iRqKm. ↗
  14. I. Drori, S. Zhang, R. Shuttleworth, L. Tang, A. Lu, E. Ke, K. Liu, L. Chen, S. Tran, N. Cheng, R. Wang, N. Singh, T. L. Patti, J. Lynch, A. Shporer, N. Verma, E. Wu, and G. Strang. A neural network solves, explains, and generates university math problems by program synthesis and few-shot learning a… — [arXiv:2112.15594](https://arxiv.org/abs/2112.15594) find
  15. B. S. Edwards and M. B. Ward. Surprises from mathematics education research: Student (mis)use of mathematical definitions. American Mathematical Monthly, 2004. ISSN 00029890. doi: 10.2307/4145268. — [doi:10.2307/4145268](https://doi.org/10.2307/4145268) find
  16. Erik G. Jensen. Thinking Like a Lawyer. In Thinking Like a Lawyer, chapter 2, "Forms. Stanford Law School, 2014. URL https://law.stanford.edu/wp-content/uploads/2018/ 04/ILEI-Forms-of-Legal-Reasoning-2014.pdf. ↗
  17. D. Ferreira and A. Freitas. Natural language premise selection: Finding supporting statements for mathematical text. In Proceedings of the 12th Language Resources and Evaluation Conference, pages 2175–2182, Marseille, France, May 2020a. European Language Resources Association. ISBN 979-10-95546-34-4… find
  18. D. Ferreira and A. Freitas. Premise selection in natural language mathematical texts. In Proceedings of the 58th Annual Meeting of the Association for Computational Linguistics, pages 7365–7374, Online, July 2020b. Association for Computational Linguistics. doi: 10.18653/v1/2020.acl-main. 657. URL h…
  19. L. Gao, S. Biderman, S. Black, L. Golding, T. Hoppe, C. Foster, J. Phang, H. He, A. Thite, N. Nabeshima, S. Presser, and C. Leahy. The Pile: An 800gb dataset of diverse text for language modeling. arXiv preprint arXiv:2101.00027, 2020. find
  20. J. M. Han, J. Rute, Y. Wu, E. W. Ayers, and S. Polu. Proof artifact co-training for theorem proving with language models, 2021a.
  21. J. M. Han, T. Xu, S. Polu, A. Neelakantan, and A. Radford. Contrastive finetuning of generative language models for informal premise selection. In AITP, 2021b. find
  22. D. Hendrycks, C. Burns, S. Kadavath, A. Arora, S. Basart, E. Tang, D. Song, and J. Steinhardt. Measuring mathematical problem solving with the math dataset, 2021.
  23. C. Hokamp and Q. Liu. Lexically constrained decoding for sequence generation using grid beam search. In Proceedings of the 55th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pages 1535–1546, Vancouver, Canada, July 2017. Association for Computational Lingui…
  24. D. H. Kaye. Penn State Law eLibrary Journal Articles Faculty Works 1992, Proof in Law and Science. Jurimetrics J, 32, 1992. URL http://elibrary.law.psu.edu/fac_works. ↗
  25. G. Lample and F. Charton. Deep learning for symbolic mathematics. In International Conference on Learning Representations, 2020. URL https://openreview.net/forum?id=S1eZYeHFDS. ↗
  26. Y. Li, D. Choi, J. Chung, N. Kushman, J. Schrittwieser, R. Leblond, T. Eccles, J. Keeling, F. Gimeno, A. D. Lago, et al. Competition-level code generation with alphacode. arXiv preprint arXiv:2203.07814, 2022.
  27. X. Lu, S. Welleck, P. West, L. Jiang, J. Kasai, D. Khashabi, R. L. Bras, L. Qin, Y. Yu, R. Zellers, N. A. Smith, and Y. Choi. Neurologic a*esque decoding: Constrained text generation with lookahead heuristics. ArXiv, abs/2112.08726, 2021a.
  28. X. Lu, P. West, R. Zellers, R. Le Bras, C. Bhagavatula, and Y. Choi. NeuroLogic decoding: (un)supervised neural text generation with predicate logic constraints. In Proceedings of the 2021 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Techn…
  29. A. Mutton, M. Dras, S. Wan, and R. Dale. Gleu: Automatic evaluation of sentence-level fluency. In Proceedings of the 45th Annual Meeting of the Association of Computational Linguistics, pages 344–351, 2007. find
  30. R. Nakano, J. Hilton, S. A. Balaji, J. Wu, L. Ouyang, C. Kim, C. Hesse, S. Jain, V. Kosaraju, W. Saunders, X. Jiang, K. Cobbe, T. Eloundou, G. Krueger, K. Button, M. Knight, B. Chess, and J. Schulman. Webgpt: Browser-assisted question-answering with human feedback. ArXiv, abs/2112.09332, 2021.
  31. M. Nye, A. J. Andreassen, G. Gur-Ari, H. Michalewski, J. Austin, D. Bieber, D. Dohan, A. Lewkowycz, M. Bosma, D. Luan, C. Sutton, and A. Odena. Show your work: Scratchpads for intermediate computation with language models. ArXiv, abs/2112.00114, 2021.
  32. S. Polu and I. Sutskever. Generative language modeling for automated theorem proving, 2020.
  33. S. Polu, J. M. Han, K. Zheng, M. Baksys, I. Babuschkin, and I. Sutskever. Formal mathematics statement curriculum learning, 2022.
  34. L. Qin, S. Welleck, D. Khashabi, and Y. Choi. Cold decoding: Energy-based constrained text generation with langevin dynamics. ArXiv, abs/2202.11705, 2022. — [arXiv:2202.11705](https://arxiv.org/abs/2202.11705) find
  35. A. Radford, J. Wu, R. Child, D. Luan, D. Amodei, and I. Sutskever. Language models are unsupervised multitask learners. arXiv, 2019. find
  36. S. Saha, S. Ghosh, S. Srivastava, and M. Bansal. PRover: Proof generation for interpretable reasoning over rules. In Proceedings of the 2020 Conference on Empirical Methods in Natural Language Processing (EMNLP), pages 122–136, Online, Nov. 2020. Association for Computational Linguistics. doi: 10.18…
  37. D. Saxton, E. Grefenstette, F. Hill, and P. Kohli. Analysing mathematical reasoning abilities of neural models. In International Conference on Learning Representations, 2019. URL https://openreview.net/forum?id=H1gR5iR5FX. ↗
  38. K. Shuster, S. Poff, M. Chen, D. Kiela, and J. Weston. Retrieval augmentation reduces hallucination in conversation. In Findings of the Association for Computational Linguistics: EMNLP 2021, pages 3784–3803, Punta Cana, Dominican Republic, Nov. 2021. Association for Computational Linguistics. doi: 1…
  39. C. Szegedy, editor. A Promising Path Towards Autoformalization and General Artificial Intelligence, 2020. find
  40. O. Tafjord, B. Dalvi, and P. Clark. ProofWriter: Generating implications, proofs, and abductive statements over natural language. In Findings of the Association for Computational Linguistics: ACL-IJCNLP 2021, pages 3621–3634, Online, Aug. 2021. Association for Computational Linguistics. doi: 10.1865…
  41. J. Urban and J. Jakubuv. First neural conjecturing datasets and experiments. In International Conference on Intelligent Computer Mathematics, pages 315–323. Springer, 2020. find
  42. J. F. Voss and M. L. Means. Learning to reason via instruction in argumentation. Learning and Instruction, 1991. ISSN 09594752. doi: 10.1016/0959-4752(91)90013-X. — [doi:10.1016/0959-4752(91)90013-x](https://doi.org/10.1016/0959-4752%2891%2990013-x) find
  43. Q. Wang, C. Brown, C. Kaliszyk, and J. Urban. Exploration of neural machine translation in autoformalization of mathematics in Mizar. In CPP 2020 - Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2020, 2020. doi: 10.1145/3372885.3373… find
  44. J. Wei, X. Wang, D. Schuurmans, M. Bosma, E. Chi, Q. Le, and D. Zhou. Chain of thought prompting elicits reasoning in large language models, 2022. — Chain-of-Thought Prompting Elicits Reasoning in Large Language Models
  45. S. Welleck, J. Liu, R. L. Bras, H. Hajishirzi, Y. Choi, and K. 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.net/ forum?id=Jvxa8adr3iY. ↗
  46. S. Welleck, P. West, J. Cao, and Y. Choi. Symbolic brittleness in sequence models: on systematic generalization in symbolic mathematics. AAAI, abs/2109.13986, 2022. — [arXiv:2109.13986](https://arxiv.org/abs/2109.13986) find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/welleck-2022-naturalprover-grounded-mathematical-proof-generation/