从编译器反馈中学习修复 Lean 证明 Learning to Repair Lean Proofs from Compiler Feedback
用 26 万条变异错误训练 LLM 修复 Lean 形式化证明
前置知识
Lean 证明助手
Lean 是一种交互式定理证明器和函数式编程语言，由 Leonardo de Moura 等人开发。用户可以用 Lean 4 编写严格的数学证明，然后由内核（kernel）逐条验证每一步推理是否合法。Lean 4.22.0-rc4 是本文使用的具体版本。编译器在发现证明错误时会生成结构化的错误信息，包括错误类型、出错位置和当前的 proof state（目标状态），这些信息是本文训练信号的核心来源。
本文的整个研究对象就是 Lean 证明的修复过程，理解 Lean 的编译验证机制和错误信息格式是读懂论文的基础。
形式化定理证明（Formal Theorem Proving）
用形式化语言书写数学命题和证明，由计算机严格验证每一步推理的正确性。与自然语言数学不同，形式化证明不允许任何歧义——一个证明要么通过内核验证（correct），要么被拒绝（incorrect）。近年来，自动化定理证明（ATP）领域大量使用 LLM 来搜索或生成证明，典型基准包括 miniF2F 和 mathlib。
论文的核心问题是：LLM 生成证明时不可避免会犯错，如何让模型学会根据编译器反馈修复错误。
监督微调（Supervised Fine-Tuning, SFT）
在预训练语言模型的基础上，用特定任务的标注数据进行进一步训练。本文使用低秩适配（LoRA, Low-Rank Adaptation）技术，将可训练参数限制在注意力层和 MLP 的投影矩阵上，通过秩为 32 的低秩分解来减少参数量。具体来说，对 q_proj、k_proj、v_proj、o_proj、gate_proj、up_proj、down_proj 七类投影层均施加 LoRA 适配器，使用 AdamW 优化器，学习率 $1 \times 10^{-4}$，余弦退火调度，有效批量大小 8，最大序列长度 2048。
本文的核心训练方法就是 SFT + LoRA，理解这一流程才能评估模型训练的可行性和复现难度。
证明修复（Proof Repair）
给定一个编译失败的 Lean 证明和对应的编译器错误信息（包括错误消息、出错行号、目标状态），模型需要生成一个修正后的证明，使其能够通过 Lean 编译器的验证。与端到端证明生成不同，证明修复任务是有条件生成：输入包含错误信号，输出需要针对该信号做出精确修正。本文将此问题形式化为监督学习任务，训练数据的每条样本包含 (错误证明, 编译器反馈, 正确证明, 自然语言解释) 的四元组。
这是论文定义的核心任务，理解其输入输出格式和评估方式是理解实验结果的关键。
变异测试（Mutation Testing）
借鉴软件工程中变异测试的思想：通过系统性地对正确程序引入小的、可控的修改（变异），生成大量错误版本。本文设计了四类变异操作——定理替换（用语义相近但不等价的定理替换）、策略替换（在同一等价类的策略间交换，如 linarith 和 nlinarith）、行级替换（用 LLM 生成的错误行替换正确行）、多行替换（截断部分证明让 LLM 补全）。所有变异后的证明都经过 Lean 编译器筛选，只保留真正产生编译错误的样本。
变异策略是构建 APRIL 数据集的核心机制，决定了训练数据的质量和多样性。
pass@1 与单次修复评估
pass@k 是定理证明领域常用的评估指标，表示在 k 次独立采样中至少有一次成功通过验证的概率。本文采用更严格的单次修复（single-shot repair）设置：模型只有一次机会修复错误证明，不使用搜索、迭代或重采样。这与实际的 agentic 证明系统形成对比——后者通常使用多轮迭代反馈和搜索策略，效率比 pass@k 高 32-128 倍（Chen et al., 2025）。本文的评估旨在隔离模型从编译器反馈中学习修复的能力。
理解评估设置才能正确解读实验数字的含义，单次修复的难度远高于带搜索的迭代修复。
研究动机
当前形式化定理证明系统的主流范式是端到端证明生成：给定一个形式化命题，直接生成完整的正确证明。训练数据几乎完全由正确证明构成——无论是 mathlib 这样的大型形式化库，还是 Lean Workbook、Herald、NuminaMath 等自动形式化数据集，都只保留最终验证通过的证明，丢弃了开发过程中所有的失败尝试和编译器反馈。这意味着模型在训练时几乎从未见过错误证明及其修复过程，缺乏直接的监督信号来理解编译器诊断信息、解释错误原因或提出针对性修正。然而，人类的证明开发过程本质上是迭代和错误驱动的：工程师编写部分证明、检查编译器诊断、逐步修改直到验证成功。Chen et al. (2025) 的研究表明，利用编译器反馈的迭代证明细化比独立采样 pass@k 高效 32-128 倍，但现有训练范式完全没有利用这一信号。
本文的目标是本文旨在将证明修复定义为一个监督学习任务：给定一个错误证明和编译器反馈（包括错误消息、出错位置、目标状态），同时预测两个对齐的输出——(1) 修正后的正确证明，(2) 基于相同反馈的自然语言诊断和修复建议。为支持这一任务，作者构建了 APRIL（Automated Proof Repair in Lean）数据集，包含 260,125 条有监督样本，每条样本由错误证明、编译器诊断、正确证明和自然语言注释组成。最终目标是证明：在编译器反馈条件下进行监督微调，可以显著提升模型的证明修复能力，为构建能够迭代修复证明的 agentic 定理证明器提供互补的训练信号。
与已有工作不同的是，本文的独特切入角度在于三点。第一，将证明修复从探索信号或策略优化的辅助角色提升为独立的监督学习目标，直接以 (错误证明, 编译器反馈) → 正确证明 作为训练对。第二，采用「逆向构建」策略：由于人类编写的错误证明稀缺，本文从正确证明出发，通过四类系统性变异操作（定理替换、策略替换、行级替换、多行替换）可控地生成大量真实感错误，每条错误都经过 Lean 编译器实际验证。第三，同时监督形式化修复和自然语言解释两个对齐任务，发现联合训练不仅能产生人类可理解的诊断，还能为下游系统（如 DeepSeek）提供有价值的修复提示——用训练后模型的解释辅助 DeepSeek 可将成功率从 4% 提升到 29%。
核心方法
整体方法路线可以概括为「逆向变异 + 编译器验证 + LLM 注释 + 监督微调」。直觉上，既然正确证明大量可得而错误证明稀缺，那就从正确证明出发系统性地「制造」错误。具体来说：首先从 Herald、Lean Workbook、NuminaMath-Lean 三个公开数据集中收集能通过 Lean 4.22.0-rc4 编译的正确证明（共 39,492 条）；然后用四类变异操作对每条证明生成多个错误版本，只保留真正触发编译器错误的样本（共 260,125 条）；接着用 DeepSeek-V3-0324 为每条错误样本生成自然语言解释和修复建议；最后用 LoRA 对 Qwen3-4B-Instruct-2507、Kimina-Prover-Distill-8B、Goedel-Prover-V2-8B 三个模型进行监督微调。整个管线的核心优势是：每条训练样本的错误信息和目标状态都是 Lean 编译器在固定环境下实际产生的，修复目标是同环境下验证通过的证明，保证了训练信号的可靠性。
与现有方法的本质区别在于训练信号的来源。传统定理证明系统以正确证明为训练目标，错误信息仅作为探索过程的反馈信号（如 MCTS 中的奖励）；而本文将错误证明本身作为输入，将编译器反馈作为条件，将正确修复作为输出目标，构建了端到端的监督学习对。另一关键创新是变异策略的设计：定理替换使用 LeanExplore 语义搜索引擎找到语义相近但不等价的定理进行替换，产生的错误可能出现在证明的远端而非变异位置；策略替换在同一等价类（如算术求解器 linarith/nlinarith/ring/omega）内交换；行级和多行替换用 LLM 生成「看似合理但实际错误」的证明步骤。这种设计确保了错误的多样性和真实感，避免了随机噪声式的错误。
方法步骤详情
方法分为数据构建和模型训练两大阶段。数据构建阶段：(1) 收集正确证明——从 Herald（30,190 条原始，过滤后 16,010 条）、Lean Workbook（10,433 条，过滤后 9,491 条）、NuminaMath-Lean（含 Autoformalizer 6,039→5,925 条和 Human 9,428→8,066 条），总计 56,090 条原始证明过滤为 39,492 条可通过 Lean 4.22.0-rc4 编译的正确证明；(2) 生成变异错误——对每条证明应用四类变异操作（定理替换使用 LeanExplore 检索语义相似声明并单次替换，策略替换在预定义的等价类内随机交换 1-3 处，行级替换用 REDACTED 标记一行后让 DeepSeek-V3 补全，多行替换截断选定行之后最多一半的证明让 LLM 补全），只保留编译失败的样本并去重；(3) LLM 注释——用 DeepSeek-V3-0324 为每条错误样本生成自然语言解释和修复建议，输入包括原始证明、变异证明、编译器错误消息和变异元数据。模型训练阶段：将每条样本转为对话格式（系统消息 + 用户消息包含错误信息、目标状态和错误证明 → 助手消息包含解释和修复），使用 LoRA（秩 32，作用于所有注意力和 MLP 投影层）进行 SFT，AdamW 优化器学习率 $1 \times 10^{-4}$，训练最多 15,000 步，早停耐心 5（1,250 步），选择验证损失最低的检查点。
技术新颖性
本文的技术新颖性体现在多个层面。在任务定义上，首次将 Lean 证明修复形式化为独立的监督学习问题，而非端到端证明生成的附属信号。在数据构建上，设计了四类有针对性的变异策略，每类都反映了真实证明开发中的常见错误模式：定理替换对应「语义相近但前提或结论不同的定理误用」（占变异的 59.5%），策略替换对应「在同一证明职责的策略间误选」，行级和多行替换对应「LLM 生成的看似合理但实际错误的证明步骤」。在评估协议上，采用严格的单次修复设置（无搜索/迭代），隔离了模型从编译器反馈中学习的能力，发现微调后的 4B 模型（27.4%）在同等设置下超过了 32B 的 Goedel-Prover-V2（26.8%）。在解释性上，发现联合训练修复和解释不仅不会严重损害修复性能（仅下降约 2-5 个百分点），还能产生有价值的诊断——用训练后模型的解释辅助 DeepSeek 可将修复成功率从 4% 提升到 29%，展示了错误诊断作为独立训练信号的潜力。
实验结果
实验结果揭示了几个重要发现。首先，监督微调在 APRIL 上能带来巨大提升：Qwen3-4B-Instruct 的修复准确率从 1.1% 飙升到 27.4%（约 25 倍），在单次修复设置下甚至略超 32B 的 Goedel-Prover-V2-32B（26.8%）。微调后的 8B 模型（Goedel-8B 达 34.6%，Kimina-8B 达 31.9%）进一步超越 32B 基线。其次，不同变异类型的修复难度差异显著：策略变异最容易（最高 42.5%），因为错误通常局限在固定证明上下文的局部；定理变异中等难度；行级变异最难（最高仅 13.5%），因为涉及纠正语义不一致或幻觉的证明步骤。第三，联合训练（在所有变异类型上训练）与单独训练相比，性能下降很小，说明不同错误类型之间存在大量结构重叠，联合训练能让模型学到跨错误类别的通用修复策略。第四，解释和修复的联合训练构成一个可控的权衡：仅训练修复可将 pass@1 从 27.4% 提升到 31.2%，但联合训练产生的解释本身具有很高的下游价值——DeepSeek 使用训练后 Qwen 的解释时成功率为 29%，远高于使用基线 Qwen 解释的 4%。
查看结构化数据
| 任务 | 指标 | 本文 | 基线 | 提升 |
|---|---|---|---|---|
| 全类型证明修复（单次修复） | Pass@1 编译成功率 | Finetuned Qwen3-4B: 27.4% | Base Qwen3-4B: 1.1% | 提升 26.3 个百分点（约 25 倍） |
| 全类型证明修复（单次修复） | Pass@1 编译成功率 | Finetuned Goedel-8B: 34.6% | Goedel-Prover-V2-32B: 26.8% | 8B 模型超越 32B 基线 7.8 个百分点 |
| 策略变异修复 | Pass@1 编译成功率 | Finetuned Qwen3-4B: 39.7% | Base Qwen3-4B: 1.8% | 提升 37.9 个百分点 |
| 定理变异修复 | Pass@1 编译成功率 | Finetuned Qwen3-4B: 26.8% | Base Qwen3-4B: 0.5% | 提升 26.3 个百分点 |
| 行级变异修复 | Pass@1 编译成功率 | Finetuned Qwen3-4B: 16.0% | Base Qwen3-4B: 2.5% | 提升 13.5 个百分点 |
| 多行变异修复 | Pass@1 编译成功率 | Finetuned Qwen3-4B: 13.2% | Base Qwen3-4B: 0.0% | 从 0% 提升到 13.2% |
| 解释辅助 DeepSeek 修复 | 修复成功率 | 用训练后 Qwen 解释: 29% | 用基线 Qwen 解释: 4% | 提升 25 个百分点 |
局限与改进
本文存在若干值得关注的局限性。首先，APRIL 数据集中的错误是通过系统性变异从正确证明「逆向」生成的，而非来自真实的人类证明开发过程。虽然变异策略设计得尽可能真实（如定理替换使用语义搜索、行级替换用 LLM 生成），但这些合成错误是否完全代表人类在实际证明开发中遇到的错误模式，仍存在不确定性。其次，评估采用严格的单次修复设置（无搜索、无迭代），这虽然能隔离模型的反馈利用能力，但与实际 agentic 证明系统的工作方式差距较大——后者通常使用多轮迭代和搜索策略，效率比 pass@k 高 32-128 倍。因此，27.4% 的单次修复准确率并不能直接代表在实际系统中的贡献。第三，微调仅使用了 LoRA 适配器，虽然高效但可能限制了模型的学习容量；更大规模的全参数微调的效果尚未探索。第四，数据集的多样性受限于三个源数据集的覆盖范围——Herald 来自 mathlib4 的中间状态、Lean Workbook 是机器生成的简短证明、Numina 包含自动形式化和人类标注，但整体上仍以数学定理为主，可能不涵盖其他形式化领域的错误模式。第五，解释质量的评估主要通过下游修复任务间接验证，缺乏独立的人类评估来衡量解释的准确性、完整性和可理解性。
独立分析的弱点
本文的一个明显弱点是变异策略虽然系统化但仍然是合成的，与真实人类错误之间存在分布差异。例如，定理替换变异只做单次替换，而人类可能同时犯多处错误或产生语义上的根本性误解；行级和多行替换依赖 DeepSeek-V3 生成「看似合理但错误」的步骤，但 LLM 的错误模式可能与人类证明者的错误模式有本质不同。改进方向包括：(1) 收集真实的人类证明开发轨迹（如从 IDE 日志或教学场景中提取），作为合成数据的补充；(2) 引入更复杂的变异组合，如同时进行多处变异以模拟人类的「系统性误解」。另一个弱点是模型仅在单次修复设置下评估，缺乏与迭代修复管线的集成实验。实际上，修复能力的真正价值在于嵌入到 agentic 系统中进行多轮迭代，但论文未展示这种集成效果。此外，微调数据的规模（260K 条）虽然不小，但考虑到错误类型的多样性，特定类型（如行级变异仅占较小比例）的样本量可能不足以让模型充分学习。
未来方向
作者在论文中将诊断条件监督定位为反馈利用型证明器的互补训练信号，暗示未来可以将 APRIL 训练的修复模型集成到迭代证明生成管线中。基于本文成果，几个有前景的研究方向包括：(1) 将修复模型嵌入到 agentic 证明系统中，作为「修复代理」与「生成代理」协作，实现真正的迭代证明细化——这与 Chen et al. (2025) 展示的 32-128 倍效率提升直接相关；(2) 探索修复能力与端到端证明生成的联合训练，让模型在训练时既学习从零构建证明，也学习从错误中恢复，可能产生更强的证明能力；(3) 将本文方法扩展到其他证明助手（如 Coq、Isabelle、Agda），构建跨系统的修复训练数据；(4) 研究解释能力的进一步提升，例如通过强化学习让模型学会生成更有助于人类理解或下游系统利用的诊断；(5) 探索在更大规模模型（如 70B+）上进行全参数微调的效果，当前 LoRA 微调可能未充分利用 260K 条数据的信息量。
复现评估
本文的复现性评估相当积极。数据方面，APRIL 数据集已在 HuggingFace 开源（uw-math-ai/APRIL），包含 260,125 条有监督样本，每条都有完整的错误证明、编译器反馈、正确修复和自然语言解释。模型方面，微调后的模型也已开源——带解释版本（uw-math-ai/gAPRIL-w-exp）和不带解释版本（uw-math-ai/gAPRIL-wo-exp）。算力方面，实验在 NVIDIA L40S 和 H200 GPU 上完成，使用 bfloat16 精度和 FlashAttention-2，对于 4B 和 8B 模型的 LoRA 微调，算力需求相对适中。数据构建管线依赖 Lean-Interact 与 Lean REPL 交互、LeanExplore 语义搜索引擎和 DeepSeek-V3-0324 生成注释，这些工具和 API 的可用性是复现的关键依赖。训练超参数（LoRA 秩 32、学习率 $1 \times 10^{-4}$、批量大小 8、最大 15,000 步）已详细报告。总体而言，在具备相应 GPU 资源和 Lean 环境的条件下，复现难度为中等偏低。
论文图表
