Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs

• URL: http://arxiv.org/abs/2301.02195v1
• Date: Thu, 5 Jan 2023 17:56:00 GMT
• Title: Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs
• Authors: Garett Cunningham, Razvan C. Bunescu, David Juedes
• Abstract summary: 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.
• Score: 5.045988012508899
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: The ever-growing complexity of mathematical proofs makes their manual verification by mathematicians very cognitively demanding. Autoformalization seeks to address this by translating proofs written in natural language into a formal representation that is computer-verifiable via interactive theorem provers. In this paper, 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. The same architecture is also trained to translate simple imperative code decorated with Hoare triples into formally verifiable proofs of correctness in Coq. Experiments on a limited domain of artificial and human-written proofs show that the models generalize well to intermediate lengths not seen during training and variations in natural language.

Related papers

• Training Neural Networks as Recognizers of Formal Languages [87.06906286950438]
  Formal language theory pertains specifically to recognizers. It is common to instead use proxy tasks that are similar in only an informal sense. We correct this mismatch by training and evaluating neural networks directly as binary classifiers of strings.
  arXiv  Detail & Related papers  (2024-11-11T16:33:25Z)
• Mathematical Formalized Problem Solving and Theorem Proving in Different Fields in Lean 4 [0.0]
  This paper explores the use of Large Language Models (LLMs) to generate formal proof steps and complete formalized proofs. The goal is to determine how AI can be leveraged to assist the mathematical formalization process and improve its performance.
  arXiv  Detail & Related papers  (2024-09-09T18:21:28Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  We present Lean-STaR, a framework for training language models to produce informal thoughts prior to each step of a proof. Lean-STaR achieves state-of-the-art results on the miniF2F-test benchmark within the Lean theorem proving environment.
  arXiv  Detail & Related papers  (2024-07-14T01:43:07Z)
• Autoformalizing Euclidean Geometry [74.72212706513318]
  We introduce a neuro-symbolic framework for autoformalizing Euclidean geometry. One challenge is that informal proofs rely on diagrams, leaving gaps in texts that are hard to formalize. We provide automatic semantic evaluation for autoformalized theorem statements.
  arXiv  Detail & Related papers  (2024-05-27T14:35:10Z)
• A New Approach Towards Autoformalization [7.275550401145199]
  Autoformalization is the task of translating natural language mathematics into a formal language that can be verified by a program. Research paper mathematics requires large amounts of background and context. We propose an avenue towards tackling autoformalization for research-level mathematics, by breaking the task into easier and more approachable subtasks.
  arXiv  Detail & Related papers  (2023-10-12T00:50:24Z)
• Trustworthy Formal Natural Language Specifications [3.8073142980733]
  This paper shows it is possible to build support for specifications written in expressive subsets of natural language. We implement a means to provide specifications in a modularly formal subset of English, and have them automatically translated into formal claims. We produce proof certificates explaining how each word was interpreted and how the sentence's structure was used to compute the meaning.
  arXiv  Detail & Related papers  (2023-10-05T20:41:47Z)
• ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics [7.607254619341369]
  We introduce ProofNet, a benchmark for autoformalization and formal proving of undergraduate-level mathematics. The ProofNet benchmarks consists of 371 examples, each consisting of a formal theorem statement in Lean 3. We report baseline results on statement autoformalization via in-context learning.
  arXiv  Detail & Related papers  (2023-02-24T03:28:46Z)
• Towards a Mathematics Formalisation Assistant using Large Language Models [5.485439959027125]
  We explore the abilities of a large language model (Codex) to help with formalisation in the Lean theorem prover. Codex is able to formalise short mathematical statements at undergrad level with nearly 75% accuracy for $120$ theorem statements. We show that with a new prompting strategy Codex can formalise these proofs in natural language with at least one out of twelve Codex completion being easy to repair into a complete proof.
  arXiv  Detail & Related papers  (2022-11-14T16:52:32Z)
• 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)
• NaturalProofs: Mathematical Theorem Proving in Natural Language [132.99913141409968]
  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.
  arXiv  Detail & Related papers  (2021-03-24T03:14:48Z)
• 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)

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.