RESEARCH · RESEARCH · #2330
Bounded compiler-guided repair improves tactic-level proof search in Lean 4
The paper introduces a bounded, online step-level repair that samples K candidate tactics per proof step and, when a tactic is rejected, feeds the compiler error message to a pretrained repair model to fix that step in place up to R times. On a 1,990-theorem subset of the LeanDojo benchmark the method yields up to a 32% relative improvement (82 additional theorems solved) across tested K∈{1,3,5,8}, replicates on the Lean Workbook benchmark (nearly doubling solve rate), and shows gains concentrate on shallow tactic-execution failures at the expense of predictable extra runtime.
KEY POINTS
- The paper introduces a bounded, online step-level repair that samples K candidate tactics per proof step and, when a tactic is rejected, feeds the compiler error message to a pretrained repair model to fix that step in place up to R times.
- On a 1,990-theorem subset of the LeanDojo benchmark the method yields up to a 32% relative improvement (82 additional theorems solved) across tested K∈{1,3,5,8}, replicates on the Lean Workbook benchmark (nearly doubling solve rate), and shows gains concentrate on shallow tactic-execution failures at the expense of predictable extra runtime.
- Shows that feeding compiler error messages into a targeted repair model significantly raises LM-driven proof assistant solve rates—especially when sampling is limited—by fixing rejected tactic executions in place.
WHY IT MATTERS
Shows that feeding compiler error messages into a targeted repair model significantly raises LM-driven proof assistant solve rates—especially when sampling is limited—by fixing rejected tactic executions in place.