修复而非单纯重采样：Lean 4 中受限的编译器引导修复机制

研究者提出一种用于 Lean 4 的在线步级修复模块，通过将编译器报错反馈给预训练修复模型来就地修正失败策略，而非直接丢弃。在包含 1,990 个定理的 LeanDojo 子集上，该方法相比纯采样基线实现最高 32% 的相对提升并多证明 82 个定理，且首次修复尝试即贡献了 84–96% 的总收益。该方法在 Lean Workbook 基准上同样成功复现，使求解率接近翻倍且零回归。