Paper Overview
Field: ML Authors: Haotian Deng, Chris Farber, Sonal Narasimha, Samskrithi Sivakumar, Yexiang Xue Published: 2026-10-22 arXiv: 2610.26942
Summary
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, the authors introduce a bounded, online step-level repair module. The search samples \(K\) candidate tactics at each step and repairs a failed tactic at most \(R\) times. Instead of discarding failed tactics, the compiler's error message is fed to a pretrained repair model to fix individual rejected steps in place.
Key Results
- Consistent improvement: Outperforms a sampling-only baseline across all tested candidate budgets (\(K \in \{1,3,5,8\}\)), with up to a 32% relative gain and 82 additional theorems solved on a 1,990-theorem subset of the LeanDojo benchmark.
- Front-loaded returns: The first repair attempt captures 84%-96% of the total gain.
- Best under constrained sampling: Repair yields the largest benefit when the sampling budget is limited.
- Error-type analysis: Gains come almost entirely from shallow tactic execution failures, not structural errors such as type mismatches.
- Cost trade-off: Repair trades extra runtime for reachable proofs, and this trade-off is predictable.
- Replication: The targeted repair approach was validated on a second benchmark (Lean Workbook), nearly doubling the solve rate with zero regressions.
Original Abstract (excerpt)
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 $82$ additional theorems on a \(1{,}990\)-theorem subset of the LeanDojo benchmark. Repair is not free...
---
*Auto-collected on 2026-10-22*