Fix, Not Just Resample: Bounded Compiler-Guided Repair in Lean 4
This work introduces a bounded, online step-level repair module that feeds the compiler's error message to a pretrained repair model to fix individual rejected steps in place and improves the solve rate over a sampling-only baseline across all tested candidate budgets.
Hao-Tian Deng, Chris Farber, Sonal Narasimha et al.
· 0 citations