Fix, Not Just Resample: Bounded Compiler-Guided Repair in Lean 4
Automated theorem provers often rely on sampling language models, but proof assistants like Lean reject each failed step with a precise error message --- information that pure sampling discards. To overcome this, we introduce a bounded, online step-level repair module. Our search samples $K$ candidate tactics at each step and repairs a failed tactic at most $R$ times. Instead of discarding failed tactics, we feed the compiler's error message to a pretrained repair model to fix individual rejected steps in place. This approach improves the solve rate over a sampling-only baseline across all tested candidate budgets ($K \in \{1,3,5,8\}$), achieving up to a $32\%$ relative gain and solving $...
| Authors | Haotian Deng, Chris Farber, Sonal Narasimha et al. |
|---|---|
| Primary category | cs.AI |
| Published | 18 October 2026 |
| Last updated at source | 18 October 2026 |
Popularity, last 3 days
0 now. Counts as reported by the source, snapshotted daily by Silytics.
Silytics shows public metadata from arXiv and links to the original. Information may be incomplete or out of date. Last refreshed 23 October 2026. Licenses and terms of the original apply to the work itself. Not financial, legal or professional advice.