NaturalProofs: Mathematical Theorem Proving in Natural Language
- URL: http://arxiv.org/abs/2104.01112v2
- Date: Mon, 7 Jun 2021 21:58:06 GMT
- Title: NaturalProofs: Mathematical Theorem Proving in Natural Language
- Authors: Sean Welleck, Jiacheng Liu, Ronan Le Bras, Hannaneh Hajishirzi, Yejin
Choi, Kyunghyun Cho
- Abstract summary: We develop NaturalProofs, a multi-domain corpus of mathematical statements and their proofs.
NaturalProofs unifies broad coverage, deep coverage, and low-resource mathematical sources.
We benchmark strong neural methods on mathematical reference retrieval and generation tasks.
- Score: 132.99913141409968
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- 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.
Related papers
- Tree-Based Representation and Generation of Natural and Mathematical
Language [77.34726150561087]
Mathematical language in scientific communications and educational scenarios is important yet relatively understudied.
Recent works on mathematical language focus either on representing stand-alone mathematical expressions, or mathematical reasoning in pre-trained natural language models.
We propose a series of modifications to existing language models to jointly represent and generate text and math.
arXiv Detail & Related papers (2023-02-15T22:38:34Z) - Towards Autoformalization of Mathematics and Code Correctness:
Experiments with Elementary Proofs [5.045988012508899]
Autoformalization seeks to address this by translating proofs written in natural language into a formal representation that is computer-verifiable via interactive theorem provers.
We introduce a semantic parsing approach, based on the Universal Transformer architecture, that translates elementary mathematical proofs into an equivalent formalization in the language of the Coq interactive theorem prover.
arXiv Detail & Related papers (2023-01-05T17:56:00Z) - A Survey of Deep Learning for Mathematical Reasoning [71.88150173381153]
We review the key tasks, datasets, and methods at the intersection of mathematical reasoning and deep learning over the past decade.
Recent advances in large-scale neural language models have opened up new benchmarks and opportunities to use deep learning for mathematical reasoning.
arXiv Detail & Related papers (2022-12-20T18:46:16Z) - UniGeo: Unifying Geometry Logical Reasoning via Reformulating
Mathematical Expression [127.68780714438103]
Two main geometry problems: calculation and proving, are usually treated as two specific tasks.
We construct a large-scale Unified Geometry problem benchmark, UniGeo, which contains 4,998 calculation problems and 9,543 proving problems.
We also present a unified multi-task Geometric Transformer framework, Geoformer, to tackle calculation and proving problems simultaneously.
arXiv Detail & Related papers (2022-12-06T04:37:51Z) - NaturalProver: Grounded Mathematical Proof Generation with Language
Models [84.2064569475095]
Theorem proving in natural mathematical language plays a central role in mathematical advances and education.
We develop NaturalProver, a language model that generates proofs by conditioning on background references.
NaturalProver is capable of proving some theorems that require short (2-6 step) proofs, and providing next-step suggestions that are rated as correct and useful over 40% of the time.
arXiv Detail & Related papers (2022-05-25T17:01:18Z) - Learning to Match Mathematical Statements with Proofs [37.38969121408295]
The task is designed to improve the processing of research-level mathematical texts.
We release a dataset for the task, consisting of over 180k statement-proof pairs.
We show that considering the assignment problem globally and using weighted bipartite matching algorithms helps a lot in tackling the task.
arXiv Detail & Related papers (2021-02-03T15:38:54Z) - Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
This work is motivated by the possibility that a major limitation of automated theorem provers compared to humans might be addressable via generation from language models.
We present an automated prover and proof assistant, GPT-f, for the Metamath formalization language, and analyze its performance.
arXiv Detail & Related papers (2020-09-07T19:50:10Z) - Natural Language Premise Selection: Finding Supporting Statements for
Mathematical Text [3.42658286826597]
We propose a new NLP task, the natural premise selection, which is used to retrieve supporting definitions and supporting propositions.
We also make available a dataset, NL-PS, which can be used to evaluate different approaches for the natural premise selection task.
arXiv Detail & Related papers (2020-04-30T17:08:03Z)
This list is automatically generated from the titles and abstracts of the papers in this site.
This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.