ATG: Benchmarking Automated Theorem Generation for Generative Language Models

• URL: http://arxiv.org/abs/2405.06677v1
• Date: Sun, 5 May 2024 02:06:37 GMT
• Title: ATG: Benchmarking Automated Theorem Generation for Generative Language Models
• Authors: Xiaohan Lin, Qingxing Cao, Yinya Huang, Zhicheng Yang, Zhengying Liu, Zhenguo Li, Xiaodan Liang,
• Abstract summary: Humans can develop new theorems to explore broader and more complex mathematical results. Current generative language models (LMs) have achieved significant improvement in automatically proving theorems. This paper proposes an Automated Theorem Generation benchmark that evaluates whether an agent can automatically generate valuable (and possibly brand new) theorems.
• Score: 83.93978859348313
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Humans can develop new theorems to explore broader and more complex mathematical results. While current generative language models (LMs) have achieved significant improvement in automatically proving theorems, their ability to generate new or reusable theorems is still under-explored. Without the new theorems, current LMs struggle to prove harder theorems that are distant from the given hypotheses with the exponentially growing search space. Therefore, this paper proposes an Automated Theorem Generation (ATG) benchmark that evaluates whether an agent can automatically generate valuable (and possibly brand new) theorems that are applicable for downstream theorem proving as reusable knowledge. Specifically, we construct the ATG benchmark by splitting the Metamath library into three sets: axioms, library, and problem based on their proving depth. We conduct extensive experiments to investigate whether current LMs can generate theorems in the library and benefit the problem theorems proving. The results demonstrate that high-quality ATG data facilitates models' performances on downstream ATP. However, there is still room for current LMs to develop better ATG and generate more advanced and human-like theorems. We hope the new ATG challenge can shed some light on advanced complex theorem proving.

Related papers

• REFACTOR: Learning to Extract Theorems from Proofs [29.44286369265644]
  We show that REFACTOR can extract 19.6% of the theorems that humans would use to write the proofs. With newly extracted theorems, we show that the existing MetaMath database can beed. We also demonstrate that the prover trained on the new-theoremed dataset proves more test theorems and outperforms state-of-the-art baselines.
  arXiv  Detail & Related papers  (2024-02-26T21:21:30Z)
• TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models [68.65075559137608]
  We propose TRIGO, an ATP benchmark that not only requires a model to reduce a trigonometric expression with step-by-step proofs but also evaluates a generative LM's reasoning ability on formulas. We gather trigonometric expressions and their reduced forms from the web, annotate the simplification process manually, and translate it into the Lean formal language system. We develop an automatic generator based on Lean-Gym to create dataset splits of varying difficulties and distributions in order to thoroughly analyze the model's generalization ability.
  arXiv  Detail & Related papers  (2023-10-16T08:42:39Z)
• LEGO-Prover: Neural Theorem Proving with Growing Libraries [86.1191481712352]
  We present LEGO-Prover, which employs a growing skill library containing verified lemmas as skills to augment the capability of LLMs used in theorem proving. By constructing the proof modularly, LEGO-Prover enables LLMs to utilize existing skills retrieved from the library and to create new skills during the proving process. Our ablation study indicates that these newly added skills are indeed helpful for proving theorems, resulting in an improvement from a success rate of 47.1% to 50.4%.
  arXiv  Detail & Related papers  (2023-10-01T12:47:59Z)
• TheoremQA: A Theorem-driven Question Answering dataset [100.39878559382694]
  GPT-4's capabilities to solve these problems are unparalleled, achieving an accuracy of 51% with Program-of-Thoughts Prompting. TheoremQA is curated by domain experts containing 800 high-quality questions covering 350 theorems.
  arXiv  Detail & Related papers  (2023-05-21T17:51:35Z)
• 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)
• Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
  We learn a neural generator that automatically synthesizes theorems and proofs for the purpose of training a theorem prover. Experiments on real-world tasks demonstrate that synthetic data from our approach improves the theorem prover.
  arXiv  Detail & Related papers  (2020-02-17T16:06:02Z)

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.