Lean Workbook: A large-scale Lean problem set formalized from natural language math problems
Lean Workbook translates natural language math problems into Lean 4 statements using synthetic data, enhancing LLM performance with a dataset of 57K pairs.
Key Findings
Methodology
We propose a novel pipeline that iteratively generates and filters synthetic data to translate natural language mathematical problems into Lean 4 statements. This method involves using the Lean compiler and Natural Language Inference (NLI) to verify formalization validity, with human experts correcting invalid formalizations. The final dataset contains 57K question pairs and 21 new IMO problems.
Key Results
- The synthetic data pipeline produced 57K question pairs with a 93.5% accuracy rate upon manual review, demonstrating significant improvements in formalization accuracy.
- Compared to datasets like MiniF2F and Mathlib, this method excels in autoformalization and theorem proving.
- In automatic theorem proving, the Pass@1024 reached 8.6%, significantly outperforming MiniF2F.
Significance
This research provides substantial data support for autoformalization and automatic theorem proving, addressing the data scarcity issue in LLMs for mathematical theorem proving. By open-sourcing the code and dataset, it fosters further research and application in academia and industry.
Technical Contribution
The study introduces a new autoformalization pipeline that significantly improves the accuracy of formalized problems. By combining active learning and human correction, it addresses data scarcity and offers new possibilities for large-scale formalization.
Novelty
This is the first application of active learning in large-scale contest math problems, significantly improving formalization accuracy and efficiency compared to existing work.
Limitations
- The method struggles with certain complex math problems, particularly integer division and extremum problems.
- The model still makes errors in translating certain types of problems, requiring further optimization.
Future Work
Future research can apply this method to a broader range of math problems and explore ways to further enhance translation accuracy and efficiency.
AI Executive Summary
Mathematical theorem proving is at the heart of mathematical research, yet existing large language models struggle with formal language theorem proving due to a lack of sufficient training data. To address this, researchers have developed a novel pipeline that generates and filters synthetic data to translate natural language math problems into Lean 4 statements. This method leverages the Lean compiler and Natural Language Inference (NLI) to verify formalization validity, with human experts correcting invalid formalizations. The final dataset includes 57K question pairs and 21 new IMO problems.
Experimental results show that this method significantly improves formalization accuracy, with 93.5% of samples passing manual review. Compared to existing datasets, this method excels in autoformalization and theorem proving, achieving a Pass@1024 of 8.6%. Researchers have open-sourced the code and dataset to promote further research and application in the field of automatic theorem proving.
Despite significant progress, the method still struggles with certain complex math problems, particularly integer division and extremum problems. Future research can apply this method to a broader range of math problems and explore ways to further enhance translation accuracy and efficiency.
Deep Analysis
Background
Mathematical theorem proving is central to mathematical research, with recent advances in large language models significantly improving problem-solving capabilities. However, formal language theorem proving remains challenging due to insufficient training data. Existing datasets like MiniF2F and Mathlib provide some support but lack scale and diversity.
Core Problem
Large language models struggle with formal language theorem proving due to a lack of sufficient training data. Formalization requires complex mathematical reasoning and rich knowledge, but existing datasets are limited in scale and diversity.
Innovation
We propose a novel pipeline that generates and filters synthetic data to translate natural language math problems into Lean 4 statements. This method combines active learning and human correction to significantly improve formalization accuracy.
Methodology
- �� Collect natural language math problems
- �� Use model to translate into Lean 4 statements
- �� Verify formalization validity with Lean compiler and NLI
- �� Human experts correct invalid formalizations
- �� Iteratively generate and filter synthetic data
Experiments
The experimental design includes comparative testing with MiniF2F and Mathlib datasets, evaluating model performance in autoformalization and theorem proving. Key metrics include formalization accuracy and Pass@1024.
Results
Experimental results show that the synthetic data pipeline produced 57K question pairs with a 93.5% accuracy rate, achieving a Pass@1024 of 8.6%.
Applications
This method can be used for autoformalization and theorem proving, with significant applications in math competitions and higher education.
Limitations & Outlook
Despite significant progress, the method struggles with certain complex math problems, particularly integer division and extremum problems.
Plain Language Accessible to non-experts
Imagine you're cooking in a kitchen. You have a recipe (natural language problem), but you need to use specific tools (Lean 4 statements) to complete the dish. Our research acts like a smart assistant, helping you translate the recipe into a language the tools can understand. Through trial and error, we've found the best translation method to make your dish even tastier.
ELI14 Explained like you're 14
Hey there! Imagine you're playing a super complex math game. You need to translate the puzzles in the game (natural language problems) into the game rules (Lean 4 statements) to solve them. Our research is like a smart helper, translating puzzles into rules so you can win the game more easily! Isn't that cool?
Glossary
Lean 4
Lean 4 is a programming language for formalizing mathematical proofs, providing an open-source platform for correct and maintainable code verification.
Used in the paper to translate natural language problems into formal statements.
Natural Language Inference (NLI)
NLI is a technique used to determine the logical relationship between two natural language statements.
Used to verify if the formalized statement matches the original problem.
Active Learning
Active learning is a machine learning approach that improves model learning efficiency by selectively labeling data.
Used to iteratively generate and filter synthetic data.
Synthetic Data
Synthetic data is algorithmically generated data used for training and testing machine learning models.
Used to supplement training data for formalization problems.
Math Contest Forum
The Math Contest Forum is an online community that gathers various math contest problems and discussions.
Used to collect natural language math problems.
Open Questions Unanswered questions from this research
- 1 How to improve model translation accuracy on complex math problems? Current methods struggle with certain issues, requiring further research.
- 2 How to apply this method to a broader range of math problems? The applicability to different types of problems needs exploration.
Applications
Immediate Applications
Math Education
This method can be used in math education to help students better understand and solve complex math problems.
Long-term Vision
Automatic Theorem Proving
This method can be used for automatic theorem proving, advancing the automation of mathematical 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.