Lean Workbook: A large-scale Lean problem set formalized from natural language math problems

• URL: http://arxiv.org/abs/2406.03847v2
• Date: Fri, 7 Jun 2024 16:12:21 GMT
• Title: Lean Workbook: A large-scale Lean problem set formalized from natural language math problems
• Authors: Huaiyuan Ying, Zijian Wu, Yihan Geng, Jiayu Wang, Dahua Lin, Kai Chen,
• Abstract summary: Large language models are not good at math theorem proving using formal languages like Lean. A significant challenge in this area is the scarcity of training data available in these formal languages. We propose a novel pipeline that iteratively generates and filters synthetic data to translate natural language mathematical problems into Lean 4 statements.
• Score: 50.22847430754973
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• Abstract: Large language models have demonstrated impressive capabilities across various natural language processing tasks, especially in solving mathematical problems. However, large language models are not good at math theorem proving using formal languages like Lean. A significant challenge in this area is the scarcity of training data available in these formal languages. To address this issue, we propose a novel pipeline that iteratively generates and filters synthetic data to translate natural language mathematical problems into Lean 4 statements, and vice versa. Our results indicate that the synthetic data pipeline can provide useful training data and improve the performance of LLMs in translating and understanding complex mathematical problems and proofs. Our final dataset contains about 57K formal-informal question pairs along with searched proof from the math contest forum and 21 new IMO questions. We open-source our code at https://github.com/InternLM/InternLM-Math and our data at https://huggingface.co/datasets/InternLM/Lean-Workbook.

Related papers

• Herald: A Natural Language Annotated Lean 4 Dataset [15.42247133378869]
  This paper introduces a novel framework for translating the Mathlib4 corpus (a unified library of mathematics in formal language Lean 4) into natural language. We present the results of this pipeline on Mathlib4 as Herald (Hierarchy and Retrieval-based Translated Lean) We also propose the Herald Translator, which is fine-tuned on Herald.
  arXiv  Detail & Related papers  (2024-10-09T10:11:24Z)
• LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN prover [56.34998574538897]
  We propose LEAN-GitHub, a dataset consisting of large-scale formal data extracted from Lean 4 repositories on GitHub. Our model achieved accuracies of 48.8% with a single pass and 54.5% with 64 passes on the Lean 4 miniF2F test, surpassing state-of-the-art method at 52%.
  arXiv  Detail & Related papers  (2024-07-24T12:28:03Z)
• JiuZhang3.0: Efficiently Improving Mathematical Reasoning by Training Small Data Synthesis Models [110.45794710162241]
  Existing work either collects large-scale math-related texts for pre-training, or relies on stronger LLMs to synthesize massive math problems. We propose an efficient way that trains a small LLM for math problem synthesis, to efficiently generate sufficient high-quality pre-training data. We leverage it to synthesize 6 million math problems for pre-training our JiuZhang3.0 model, which only needs to invoke GPT-4 API 9.3k times and pre-train on 4.6B data.
  arXiv  Detail & Related papers  (2024-05-23T09:43:19Z)
• ChatGLM-Math: Improving Math Problem-Solving in Large Language Models with a Self-Critique Pipeline [42.61538071832468]
  Large language models (LLMs) have shown excellent mastering of human language, but still struggle in real-world applications that require mathematical problem-solving. We tailor the Self-Critique pipeline, which addresses the challenge in the feedback learning stage of LLM alignment.
  arXiv  Detail & Related papers  (2024-04-03T17:51:18Z)
• Can LLM Generate Culturally Relevant Commonsense QA Data? Case Study in Indonesian and Sundanese [14.463110500907492]
  Large Language Models (LLMs) are increasingly being used to generate synthetic data for training and evaluating models. It is unclear whether they can generate a good quality of question answering (QA) dataset that incorporates knowledge and cultural nuance embedded in a language. In this study, we investigate the effectiveness of using LLMs in generating culturally relevant commonsense QA datasets for Indonesian and Sundanese languages.
  arXiv  Detail & Related papers  (2024-02-27T08:24:32Z)
• MARIO: MAth Reasoning with code Interpreter Output -- A Reproducible Pipeline [12.186691561822256]
  We postulate that the inherent nature of large language models (LLMs) presents challenges in modeling mathematical reasoning. This paper introduces a novel math dataset, enhanced with a capability to utilize a Python code interpreter. We propose a tentative, easily replicable protocol for the fine-tuning of math-specific LLMs.
  arXiv  Detail & Related papers  (2024-01-16T08:08:01Z)
• MathCoder: Seamless Code Integration in LLMs for Enhanced Mathematical Reasoning [52.97768001837269]
  We present a method to fine-tune open-source language models, enabling them to use code for modeling and deriving math equations. We propose a method of generating novel and high-quality datasets with math problems and their code-based solutions. This approach yields the MathCoder models, a family of models capable of generating code-based solutions for solving challenging math problems.
  arXiv  Detail & Related papers  (2023-10-05T17:52:09Z)
• Simultaneous Machine Translation with Large Language Models [51.470478122113356]
  We investigate the possibility of applying Large Language Models to SimulMT tasks. We conducted experiments using the textttLlama2-7b-chat model on nine different languages from the MUST-C dataset. The results show that LLM outperforms dedicated MT models in terms of BLEU and LAAL metrics.
  arXiv  Detail & Related papers  (2023-09-13T04:06:47Z)
• PAL: Program-aided Language Models [112.94785609781503]
  We present Program-Aided Language models (PaL) to understand natural language problems. PaL offloads the solution step to a programmatic runtime such as a Python interpreter. We set new state-of-the-art results in all 12 benchmarks.
  arXiv  Detail & Related papers  (2022-11-18T18:56:13Z)

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.