Elamur Research⌕
☰
home / papers / 2021 / NaturalProofs: Mathematical Theorem Proving in Natural Language

NaturalProofs: Mathematical Theorem Proving in Natural Language

Paper · 2021 · Sean Welleck, Jiacheng Liu, Ronan Le Bras et al.

Summary

Most machine-learning work on theorem proving targets formal systems such as Lean, Mizar or Metamath. It largely ignores the informal mathematics people actually write, where LaTeX formulas sit inside ordinary prose. NaturalProofs fills this gap with a corpus of theorems, definitions and proofs drawn from three kinds of sources: community-written ProofWiki for breadth, the Stacks project on algebraic geometry for depth, and two open textbooks (real analysis and number theory) as a low-resource setting. All sources share one schema, and the citation links between statements form a reference graph.

The authors define two tasks on this corpus. The first is retrieving the theorems, lemmas and definitions cited in a theorem's proof, which resembles premise selection. The second is generating the ordered sequence of those citations. They compare TF-IDF with BERT-based pairwise, joint and autoregressive models. Neural models clearly outperform classical retrieval on in-domain data but lose that advantage on unseen sources. Generation rarely recovers complete reference lists. The resource matters because it supports both in-distribution and zero-shot evaluation on authentic, human-written mathematics.

Key points

  • Corpus size: about 32k theorems with proofs, 14k definitions and 2k other pages such as axioms and corollaries. ProofWiki contributes 19,734 theorems and Stacks 12,479. The textbooks are Trench's Introduction to Real Analysis and Stein's Elementary Number Theory.
  • Data pipeline: ProofWiki data comes from its XML dump, filtered by hand-written rules. Stacks and textbook statements are extracted from LaTeX environments. Code and data are released at github.com/wellecks/naturalproofs.
  • Reference generation: the autoregressive model reproduces the exact reference sequence only about 3% of the time. An oracle that gets half of each sequence right would raise ProofWiki BLEU 4 from 5.48 to 25.88.
  • Ablations on initialization and training (pairwise and autoregressive retrieval, mAP):
    • Language pretraining without NaturalProofs finetuning yields near-zero mAP, and so does training from scratch.
    • Combining both reaches 16.99 on ProofWiki and 21.21 on Stacks.
    • The joint model initialized from the pairwise one scores best (37.51 on ProofWiki).
  • Title vs. content ablation: on ProofWiki, using titles only gives better results than titles plus content (BERT 24.48 vs 16.99 mAP). This suggests models still struggle to exploit the symbolic content.

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

🎓University of WashingtonSeattle · United States402 works · 212,763 citations

 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 1Research subjects and languages the work is about.Reasoning · 1,685 works

Cite

Cite as Sean Welleck, Jiacheng Liu, Ronan Le Bras, Hannaneh Hajishirzi, Yejin Choi and Kyunghyun Cho. 2021. NaturalProofs: Mathematical Theorem Proving in Natural Language. arXiv:2104.01112.

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

@misc{welleck2021naturalproofs,
  title = {{NaturalProofs: Mathematical Theorem Proving in Natural Language}},
  author = {Sean Welleck, Jiacheng Liu, Ronan {Le Bras}, Hannaneh Hajishirzi, Yejin Choi and Kyunghyun Cho},
  year = {2021},
  doi = {10.48550/arxiv.2104.01112},
  eprint = {2104.01112},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2104.01112}
}

References

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

  1. A. A. Alemi, F. Chollet, N. Een, G. Irving, C. Szegedy, and J. Urban. DeepMath - Deep sequence models for premise selection. In Advances in Neural Information Processing Systems, pages 2243–2251, 2016.
  2. A. Amini, S. Gabriel, S. Lin, R. Koncel-Kedziorski, Y. Choi, and H. Hajishirzi. MathQA: Towards interpretable math word problem solving with operation-based formalisms. In NAACL HLT 2019 - 2019 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language…
  3. K. Bansal, S. Loos, M. Rabe, C. Szegedy, and S. Wilcox. Holist: An environment for machine learning of higher-order theorem proving. In 36th International Conference on Machine Learning, ICML 2019, volume 2019-June, 2019.
  4. T. Brown, B. Mann, N. Ryder, M. Subbiah, J. D. Kaplan, P. Dhariwal, A. Neelakantan, P. Shyam, G. Sastry, A. Askell, S. Agarwal, A. Herbert-Voss, G. Krueger, T. Henighan, R. Child, A. Ramesh, D. Ziegler, J. Wu, C. Winter, C. Hesse, M. Chen, E. Sigler, M. Litwin, S. Gray, B. Chess, J. Clark, C. Berner… — Language Models are Few-Shot Learners
  5. N. C. Carter and K. G. Monks. Lurch: a word processor that can grade students’ proofs. In C. Lange, D. Aspinall, J. Carette, J. H. Davenport, A. Kohlhase, M. Kohlhase, P. Libbrecht, P. Quaresma, F. Rabe, P. Sojka, I. Whiteside, and W. Windsteiger, editors, Joint Proceedings of the MathUI, OpenMath,… find
  6. P. Clark, O. Tafjord, and K. Richardson. Transformers as Soft Reasoners over Language. In C. Bessiere, editor, Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence, IJCAI-20, pages 3882–3890. International Joint Conferences on Artificial Intelligence Organization…
  7. 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… ↗
  8. J. Devlin, M.-W. Chang, K. Lee, and K. Toutanova. BERT: Pre-training of deep bidirectional transformers for language understanding. In Proceedings of the 2019 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies, Volume 1 (Long and Sh…
  9. A. Ebrahimi, M. Mager, A. Oncevay, V. Chaudhary, L. Chiruzzo, A. Fan, J. Ortega, R. Ramos, A. Rios, I. Vladimir, G. A. Giménez-Lugo, E. Mager, G. Neubig, A. Palmer, R. A. C. Solano, N. T. Vu, and K. Kann. Americasnli: Evaluating zero-shot natural language understanding of pretrained multilingual mod… — AmericasNLI: Evaluating Zero-shot Natural Language Understanding of Pretrained Multilingual Models in Truly Low-resource Languages
  10. European Organization For Nuclear Research and OpenAIRE. Zenodo, 2013. URL https://www.zenodo.org/. ↗
  11. 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 2020. European Language Resources Association. ISBN 979-10-95546-34-4.… find
  12. 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 2020. Association for Computational Linguistics. doi: 10.18653/v1/2020.acl-main.657. URL htt…
  13. T. Gowers, J. Barrow-Green, and I. Leader. The Princeton Companion to Mathematics. Princeton University Press, USA, illustrated edition edition, 2008. ISBN 0691118809. find
  14. D. Hendrycks, X. Liu, E. Wallace, A. Dziedzic, R. Krishnan, and D. Song. Pretrained transformers improve out-of-distribution robustness, 2020.
  15. 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.
  16. S. Holland, A. Hosny, S. Newman, J. Joseph, and K. Chmielinski. The dataset nutrition label: A framework to drive higher data quality standards. arXiv preprint arXiv:1805.03677, 2018. find
  17. J. Hu, S. Ruder, A. Siddhant, G. Neubig, O. Firat, and M. Johnson. XTREME: A massively multilingual multi-task benchmark for evaluating cross-lingual generalisation. In H. D. III and A. Singh, editors, Proceedings of the 37th International Conference on Machine Learning, volume 119 of Proceedings of… find
  18. D. Huang, P. Dhariwal, D. Song, and I. Sutskever. Gamepad: A learning environment for theorem proving. In International Conference on Learning Representations, 2019. URL https://openreview.net/forum?id=r1xwKoR9Y7. ↗
  19. D. Kang, A. Head, R. Sidhu, K. Lo, D. Weld, and M. A. Hearst. Document-Level Definition Detection in Scholarly Documents: Existing Models, Error Analyses, and Future Directions. In Proceedings of the First Workshop on Scholarly Document Processing, pages 196–206, Online, Nov. 2020. Association for C… find
  20. V. Karpukhin, B. Oğuz, S. Min, L. Wu, S. Edunov, D. Chen, and W.-t. Yih. Dense passage retrieval for open-domain question answering. arXiv preprint arXiv:2004.04906, 2020.
  21. G. Lample and F. Charton. Deep learning for symbolic mathematics. In International Conference on Learning Representations, 2020. URL https://openreview.net/forum?id=S1eZYeHFDS. ↗
  22. R. Le Bras, S. Swayamdipta, C. Bhagavatula, R. Zellers, M. E. Peters, A. Sabharwal, and Y. Choi. Adversarial filters of dataset biases, 2020. ISSN 23318422. find
  23. W. Li, L. Yu, Y. Wu, and L. C. Paulson. Isarstep: a benchmark for high-level mathematical reasoning. In International Conference on Learning Representations, 2021. URL https://openreview.net/forum?id=Pzj6fzU6wkj. ↗
  24. W. Ling, D. Yogatama, C. Dyer, and P. Blunsom. Program induction by rationale generation: Learning to solve and explain algebraic word problems. In ACL 2017 - 55th Annual Meeting of the Association for Computational Linguistics, Proceedings of the Conference (Long Papers), volume 1, 2017. doi: 10.18… find
  25. N. D. Megill and D. A. Wheeler. Metamath: for Mathematical Proofs. Lulu Press, Morrisville, http://us.metamath.org/downloads/metamath.pdf. ↗
  26. R. Nogueira and K. Cho. Passage re-ranking with bert, 2020.
  27. C. Nogueira dos Santos, X. Ma, R. Nallapati, Z. Huang, and B. Xiang. Beyond [CLS] through ranking by generation. In Proceedings of the 2020 Conference on Empirical Methods in Natural Language Processing (EMNLP), pages 1722–1727, Online, Nov. 2020. Association for Computational Linguistics. doi: 10.1… find
  28. F. Petroni, T. Rocktäschel, P. Lewis, A. Bakhtin, Y. Wu, A. H. Miller, and S. Riedel. Language models as knowledge bases? In EMNLP-IJCNLP 2019 - 2019 Conference on Empirical Methods in Natural Language Processing and 9th International Joint Conference on Natural Language Processing, Proceedings of t…
  29. S. Polu and I. Sutskever. Generative language modeling for automated theorem proving, 2020.
  30. M. N. Rabe, D. Lee, K. Bansal, and C. Szegedy. Mathematical reasoning via self-supervised skip-tree training. In International Conference on Learning Representations, 2021. URL https://openreview.net/forum?id=YmqAnY0CMEy. ↗
  31. A. Radford, J. Wu, R. Child, D. Luan, D. Amodei, and I. Sutskever. Language models are unsupervised multitask learners. 2019. find
  32. C. Raffel, N. Shazeer, A. Roberts, K. Lee, S. Narang, M. Matena, Y. Zhou, W. Li, and P. J. Liu. Exploring the limits of transfer learning with a unified text-to-text transformer. Journal of Machine Learning Research, 21(140):1–67, 2020. URL http://jmlr.org/papers/v21/20-074.html. ↗
  33. S. Rothe, S. Narayan, and A. Severyn. Leveraging pre-trained checkpoints for sequence generation tasks. Transactions of the Association for Computational Linguistics, 8:264–280, 2020. doi: 10.1162/tacl_a_00313. URL https://www.aclweb.org/anthology/2020.tacl-1.18. ↗
  34. S. Roy and D. Roth. Solving general arithmetic word problems. In Conference Proceedings - EMNLP 2015: Conference on Empirical Methods in Natural Language Processing, 2015. doi: 10.18653/v1/d15-1202.
  35. 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. ↗
  36. C. Szegedy, editor. A Promising Path Towards Autoformalization and General Artificial Intelligence, 2020. find
  37. O. Tafjord, B. D. Mishra, and P. Clark. Proofwriter: Generating implications, proofs, and abductive statements over natural language. ArXiv, abs/2012.13048, 2020.
  38. N. Thakur, N. Reimers, A. Rücklé, A. Srivastava, and I. Gurevych. Beir: A heterogenous benchmark for zero-shot evaluation of information retrieval models. arXiv preprint arXiv:2104.08663, 4 2021. URL https://arxiv.org/abs/2104.08663. ↗
  39. W. P. Thurston. On proof and progress in mathematics. arXiv:math/9404236, Mar. 1994. URL http://arxiv.org/abs/math/9404236. arXiv: math/9404236. — [arXiv:math/9404236](https://arxiv.org/abs/math/9404236) ↗
  40. J. Urban. Mptp 0.2: Design, implementation, and initial experiments. J. Autom. Reason., 37 (1–2):21–43, Aug. 2006. ISSN 0168-7433. doi: 10.1007/s10817-006-9032-3. URL https://doi.org/10.1007/s10817-006-9032-3. — [doi:10.1007/s10817-006-9032-3](https://doi.org/10.1007/s10817-006-9032-3) ↗
  41. M. Wang and J. Deng. Learning to Prove Theorems by Learning to Generate Theorems. In H. Larochelle, M. Ranzato, R. Hadsell, M. F. Balcan, and H. Lin, editors, Advances in Neural Information Processing Systems, volume 33, pages 18146–18157. Curran Associates, Inc., 2020. URL https://proceedings.neuri… ↗
  42. 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
  43. D. Whalen. Holophrasm: a neural automated theorem prover for higher-order logic, 2016. find
  44. A. Williams, N. Nangia, and S. R. Bowman. A broad-coverage challenge corpus for sentence understanding through inference. In NAACL HLT 2018 - 2018 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies - Proceedings of the Conference, 2…
  45. T. Wolf, L. Debut, V. Sanh, J. Chaumond, C. Delangue, A. Moi, P. Cistac, T. Rault, R. Louf, M. Funtowicz, J. Davison, S. Shleifer, P. von Platen, C. Ma, Y. Jernite, J. Plu, C. Xu, T. L. Scao, S. Gugger, M. Drame, Q. Lhoest, and A. M. Rush. Transformers: State-of-the-art natural language processing.…
  46. Y. Wu, M. Rabe, W. Li, J. Ba, R. Grosse, and C. Szegedy. Lime: Learning inductive bias for primitives of mathematical reasoning, 2021. find
  47. K. Yang and J. Deng. Learning to prove theorems via interacting with proof assistants. In 36th International Conference on Machine Learning, ICML 2019, volume 2019-June, 2019.

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/welleck-2021-naturalproofs-mathematical-theorem-proving-natural/