Process-Driven Autoformalization in Lean 4

原链接

摘要 自动形式化，即将自然语言数学转换为形式语言，具有推动数学推理发展的巨大潜力。然而，现有的努力仅限于具有大量在线语料的形式语言，难以跟上快速发展的语言如Lean 4。为了弥补这一差距，我们提出了一个新的基准Formalization for Lean 4（FormL4），旨在评估大型语言模型（LLMs）的自动形式化能力。该基准包含问题、答案、形式化语句和证明的全面评估。此外，我们引入了一个过程监督验证器（PSV）模型，该模型利用Lean 4编译器的精确反馈来增强自动形式化。我们的实验表明，PSV方法提高了自动形式化的准确性，使用较少过滤的训练数据实现了更高的精度。此外，当使用包含详细过程信息的数据进行微调时，PSV能够更有效地利用数据，从而显著改善Lean 4的自动形式化。我们的数据集和代码可在https://github.com/rookie-joe/PDA获取。

1 引言 自动形式化，即自动将自然语言数学转换为形式语言，具有革命性地改变数学推理的潜力（WangKU18, Szegedy20）。它降低了形式化的高成本，弥合了自动数学推理研究与大量自然语言数学知识之间的鸿沟（Yuhuai2022nips, JiangWZL0LJLW23）。

近年来，LLMs在广泛任务中的表现显示出巨大的潜力（GPT35turbo, GPT4, Claude3, Llama3），为自动形式化开辟了令人兴奋的可能性。尽管研究人员探索了使用少样本提示（Yuhuai2022nips, Gadgil2022towards）或在包含非正式和正式数学数据的大规模数据集上训练LLMs（AzerbayevProofNet2023, AzerbayevLLemma2023, JiangMMA2023, YingIntern2024），现有的努力仅限于具有大量在线语料的形式语言，如Lean 3（Leonardo2015lean）。然而，社区最近将重点转向Lean 4（LeonardoLean42021），一个新版本的Lean定理证明器，它解决了先前的限制并引入了高效编程的新功能（ullrich2022LMCS, Sebastian2022ACM, Wojciech2023ITP）。

Lean 4的快速发展给自动形式化带来了重大挑战，因为跟上不断变化的语法、语义、库和其他方面需要大量的专业知识和持续的社区参与。这一挑战不仅限于人类专家，也包括LLMs，因为缺乏专门针对Lean 4的训练数据和基准阻碍了它们的进展。为了解决这一问题，我们提出了一个新的基准Formalization for Lean 4（FormL4），专门设计用于评估LLMs在Lean 4中的自动形式化能力。FormL4包含问题、答案、形式化语句和证明，提供对LLMs的全面评估。与现有的数据集MMA（JiangMMA2023）仅限于将问题翻译为语句不同，FormL4提供了从自然语言问题和答案到Lean 4中的语句和证明的“完整”自动形式化。这更加具有挑战性，因为它需要理解Lean 4的语法和每个证明中涉及的推理步骤。我们在附录E中详细比较了FormL4与MMA。

形式语言的一个关键优势是它们的编译器可以提供关于生成证明的详细步骤级信息。使用FormL4，我们可以充分利用来自Lean 4编译器的反馈，这些反馈不仅包括语法检查，还包括推理验证。这与仅关注翻译语句而不涉及证明的方法形成对比。来自编译器的过程信息提供了对数学推理过程的宝贵见解。最近的研究表明，过程信息在增强非正式语言的数学推理方面具有潜力（UesatoProcess2022, LiStepAware2023, LightmanStep2023, MaRewardStep2023）。

基于这些进展，我们提出利用Lean 4编译器自然提供的精确反馈来改善自动形式化，如图1所示。与依赖人类或机器注释的现有非正式方法不同（LightmanStep2023, WangShepherd2023），我们的广泛实验表明，过程监督验证器（PSV）可以显著增强自动形式化器，使其在使用较少过滤的训练数据时实现更高的性能。此外，当PSV使用包含详细过程信息的高质量训练数据进行微调时，它可以更有效地利用数据，从而在自动形式化方面取得更大的改进。我们总结了以下关键贡献：

参见图例 图1：过程驱动的自动形式化框架概述，该框架在FormL4上训练，并通过过程监督验证器（PSV）进一步增强。具体来说，图中展示了四个主要过程：（1）通过提示GPT-4对从Mathlib 4中提取的定理进行非正式化构建FormL4基准；（2）在FormL4上训练自动形式化模型，并将输出发送到Lean 4编译器以获得自动反馈；（3）编译反馈可以为自动形式化器提供过程级注释，用于训练有效的PSV模型；（4）为了进一步增强，自动形式化器随后通过验证器的反馈进行微调，而验证器可以再次从改进的自动形式化器的高质量输出数据中受益。

2 相关工作 使用LLMs进行自动形式化 自动形式化是将非正式定理和证明自动转换为机器可验证格式的任务（WangKU18, Szegedy20）。早期的方法采用神经机器翻译方法将文本翻译成Mizar语言（WangBKU20）。LLMs的最新进展为自动形式化开辟了新可能性。研究人员探索了使用少样本提示使LLMs能够将数学问题翻译成形式化格式，包括Isabelle和Lean（Yuhuai2022nips, Gadgil2022towards）。其他研究采用了更结构化的方法来完成这项任务。值得注意的是，DSP系统（JiangWZL0LJLW23）使用LLMs起草非正式证明并将其映射到形式化草图中，自动定理证明系统则用于填补证明草图中的缺失细节。此外，一些研究专注于在包含非正式和正式数学数据的大规模数据集上训练LLMs，以评估它们在自动形式化中的表现（AzerbayevProofNet2023, AzerbayevLLemma2023, JiangMMA2023, YingIntern2024）。与现有的往往忽视ITPs中可用的详细编译信息的方法不同，我们提出的方法利用Lean 4编译器的过程反馈进一步提高LLMs的自动形式化能力。

过程和结果监督 最近的努力集中于通过验证器增强LLMs的数学推理能力，从多个候选中选择最佳答案。验证器主要有两种类型：结果监督验证器（OSV）和过程监督验证器（PSV）。OSV以最终答案为基础进行监督（CobbeGSM8k2021, YuOVM2023），而PSV则需要评估个体推理步骤的详细反馈（UesatoProcess2022, LiStepAware2023, LightmanStep2023, MaRewardStep2023）。尽管注释成本高昂，PSV提供的细粒度反馈可以指出错误位置，这对于强化学习和自动纠正非常有价值（LightmanStep2023, WuGrained2023）。为了减少大量的人类注释需求，最近的方法（WangShepherd2023, WangMiPS2024）提出了使用蒙特卡罗树搜索（Coulom06, SilverHMGSDSAPL16）的机器注释框架。这个注释过程需要大量计算资源，可能对使用施加限制。我们的方法利用形式语言能够自然提供的精确反馈进行推理过程的自动注释，无需大量人类或机器注释成本。

3 FormL4：数据集构建 Lean 4（LeonardoLean42021）的快速发展，这是一种强大的形式语言，相对于其前身Lean 3（Leonardo2015lean）有了显著改进，迫切需要一个专门的基准来评估在这个新环境中的自动形式化能力。现有的数据集MMA（JiangMMA2023）主要关注将问题翻译为语句，忽略了将非正式解决方案翻译为证明的关键步骤。这一限制阻碍了利用Lean 4编译器提供的全面反馈的能力，这些反馈可以检查语法并

验证证明内的推理。

为了解决这一问题，我们引入了专门设计用于评估完整自动形式化过程的FormL4。FormL4超越了语句翻译，包含了问题、答案、形式化语句和证明。这种全面的方法允许更准确地评估LLM理解Lean 4语法并在语言框架内进行逻辑推理的能力。在本节中，我们将介绍如何创建高质量的平行语料库（第3.1节）、保证质量（第3.2节）和分割数据（第3.3节）。

3.1 非正式化 我们利用GPT-4自动生成形式化数学语句及其证明（形式化）的非正式描述。我们的方法超越了之前的工作（JiangMMA2023），旨在将形式化内容的各个方面（语句和证明）转换为每个数据点的自然语言。这是一项更具挑战性和计算成本更高的任务，要求GPT-4理解Lean 4的语法和每个证明中的逻辑推理步骤。

由于GPT-4直接生成Lean 4代码的能力有限（JiangMMA2023）（形式化比非正式化更困难），我们从mathlib4库中提取用Lean 4格式编写的定理（包括语句和证明），并将其输入GPT-4以非正式化为自然语言描述。值得注意的是，Lean 4中的mathlib4是可用的最广泛的形式数学库之一。我们提供了特定的指令，以提示GPT-4将这些定理转换为自然语言问题和答案，详细说明可见附录D。

3.2 筛选过程 预处理 我们从Mathlib 4中提取了70,000个定理，包括它们的语句和证明。此过程基于LeanDojo（Kaiyu2023Leandojo）的脚本，但进行了某些修改。我们采用LeanDojo4代码搜索并从Mathlib 4中提取定理。然而，与原始脚本专注于提取定理名称和定理证明策略不同，我们提取了语句和证明的完整内容。我们不减少证明步骤，旨在提供全面内容以改进自动形式化。

我们在证明中保留了“#align”命令，Mathport6使用该命令将Lean 3名称连接到Lean 4名称。这一包含旨在促进GPT-4在数据构建过程中理解Lean 4语言，因为我们假设GPT-4如果能连接到更熟悉的Lean 3语言将更好地理解Lean 4语言。

后处理 我们对从GPT-4非正式化获得的数据进行手动和自动筛选，以确保为自动形式化提供高质量的训练和测试数据。更多详细信息请参见第H.2节。

我们提供了一个“定理环境”，其中包括每个定理的完整依赖项和前提，方便编译。具体来说，只需将“定理环境”与自动形式化结果连接即可验证后者，无需深入Mathlib的细节。我们相信这种方法简化了编译过程。

表1：FormL4的统计数据。测试集不一定需要Lean 4的真实语句和证明，因为自动形式化的输出可以由编译器验证。实际测试集仅包含自然语言查询和答案，不包含任何对应的Lean 4语句。 | 数据集 | 大小 | Lean 4 | 自然语言 | | — | — | — | — | | # 字符，语句 & 证明 | # 字符，Q & A | | 平均值 | 中位数 | 最小值 | 最大值 | 平均值 | 中位数 | 最小值 | 最大值 | | 训练 | 14,510 | 210 | 179 | 101 | 5515 | 1900 | 1905 | 449 | 5706 | | 随机测试 | 970 | 214 | 180 | 103 | 3242 | 1918 | 1921 | 677 | 4681 | | 基础测试 | 981 | 205 | 165 | 111 | 2882 | 1781 | 1775 | 481 | 4856 | | 真实测试 | 1,000 | - | - | - | - | 893 | 763 | 401 | 3812 |

3.3 数据集划分 我们首先创建一个训练集和一个随机测试集，用于训练和评估LLMs。这两个集合通过从提取的Lean 4源文件中采样定理（包括其语句和证明）构建，每次选择后不将其放回池中。附录E中展示了一个示例。除了随机测试集外，我们还包括一个基础测试集和一个真实测试集以进行更全面的评估。基础测试集评估模型在基本定理自动形式化中的能力，最少依赖先验知识或已建立的引理。这些定理通常出现在如Mathlib/Geometry/Euclidean/Basic.lean等文件中，建立基本几何概念并证明关于实内积空间和欧几里得仿射空间的简单结果。此外，我们通过从Arithmo测试集（arithmo2023jindal）收集1,000个自然语言数学问题和答案构建真实测试集。表1详细列出了FormL4的统计数据，包括Lean 4和自然语言的语句长度字符数。数据集划分和真实测试集环境的详细信息可见附录H。

4 方法：过程驱动的自动形式化 本节概述了我们通过过程反馈改进LLMs自动形式化能力的策略。我们首先通过微调Mistral-7B（Albert2023Mistral）在自动形式化训练数据上设定基准基线。然后，我们引入一个过程监督验证器（PSV）模型，在训练阶段结合Lean 4编译器的详细反馈（第4.1节）。最后，我们提出一种连续改进的方法，通过Lean 4编译器的客观评价迭代精炼自动形式化和验证模型（第4.2节）。

4.1 验证模型 我们的方法利用Lean 4编译器提供的详细过程级反馈来增强验证器模型的训练。我们偏离了之前的方法（Yuhuai2022nips），该方法仅依赖于编译成功或失败的最终结果。相反，我们采用了一种细化策略，根据UesatoProcess2022的“首错误位置”策略，将训练数据中的每一步标记为正确或错误。Lean 4编译器检测到的首个错误之前的步骤标记为“正确”，之后的步骤标记为“错误”。这种标记方式使我们能够在整个编译过程中纳入丰富的过程信息。我们的方法与传统的结果中心方法使用拒绝采样或直接应用结果训练奖励或验证模型形成对比。通过利用Lean 4编译器的过程反馈，我们提出的方法更适合和高效的自动形式化任务。为了展示过程监督训练的有效性，我们比较了两种模型：

[ \mathcal{L}{\text{OSV}}(q; S_i(1:t), Y_i, \theta) = \frac{1}{n} \sum{i=1}^{n} \frac{1}{m_i} \sum_{t=1}^{m_i} [y_i \log(r_i) + (1 - y_i) \log(1 - r_i)] ]

(q) 代表问题，(S_i) 为样本集，(S_i(1:t)) 为样本 (S_i) 的第(t)步。(Y_i) 是第(i)个样本的标签集，(y_i) 为每个(t)的逐步标签。(n) 是样本总数，(m_i) 是(S_i)中的步骤数，(r_i = f_\theta(q; S_i(1:t))) 为正确类别的预测概率。

[ \mathcal{L}{\text{PSV}}(q; S_i(1:t), Y_i, \theta) = \frac{1}{n} \sum{i=1}^{n} \frac{1}{m_i} \sum_{t=1}^{m_i} [y_i^t \log(r_i) + (1 - y_i^t) \log(1 - r_i)] ]

损失函数计算所有样本和解决步骤的平均交叉熵损失，类似于OSV模型。然而，逐步标签 (y_i^t) 是基于“首错误位置”标记策略的

样本 (S_i) 中第(t)步。

注意： 为了公平比较PSV和OSV，两个模型都在标准语言建模框架中进行训练。训练期间，两个特殊标记代表“正确”和“错误”标签。表5中呈现了性能比较。

4.2 通过反向传播过程反馈进一步增强 为了进一步提升自动形式化器和验证器的能力，我们采用由Lean 4编译器反馈指导的持续改进策略。通过以下步骤迭代提升模型性能：

这一以编译器反馈为核心的循环过程具有显著优势。它提供了进展的客观度量，减轻了自动形式化器和验证器之间孤立互动可能带来的偏差。通过持续根据编译器反馈精炼模型，我们确保自动形式化器和验证器沿着符合成功编译的实际需求的方向进化。

5 实验 我们首先介绍现有LLMs在FormL4自动形式化任务中的局限性，详见第5.1节。然后在第5.2节展示主要结果，包括通过PSV模型实现的自动形式化提升（第5.2.2节），以及受益于增强的自动形式化器生成的高质量输出数据，PSV模型验证性能的进一步提升（第5.2.3节）。

5.1 现有LLMs在FormL4上的局限性 我们评估了开源和专有LLMs在FormL4测试集上的自动形式化能力。表2详细说明了当前LLMs（包括GPT-4）在Lean 4自动形式化任务中的挑战。低性能结果表明在该领域需要方法改进。如何查询这些LLMs及其性能分析的更多详细信息请见附录I。

表2：LLMs在FormL4上的性能，按贪心和pass@k分数计算。我们包括声称在其预训练/微调中集成形式语言的开源LLMs。报告结果表示在所有生成输出中成功编译的百分比（%）。 | 模型 | 随机测试 | 基础测试 | 真实测试 | | — | — | — | — | | 贪心 | Pass@1 | Pass@5 | 贪心 | Pass@1 | Pass@5 | 贪心 | Pass@1 | Pass@5 | | 闭源LLMs | | | GPT-3.5-Turbo (GPT4) | 0.41 | 0.32 | 0.73 | 0.29 | 0.00 | 0.66 | 5.10 | 3.80 | 17.00 | | GPT-4-Turbo (GPT35turbo) | 0.49 | 0.41 | 3.42 | 1.47 | 1.14 | 4.38 | 10.20 | 8.70 | 25.10 | | 开源LLMs | | | DeepSeek-Math-Base-7B (Zhihong2024Deepseek-math) | 0.17 | 0.21 | 0.95 | 0.34 | 0.22 | 0.81 | 0.00 | 0.00 | 0.00 | | DeepSeek-Math-Instruct-7B (Zhihong2024Deepseek-math) | 0.58 | 0.22 | 1.71 | 1.16 | 0.47 | 3.04 | 0.30 | 1.60 | 5.30 | | LLEMMA-7B (AzerbayevLLemma2023) | 0.00 | 0.00 | 0.77 | 0.17 | 0.10 | 0.45 | 0.00 | 0.00 | 0.00 | | LLEMMA-34B (AzerbayevLLemma2023) | 0.00 | 0.00 | 0.18 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | | InternLM-Math-7B (Huaiyuan2024InternLM-Math) | 0.00 | 0.00 | 0.18 | 0.19 | 0.14 | 0.26 | 1.10 | 1.00 | 3.70 | | InternLM-Math-20B (Huaiyuan2024InternLM-Math) | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 0.00 | 0.20 | 0.70 | 2.30 | | Mistral-Instruct-v0.2-7B (Albert2023Mistral) | 0.28 | 0.21 | 1.86 | 0.45 | 0.77 | 1.82 | 0.30 | 0.50 | 1.90 |

5.2 自动形式化增强 我们展示了使用我们提出的过程驱动自动形式化框架进行实验的主要发现。在第5.2.1节中，我们概述了如何设置基准，包括自动形式化的基线模型和PSV模型。我们还详细说明了评估指标。在第5.2.2节中，我们展示了第4.2节中描述的增强自动形式化器的结果。在第5.2.3节中，我们展示了进一步增强的PSV模型的结果，并将其性能与OSV模型进行比较。

5.2.1 实验设置 基线 首先使用FormL4提供的14,510条数据集的完整数据集训练基线。此初始步骤建立了一个初步的自动形式化水平。为了增强其在真实测试场景中的表现，训练后的基线模型被用来对自然语言数学数据集（即GSM8K（CobbeGSM8k2021）和MATH（Hendrycks2021Nips））的未标注示例进行自动形式化。通过Lean 4编译器成功编译的输出用于进一步微调最终基线模型。

验证器 我们使用训练后的基线生成多个样本，基于其训练的未标注提示。每个样本通过Lean 4编译器测试以确定其编译成功并提供详细的编译信息。随后，我们利用从编译器反馈中提取的逐步过程监督微调验证器模型。此外，我们微调一个结果监督验证器（OSV）模型，如第4.1节所述，并在表5中列出了比较实验结果。

评估 为了评估验证器的性能，我们评估其选择自动形式化器生成的样本中能成功通过Lean 4编译器的一个候选样本的能力。具体来说，我们选择验证器评估为“正确”的候选样本。当多个候选样本被标记为“正确”时，我们优先选择预测“正确”标签时对数概率最高的样本。这个性能指标被称为多重选择（MP1）。我们进一步计算精度（Prec.），即成功编译的样本中被验证器选择的样本的比例，以及召回率，即验证器选择的成功编译样本的比例，以提供对验证器更全面的评估。

5.2.2 增强自动形式化器 我们展示了基于基线模型的增强自动形式化方法的实验结果。具体来说，我们利用基线模型在FormL4、MATH和GSM8K的训练集上生成多个自动形式化输出。

PSV用于评估基线模型生成的每个输出。评估为“正确”的输出被选中用于进一步微调基线模型，形成验证器增强的自动形式化模型。此增强模型的性能称为“验证器（我们的）”。

我们将验证器增强的自动形式化模型与ScalingRelationship2023和Yuhuai2022nips中描述的拒绝采样微调（RFT）增强版本进行比较。RFT方法选择成功编译的输出以进一步微调基线模型。此外，我们将验证器评估与RFT结合，选择不仅成功编译而

且被PSV评估为“正确”的输出，以进一步增强基线模型。我们将结果记录为“RFT + Verifier（我们的）”。我们在表3中展示了整体比较性能。

表3：增强自动形式化器的性能比较。 | 模型 | 训练数据 | 测试集 | | — | — | — | | 数量 | 质量（准确率） | 基础 | 随机 | 真实 | | 基线 | - | - | 40.92 | 35.88 | 23.90 | | RFT | + 65K | 100% | 44.50 | 38.70 | 26.50 | | Verifier (Ours) | + 74K | 80.50% | 43.80 | 38.04 | 25.70 | | RFT + Verifier (Ours) | + 60K | 100% | 46.28 | 39.38 | 27.90 |

RFT有效但耗时：RFT在所有测试集中显著改进了自动形式化过程，验证了之前研究的发现。然而，RFT依赖于Lean 4编译器的编译结果进行数据筛选，可能耗时，如第F.3节所述。

验证器补充RFT以获得更好的自动形式化：相比之下，我们的方法引入了一种更高效的时间数据筛选方法，通过为样本分配预测标签。尽管这种方法可能无法保证与RFT相同的数据质量，但将验证器与RFT结合显著提高了所有测试集的性能。这种协同作用表明，组合方法可以带来更好的自动形式化结果。

虽然RFT以时间为代价确保高质量数据，但验证器简化了筛选过程但可能损害数据质量。然而，它们的结合利用了两者的优势，如所有测试集的改进性能指标所示，突显了这种组合方法在改进自动形式化方法方面的潜力。

5.2.3 进一步增强验证器 我们利用增强的自动形式化器生成更高质量的训练数据（由Lean 4编译器监督），用于进一步微调验证器模型。具体来说，我们使用增强的自动形式化器，即RFT + Verifier（Ours），在FormL4、MATH和GSM8K的训练集上生成样本。每个生成的样本通过Lean 4编译器测试，以确定其编译成功并获得详细的编译信息。随后，我们利用这些数据进一步微调PSV模型，结合从编译器反馈中提取的逐步过程监督。

为了评估我们进一步微调的验证器，我们首先报告RFT + Verifier模型的全面性能，使用与附录I中描述的相似的贪心解码和pass@k采样进行评估。然后，我们按照第5.2.1节定义的评估指标验证RFT + Verifier模型的输出。我们比较结果监督和过程监督的训练方法，如第4.1节所述。“PSV +”表示基于“PSV”进一步进行过程监督微调，而“OSV +”表示在“OSV”基础上进行结果监督的额外改进。

表4：增强自动形式化器的全面性能。 | 模型 | 数据集 | 贪心 | Pass@1 | Pass@5 | | — | — | — | — | — | | 基础 | 46.28 | 42.71 | 54.33 | | RFT + Verifier | 随机 | 39.38 | 36.91 | 50.21 | | 真实 | 23.90 | 22.80 | 48.10 |

表5：增强验证器模型的比较性能。 | 数据集 | OSV | OSV + | PSV | PSV + | | — | — | — | — | — | | MP1 | Prec. | Recall | MP1 | Prec. | Recall | MP1 | Prec. | Recall | MP1 | Prec. | Recall | | 基础 | 40.71 | 81.34 | 80.12 | 45.13 | 84.22 | 83.18 | 41.49 | 84.59 | 82.73 | 47.30 | 89.14 | 94.17 | | 随机 | 36.14 | 81.16 | 81.07 | 38.21 | 83.13 | 84.45 | 37.52 | 84.68 | 83.47 | 44.32 | 84.20 | 93.70 | | 真实 | 25.75 | 84.45 | 86.21 | 33.41 | 84.45 | 86.21 | 33.42 | 84.34 | 81.08 | 45.10 | 94.18 | 89.31 |

高质量数据提高性能：如表5所示，与OSV和PSV模型相比，OSV +和PSV +模型在所有三个评估指标（MP1、精度和召回率）上均有提升。这种改进在所有数据集中是一致的，证明了高质量数据微调增强了结果监督和过程监督的训练方法。

过程监督微调的优越性：表格显示PSV +在所有指标和数据集上始终优于OSV +。在基础数据集中，PSV +的MP1得分为47.30，而OSV +为45.13。同样，在真实数据集中，PSV +的MP1得分为45.10，显著高于OSV +的33.41。此外，PSV +在所有数据集上的精度和召回率均优于OSV +，如真实数据集中的精度为94.18%，而OSV +仅为84.45%。这表明基于过程的监督更有效地利用训练数据，导致整体性能提升。

表3和表5中展示的增强结果证明了自动形式化器、验证器和Lean 4编译器之间迭代训练互动的潜力。在Lean 4编译器监督下对自动形式化器和验证器的迭代改进，可能是未来工作的一个有前途的方向。

6 FormL4中训练和测试数据的分析 为了展示FormL4提供的训练数据与测试集之间的联系，我们在Mistral-7B（Albert2023Mistral）模型上进行标准监督微调，使用FormL4提供的训练数据，训练超参数详见第F.1节。我们将其与在FormL4提供的5k样本训练数据上训练的模型进行比较。它们在三个测试集上的自动形式化性能列在表6中。

表6：在不同数据量上训练的模型的比较。 | 模型 | 基础 | 随机 | 真实 | | — | — | — | — | | Mistral | 0.12 | 0.00 | 0.20 | | Mistral (5K) | 33.15 | 28.4 | 1.80 | | Mistral (Full) | 40.55 | 35.8 | 2.70 |

我们展示了以下见解：

训练数据总是重要的：我们的研究揭示了FormL4提供的测试数据与训练数据之间的强相关性。通过将训练数据集从5k扩大到完整的14.51k样本，我们观察到三个测试集的编译率显著提高。这表明增加训练数据量对模型在测试集上的性能有积极影响，如表6所示。

真实测试仍然具有挑战性：尽管在所有测试集中都有改进，但在真实测试集中仍有很大提升空间，即自然语言基准，如表6所示。这种差异可以归因于两个主要因素：i. 测试域外分布：真实测试集相比两个Mathlib Lean 4测试集（即随机和基础）表示为OOD测试域。因此，仅在Mathlib Lean 4训练集上微调的模型可能难以有效泛化到这些基准。ii. 缺乏对预定义引理或基本术语的依赖：与Mathlib Lean 4测试集不同，真实测试集通常缺乏对预定义引理或基本术语的依赖。如第3.3节所述，这种缺失可能会影响模型的表现，突显出潜在的改进领域。

此外，我们在两个数学推理基准（即GSM8K CobbeGSM8k2021和MATH Hendrycks2021Nips）上评估了自动形式化效率。我们注意到，SFT模型在真实测试集上的表现与表3中列出的基线模型不同。这是因为本节旨在探索FormL4提供的训练和测试集之间的联系。因此，本节中的两个SFT模型未在MATH和GSM8K数据集上进行进一步微调，如第5.2.1节所述。

7 结论 本文旨在弥合自然语言和形式语言之间的差距。我们提出了一个新的基准FormL4，专门设计用于评估LLMs在Lean 4中的自动形式化能力，这是一种

强大且不断发展的形式语言。与现有数据集仅关注将问题翻译为语句不同，FormL4提供了从自然语言问题和答案到Lean 4中的语句和证明的“完整”自动形式化。重要的是，我们进一步引入了一种新方法，利用Lean 4编译器自然提供的精确反馈来改善自动形式化，显著提高性能并更有效地利用高质量训练数据。未来工作中，我们希望扩展我们的基准并将我们的方法应用于更多的形式语言，如Isabelle、HOL Light和Coq。这将进一步增强LLMs的自动形式化能力，开辟数学探索和发现的新可能性。本文的局限性和更广泛的影响在附录A和B中讨论。