2021

NaturalProofs: Mathematical Theorem Proving in Natural Language

Welleck, Sean, Liu, Jiacheng, Bras, Ronan Le et al.

Understand

Understanding and creating mathematics using natural mathematical language - the mixture of symbolic and natural language used by humans - is a challenging and important problem for driving progress in machine learning.

As a step in this direction, we develop NaturalProofs, a multi-domain corpus of mathematical statements and their proofs, written in natural mathematical language.
NaturalProofs unifies broad coverage, deep coverage, and low-resource mathematical sources, allowing for evaluating both in-distribution and zero-shot generalization.
Using NaturalProofs, we benchmark strong neural methods on mathematical reference retrieval and generation tasks which test a system's ability to determine key results that appear in a proof.

Built on

On proof and progress in mathematics
W. P. Thurston · 1994
Earlier work this paper cites.
Mptp 0.2: Design, implementation, and initial experiments
J. Urban · 2006
Earlier work this paper cites.
The Princeton Companion to Mathematics
T. Gowers, J. Barrow-Green, and I. Leader · 2008
Earlier work this paper cites.
Lurch: a word processor that can grade students’ proofs
N. C. Carter and K. G. Monks · 2013
Earlier work this paper cites.
Zenodo, 2013
European Organization For Nuclear Research and OpenAIRE · 2013
Earlier work this paper cites.
The lean theorem prover (system description)
L. M. de Moura, S. Kong, J. Avigad, F. van Doorn, and J. von Raumer · 2015
Earlier work this paper cites.
Solving general arithmetic word problems
S. Roy and D. Roth · 2015
Earlier work this paper cites.
DeepMath - Deep sequence models for premise selection
A. A. Alemi, F. Chollet, N. Een, G. Irving, C. Szegedy, and J. Urban · 2016
Earlier work this paper cites.
Holophrasm: a neural automated theorem prover for higher-order logic, 2016
D. Whalen · 2016
Earlier work this paper cites.
Program induction by rationale generation: Learning to solve and explain algebraic word problems
W. Ling, D. Yogatama, C. Dyer, and P. Blunsom · 2017
Earlier work this paper cites.
The dataset nutrition label: A framework to drive higher data quality standards
Original
S. Holland, A. Hosny, S. Newman, J. Joseph, and K. Chmielinski · 2018
Earlier work this paper cites.
A broad-coverage challenge corpus for sentence understanding through inference
A. Williams, N. Nangia, and S. R. Bowman · 2018
Earlier work this paper cites.
MathQA: Towards interpretable math word problem solving with operation-based formalisms
A. Amini, S. Gabriel, S. Lin, R. Koncel-Kedziorski, Y. Choi, and H. Hajishirzi · 2019
Earlier work this paper cites.
Holist: An environment for machine learning of higher-order theorem proving
K. Bansal, S. Loos, M. Rabe, C. Szegedy, and S. Wilcox · 2019
Earlier work this paper cites.
BERT: Pre-training of deep bidirectional transformers for language understanding
J. Devlin, M.-W. Chang, K. Lee, and K. Toutanova · 2019
Earlier work this paper cites.
Gamepad: A learning environment for theorem proving
D. Huang, P. Dhariwal, D. Song, and I. Sutskever · 2019
Earlier work this paper cites.

Similar

Metamath: A Computer Language for Mathematical Proofs
N. D. Megill and D. A. Wheeler · 2019
Cited alongside, same era.
Language models are unsupervised multitask learners
A. Radford, J. Wu, R. Child, D. Luan, D. Amodei, and I. Sutskever · 2019
Cited alongside, same era.
Analysing mathematical reasoning abilities of neural models
D. Saxton, E. Grefenstette, F. Hill, and P. Kohli · 2019
Cited alongside, same era.
Learning to prove theorems via interacting with proof assistants
K. Yang and J. Deng · 2019
Cited alongside, same era.
Language Models are Few-Shot Learners
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, S. McCandlish, A. Radford, I. Sutskever, and D. Amodei · 2020
Cited alongside, same era.
Transformers as Soft Reasoners over Language
P. Clark, O. Tafjord, and K. Richardson · 2020
Cited alongside, same era.
Natural language premise selection: Finding supporting statements for mathematical text
D. Ferreira and A. Freitas · 2020
Cited alongside, same era.
Premise selection in natural language mathematical texts
D. Ferreira and A. Freitas · 2020
Cited alongside, same era.
Pretrained transformers improve out-of-distribution robustness, 2020
D. Hendrycks, X. Liu, E. Wallace, A. Dziedzic, R. Krishnan, and D. Song · 2020
Cited alongside, same era.
XTREME: A massively multilingual multi-task benchmark for evaluating cross-lingual generalisation
J. Hu, S. Ruder, A. Siddhant, G. Neubig, O. Firat, and M. Johnson · 2020
Cited alongside, same era.
Document-Level Definition Detection in Scholarly Documents: Existing Models, Error Analyses, and Future Directions
D. Kang, A. Head, R. Sidhu, K. Lo, D. Weld, and M. A. Hearst · 2020
Cited alongside, same era.
Dense passage retrieval for open-domain question answering
Original
V. Karpukhin, B. Oğuz, S. Min, L. Wu, S. Edunov, D. Chen, and W.-t. Yih · 2020
Cited alongside, same era.

Then

Language models as knowledge bases?
F. Petroni, T. Rocktäschel, P. Lewis, A. Bakhtin, Y. Wu, A. H. Miller, and S. Riedel · 2020
Later among the works it cites.
Generative language modeling for automated theorem proving, 2020
S. Polu and I. Sutskever · 2020
Later among the works it cites.
Exploring the limits of transfer learning with a unified text-to-text transformer
C. Raffel, N. Shazeer, A. Roberts, K. Lee, S. Narang, M. Matena, Y. Zhou, W. Li, and P. J. Liu · 2020
Later among the works it cites.
Leveraging pre-trained checkpoints for sequence generation tasks
S. Rothe, S. Narayan, and A. Severyn · 2020
Later among the works it cites.
A Promising Path Towards Autoformalization and General Artificial Intelligence , 2020
C. Szegedy, editor · 2020
Later among the works it cites.
Proofwriter: Generating implications, proofs, and abductive statements over natural language
Original
O. Tafjord, B. D. Mishra, and P. Clark · 2020
Later among the works it cites.
Learning to Prove Theorems by Learning to Generate Theorems
M. Wang and J. Deng · 2020
Later among the works it cites.
Exploration of neural machine translation in autoformalization of mathematics in Mizar
Q. Wang, C. Brown, C. Kaliszyk, and J. Urban · 2020
Later among the works it cites.
Transformers: State-of-the-art natural language processing
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 · 2020
Later among the works it cites.
Americasnli: Evaluating zero-shot natural language understanding of pretrained multilingual models in truly low-resource languages, 2021
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 · 2021
Closest in time.
Measuring mathematical problem solving with the math dataset, 2021
D. Hendrycks, C. Burns, S. Kadavath, A. Arora, S. Basart, E. Tang, D. Song, and J. Steinhardt · 2021
Closest in time.
Isarstep: a benchmark for high-level mathematical reasoning
W. Li, L. Yu, Y. Wu, and L. C. Paulson · 2021
Closest in time.
Mathematical reasoning via self-supervised skip-tree training
M. N. Rabe, D. Lee, K. Bansal, and C. Szegedy · 2021
Closest in time.
Beir: A heterogenous benchmark for zero-shot evaluation of information retrieval models
Original
N. Thakur, N. Reimers, A. Rücklé, A. Srivastava, and I. Gurevych · 2021
Closest in time.
Lime: Learning inductive bias for primitives of mathematical reasoning, 2021
Y. Wu, M. Rabe, W. Li, J. Ba, R. Grosse, and C. Szegedy · 2021
Closest in time.

Beyond the bibliography

alphaXiv searches the wider corpus for related work and actual follow-ups.

Open on alphaXiv

alphaXiv is searching for related work…

Reading the bibliography…