NaturalProofs: Mathematical Theorem Proving in Natural Language
arXiv:2104.01112
Abstract
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. Large-scale sequence models show promise compared to classical information retrieval methods, yet their performance and out-of-domain generalization leave substantial room for improvement. NaturalProofs opens many avenues for research on challenging mathematical tasks.
References in corpus (14)
- Leveraging Pre-trained Checkpoints for Sequence Generation Tasks
- Passage Re-ranking with BERT
- XTREME: A Massively Multilingual Multi-task Benchmark for Evaluating Cross-lingual Generalization
- Measuring Mathematical Problem Solving With the MATH Dataset
- DeepMath - Deep Sequence Models for Premise Selection
- The Dataset Nutrition Label: A Framework To Drive Higher Data Quality Standards
- GamePad: A Learning Environment for Theorem Proving
- Generative Language Modeling for Automated Theorem Proving
- Learning to Prove Theorems via Interacting with Proof Assistants
- Holophrasm: a neural Automated Theorem Prover for higher-order logic
- Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar
- HOList: An Environment for Machine Learning of Higher-Order Theorem Proving
- LIME: Learning Inductive Bias for Primitives of Mathematical Reasoning
- On proof and progress in mathematics