Lean4数据集的建设
摘要 大型语言模型在各种自然语言处理任务中展示了令人印象深刻的能力，尤其是在解决数学问题方面。然而，大型语言模型在使用形式化语言（如Lean）进行数学定理证明方面表现不佳。这一领域的一个重大挑战是缺乏可用的形式化语言训练数据。为了解决这个问题，我们提出了一种新颖的管道方法，通过迭代生成和过滤合成数据，将自然语言数学问题翻译成Lean 4语句，反之亦然。我们的结果表明，这种合成数据管道可以提供有用的训练数据，并提高LLM在翻译和理解复杂数学问题和证明方面的表现。我们的最终数据集包含大约57K的形式化-非形式化问题对以及从数学竞赛论坛和21个新IMO问题中搜索到的证明。我们在https://github.com/InternLM/InternLM-Math 开源了我们的代码，并在https://huggingface.co/datasets/InternLM/Lean-Workbook 开源了我们的数据。
1 引言 证明定理是数学的最基本目标之一，这需要复杂的数学推理和丰富的数学知识。最近，大型语言模型（LLM）在通过链式推理（cot）解决小学（gsm8k）和甚至高中数学问题（MATH）方面取得了很大进展。LLM还可以与证明助理（如Lean、Coq或Isabelle）互动来证明定理。然而，LLM在定理证明方面的表现并不令人满意。
这一弱点的一个原因是数据稀缺。LLM学习定理证明的主流方法是通过专家迭代。LLM在给定的数学问题和语句集（如MiniF2F和Mathlib）中搜索证明，并从其成功轨迹中学习。然而，由于形式化问题需要人类专家的巨大劳动，MiniF2F中的数据量有限。尽管Mathlib是一个包含不同数学学科的形式化的大型数据集，但它主要证明的是基础数学定理，而不是竞赛级别的问题。因此，迈向更好自动定理证明模型的初步步骤是创建足够高质量的形式化语句。
在这项工作中，我们提出了Lean Workbook：一个迭代自动形式化管道，以及一个大规模的Lean问题集。我们基于主动学习训练我们的自动形式化模型。在每一轮中，我们使用模型将自然语言问题翻译成形式化语句，并将从数学竞赛论坛收集到的自然语言问题回译成形式化语句。我们使用Lean编译器和自然语言推理（NLI）来检查它是否是有效的形式化语句。我们抽样无效的形式化语句，并要求人类专家将其修改为有效的形式化语句，并将其添加到训练集中。通过补充人工标注的数据对，翻译模型逐渐学会在Lean 4形式语言和不同类型问题的自然语言之间进行翻译。
在最终轮次中，我们自动形式化了57K数学问题。人工检查报告Lean Workbook的随机样本准确率为93.5%。相同的过滤过程生成了21个新的IMO问题的形式化语句，这些问题未出现在Compfiles中。
总之，我们的贡献可以总结如下：
- 我们提出了一个主动学习管道，用于自动形式化自然语言问题。
- 我们开源了我们的翻译模型和管道，可用于自动形式化各种数学语句。
- 我们开源了一个包含57K形式化数学问题的数据集（其中5K有形式化解答），可用于自动形式化和自动定理证明。
- 我们形式化了21个未出现在Compfiles中的新的IMO问题。
参见图例 图1：我们的Lean Workbook管道的数据贡献。三轮过滤将大大确保输出数据的准确性。通过将管道分别应用于AOPS和Compfiles数据源，我们得出21个形式化的IMO问题和约57K用于自动形式化的合成训练数据。
2 预备知识 形式化证明涉及用编程语言精确表达的数学术语来建立声明。Lean 4是最新版本的Lean定理证明器，旨在提供一个开源平台，用于正确和可维护的代码进行形式验证。Lean语言可以声明一个定理并通过策略证明它，或者假装用“sorry”完成证明。如果证明完成，Lean 4将返回“无目标”信号。
Mathlib是一个由用户维护的Lean 4库。在Mathlib的帮助下，我们可以利用他人之前形式化的定理或函数来陈述我们的定理和证明过程。因此，在以下段落中，我们默认谈论在其环境中应用Mathlib和MiniF2F。
我们的工作重点是问题的翻译而不是证明。因此，我们将总是使用“sorry”来完成证明。一个典型的Lean 4语句如下所示。‘theorem’声明了这个命题的类型，接着是定理名称。然后它指定了所有变量及其类型，以及用括号分隔的几个条件。最后，结论从冒号开始，”:= by sorry”完成证明。以下是一个示例：
theorem ex_1 (n p : ℕ) (hp: Nat.Prime p) (h₁ : p \mid n) : { (x, y) : ℕ × ℕ | x + y = n ∧ Nat.gcd x y = p }.Finite := by sorry
3 相关工作 3.1 自动形式化 自动形式化是指将自然语言数学语句或证明翻译成形式化语言。之前的工作已经自动形式化了不同级别的数学，包括小学级别、高中竞赛级别和本科级别数学，利用上下文学习或微调LLM。我们的工作重点是大规模形式化高中竞赛级别的数学问题。类似且同步的工作是DeepSeek-prover，它将高中问题大规模翻译成Lean问题集。与DeepSeek-prover相比，我们应用了主动学习以减少错误形式化，并手动评估了我们提出的数据集，发现其形式化准确率很高。
3.2 自动定理证明 使用大型语言模型自动证明数学定理没有统一的方法。主流方法是在证明状态上进行最佳优先搜索或树搜索。这种方法可以防止生成无效的策略，因为它们会立即被编译器拒绝，但模型不能基于整体视角预测策略。相比之下，另一种方法是利用LLM基于自身生成整个证明。
数据构建流程
在这一部分中，我们将详细描述如图2所示的整个流水线，逐步翻译和筛选正确样本，并演示最终的数据集构建过程。
图2说明
图2展示了我们的流水线主要流程。从初始训练数据开始，我们微调翻译模型，并将其应用于自然语言问题集。翻译后的数据通过 Lean 4 编译、回译和自然语言推理 (NLI) 测试及人工诊断进行筛选。如果标注者认为样本达到了足够的准确性，则导出这些筛选后的样本。
4.1 第一轮流水线
首先，我们从 MiniF2F（zheng2021minif2f）和 ProofNet（azerbayev2023proofnet）中收集 Lean 4 形式化陈述及其对应的自然语言问题。由于我们不在 MiniF2F 和 ProofNet 上测试自动形式化，因此使用这两个数据集的所有样本。
证明将使用“:= sorry”声明。所有样本对将从两个方向组织到训练数据中，以实现形式化语言和自然语言之间的双向翻译。我们还包括多任务 Lean 4 指令数据，包括证明定理、预测下一个策略，并使用自然语言解释 Lean 证明（如 pact 和 jiang2023multilingual）进行训练。
训练数据可以分为证明问题和有明确答案的问题。然而，Lean 4 只支持证明问题，所以我们通过添加证明目标重新措辞所有解决方案问题。具体来说，我们在原始自然问题后附加“证明它是{答案}。”，而形式化陈述中的证明目标则更改为证明解决方案应该是正确答案。
第一轮数据收集被送入我们的翻译模型，该模型从 InternLM-Math-Plus-20B（2023internlm）初始化，预训练于 Lean 相关数据集。该模型以学习率 $4 \times 10^{-5}$ 进行三轮微调，每个翻译方向使用两个不同但固定的提示。这些翻译数据作为进一步迭代的起点。微调使用32个A100 GPU，数小时内可完成。
在训练翻译模型后，我们希望改进模型在不同数学主题上形式化问题的能力。我们从数学竞赛论坛5收集数学问题作为主动学习数据集。该数据集包含中学到高中的数学问题，难度不一，涵盖奥林匹克水平。我们利用 Qwen-1.5-14B-Chat（qwen）从论坛帖子中提取问题、解决方案和正确答案，使用以下提示：
你是数据标注者。以下是数学学生之间的讨论，可能包含多个问题和多个解决方案。请以 JSON 格式提取它们。每个问题是一个元素，包含键包括 problem（字符串，不能遗漏任何假设，如非负数），answer（计算问题返回数字字符串，证明问题返回空字符串），和 tags（字符串列表）。标签应识别数学问题的类别。可能的标签包括：方程，不等式，数论，代数，概率，组合，三角函数等。
注意到某些问题不适合形式化，同时提取过程不稳定，可能导致不合适的问题。首先，我们只保留以下标签的问题：不等式、数论、三角函数、模运算、归纳法、函数方程、复数和多项式。其次，我们询问 Qwen 模型问题是否定义明确，使用以下提示：
请检查以下数学问题是否定义明确？请遵循以下规则：
1. 考虑问题中给出的每个条件，如果某个变量未在问题中定义，则问题不明确。
2. 如果问题包含多个目标或没有明确目标，则问题不明确。
3. 注意不等式可能省略变量为实数的声明，但它们是明确的，不要判断为不明确。
4. 请在最后一句话中回复 **well-defined** 或 **ill-defined**，确保不误判明确的问题。
我们筛除不明确的问题。手动检查几乎没有留下不明确的问题，尽管少数明确的问题被错误忽略。清理后，我们使用初始翻译模型将所有筛选后的问题翻译为形式化陈述。
明确定义的子集总计包含6652个不同标签，其中223个标签包含超过100个样本。这些标签涵盖从竞赛级别知识点到高中课程的大量问题。超过三分之二的样本标有代数相关标签，而几乎没有几何相关标签。还注意到某些标签错误，特别是“数论”标签经常被分配给不等式问题。根据这些发现，在后续分析中，我们将继续关注样本超过100个的标签，并在人工诊断过程中特别注意错误标签。
4.2 数据诊断和迭代流程
编译正确性测试 为了确保我们的翻译流水线生成的形式化陈述的准确性，每个翻译的形式化定理都在 Lean 4 环境中进行正确性检查。最初，定理陈述独立验证，使用“by sorry”占位符过滤出不正确的陈述。然后检查完整的定理，包括证明。此步骤的主要瓶颈是 Lean 4 项目的编译成本。为了加速过程，我们建立了一个 Lean 4 读-评-打印循环（REPL），利用 Lean 4 的运行时元编程功能，允许在解释模式下验证 Lean 4 陈述。正确性测试程序可以以多进程方式执行，使用32核 CPU 一小时内完成。我们的测试环境基于 Lean v4.7.0，使用相同版本的 Mathlib4（可以通过指定标签 v4.7.0 克隆）。Minif2f 环境等同于 https://huggingface.co/datasets/internlm/Lean-Workbook/discussions/1 中的头文件。
数据过滤 首先，通过编译正确性测试处理所有问题的合成翻译。然而，通常看到正确编译的翻译实际上并未遵循原始问题。第二步过滤基于我们的模型的回译能力。在形式化陈述回译为自然问题后，我们可以使用通用领域的 LLM 利用其自然语言推理能力。在我们的流水线中，我们继续查询 Qwen-1.5-14B-Chat 判断原始问题是否与回译版本相同。如果未得到肯定答复，样本标记为需要人工修正。提示如下：
请检查以下两个数学问题是相同还是不同？请考虑两个问题中的每个陈述，如果任何陈述不同，它们就是不同的。请指出发现的任何差异。请在最后一句话中回复 **same** 或 **different**，并用粗体格式标出。
诊断和人工标注 数据诊断主要关注两种样本：未通过编译正确性测试的样本，以及通过测试但未通过 NLI 反馈的正确翻译样本。其他通过 NLI 测试的样本暂时认为是正确的。在前三轮迭代中，这两种样本都有相对明显的模式。因此，我们总结并相应地修改这些样本，使用三位熟悉 Lean 和竞赛级数学问题的专家6。
手动修改的样本被添加到训练数据中，新翻译模型被微调，用于下一轮生成和筛选合成样本进行人工诊断。这两个过程与前段描述相同。每次迭代将平均添加约30个人工标注样本到训练数据中，解决当前模型的弱点。
经过几轮后，难以总结模式。我们改变诊断模式，按标签随机抽取数学问题。通过手动检查样本，将正确或修改的样本添加到训练数据中，并记录通过 NLI 测试的样本的正确率。每轮迭代将获得更多通过 NLI 测试的样本，正确率也会提高。在第六轮迭代后，正确率几乎达到95%，我们在迭代过程中共添加了341个问题到训练集。
5 结果 本节将介绍我们的评估指标、数据集统计和案例研究，以及我们对这些案例的分析。
5.1 评估设置 与完全依赖于Lean 4编程来检查准确性的自动定理证明不同，我们对管道和最终翻译数据集的评估包括三个指标： (1) 编译通过数（CPN）：在Mathlib环境下使用Lean 4正确编译的所有生成的形式化语句的数量。 (2) 自然语言推理通过数（NPN）：既可以编译通过且回译与原始问题相同的生成形式化语句的数量。 (3) 正确翻译率：在人类专家认为通过NLI测试的生成形式化语句中，准确翻译的比例。在实际设置中，手动审查所有合成数据过于耗时，因此报告的值是基于问题类型的采样子集的比率。
5.2 数据集统计和评估结果 原始主动学习数据集有1088678个问题，其中458692个问题被认为是定义良好的。定义不良的问题来自不完整的网页提取或包含特定问题尝试和部分解决方案的帖子。过滤标签后，我们在实验中选择了327870个问题进行形式化。
经过六轮迭代，我们的模型输出了205079个通过编译正确性测试的问题，其中57231个翻译通过了NLI测试。我们随机选择每个常见标签（样本数超过100的标签）五到十个样本，并手动检查它们是否确实正确。结果见表1。对于最常见的三个标签，我们抽样了10个问题，它们的抽样准确率都超过90%。其他标签代表在数学竞赛和大学考试中出现的一种特殊问题类型，几乎所有标签最多有一个错误翻译。
我们使用InternLM-Math-Plus通过采样多个完整证明并通过我们的正确性检查器来检查Lean Workbook中的证明。我们为每个问题抽样1024个证明，解决了其中的4898个（即Pass@1024为8.6%），这比MiniF2F要难得多。我们还将开源这些解决方案以帮助改进自动定理证明。
表1：Lean Workbook中的标签准确率。这些标签在我们最终数据集中出现超过100次。前三个最常见的标签每个标签抽样10个问题，其他标签抽样5个问题。值得注意的是，由于标签模型的错误，一些标签是不正确的，如果我们认为当前样本不合适，将选择另一个样本。
| 标签 | 样本数 | 抽样准确率 |
|---|---|---|
| 不等式 | 46847 | 10/10 |
| 代数 | 45218 | 9/10 |
| 数论 | 22474 | 9/10 |
| 三角学 | 4133 | 4/5 |
| 方程 | 3255 | 5/5 |
| 证明 | 3172 | 5/5 |
| 微积分 | 1061 | 4/5 |
| 序列 | 926 | 4/5 |
| 组合数学 | 893 | 4/5 |
| 数列 | 418 | 5/5 |
| 函数 | 351 | 4/5 |
| 模运算 | 339 | 4/5 |
| 归纳法 | 285 | 5/5 |
| 对数 | 269 | 5/5 |
| 极限 | 224 | 3/5 |
| 实分析 | 170 | 5/5 |
| 加权平均 | - | 0.935 |
虽然整体准确率已经达到较高水平，但仍偶尔会发生某些类型的错误，这在表中也有所显示，因为并非所有标签都达到100%准确率。另一方面，许多模式在迭代过程中得到了纠正。这些模式包含编译错误，如冲突类型和函数，以及连续不等式，其纠正可以显著提高CPN。我们的模型在这些样本中表现出良好的学习能力。如果模型不知道如何翻译某种问题，三个手写语句将有助于模型学习如何翻译。然而，当涉及解释竞赛问题的错误时，迭代添加人工标注样本的有效性会降低。例如，当一个整数除以另一个整数而没有指定类型时，Lean语言将返回实际商的整数部分。因此，我们将类型 ℝ 添加到它们中，但模型只能正确执行约一半时间。这可能归因于实际数除法的混淆，但形式相同。其他实例包括模型仅陈述单边不等式但忽略了最小值（存在）的最小/最大问题。下表列出了在手动诊断过程中发现的常见模式。我们还发现，表中的一些错误可以通过后处理部分修复。
表2：错误模式的案例研究。我们列出了迭代诊断过程中总结的常见模式。该表列出了每个模式的一个典型错误，并展示了一个启发式修正。最后，“当前性能”列说明了在手动检查中模型在迭代后可以正确翻译的比例。
| 模式 | 错误示例 | 修改 | 性能 |
|---|---|---|---|
| 类型混淆 | a,b,c : ℝ, sqrt (a ^ 2 + 8 * b * c) | sqrt → Real.sqrt | 基本正确 |
| 连续不等式 | a >= b >= c > 0 | a >= b ∧ b >= c ∧ c > 0 | 基本正确 |
| 缺少运算符 | 2a+3b >= 0 | 2a+3b >= 0 | 基本正确 |
| 整数除法 | (abc)^(1/3) | (abc) ^((1: ℝ)/3) | 一半正确 |
| 三角形条件 | 𝑎, 𝑏, 𝑐 是三角形的边长：未翻译 | (hx: a > 0 ∧ b > 0 ∧ c > 0) (hab : a + b > c) (hbc : b + c > a) (hca : a + c > b) | 基本正确 |
| 所有解 | (x,y)=(1,5),(2,3) | (x=1 ∧ y=5) ∨ (x=2 ∧ y=3) | 基本正确 |
| 解的数量/和 | (x,y)=(1,5),(2,3) | A : Finset {x,y∣…} A.card=2 | 基本正确 |
| 最小/最大 | 𝑎的最大值是10：a <= 10 | IsGreatest {a∣…} 10 | 一半正确 |
| 存在无穷多个 | 无法翻译 | ∀N: N, ∃n > N, …. | 基本正确 |
| 数位 | n =abcde, a+b = … | Finset {n∣ sumOflist (Nat.digits 10 n) | 一半正确 |
5.3 有效性和讨论 为了直观地比较我们主动学习管道的有效性，我们得出了三个模型的CPN和NPN：用于初始过滤的第一轮模型，生成我们数据集的最终轮模型，以及进一步在我们数据集Lean Workbook上微调的最终模型。结果见表3。
表3：我们在迭代过程中报告了每个模型的CPN（编译通过数）和NPN（自然语言推理通过数）。
| 训练数据集 | 模型 | CPN | NPN |
|---|---|---|---|
| MiniF2F + ProofNet + MultiTask | 第一轮模型 | 136670 | 37122 |
| + 人工标注 | 最终轮模型 | 205079 | 57231 |
| + Lean Workbook | 最终轮模型 + Lean Workbook | 228928 | 82893 |
该表清楚地显示了我们的管道和数据集的有效性。人工标注的数据和过滤后的数据集在编译测试和NLI测试中分别多出了20000多个正确样本，令人鼓舞地表明这种形式的主动学习可以进一步迭代利用。
通过添加Lean Workbook数据进行翻译，模型可以进一步提高通过数，我们也将开源这个数据集（命名为Lean Workbook Plus）。虽然它在NLI通过率上显示出更高的数值，但人类评估发现该数据集在数论问题上错误较多，尤其是在涉及质数和最大/最小值的问题上。
5.4 形式化IMO问题 准确率表和案例研究表让我们对模型的表现有信心。作为高层次应用，我们尝试使用模型翻译新的IMO问题。
我们汇总了未被形式化的Compfiles问题。每个问题在温度为0.7的情况下被翻译100次，并通过编译测试和NLI测试删除错误翻译。最终，23个至少有一个正确翻译通过NLI的问题被筛选出来，21个问题在
人工评估后保留，包括14个代数问题、5个数论问题和2个组合问题。我们还手动检查并对结论部分进行了轻微修改，以确保这些翻译正确。这些形式化语句将提交给Compfiles项目。以下是一个案例，展示了我们的模型已经能够熟练使用“Finset”函数来优化形式化语句并避免语法错误。更多案例列在附录B中。
/–
IMO 1983 P5
是否可以选择1983个不同的正整数，所有这些数都不大于10^5，且没有三个数是等差数列的连续项？
–/
theorem IMO1983_P5 :
∃ S : Finset ℕ, S.card = 1983 ∧ (∀ x ∈ S, x ≤ 10^5) ∧ ∀ x ∈ S, ∀ y ∈ S, ∀ z ∈ S, x < y ∧ y < z → x + z ≠ 2 * y := by sorry
6 结论 在本文中，我们介绍了一个自动管道，可以高准确率地将竞赛级别的数学问题翻译成Lean形式化语句。主动学习在数据稀缺的情况下证明了其有效性。我们开源了Lean Workbook，以帮助机器学习社区提高自动形式化和自动定理证明的能力。
局限性 我们发现我们提出的数据集存在一些难以去重的类似问题。此外，我们的模型在主动学习过程中侧重于竞赛级别的问题，可能不适合形式化其他级别的数学问题。