PaperlayerView exact revision on arXiv

Source-linked AI summary

Grading the Graders: Verification Autonomy Levels (L0-L5) for LLM Reasoning

Yajie Yin

arXiv:2608.19009v1cs.CL

TL;DR

The literature lacks a single account of what verification schemes can guarantee. This paper introduces VAL to classify verification by its epistemic anchor, finding a persistent completeness blind spot in L2-style verification.

  • Problem

    The literature has not explicitly asked what a given verification scheme can guarantee.

  • Method

    VAL classifies verification schemes by answering three decisive questions about their epistemic anchor and guarantees.

  • Results

    The completeness blind spot is invisible to the verifier, is not fixed by more data or denser sampling, and can be moved up the ladder.

  • Takeaways & Limitations

    For deployers, VAL provides a pre-purchase checklist for asking where a verification specification comes from.

  • Takeaways & Limitations

    VAL states an anchor’s epistemic status rather than verdict correctness probability, so level and reliability are orthogonal.

Abstract

from arXiv · show

Large language models (LLMs) are increasingly paired with verifiers (step checkers, self-consistency filters, tool-based fact checkers, formal proof assistants) that claim to detect the model's errors. Yet the verification literature uses the word "level" to mean at least five different things: verification granularity, concept abstraction, risk tier, system-stack layer, and the epistemic source of the ground truth. We propose Verification Autonomy Levels (VAL), a meta-standard classifying verification schemes along a single axis: where does the verification spec come from, and what does the verdict guarantee? VAL ranges from L0 (LLM self-declaration, no deterministic anchor) through L2 (objective ground truth, correctness only) to L3/L4 (decidable systems with single-property or domain-level completeness), with L5 impossible in the unrestricted case. Central to VAL is the completeness blind spot: substitution- and sampling-based verifiers can confirm that proposed candidates hold, but cannot prove that no candidate was missed. We further identify a dichotomy the literature has not stated: completeness is reachable only for formally specifiable properties, while empirical open-world verification (fact-checking, diagnosis) caps at anchored correctness (L2). We document this across four domains (symbolic mathematics, behavior monitoring, medical diagnosis, and code generation) and in the strongest existing formal-verification baseline, whose authors note the verifier "focuses on the correctness of each step." We show the levels of granularity, concept hierarchy, risk, and system stack are orthogonal to VAL, resolving a systematic conflation across 17 surveyed papers. Code and full assessment are released as supplementary material.

1. Introduction

The paper introduces Verification Autonomy Levels (VAL), a six-level taxonomy classifying verification by the source of its specification and the guarantee its verdict provides. It argues that verification correctness does not imply completeness, especially for empirical open-world properties, and uses four cross-domain studies to demonstrate the framework’s structural claims.

  • Completeness: Completeness is achievable only for formally specifiable properties, whereas empirical open-world verification caps at anchored correctness (L2).Formalized sub-fragments may achieve rule-scoped completeness, but that guarantee remains silent about the unrestricted open world.
  • Framework: The paper separates VAL from granularity, concept abstraction, risk, and system-stack levels, locating 17 representative papers in the resulting multidimensional space.These four axes describe what is checked, how it is abstracted, what the verdict triggers, and which system component is audited; none specifies the verdict’s epistemic anchor.
  • Framework: VAL classifies verification schemes by epistemic anchoring—the source of ground truth—and whether the verdict guarantees correctness, completeness, neither, or both.The authors present VAL as a six-level structure with a deterministic decision procedure and runnable classifier.
  • Empirical findings: Across four domains, verification failures were traced to specification anchoring rather than judge calibration, including contaminated decomposition, combination tampering, and trust recursion.A well-calibrated verifier achieved 42/42 unit cases, yet the checked object or condition could still be improperly supplied by the model.
  • Completeness: Substitution-, sampling-, and threshold-based verifiers can confirm proposed candidates but cannot establish that no candidate was missed.The paper names this limitation the completeness blind spot and argues that it is intrinsic to the verification paradigm rather than a tuning failure.
  • Empirical findings: The four case studies—symbolic mathematics, behavior monitoring, medical diagnosis, and code generation—exercise VAL end-to-end while reporting no empirical superiority claims.Two studies report clean negative results: the verification architecture does not improve accuracy in mathematics or code generation.

2. Related Work: Five Axes, One Word

The surveyed literature uses “levels” for five orthogonal axes, while VAL isolates the epistemic source of the verification specification and its trust anchor. Across 17 papers, no scheme treated verification completeness itself as an object of study, enabling credibility to transfer across non-entailing axes.

  • Five axes: The review classifies 17 representative papers along five axes, but identifies verification granularity, concept abstraction, risk, and system-stack layer as distinct from the anchor axis.Granularity ladders decompose checks from claims or steps to documents or narratives; concept hierarchies organize mathematical abstractions; risk tiers govern dispositions; stack layers define audit scope.
  • Orthogonality: The same granularity ladder can use LLM judgment at L0 or objective ground truth, so granularity and epistemic anchoring do not entail one another.A formal-kernel proof checker can be L4 even when theorem statements are LLM-generated at L0, while a five-level concept hierarchy remains orthogonal to the anchor.
  • Survey finding: Across all 17 papers, none formalizes the anchor as a ladder or treats verification-scheme completeness as an object of study.The strongest formal baseline explicitly acknowledges the gap, while the resulting conflation lets papers inherit credibility across axes that do not entail one another.
  • Anchor axis: VAL classifies verification by who supplies the specification and whether it has an independent anchor, ranging from LLM-declared checks through objective truth to decidable systems.The anchor-source axis distinguishes L0, L1, L2, and L3/L4 according to whether the specification is LLM-declared, problem-derived, objectively grounded, or encoded in a decidable system.
  • Auditability: A full-text review corrected one paper from L1/L2 to L0/L1 after finding that its verdict was delegated to a GPT-4-based judge.The authors present the correction trail as an application of their framework: assessments are claims, and claims require anchors.

3. The VAL Framework

VAL classifies verification mechanisms by their specification anchor and the guarantee a PASS provides, distinguishing correctness from completeness and limiting higher levels to explicitly defined decidable domains. The framework is deterministic, component- and claim-relative, and does not equate level with reliability or utility.

  • Classification questions: The classifier asks, in order, who supplies the specification, whether PASS guarantees correctness or completeness, and what scope a completeness claim covers.Specification sources range from the LLM itself and deterministic rules to independent objective references and decidable systems.
  • Classification rules: VAL levels are determined by the anchor source and guarantee: correctness with a gold-label anchor is L2, while completeness yields L3 for a single property and L4 for a domain.Universal-scope completeness would be L5, but is rejected as impossible in the unrestricted case; silver-anchor recomputation is classified at the L1/L2 boundary as L1.
  • Composition: VAL classifies verification mechanisms per component and claim, so a mixed system has no single scalar level and may receive different levels for different claims.For example, one system can be L4 regarding whether a theorem is proven but L0 regarding whether its answer is correct.
  • Operational design domain: Completeness is relative to a pre-declared operational design domain (ODD), so raising VAL requires enlarging the decidable domain rather than intensifying sampling.The L2→L3 transition can re-encode “find all solutions” as solution-set equality; L3→L4 covers a whole class of properties under one decidable system.
  • Interpretation: VAL is neither a reliability measure nor a utility ranking: an L2 verifier can outperform an L3 verifier in accuracy, and higher levels are not asserted to be universally better.The paper reports 42/42 unit tests spanning L2 and L3 while explicitly separating epistemic status from verdict-correctness probability.

4. The Completeness Blind Spot

Substitution- and sampling-based verification can establish correctness for proposed candidates but cannot establish completeness, because missed candidates remain invisible. Completeness requires re-encoding a formally specifiable property in a decidable system, while empirical open-world properties are limited to anchored correctness.

  • Raising the anchor: Re-encoding a property as a decidable system enables completeness at L3/L4, but the completeness question can move upward into unchecked theorem statements or coverage declarations.The surveyed Safe baseline verifies each proof step relative to the stated theorem, while theorem statements and case-split coverage are LLM-generated and unchecked.
  • Formal distinction: Correctness and completeness are logically independent: checking every proposed candidate satisfies P does not show that every satisfying value was proposed.The relevant conditions are ∀ c ∈ C : P(c) for correctness and ∀ x : P(x) ⇒ x ∈ C for completeness.
  • Substitution blind spot: Substitution verification cannot detect omitted candidates because it evaluates P only on candidates the system supplies.In the reported math experiment, a = 2 received PASS although the true answer was {0, 2}, leaving a = 0 undetectable.
  • Sampling blind spot: Sampling can falsify a claim by finding a sampled counterexample but cannot certify it, since missed candidates or interior gaps remain outside the sample.Across 20 problems, all three false passes arose because the missed candidate or interior void was not sampled; denser sampling narrows but never removes this ceiling.
  • VAL boundary: Completeness is achievable for restricted decidable properties but not for unrestricted arbitrary properties; empirical open-world claims therefore cap at anchored correctness L2.Formalized sub-fragments can support rule-scoped completeness, whereas open-world truth cannot be re-encoded into a complete decidable fragment.
  • Operational prescription: The framework prescribes raising the verification anchor to L3/L4 when a property is encodable and labeling non-encodable verification as a correctness probe.The blind spot remains invisible to the verifier, is not removed by more data or denser sampling, and can only be moved up the ladder.

5. Empirical Case Studies

Across four domains, verification added value mainly through error reportability, bounded detection, over-confidence catching, or completeness rather than improved accuracy. The studies also exposed domain-specific ceilings: L2 anchors cannot guarantee completeness, while L3 gains depend on formally specified properties and valid tests or decision rules.

  • Cross-domain pattern: The four studies used a common audit, value-window, failure-mode, and judge-testing protocol, including honest negative results.They covered symbolic mathematics, behavior monitoring, medical diagnosis, and code generation.
  • Symbolic mathematics: In symbolic mathematics, the full architecture scored 16/15/13 across three runs on 20 problems, versus 20/20 for the raw-LLM baseline.Verification did not improve accuracy and sometimes hurt it, but it made errors reportable and enabled L3 solution-set checks to catch missed solutions.
  • Medical diagnosis: In medical diagnosis, the deterministic information-completeness judge flagged 3/3 true over-confidence failures with zero false positives, including one missed by human review.Replacing the heuristic with the validated Alvarado rule preserved the flagged set at 3/3 while providing a decidable boundary and explicit missing-data semantics.
  • Cross-domain pattern: Across studies, accuracy windows were empty near the training distribution, while non-empty verification windows covered reportability, bounded detection, over-confidence catching, and L3-anchor repair.The framework therefore assigns L2 judges reportability rather than accuracy, and L3 judges completeness only within their operational domain of discourse.

6. Discussion

The discussion frames VAL as a deployment checklist that anchors verification in decidable kernels or explicit standards while recognizing that universal termination is impossible. It separates accuracy from verification value, emphasizing error reportability and completeness awareness rather than improved raw accuracy.

  • Trust recursion: VAL terminates trust recursion at a decidable kernel or definitional anchor, while Rice’s theorem rules out universal termination at L5.The practical question is which kernel, anchor, or conventional standard terminates a particular verification chain.
  • Canonical architecture: VAL assigns complementary roles: the LLM translates and declares, deterministic judges operate within their ODD, and humans anchor specifications and audit judges.Failures arise when the LLM self-declares verification, judges operate outside their ODD, or humans re-derive deterministic decisions.
  • Deployment guidance: Verifier-level selection depends on the cost of silent errors and property encodability, making VAL a deployment checklist rather than a competition ladder.An L0 self-check may suit a low-stakes summarizer but not a clinical decision aid; deployment should specify the property, ODD, guarantee, abstention contract, and audit anchor.
  • Interpreting results: The architecture is no better than the raw baseline in accuracy, but its value lies in error reportability and completeness awareness.Accuracy is the LLM’s axis, whereas reportability and completeness are the verifier’s; the architecture is intended for deployers who need to know when answers are untrustworthy.

7. Limitations

The study’s evidence is limited by abstract-level literature review, single-model synthetic case studies, unvalidated rating reproducibility, and bounded mathematics experiments. VAL’s scope, fuzzy ODD boundaries, orthogonality to reliability, and unquantified reportability further constrain its conclusions.

  • Evidence base: 11 of 17 papers were assessed only at the abstract level, so classifications may shift with full-text review although the axis structure is unaffected.Six anchor-axis papers were verified against full text.
  • Evidence base: Case studies use one model family, deepseek-chat, and synthetic data, including fictional medical cases without patient data.The framework’s claims are structural, but its empirical illustrations are single-model.
  • Framework boundaries: VAL classifies epistemic anchors rather than verdict accuracy, so level and reliability are orthogonal; ODD boundaries also depend on tooling and remain an audit target.An L2 verifier can be more accurate than an L3 verifier on in-ODD cases, while encodability varies with solvers, type systems, and rule inputs.
  • Framework boundaries: VAL’s decision procedure is deterministic by construction but lacks scale-tested inter-rater reliability, leaving reproducibility of Q1/Q2 judgments an open empirical question.The authors plan to address this with a larger corpus.
  • Empirical evaluation: 20/20 baseline accuracy leaves no headroom, so the mathematics result supports only no improvement on in-distribution problems, not a general impossibility claim.The study also lacks comparisons with published verification architectures, and its 42/42 calibration tests and #105 adjudication were author-designed or adjudicated.
  • Scope: The survey excludes anchor-less verification families, for which VAL offers only the L0–L2 distinction and honesty rather than completeness.Excluded examples include calibration and uncertainty estimation, red-teaming, RAG citation verification, and reward-model verification.
  • Empirical evaluation: 25–35% mathematics accuracy loss is not weighed against error-reportability costs, because true-positive, false-positive, false-alarm, and cost–benefit measures are unreported.The reportability claim therefore remains a hypothesis rather than a measured benefit.

8. Conclusion

The paper proposes VAL, a six-level taxonomy centered on the source of ground truth and the guarantee a verifier can deliver. It concludes that verification strength is bounded by domain correctness, ODD completeness, and honest abstention, while identifying directions for validation, medical extension, and broader assurance applications.

  • Core framework: VAL classifies verification schemes by where ground truth comes from and what the verdict guarantees, using six levels from L0 to L5.The paper also provides a deterministic decision procedure and runnable classifier.
  • Core framework: The highest grade a verifier can earn is a guarantee of correctness within its domain, completeness within its ODD, and honesty when it must abstain.This is the paper’s headline conclusion about grading verification systems rather than answers.
  • Future directions: Future work should validate VAL on a larger corpus, measure inter-rater agreement, and stress-test boundary cases such as L1/L2 borders in RAG-grounded and tool-augmented checkers.The proposed validation targets the standard itself and its decision procedure.
  • Future directions: The demonstrated medical L2→L3 upgrade should be extended to additional decision rules and ODDs, including PERC/Wells for pulmonary-embolism and chest-pain presentations.The appendicitis example is identified as the existing demonstration.
  • Future directions: The same anchor source × guarantee × scope structure may extend beyond verification to automated assurance applications ranging from unit testing to regulatory attestation.The paper explicitly proposes exporting the framework beyond verification.

Appendix A: The decision procedure (runnable)

The appendix provides a runnable implementation of the VAL classification procedure, with ten passing self-tests and explicit mappings from verifier types to levels L0–L5. It rejects L5 for unrestricted universal completeness while distinguishing lower-level anchors and completeness guarantees.

  • Implementation: The classification procedure is implemented in val_standard.py, with 10 self-tests all passing.The implementation corresponds to the procedure described in Section 3.3.
  • Level mapping: LLM self-checks map to L0, problem-derived deterministic rules to L1, and substitution with a gold-label anchor to L2.The procedure labels these as self-declaration without a deterministic anchor, deterministic rules from problem text, and correctness plus a gold-label anchor, respectively.
  • Level mapping: Solution-set equality maps to L3, the Rust borrow checker to L4, and unrestricted universal completeness to impossible L5.L3 denotes single-property completeness in a decidable system, L4 domain-level proof-system completeness, and L5 is rejected as impossible in the unrestricted case.

Appendix B: The 17-paper classification

Appendix B provides a full versioned assessment with per-paper evidence and a compact summary organized around the anchor axis.

  • Per-paper assessment: The appendix includes a full versioned assessment with evidence for each paper.The assessment is available in the referenced documentation.
  • Compact summary: It also provides a compact summary focused on the anchor axis.The compact summary is presented separately from the full assessment.
  • Documentation: The assessment materials are located at docs/07.The passage identifies docs/07 as the location of the full versioned assessment and per-paper evidence.

Appendix C: Experiment archives

The appendix archives the implementation, evaluation, and data artifacts for four experiments spanning mathematics, behavior monitoring, medical diagnosis, and code generation. The mathematics archive includes a 42/42 verifier test result and anchor-level definitions, while the other chapters provide reports, analysis scripts, protocols, and result files.

  • Chapter 1 (math): The mathematics archive includes RESULTS.md, EVALUATION.md, test results, test_verifier.py, and verifier.py with ANCHOR_LEVELS.test_verifier.py reports 42/42.
  • Chapter 2 (behavior): The behavior archive contains a report, analysis scripts, and raw data files.The listed artifacts are behavior/REPORT.md, behavior/analyze*.py, and behavior/data_raw*.json.
  • Chapter 3 (medical): The medical archive contains a report, diagnostic verification code, and the Alvarado implementation.The listed artifacts are medical/REPORT.md, medical/verify_diag.py, and medical/alvarado.py.
  • Chapter 4 (code): The code archive contains prediction and protocol documentation, experiment scripts, hard-problem scripts, and JSON result files.The listed artifacts include docs/08, chapter4/p3_experiment.py, chapter4/hard_problems.py, and chapter4/p3_*.json.
Loading 2608.19009v1…