修复而非仅重采样：Lean 4 中有界的编译器引导证明修复方法

论文提出一种有界的在线步级修复模块，在 Lean 4 自动定理证明中不再丢弃失败的 tactic，而是把编译器错误信息喂给预训练修复模型原位修复。该方法在 LeanDojo 基准 1,990 题子集上相对纯采样基线最多提升 32%，多解出 82 题且在 K∈{1,3,5,8} 各预算下均有效；首次修复尝试即贡献 84–96% 的总增益，并在 Lean Workbook 上近乎翻倍解题率且零回退。