Technical Summary: Risk-Controlled Lean-as-Judge for Natural-Language Mathematical Reasoning

1. Problem Statement

The paper addresses the challenge of using formal proof assistants (specifically Lean) as judges for natural-language mathematical reasoning generated by Large Language Models (LLMs). While a successful Lean proof provides strong positive evidence for a formal statement, the absence of a proof is an ambiguous signal. A failed proof may indicate a mathematically incorrect answer, but it may equally result from an ill-typed formalization, missing library facts, or proof-search timeouts.

Current approaches often treat proof failure as a negative correctness signal, risking the conflation of mathematical incorrectness with a lack of formal coverage. The authors identify a "coverage cliff": the reliability of formal selection is sharply dependent on the proportion of candidate answers that can be successfully formalized and proved. When coverage is high, formal selection is highly accurate; when coverage is low, the signal becomes unreliable.

The core problem is to determine when a downstream system should trust a formal Lean signal and when it should treat the signal as out-of-coverage (i.e., unresolved) rather than incorrect, while providing a finite-sample risk guarantee for the accepted answers.

2. Methodology: COVCAL

The authors propose COVCAL (Coverage-Calibrated Lean), a risk-controlled selective wrapper that decides whether to accept a formal answer or abstain based on coverage diagnostics.

2.1 Partial Observation Framework

The system treats the formal pipeline as a partial observation mechanism. It does not observe the truth of every candidate answer but only observes:

1. Which normalized answer classes reach a well-formed Lean statement (Typed Coverage).
2. Which of those classes are successfully proved (Proved Coverage).
3. The weight of the highest-weight proved class versus the highest-weight unresolved rival (Formal Margin).

An answer class is defined as a group of candidate strings denoting the same final answer (e.g., $1/2$, $0.5$, $2/4$). Classes that are not formalized or not proved are considered unresolved, not automatically wrong.

2.2 Coverage Diagnostics

COVCAL computes four key metrics for a given problem $x$:

• Typed Coverage ($C_{typ}$): The total weight of candidate classes that reached a well-formed Lean statement (status: proved, typechecked, or timeout).
• Proved Coverage ($C_{prf}$): The total weight of candidate classes that received a kernel-checked proof.
• Unresolved Rival Mass ($R_{unres}$): The weight of the highest-weight answer class that was not proved.
• Formal Margin ($M$): The difference between the weight of the highest-weight proved class and the unresolved rival mass.

2.3 Selection and Certification

COVCAL accepts the highest-weight proved class only if a pre-declared rule based on thresholds $(\tau_{typ}, \tau_{prf}, \tau_M)$ is satisfied. If the rule is not met, the system abstains (or falls back to a non-formal method like self-consistency).

To ensure reliability, COVCAL employs finite-sample selective-risk certification. It guarantees that, with probability $1-\delta$, the selective risk (error rate) of accepted answers is at most $\epsilon$. Two certification regimes are proposed:

1. Bonferroni Regime: Searches over a grid of thresholds on a calibration split and applies a union-bound correction ($\delta/|T|$) to account for the multiple comparisons. This is conservative and requires high signal density to be feasible.
2. Dev-then-Cal Regime: Selects the threshold on an independent development split and certifies it once on the calibration split using a single Clopper-Pearson bound ($\delta$). This is more sample-efficient but requires strict separation between development and calibration data.

2.4 Theoretical Limits

The paper proves that without coverage diagnostics (i.e., relying solely on the existence of a proof), no non-vacuous pointwise correctness certificate can be derived if an unresolved, inequivalent rival class exists. Missing formal evidence is not evidence of mathematical falsehood; it is evidence of unresolved status.

3. Key Contributions

1. Coverage Cliff Characterization: On the MATH-500 dataset, the authors demonstrate that the "proof-winning" answer is correct 96% of the time at high proved coverage but only 20% at low coverage. This establishes that Lean proofs are reliable only when coverage and margin are high.
2. Signal Sparsity and Faithfulness: The formal signal is sparse and imperfect. A 7B auto-formalizer proves a class for only 28% of problems. Furthermore, a manual audit reveals that only $\approx 43\%$ of these proofs are faithful to the original problem (the rest are trivial identities or true-but-irrelevant statements).
3. COVCAL Method: A selective prediction framework that certifies risk under partial observation. It explicitly handles the asymmetry of proof failure and provides finite-sample guarantees for accepted predictions.
4. Formalizer-Dependent Feasibility: The paper demonstrates that certificate feasibility is governed by auto-formalization coverage. A 7B formalizer yields a signal too sparse for the conservative Bonferroni regime (rejecting all 20 bootstrap partitions), whereas a prover-specialized formalizer (Goedel-Prover-V2-8B) achieving 79% coverage makes the method feasible on 17/20 partitions.

4. Experimental Results

Experiments were conducted on a filtered subset of MATH-500 (378 examples) using Qwen2.5-Math-7B for generation and various formalizers for auto-formalization.

• Baseline Performance: Self-consistency alone achieves 91% accuracy without abstention.
• COVCAL Performance:
  • Under the Bonferroni regime with a 7B formalizer, the method rejects all inputs (0/20 partitions) because the signal is too sparse to satisfy the strict union bound.
  • Under the dev-then-cal regime with the 7B formalizer, 12/20 partitions are certified. The accepted fraction is $\approx 21\%$, with an accepted accuracy of 0.93.
  • With the Goedel-Prover-V2-8B (specialized formalizer), proved coverage rises to 79%. Bonferroni becomes feasible on 17/20 partitions, accepting $\approx 48\%$ of problems with 0.98 accepted accuracy.
• Faithfulness Audit: A manual audit of 45 stratified examples showed that while 73.6% of proved statements were non-trivial and correct, only 43% were faithful to the problem statement. Many "proved" statements were true side-facts or trivial identities that did not capture the problem's constraints.

5. Significance and Claims

The paper claims that its primary contribution is a precise account of when and with which formalizer a partial formal signal can be trusted under risk control, rather than simply improving raw accuracy.

• Risk Control over Raw Accuracy: Since self-consistency is already 91% accurate, the value of COVCAL lies in its ability to provide a certificate for the subset of answers it accepts, distinguishing between "verified" and "unresolved" rather than "correct" and "incorrect."
• Handling Partial Observations: The work reframes formal verification as a selective prediction problem where missing proofs are treated as unresolved candidates, preventing the mislabeling of correct reasoning as incorrect due to formalization failures.
• Dependency on Specialization: The results highlight that raw model scale is not a substitute for specialization. A prover-specialized formalizer significantly outperforms a larger generalist model in terms of proving coverage, which is the binding constraint for certifiable risk control.

The authors conclude that COVCAL serves as a conservative interface for using Lean as a judge: it is feasible and informative only when the auto-formalizer covers enough answer mass to support a risk certificate, but it does not guarantee that all answers are verified.