Saved in:
| Main Authors: | , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2406.03847 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866915349291597824 |
|---|---|
| author | Ying, Huaiyuan Wu, Zijian Geng, Yihan Yuan, Zheng Lin, Dahua Chen, Kai |
| author_facet | Ying, Huaiyuan Wu, Zijian Geng, Yihan Yuan, Zheng Lin, Dahua Chen, Kai |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2406_03847 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Lean Workbook: A large-scale Lean problem set formalized from natural language math problems Ying, Huaiyuan Wu, Zijian Geng, Yihan Yuan, Zheng Lin, Dahua Chen, Kai Computation and Language 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. |
| title | Lean Workbook: A large-scale Lean problem set formalized from natural language math problems |
| topic | Computation and Language |
| url | https://arxiv.org/abs/2406.03847 |