Risk-Controlled Lean-as-Judge for Natural-Language Mathematical Reasoning
For researchers using formal verifiers to judge natural-language reasoning, this paper provides a precise, risk-controlled method to trust partial formal signals, but its feasibility depends heavily on autoformalization coverage.
The paper shows that Lean's signal for judging natural-language math answers is coverage-dependent and often unfaithful, and proposes COVCAL, a risk-controlled selector that certifies a bound on accepted accuracy. With a prover-specialized formalizer reaching 79% coverage, COVCAL accepts ~48% of problems at 0.98 accuracy, whereas a 7B formalizer's sparse signal makes the approach infeasible.
Lean is increasingly used to judge natural-language mathematical answers, but its signal is partial: many answers never formalize, and a failed proof may reflect an ill-typed statement or a missing library fact, not a wrong answer. On MATH-500 we show this signal is (i) sharply coverage-dependent, that is the proof-winning answer is correct 96% of the time at high proved coverage but 20% at low, and (ii) sparse and often unfaithful: a 7B autoformalizer proves a class for only 28% of problems, and a manual audit finds only approximately 43% of those proofs faithful. We propose COVCAL, a selector over Lean-trace diagnostics that certifies a finite-sample selective-risk bound on accepted answers or abstains, under two regimes (a conservative Bonferroni bound and a tighter dev-then-cal rule). Feasibility depends on autoformalization coverage: with the 7B formalizer the signal is too sparse and Bonferroni abstains on all 20 bootstrap partitions, whereas a prover-specialized formalizer reaches 79% coverage and flips it to feasible on 17 of 20, accepting approximately 48% of problems at 0.98 accepted accuracy. Since self-consistency alone is already 91% accurate, our contribution is a precise account of when, and with which formalizer, a partial formal signal can be trusted under risk control.