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 this https URL and our data
at this https URL

通过提出一种新的流程，我们利用合成数据来将自然语言数学问题转化为 Lean 4 语句，并相应地进行过滤，从而为解决 LLMs 在理解复杂数学问题和证明上的性能提供有用的训练数据。最终数据集包含约 57K 个正式 - 非正式问题对以及来自数学竞赛论坛的搜索证明和 21 个新的 IMO 问题。