Source-linked AI summary
When to Trust the Cheap Check: Weak and Strong Verification for Reasoning
Shayan Kiyani, Sima Noorani, George Pappas, Hamed Hassani
TL;DR
LLM reasoning systems need a way to balance costly, trusted strong verification against fast but imperfect weak checks. The paper formalizes selective deferral and develops an online algorithm with error-control guarantees; its analysis identifies a two-threshold policy structure and properties that govern weak-verifier effectiveness.
Problem
Method
The paper formalizes weak–strong verification policies and develops an online algorithm that controls type-I and type-II errors without assumptions on the query stream, language model, or weak verifier.
Source: §1 · p. 2Results
Population-optimal policies have a two-threshold structure, while calibration and sharpness govern weak-verifier effectiveness; SSV maintains target error rates in finite samples and achieves near-oracle accuracy with significantly fewer costly calls.
Source: §1 · p. 2Takeaways & Limitations
The framework achieves reasoning performance comparable to always applying strong verification while querying the strong verifier only a small fraction of the time.
Source: §7 · p. 13Strong-verification decisions depend only on the weak score, so the guarantees control type-I and type-II errors marginally, averaged over rounds.
Source: §7 · p. 13
Abstract
from arXiv · showhide
Reasoning with LLMs increasingly unfolds inside a broader verification loop. Internally, systems use cheap checks, such as self-consistency or proxy rewards, which we call weak verification. Externally, users inspect outputs and steer the model through feedback until results are trustworthy, which we call strong verification. These signals differ sharply in cost and reliability: strong verification can establish trust but is resource-intensive, while weak verification is fast and scalable but noisy and imperfect. We formalize this tension through weak--strong verification policies, which decide when to accept or reject based on weak verification and when to defer to strong verification. We introduce metrics capturing incorrect acceptance, incorrect rejection, and strong-verification frequency. Over population, we show that optimal policies admit a two-threshold structure and that calibration and sharpness govern the value of weak verifiers. Building on this, we develop an online algorithm that provably controls acceptance and rejection errors without assumptions on the query stream, the language model, or the weak verifier.
1 Introduction
The paper frames reasoning as a verification problem: strong checks can establish trust but are costly, while scalable weak checks are imperfect. It formalizes when to trust weak signals or defer to strong verification, then develops and evaluates an online algorithm for controlling verification errors.
1 Introduction
- Strong verification evaluates outputs using user context and domain knowledge, while weak verification uses fast, scalable checks that approximate user judgments.Weak checks may certify narrow aspects of an output without judging whether the overall reasoning is promising.Source: §1 · pp. 1–2
- The framework addresses how to match the reliability of strong verification while applying it to only a small, carefully chosen fraction of reasoning.The paper identifies orchestration of verification sources as the missing capability.Source: §1 · p. 2
- Weak–strong policies choose when to accept or reject using only a weak verifier and when to defer to a strong verifier, with errors and strong-verification frequency capturing the tradeoffs.Type-I error is incorrect acceptance, and type-II error is incorrect rejection.Source: §1 · p. 2
- Population-optimal policies have a two-threshold structure, and calibration and sharpness govern weak-verifier effectiveness.This structure underpins the paper’s algorithm.Source: §1 · p. 2
- SSV provably controls type-I and type-II errors without assumptions on the query stream, language-model behavior, or weak-verifier quality.The paper evaluates this algorithm on outcome-level mathematical reasoning and process-level sequential puzzle solving.Source: §1 · p. 2
- SSV maintains target error rates in finite samples while achieving near-oracle accuracy with significantly fewer costly calls.The evaluation covers outcome-level mathematical reasoning and process-level sequential puzzle solving.Source: §1 · p. 2
2 Related Works
Prior work improves either reasoning procedures or weak-verification signals, while this paper studies how to orchestrate verification sources. Its setup also relates to selective prediction and learning-to-defer.
2 Related Works
- Reasoning-process research improves inference-time reasoning or training, generally treating weak signals as fixed.Examples include structured prompting [29] [34], search [31] [32], decoding strategies [30], and training approaches [22] [27].Source: §2 · p. 3
- Weak-verification research improves the signal itself, whereas this work takes the verifier and reasoning procedure as fixed and studies when to trust or defer.The framework is described as applying across reasoning procedures and scoring models.Source: §2 · p. 3
- The setup is an instance of learning-to-defer in which deferral means invoking strong verification, with distribution-free online calibration and separate Type-I/II error control.The authors identify this combination, alongside partial feedback, as potentially relevant to the broader learning-to-defer literature.Source: §2 · p. 3
3 Weak–Strong Verification Policies and Metrics
The section defines a sequential setting in which a weak score guides decisions to accept, reject, or call a strong verifier. It measures incorrect acceptance, incorrect rejection, and verification frequency, exposing a tradeoff among output quality, latency, and cost.
3 Weak–Strong Verification Policies and Metrics
- The strong verifier gives a binary correctness judgment, while the weak verifier supplies a confidence score intended to approximate that judgment.Higher weak scores indicate greater confidence in correctness.Source: §3 · p. 3
- At each round, a policy uses the weak score to accept, reject, or defer to strong verification, and the query stream may depend arbitrarily on past outcomes.The stream may consist of independent prompts, intermediate reasoning steps, or a combination.Source: §3 · p. 4
- Type-I error measures incorrect acceptance, type-II error measures incorrect rejection, and strong-verification frequency measures how often the costly verifier is queried.The error rates are conditioned on responses the strong verifier judges incorrect or correct, respectively.Source: §3 · p. 5
- Keeping both error rates small may require more strong-verification calls, trading output quality against latency and operational cost.The section frames choosing among these competing objectives as an engineering decision.Source: §3 · pp. 5–6
4 Fundamental Tradeoffs of Weak-Strong Verification
The population-level analysis characterizes a one-shot setting and shows that, under calibration, optimal policies reject low weak scores, accept high scores, and defer ambiguous scores to strong verification. The value of a weak verifier also depends on sharpness: decisive scores can reduce reliance on strong verification, while ambiguous scores cannot.
4 Fundamental Tradeoffs of Weak-Strong Verification
- The population formulation treats the model and verifiers as fixed and abstracts away temporal dependence to characterize expected tradeoffs.Policies choose accept, reject, or strong verification from the weak score; varying error and query-cost penalties traces achievable operating points.Source: §4 · p. 6
- Under calibration, an optimal policy rejects below a lower threshold, accepts above an upper threshold, and uses strong verification between them.The analysis studies this structure in a simplified population-level setting rather than the sequential problem.Source: §4 · p. 7
What properties of the weak verifier matter?
- Calibration alone is insufficient: a verifier that always reports the marginal correctness probability is calibrated but carries no instance-specific information.Without a link between weak scores and correctness, the weak verifier could be arbitrary and provide no actionable information.Source: §4 · p. 7
- The optimal objective compares strong-verification cost with the calibrated type-I risk of accepting and type-II risk of rejecting at each weak score.The pointwise policy chooses the cheapest of the three actions, and the objective is the expected cost of that choice.Source: What properties of the weak verifier… · p. 7
- Sharp scores near 0 or 1 make rejection or acceptance relatively low-risk, while ambiguous scores near 1/2 leave both risks substantial and call for more strong verification.Calibration makes scores interpretable as correctness probabilities; sharpness determines how often those scores are decisive.Source: What properties of the weak verifier… · p. 8
5 Selective Strong Verification and Guarantees
Selective Strong Verification uses adaptive thresholds and randomized strong-verification queries to control empirical acceptance and rejection errors over time. Its guarantee holds without assumptions on the query stream, up to finite-sample slack, while exploration trades verification cost against error control.
5 Selective Strong Verification and Guarantees
- SSV uses two adaptive thresholds to accept, reject, or defer uncertain responses, while querying strong verification with small probabilities even in decisive regions.In the uncertain region it always queries the strong verifier; in accept and reject regions it usually acts without observing the strong signal.Source: §5 · p. 8
- Theorem 5.1 provides distribution-free control of empirical type-I and type-II errors for every horizon, up to finite-sample slack.The guarantee holds with probability at least 1 − δ over the algorithm’s internal randomness.Source: §5 · pp. 8, 10
- Randomized queries provide feedback needed to detect and correct error-constraint violations that deterministic accept or reject decisions could leave unobserved.Without strong-verifier feedback, repeated decisive-region decisions may produce many acceptances while leaving type-I errors undetected.Source: §5 · pp. 9–10
- The error bound combines threshold-tracking slack with partial-feedback and exploration terms, so larger exploration probabilities ease error control but increase strong-verification frequency.The tracking term of order 1/(ηN) remains even if strong feedback were always revealed; exploration probabilities are tunable hyperparameters.Source: §5 · p. 10
6 Experimental Results
Across MATH reasoning and sequential Sudoku solving, SSV controls empirical Type-I and Type-II errors near their targets while navigating accuracy–verification-cost tradeoffs. It reaches near-oracle performance with fewer strong-verifier calls when weak signals are sharp.
6 Experimental Results
- The experiments cover outcome-level verification of complete MATH solutions at difficulty levels 2, 3, and 5, and step-by-step verification of Sudoku moves.For Sudoku, each proposed digit and its coordinates are evaluated against the current board state.Source: §6 · pp. 10–11
6.1 Empirical Error Control
- Across MATH and Sudoku, running-average Type-I and Type-II errors stabilize near the nominal targets α = β = 0.15.The reported trajectories reflect online quantile tracking; learning rate η trades off adaptation speed and stability.Source: Figure 2 · p. 11, §6.1 · p. 12
6.2 Reasoning Performance vs. Verification Cost
- 43.1% accuracy at α = β = 0.01 with 2.87 strong calls per Sudoku puzzle (46% fewer calls), versus the Oracle’s 44.2% accuracy with 5.32 calls.The adaptive policy’s accuracy is described as comparable to the Strong-Only Oracle.Source: Figure 3 · p. 12, §6.2 · pp. 12–13
- High-sharpness weak signals in Easy MATH and Sudoku yield steeper accuracy–verification-cost curves, enabling near-Oracle accuracy with a fraction of strong calls.In level-5 MATH, the relationship is more linear as weak signals become less decisive.Source: §6.2 · pp. 12–13
- 60% accuracy with 2 strong calls per problem in level-5 MATH, compared with the Oracle’s 63.5% accuracy with 2.8 calls.In this hardest setting, higher accuracy requires an approximately proportional increase in strong verification as weak signals become less decisive.Source: §6.2 · p. 13
- SSV avoids redundant Sudoku reasoning steps by accepting confident results early or escalating to strong verification when weak evidence cannot support the target reliability.SSV averages 4.8–5.2 weak calls across operating points, compared with 6.00 for the Weak-Only baseline.Source: §6.2 · p. 13
- Across both reasoning tasks, SSV maintains target error rates and offers a smooth accuracy–cost frontier, achieving near-oracle performance with a fraction of costly verification when possible.The experiments report this pattern across mathematical reasoning and sequential puzzle-solving.Source: §6.2 · p. 13
7 Discussion and Future Work
The paper presents a framework for allocating verification in LLM reasoning, with performance comparable to always using strong verification while calling the strong verifier only a small fraction of the time. Its current policy uses weak scores alone, so its error guarantees are marginal rather than context-conditional.
7 Discussion and Future Work
- The framework makes reasoning performance comparable to always applying strong verification possible while querying the strong verifier only a small fraction of the time.The paper reports theoretical and empirical support for this result.Source: §7 · p. 13
- Because strong-verification decisions depend only on weak scores, the guarantees control Type-I and Type-II errors only marginally, averaged over rounds.The policy does not condition those decisions on the broader prompt–response context.Source: §7 · p. 13
- Context-dependent thresholds and conditional error control under partial feedback could support finer-grained allocation of strong verification, but require more complex online calibration.Source: §7 · p. 13
Impact Statement
The impact statement argues that allocating verification resources more selectively can lower deployment costs while preserving correctness guarantees.
Impact Statement
- The approach is presented as a way to reduce unnecessary human and computational verification while preserving correctness guarantees, lowering deployment costs and improving trustworthiness in AI-assisted decision making.Source: Impact Statement · p. 14
A Proofs
The proofs establish pointwise optimality and a two-threshold structure for population policies, then analyze online threshold updates that control errors. Additional results aim to show empirical error convergence across target configurations.
A Proofs
- An optimal population policy can be deterministic and pointwise, choosing the action with minimum cost at each weak-score value.Randomized policies have conditional expected costs that are convex combinations of the three action costs.Source: A Proofs · p. 19
- When both error weights are positive and t_low ≤ t_high, the optimal policy rejects below t_low, uses strong verification between the thresholds, and accepts above t_high.The thresholds are t_low = 1/b and t_high = 1 − 1/a; ties may be broken arbitrarily.Source: A Proofs · p. 19
- The online proof tracks threshold-induced error rates against their targets using importance weighting, controls tracking error with a Freedman bound, and bounds threshold drift deterministically.Source: A Proofs · p. 19
B.1 Additional Error Control Results
- Additional experiments are intended to show that online calibration works across varying target error configurations, regardless of the service provider’s chosen reliability requirements.Source: §B.1 · p. 24
B.1.1 Outcome-Level Verification (MATH Dataset)
The appendix reports error-convergence runs for outcome-level MATH verification and sequential Sudoku verification. The Sudoku runs maintain stable error rates across a stream whose weak-score distribution shifts as the board nears completion.
B.1.1 Outcome-Level Verification (MATH Dataset)
- Figures 4–6 show running error convergence for MATH across three difficulty levels.Each panel includes a histogram of final cumulative running errors.Source: §B.1.1 · p. 24, Figure 4 · p. 24, Figure 5 · p. 25
- Tables 2–4 report the hyperparameters and final empirical Err A/R rates for the MATH runs.The tables include learning rates η and initial thresholds τ0.Source: §B.1.1 · p. 24, Table 2 · p. 24, Table 3 · p. 25
B.1.2 Step-by-step Verification (Sudoku)
- In sequential Sudoku, the two-threshold policy maintains a stable error rate as the board approaches completion.Convergence plots cover α = β = 0.10 and α = β = 0.05.Source: §B.1.2 · p. 24, Figure 7 · p. 26
B.2 Detailed Reasoning-Cost Tradeoffs
Decoupling the error targets produces multiple accuracy–cost tradeoff curves rather than one frontier. Fixing one target constrains its corresponding threshold, while varying the other changes the operating point.
B.2 Detailed Reasoning-Cost Tradeoffs
- One-sided sweeps produce families of curves because changing the fixed error target changes which reliability constraint shapes the accuracy–cost tradeoff.The main text instead sweeps under α = β as a one-parameter summary.Source: §B.2 · p. 26
- Fixing α anchors the accept threshold and sweeping β moves the reject threshold; fixing β anchors the reject threshold while varying α controls acceptance.Smaller α raises the accept threshold, while smaller β lowers the reject threshold.Source: §B.2 · p. 26
- Different fixed values of α or β yield different Pareto frontiers, providing finer-grained operating points for deployment constraints.The plots include one-sided MATH sweeps and analogous step-by-step Sudoku sweeps.Source: §B.2 · pp. 26–27, Figure 8 · p. 26, Figure 9 · p. 27
B.3 Analysis of Weak Verifier Scores
The weak verifier’s sharpness and calibration help explain how its scores relate to accuracy–cost tradeoffs. The appendix also specifies the verifier setup used for MATH and Sudoku.
B.3 Analysis of Weak Verifier Scores
- Mean sharpness is 0.467 for Easy and 0.448 for Medium, with separations of 0.57 and 0.54, respectively.The paper links these decisive scores to steeper accuracy–cost curves and fewer strong-verification calls.Source: §B.3 · p. 27, Table 7 · p. 28, Figure 12 · p. 29
- For Hard, mean sharpness is 0.358 and separation is 0.37; greater score overlap corresponds to a more linear tradeoff and more frequent strong verification.The paper describes the weak signal as ambiguous in this regime.Source: §B.3 · pp. 27–28, Figure 13 · p. 30
- Easy and Medium have stronger separation between correct and incorrect responses, while Hard shows substantial overlap; Figure 14 compares weak scores with empirical correctness rates.The appendix relates these patterns to reliable accept/reject decisions at score extremes and more frequent strong verification for Hard.Source: §B.3 · p. 28, Figure 14 · p. 30
B.4 Verifier Implementation Details and Prompt Specifications
- Both tasks use GPT-4o-mini to generate solutions or moves and DeepSeek-Chat as the weak verifier; MATH uses GPT-4o as strong verifier, while Sudoku uses a deterministic move check.The Sudoku check validates moves against the unique ground-truth solution of the 4 × 4 grid.Source: §B.4 · p. 29