Fix, Not Just Resample: Bounded Compiler-Guided Repair in Lean 4 研究提出有界编译器引导修复机制

针对Lean 4证明助手，引入有界在线步骤级修复模块，利用编译器错误信息就地修复被拒战术。 在LeanDojo基准的1990个定理子集上，该方法在K∈{1,3,5,8}所有候选预算下提升解题率，最高相对增益达32%，额外解决82个定理。 修复收益前置，首次尝试捕获84%--96%总增益；在Lean Workbook基准上近乎翻倍解题率且无回归。