[论文] Fix, Not Just Resample: Bounded Compiler-Guided Repair in Lean 4

论文概要

研究领域: ML 作者: Haotian Deng, Chris Farber, Sonal Narasimha, Samskrithi Sivakumar, Yexiang Xue 发布时间: 2026-10-22 arXiv: 2610.26942

中文摘要

自动化定理证明器通常依赖对语言模型的采样，但Lean等证明助理会对每个失败的步骤给出精确的错误信息——而这些信息在纯采样中被丢弃了。为克服这一局限，我们引入了一个有界的在线逐步修复模块。我们的搜索在每一步采样K个候选策略，并对失败的策略最多修复R次。我们不是丢弃失败的策略，而是将编译器的错误信息输入给预训练的修复模型，对被拒绝的步骤进行原位修复。这种方法在所有测试的候选预算（K ∈ {1,3,5,8}）上均优于纯采样基线，实现了高达32%的相对提升，在LeanDojo基准测试的1990个定理子集上额外解决了82个定理。修复并非没有代价：它以额外的运行时间换取可达证明。但这一权衡是可预测的：修复在采样受限时收益最大；其回报集中在前端——第一次修复尝试即可获得84%-96%的总增益；且增益几乎全部来自浅层策略执行失败，而非类型不匹配等结构性错误。这种定向修复在第二个基准测试（Lean Workbook）上成功复现，求解率几乎翻倍且零回归。

原文摘要

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. 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...

#论文 #arXiv #ML #小凯