自动定理证明器常通过采样语言模型生成策略，但交互式证明助理如 Lean 在每一步失败时会给出精确的错误信息，而纯采样会忽略这些信息。为此我们提出一种有界、在线的逐步修复模块。搜索在每一步采样 $K$ 个候选 tactic，并最多对同一步进行 $R$ 次修复。我们不丢弃失败的 tactic，而是将编译器的错误信息送入预训练的修复模型，对被拒的步骤就地修正。实验表明，在所有候选预算 $K\in\{1,3,5,8\}$ 下，该方法相较仅采样的基线提升了解题率，最高相对增益 $32\%$，在 1990 条 LeanDojo 子集上额外解决了 82 条定理。修复并非免费：它以额外运行时间换取可达的证明，但这种权衡是可预测的——当采样受限时修复收益最大，收益前置，首次修复尝试捕获了总增益的 $84\text{--}96\%$，且收益几乎全部来源于浅层 tactic 执行失败，而非类型不匹配等结构性错误。该针对性修复在第二个基准（Lean Workbook）上同样成功，解题率几乎翻倍且没有回退。
点评