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

TL;DR

This paper introduces a pipeline for generating synthetic data to improve large language models' ability to translate and understand formal mathematical problems in Lean 4, addressing data scarcity issues.

Contribution

It presents a novel iterative data generation and filtering pipeline that creates a large dataset of formal-informal math problem pairs for training LLMs.

Findings

Synthetic data improves LLM performance in formal language translation.

The dataset includes 57K question pairs and 21 new IMO questions.

Open-source code and data facilitate further research.

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.