Fix, Not Just Resample: Bounded Compiler-Guided Repair in Lean 4

Computer Science > Artificial Intelligence arXiv:2610.26942 (cs) [Submitted on 18 Oct 2026] Title:Fix, Not Just Resample: Bounded Compiler-Guided Repair in Lean 4 Authors:Haotian Deng, Chris Farber, Sonal Narasimha, Samskrithi Sivakumar, Yexiang Xue View a PDF of the paper titled Fix, Not Just Resample: Bounded Compiler-Guided Repair in Lean 4, by Haotian Deng and 4 other authors View PDF HTML (experimental)

计算机科学 > 人工智能 arXiv:2610.26942 (cs) [提交于 2026 年 10 月 18 日] 标题：修复，而非仅仅重采样：Lean 4 中有界编译器引导的修复 作者：Haotian Deng, Chris Farber, Sonal Narasimha, Samskrithi Sivakumar, Yexiang Xue 查看标题为《修复，而非仅仅重采样：Lean 4 中有界编译器引导的修复》的论文 PDF，作者为 Haotian Deng 及其他 4 位作者 查看 PDF HTML（实验性）

Abstract:Automated theorem provers often rely on sampling language models, but proof assistants like Lean reject each failed step with a precise error message --- information that pure sampling discards. To overcome this, we introduce a bounded, online step-level repair module. Our search samples $K$ candidate tactics at each step and repairs a failed tactic at most $R$ times. Instead of discarding failed tactics, we feed the compiler’s error message to a pretrained repair model to fix individual rejected steps in place.

摘要：自动定理证明器通常依赖于对语言模型进行采样，但像 Lean 这样的证明助手会通过精确的错误消息拒绝每一个失败的步骤——而纯采样会丢弃这些信息。为了克服这一点，我们引入了一个有界的、在线的步骤级修复模块。我们的搜索在每一步采样 $K$ 个候选策略，并对失败的策略最多修复 $R$ 次。我们没有丢弃失败的策略，而是将编译器的错误消息输入到一个预训练的修复模型中，以原地修复被拒绝的单个步骤。

This approach improves the solve rate over a sampling-only baseline across all tested candidate budgets ($K \in {1,3,5,8}$), achieving up to a $32%$ relative gain and solving $82$ additional theorems on a $1{,}990$-theorem subset of the LeanDojo benchmark. Repair is not free: it trades extra runtime for reachable proofs. But the trade is predictable: repair pays most when sampling is constrained; its return is front-loaded, with the first repair attempt capturing $84\text{—}96%$ of the total gain; and the gain comes almost entirely from shallow tactic-execution failures rather than structural errors such as type mismatches.

这种方法在所有测试的候选预算（$K \in {1,3,5,8}$）下，相比仅采样的基准提高了求解率，实现了高达 $32%$ 的相对增益，并在 LeanDojo 基准测试的 $1{,}990$ 个定理子集中额外解决了 $82$ 个定理。修复并非没有代价：它以额外的运行时间换取可达到的证明。但这种权衡是可预测的：当采样受限时，修复的收益最大；其回报是前置的，第一次修复尝试就获得了总增益的 $84\text{—}96% $；且增益几乎完全来自浅层的策略执行失败，而非类型不匹配等结构性错误。

This targeted repair successfully replicates on a second benchmark (Lean Workbook), nearly doubling the solve rate with zero regressions. Subjects: Artificial Intelligence (cs.AI) Cite as: arXiv:2610.26942 [cs.AI] (or arXiv:2610.26942v1 [cs.AI] for this version)

这种针对性修复在第二个基准测试（Lean Workbook）上成功复现，求解率几乎翻倍且零回归。学科：人工智能 (cs.AI) 引用方式：arXiv:2610.26942 [cs.AI]（或此版本的 arXiv:2610.26942v1 [cs.AI]）