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

研究者提出一种在 Lean 4 中结合编译器报错信息的在线单步受限修复模块，通过预训练修复模型就地修正失败策略而非直接丢弃。在 LeanDojo 基准 1,990 个定理子集上，该方法相比纯采样基线取得最高 32% 的相对提升并多解决 82 个定理，首轮修复即可贡献 84%–96% 的收益。该方案在 Lean Workbook 基准上同样实现解题率接近翻倍且无性能回退。