Risk-Controlled Lean-as-Judge for Natural-Language Mathematical Reasoning

• URL: http://arxiv.org/abs/2605.28365v1
• Date: Wed, 27 May 2026 11:59:28 GMT
• Title: Risk-Controlled Lean-as-Judge for Natural-Language Mathematical Reasoning
• Abstract summary: Lean is increasingly used to judge natural-language mathematical answers, but its signal is partial.<n>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.<n>A 7B autoformalizer proves a class for only 28% of problems, and a manual audit finds only approximately 43% of those faithful.<n>We propose COVCAL, a selector over Lean-trace diagnostics that certifies a finite-sample selective-risk bound on accepted answers or abstains.
• Score: 16.398764816978584
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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.

Related papers

• Rethinking LLM Verification: Evidence Structure, Uncertainty, and Selective Refinement [8.78288626457356]
  We propose a two-stage framework for medical hypothesis verification in multiple-choice settings.<n>We show that abstention is not random but reflects genuine uncertainty, with abstained predictions associated with lower confidence.<n>Our experiments conducted on MedReason and MedQA show that abstention can be repurposed as a control signal for selective reasoning refinement.
  arXiv  Detail & Related papers  (2026-08-11T09:43:14Z)
• Cross-Fitted Residual Utility for Primary-Preserving Cognitive Decision Correction in Automatic Modulation Classification [1.547549252134621]
  We study a post-inference problem through cross-fitted residual utility and a primary-preserving cognitive decision policy.<n>A structured KAN-Fourier classifier supplies the default probability, while neural and non-neural candidates provide observable evidence.<n>On RMLA, RMLB, and HISAR, the complete system improves overall accuracy from 63.632% to 66.332%, 65.161% to 66.168%, and 77.769% to 79.867%.
  arXiv  Detail & Related papers  (2026-08-03T11:07:37Z)
• Theoria: Rewrite-Acceptability Verification over Informal Reasoning States [0.0]
  We present Theoria, a verification architecture that closes this gap.<n>A candidate solution is rewritten into a sequence of typed state transitions.<n>Every transition is independently auditable.
  arXiv  Detail & Related papers  (2026-07-01T17:56:42Z)
• When Confidence Takes the Wrong Path: Diagnosing Retrieval-State Lock-In in RAG [0.0]
  Many black-box uncertainty methods still read agreement among sampled answers as confidence.<n>The problem is recognised in deployed RAG, but it has lacked a name, a measurable signature, and a prevalence bound.<n>We name the failure retrieval-state lock-in and diagnose it by separating the three objects a single confidence score conflates.
  arXiv  Detail & Related papers  (2026-06-22T00:08:00Z)
• Geometry-Calibrated Conformal Abstention for Language Models [25.731621771885887]
  Retraining models to reward admitting ignorance can lead to overly conservative behaviors.<n>We propose a post hoc framework, Conformal Abstention (CA), adapted from conformal prediction (CP) to determine whether to abstain from answering a query.
  arXiv  Detail & Related papers  (2026-04-30T14:20:16Z)
• Causal-Audit: A Framework for Risk Assessment of Assumption Violations in Time-Series Causal Discovery [1.7192141121569653]
  Causal-Audit is a framework that formalizes assumption validation as calibrated risk assessment.<n>The framework computes effect-size diagnostics across five assumption families.<n>It applies an abstention-aware decision policy that recommends methods only when evidence supports reliable inference.
  arXiv  Detail & Related papers  (2026-04-02T19:43:57Z)
• When Chain-of-Thought Backfires: Evaluating Prompt Sensitivity in Medical Language Models [2.064612766965483]
  We evaluate MedGemma (4B and 27B parameters) on MedMCQA (4,183 questions) and PubMedQA (1,000 questions)<n>Our experiments reveal several concerning findings.
  arXiv  Detail & Related papers  (2026-03-26T23:04:20Z)
• LEC: Linear Expectation Constraints for False-Discovery Control in Selective Prediction and Routing Systems [95.35293543918762]
  Large language models (LLMs) often generate unreliable answers, while uncertainty methods fail to fully distinguish correct from incorrect predictions.<n>We address this issue through the lens of false discovery rate (FDR) control, ensuring that among all accepted predictions, the proportion of errors does not exceed a target risk level.<n>We propose LEC, which reinterprets selective prediction as a constrained decision problem by enforcing a Linear Expectation Constraint.
  arXiv  Detail & Related papers  (2025-12-01T11:27:09Z)
• CGES: Confidence-Guided Early Stopping for Efficient and Accurate Self-Consistency [3.2807118426157493]
  Large language models (LLMs) are often queried multiple times at test time, with predictions aggregated by majority vote.<n>We introduce Confidence-Guided Early Stopping (CGES), a Bayesian framework that forms posteriors over candidate answers.<n>CGES adaptively halts sampling once the posterior mass of a candidate exceeds a threshold.
  arXiv  Detail & Related papers  (2025-11-04T14:25:54Z)
• CLUE: Non-parametric Verification from Experience via Hidden-State Clustering [64.50919789875233]
  We show that correctness of a solution is encoded as a geometrically separable signature within the trajectory of hidden activations.<n>ClUE consistently outperforms LLM-as-a-judge baselines and matches or exceeds modern confidence-based methods in reranking candidates.
  arXiv  Detail & Related papers  (2025-10-02T02:14:33Z)
• Selective Risk Certification for LLM Outputs via Information-Lift Statistics: PAC-Bayes, Robustness, and Skeleton Design [6.908972852063454]
  We develop information-lift certificates that compare model probabilities to a skeleton baseline, accumulating evidence into PAC-Bayes valid under heavy-tailed bounds.<n>Across eight datasets, our method achieves 77.2% coverage at 2% risk, outperforming recent 2023-2024 baselines by 8.6-15.1 percentage points.
  arXiv  Detail & Related papers  (2025-09-16T00:05:54Z)
• COIN: Uncertainty-Guarding Selective Question Answering for Foundation Models with Provable Risk Guarantees [51.5976496056012]
  COIN is an uncertainty-guarding selection framework that calibrates statistically valid thresholds to filter a single generated answer per question.<n>COIN estimates the empirical error rate on a calibration set and applies confidence interval methods to establish a high-probability upper bound on the true error rate.<n>We demonstrate COIN's robustness in risk control, strong test-time power in retaining admissible answers, and predictive efficiency under limited calibration data.
  arXiv  Detail & Related papers  (2025-06-25T07:04:49Z)
• Exploring Response Uncertainty in MLLMs: An Empirical Evaluation under Misleading Scenarios [49.53589774730807]
  Multimodal large language models (MLLMs) have recently achieved state-of-the-art performance on tasks ranging from visual question answering to video understanding.<n>We reveal a response uncertainty phenomenon: twelve state-of-the-art open-source MLLMs overturn a previously correct answer in 65% of cases after receiving a single deceptive cue.
  arXiv  Detail & Related papers  (2024-11-05T01:11:28Z)
• Improving Selective Visual Question Answering by Learning from Your Peers [74.20167944693424]
  Visual Question Answering (VQA) models can have difficulties abstaining from answering when they are wrong. We propose Learning from Your Peers (LYP) approach for training multimodal selection functions for making abstention decisions. Our approach uses predictions from models trained on distinct subsets of the training data as targets for optimizing a Selective VQA model.
  arXiv  Detail & Related papers  (2023-06-14T21:22:01Z)
• Reliable Visual Question Answering: Abstain Rather Than Answer Incorrectly [100.60560477391732]
  We promote a problem formulation for reliable visual question answering (VQA) We analyze both their coverage, the portion of questions answered, and risk, the error on that portion. We find that although the best performing models achieve over 71% accuracy on the VQA v2 dataset, introducing the option to abstain limits them to answering less than 8% of the questions to achieve a low risk of error (i.e., 1%) This motivates us to utilize a multimodal selection function to directly estimate the correctness of the predicted answers, which we show can triple the coverage from, for example, 5.0% to 16.7% at
  arXiv  Detail & Related papers  (2022-04-28T16:51:27Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.