The verification hierarchy, demoted

The verification hierarchy orders evaluator signals by expected grounding strength: formal verifiers, then execution feedback, then learned judges, then intrinsic signals. It answers one question — how strongly is a signal grounded, given a target property? — and is a useful prior on the answer, never a verdict on validity.

What the hierarchy asks#

The ordering comes from the RSI survey (Chen, Wang & Qu, 2026, §5.2), which ranks the signals that drive self-improvement loops from formal verifiers down to the model's own confidence and observes that demonstrated self-improvement tends to be stronger where feedback is more externally grounded and harder to game. The question the ordering answers is this: if this signal says a candidate is better, how strong is the evidential basis for believing it?

Three features of that question matter. It is about a signal: the hierarchy orders evidence channels, not evaluator artifacts, so rubrics, gold answers, and PRMs have no rung of their own (Vocabulary without category errors). It is conditional on a target property: a rung says how well the signal tracks the property its specification names, not whether that property is the right one. And it describes expected strength, a prior to be replaced by measurement.

One evaluator rarely sits on one rung. The evaluator of SQLAgent, the text-to-SQL agent of Case C, formalizes access policy with read-only credentials and row-level permissions, checks answers by executing queries against pinned snapshots, applies a rubric-guided judge to ambiguity handling, and sends semantic edge cases to business SMEs. "Which rung is SQLAgent's evaluator on?" has no answer; "which rung is each criterion's signal on?" has a different answer for each criterion.

Four rungs#

The members and signatures extend those of the RSI survey (Chen, Wang & Qu, 2026, §5.2). Mechanism families treats each family in depth.

Soundness is what puts formal verifiers on top. A verifier $V_\psi$ checking property $\psi$ is sound when

$$V_\psi(y) = 1 \;\Rightarrow\; \psi(y) = 1$$

where:

• $y$ is the artifact under evaluation, such as a proof or a program;
• $V_\psi(y) = 1$ means the verifier accepts it;
• $\psi(y) = 1$ means it satisfies the property under the formal semantics.

In words: anything the verifier accepts truly has the property, provided the verifier and its trusted base behave as claimed. Completeness is the separate question of whether every true instance is accepted; real systems can trade it for tractability, but soundness is what makes "accept" unusually trustworthy. With a trusted implementation, the verifier's false-positive probability for the formal property is constrained by the semantics rather than estimated from a sample.

Execution checkers usually lack the implication. Passing a test suite means that no tested counterexample was found, not that the program is correct for all possible inputs. That is why execution sits below proof checking even when both are deterministic. A query that returns the right rows on one snapshot can return wrong rows on another, which is why SQLAgent's evaluator adds metamorphic tests and multiple database instances.

The configured trusted base#

A formal guarantee belongs to a configured system, not to an abstract checker. The configured trusted base is everything the guarantee is relative to: permitted axioms, theorem statements, checker version, proof-kernel configuration, environment assumptions, and whether the optimizer can modify any of them.

Inside the formal property, a correct proof checker leaves an optimizer no way to obtain an accepted but invalid proof. Outside it, the guarantee says nothing: the larger system can still optimize the wrong formal property, and the vulnerability moves to specification design, environment assumptions, and the interface between formal and real-world semantics. The Goodhart boundary moves to these surfaces rather than disappearing.

Case A, mathematical reasoning, puts this to work: its validation plan lists the proof checker's trusted base next to checker normalization and contamination. If a solver can add an axiom, weaken the statement it was asked to prove, or change the checker's configuration, the kernel will faithfully accept a proof of the wrong thing. Listing what is trusted, and confirming that none of it lies inside the optimizer's modification surface, is part of the evaluator. The same holds for structural guarantees such as sandboxes and permissions, which guarantee only what the deployed configuration enforces (Guarantee before you estimate).

Human judgment sits beside the ladder#

Human judgment is not a fifth rung. It plays two roles that must not be conflated:

1. a measurement mechanism with ordinary error, inconsistency, cost, and bias;
2. a reference authority, or trust root, where the evaluate-the-evaluator chain stops for value-laden constructs.

An expert panel can define or adjudicate a standard and still have measurable inter-rater disagreement. The first role means a human rater or panel is characterized like any other mechanism (Mechanism families); the second means someone must say where the recursion stops, and why. The Berkeley agent-evaluation lecture notes that human evaluations are "regarded as gold standards", then lists why that needs qualifying: they are slow, expensive, not reproducible, and subject to disagreement between annotators and within one annotator over time (Song, 2025, slide 20).

DocsAgent, the documentation agent of Case G, separates the two roles. Double-labeled SME examples measure agreement and calibrate its judges; a panel of those SMEs, with measured reliability and an explicit mandate to adjudicate, can serve as the trust root its validity statement names.

The map below draws the ladder this way. Select each rung to see the mechanism families it covers and what its prior leaves open, then select Human judgment, drawn beside the ladder rather than above it.

A regularity, not a law#

The ordering earns its place by tracking an observed pattern. Across the survey's corpus, demonstrated self-improvement strength tracks the hierarchy: evolutionary discovery systems such as FunSearch and AlphaEvolve work on the top two rungs, and the self-refinement methods that survived 2024's negative results are the ones that moved up the hierarchy (Chen, Wang & Qu, 2026, §5.2). The authors present this as a qualitative pattern, not a measured law, and it does not imply construct validity.

Two results mark the bottom of the ladder. Without external feedback, LLMs largely cannot self-correct their reasoning, and naive self-correction can make answers worse (Huang et al., 2024, via Chen, Wang & Qu, 2026, §3.1); the field responded by grounding critique in execution, retrieval, detectors, or solvers. The Mirror Loop study ran three providers' models through ten rounds of ungrounded self-critique across four task families and found informational change declining by 55% across iterations, while a single verification step at the third iteration restored forward movement (DeVilling, 2025, via Chen, Wang & Qu, 2026, §5.2).

A higher rung is not better for every purpose. Formal verification is strong but narrow, because it needs a formal property; learned judgment is broad but empirical; intrinsic signals are cheap enough to use everywhere but are not independent of the generator. Signal reliability rises toward the top while task coverage widens toward the bottom. This reliability–coverage trade-off is why the design problem is not to force a whole task onto one rung but to decompose the judgment and push each criterion as high as it can legitimately go, leaving learned judgment for the residue — the subject of Verifiability engineering.

A prior, not a verdict#

The framework demotes the hierarchy to exactly that role: treat hierarchy position as a prior over expected error structure, not as the final verdict on evaluator quality, because what matters operationally is the measured error profile of the configured evaluator in its intended regime. A rung is where you start. A test suite that misses a criterion's hard cases is execution feedback and still weak evidence, since for code the evaluator's largest uncertainty may be test completeness rather than judge noise, and a proof checker can be perfectly sound for the wrong theorem.

What replaces the prior is the validation profile $\Pi = (N, E, T, G, C, D)$: natural error, exploitability curve, transport, generator coupling, channel coupling, and drift profile, measured for the configured evaluator (The validation profile and validity statement).

In practice#

Place each criterion of one evaluator on the ladder, then plan what will replace the placement.

1. Split the evaluator into criteria. A single rung for a whole evaluator hides more than it shows.
2. Name each criterion's mechanism and rung. Mark anything a person decides as frontier, not as a rung. Give rubrics and gold answers no rung of their own: classify the mechanism that applies them.
3. List the trusted base of every formal or structural check: axioms, property statements, checker version and configuration, environment assumptions, and who can modify each. Confirm the optimizer cannot.
4. For every execution check, state what is not tested: coverage, and the input regions the tests never reach.
5. For every learned judge or intrinsic signal, plan the error measurement against adjudicated labels, by criterion and slice; never rely on an intrinsic signal without an external check.
6. Ask whether a criterion can move up. Can it be guaranteed by construction, checked by execution, or split into deterministic subclaims before you accept a judge?
7. Record each rung as a prior, next to the validation-profile entry that will replace it.

The artifact is a criterion-by-rung table with a trusted-base list for every formal check: the mechanisms entry of the evaluator dossier.

Common failure modes#

• Rung as verdict — "it's a formal verifier, so the eval is sound" → name the property, the trusted base, and the claim the guarantee supports, then validate the system that contains the checker. See The evaluator system.
• Tests reported as proof — a passing suite is reported as correctness → state what was and was not tested, and add property-based or metamorphic tests where the claim needs breadth. See grader gaming.
• Self-critique as evidence — a loop graded by its own confidence or critique reports steady gains → add an external check and measure generator coupling. See self-confirming loop.
• Trusted base inside the modification surface — the optimizer can edit the theorem statement, the tests, or the checker configuration → move them outside what the loop can change, and log access. See wireheading.

Check yourself#

Analyze. Classify a unit test, a type checker, a reward model, and a self-consistency vote by rung, then say what each rung's signature leaves unmeasured for that evaluator.

Hint

Type checker: formal, but only for the type property. Unit test: execution, silent about untested inputs. Reward model: learned judge, with error still to measure. Self-consistency: intrinsic, not independent of the generator.

Evaluate. Identify a case where moving a criterion to a "stronger" evaluator would reduce construct validity.

Hint

A deterministic trajectory checker that demands one canonical sequence sits higher than a judge of whether the path was acceptable, but when process is not part of the construct it penalizes valid novel strategies.

Create. For a research-agent task, name one criterion you could move up a rung by changing the artifact the agent must emit, and list the trusted base or reference anchor the new check depends on.

Hint

Requiring code, an experiment manifest, raw metrics, and seeds moves reproducibility from a judge's reading toward execution. The new check then depends on the pinned environment that reruns the code.

Further reading#

• Vocabulary without category errors — the second map, and why the hierarchy is not a taxonomy of artifacts.
• Anchors and evidence views — what a gold answer is, and how evidence architecture moves criteria up the ladder.
• The validation profile and validity statement — the measurements that replace the prior.
• Chen, Wang & Qu (2026), "Recursive Self-Improvement in AI: From Bounded Self-Refinement to Autonomous Research Loops" — §5.2 for the hierarchy and the evidence that self-improvement tracks it.
• Huang et al. (2024), "Large language models cannot self-correct reasoning yet" — the negative result beneath the intrinsic rung.