https://arxiv.org/abs/2205.12910

close this message
arXiv smileybones icon

Giving Week!

Show your support for Open Science by donating to arXiv during Giving
Week, April 25th-29th.

DONATE
Skip to main content
Cornell University
We gratefully acknowledge support from
the Simons Foundation and member institutions.
 
arxiv logo > cs > arXiv:2205.12910
[                    ]

Help | Advanced Search

[All fields        ]
Search
arXiv logo
Cornell University Logo
[                    ] GO
quick links

  * Login
  * Help Pages
  * About

Computer Science > Computation and Language

arXiv:2205.12910 (cs)
[Submitted on 25 May 2022]

Title:NaturalProver: Grounded Mathematical Proof Generation with
Language Models

Authors:Sean Welleck, Jiacheng Liu, Ximing Lu, Hannaneh Hajishirzi,
Yejin Choi
Download PDF

    Abstract: Theorem proving in natural mathematical language - the
    mixture of symbolic and natural language used by humans - plays a
    central role in mathematical advances and education, and tests
    aspects of reasoning that are core to intelligence. Yet it has
    remained underexplored with modern generative models. We study
    large-scale language models on two new generation tasks:
    suggesting the next step in a mathematical proof, and full proof
    generation. Naively applying language models to these problems
    yields proofs riddled with hallucinations and logical
    incoherence. We develop NaturalProver, a language model that
    generates proofs by conditioning on background references (e.g.
    theorems and definitions that are either retrieved or
    human-provided), and optionally enforces their presence with
    constrained decoding. On theorems from the NaturalProofs
    benchmark, NaturalProver improves the quality of next-step
    suggestions and generated proofs over fine-tuned GPT-3, according
    to human evaluations from university-level mathematics students.
    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, which is to
    our knowledge the first demonstration of these capabilities using
    neural language models.

Subjects: Computation and Language (cs.CL); Artificial Intelligence
          (cs.AI)
Cite as:  arXiv:2205.12910 [cs.CL]
          (or arXiv:2205.12910v1 [cs.CL] for this version)
          https://doi.org/10.48550/arXiv.2205.12910
          Focus to learn more
          arXiv-issued DOI via DataCite

Submission history

From: Jiacheng Liu [view email]
[v1] Wed, 25 May 2022 17:01:18 UTC (9,713 KB)
Full-text links:

Download:

  * PDF
  * Other formats

[by-4]
Current browse context:
cs.CL
< prev   |   next >
new | recent | 2205
Change to browse by:
cs
cs.AI

References & Citations

  * NASA ADS
  * Google Scholar
  * Semantic Scholar

a export bibtex citation Loading...

Bibtex formatted citation

x
[loading...          ]
Data provided by:

Bookmark

BibSonomy logo Mendeley logo Reddit logo ScienceWISE logo
(*) Bibliographic Tools

Bibliographic and Citation Tools

[ ] Bibliographic Explorer Toggle
Bibliographic Explorer (What is the Explorer?)
[ ] Litmaps Toggle
Litmaps (What is Litmaps?)
[ ] scite.ai Toggle
scite Smart Citations (What are Smart Citations?)
( ) Code & Data

Code and Data Associated with this Article

[ ] arXiv Links to Code Toggle
arXiv Links to Code & Data (What is Links to Code & Data?)
( ) Demos

Demos

[ ] Replicate Toggle
Replicate (What is Replicate?)
( ) Related Papers

Recommenders and Search Tools

[ ] Connected Papers Toggle
Connected Papers (What is Connected Papers?)
[ ] Core recommender toggle
CORE Recommender (What is CORE?)
( ) About arXivLabs

arXivLabs: experimental projects with community collaborators

arXivLabs is a framework that allows collaborators to develop and
share new arXiv features directly on our website.

Both individuals and organizations that work with arXivLabs have
embraced and accepted our values of openness, community, excellence,
and user data privacy. arXiv is committed to these values and only
works with partners that adhere to them.

Have an idea for a project that will add value for arXiv's community?
Learn more about arXivLabs and how to get involved.

Which authors of this paper are endorsers? | Disable MathJax (What is
MathJax?)

  * About
  * Help

  * Click here to contact arXiv Contact
  * Click here to subscribe Subscribe

  * Copyright
  * Privacy Policy

  * Web Accessibility Assistance
  * arXiv Operational Status
    Get status notifications via email or slack