---
title: "Verification Asymmetry · Agentic Atlas"
description: "Verification Asymmetry: why checking ≪ doing lets verification work at all; the ladder + coverage, and the three failure modes (coverage exhaustion /…"
canonical: "https://agentic-atlas.dev/nodes/verification-asymmetry"
last-updated: "2026-08-19"
---

# Verification Asymmetry · Agentic Atlas

[← the survey](https://agentic-atlas.dev/atlas)

1. concept
   Verification Asymmetry
   Hook
   why checking ≪ doing lets verification work at all; the ladder + coverage, and the three failure modes (coverage exhaustion / discrimination collapse / quantifier inversion)
   Thesis
   Verification can guard a probabilistic producer only where checking a candidate against its contract is materially easier and more reliable than producing it; knowing when that holds is knowing when verification is worth its cost at all.
   Laws & fences
  - The gap belongs to the task and contract pair, so a contract rewrite can widen it, and the asymmetry fails where clause-writing runs out.
  - Every rung of the ladder is external; a producer judging its own output is not on it, and only a deterministic check terminates the regress.
  - The check guarantees the contract, never the goal; the human gate or accepted risk lives in the gap between them.
   When to reach
  - Reach for it when deciding whether verification is worth its cost at a seam and which of the three failure modes you are in.
  - Expect the premise to invert on absence claims such as no bug exists, where verifying is categorically harder than producing; re-scope the clause to bounded, witnessed forms and treat the unbounded remainder as residue.
   Provenance
   [verification-asymmetry/definition](https://agentic-atlas.dev/nodes/verification-asymmetry#definition) · v1.0.2
   Addresses
   atlas_cards verification-asymmetry
2. [
   Foundations
   ](https://agentic-atlas.dev/nodes/foundations)
3. [
   Statelessness
   ](https://agentic-atlas.dev/nodes/statelessness)

The card, in place · its connections drawn edges from atlas_links verification-asymmetry

On this plate

[definition](https://agentic-atlas.dev#definition)[why-it-matters](https://agentic-atlas.dev#why-it-matters)[model-and-claims](https://agentic-atlas.dev#model-and-claims)[scope-and-boundaries-where-the-asymmetry-fails](https://agentic-atlas.dev#scope-and-boundaries-where-the-asymmetry-fails)[implications-the-consequence-map](https://agentic-atlas.dev#implications-the-consequence-map)[evidence-the-grounding-pass](https://agentic-atlas.dev#evidence-the-grounding-pass)[relationships](https://agentic-atlas.dev#relationships)[lineage](https://agentic-atlas.dev#lineage) [relationships](https://agentic-atlas.dev#relationships)

Every section is addressable on its own. Read only the ground you need.

## Definition

[](https://agentic-atlas.dev#definition)

definition.md

*(Premise, not a move.)* The **generation–verification gap**: for some task–contract–checker triples, verifying a candidate against a documented spec is materially easier—and measurably more reliable—than generating the candidate. When checking ≪ doing, an external check can improve reliability instead of merely stacking another correlated failure. One level terminates the regress only on a deterministic rung; elsewhere, the residual risk must be measured and accepted.

## Why it matters

[](https://agentic-atlas.dev#why-it-matters)

why-it-matters.md

The keystone says verification moves contract clauses toward enforcement — but the verifier is the same kind of probabilistic reader as the producer. Why doesn't the check need its own checker, all the way down? The library's whole verification family rests on an answer it never states — and on knowing where that answer stops holding.

## Model and claims

[](https://agentic-atlas.dev#model-and-claims)

model-and-claims.md

Two refinements the naive statement omits:

- **The gap is a property of the (task, contract) pair, not the task alone.** A contract rewrite can widen it — that is half of what contract-writing *is for* (`contract-documentation/contract-documentation.md`). "Where the asymmetry fails" is therefore mostly a statement about where contract-writing runs out, not a taxonomy of doomed task labels.
- **The asymmetry holds for the covered portion of intent.** The validated [seam](https://agentic-atlas.dev/glossary/seam) guarantees the *contract*, never the *goal*. The gap between them is where the human [gate](https://agentic-atlas.dev/glossary/gate), or accepted risk, lives.

### The determinism ladder

*(2026-07-05, foundations grilling — gap-widening operationalized, per contract clause.)* Deterministic check (verifier error ≈ 0; the gap is infinite and the who-checks-the-checker regress *terminates*, not merely attenuates) → cheap LLM verifier → panel / voting (`../verification/panel-voting.md` — conditional; see failure mode 2) → unverifiable (the asymmetry fails; the human gate takes over). Every contract splits into mechanical clauses (deterministically checkable — schema, presence, tests) and semantic clauses (probabilistic residue); push each clause as far down the ladder as it goes. A deterministic checker also forces the seam's *effective receiver type* to deterministic, ratcheting tier-1 schema exactness up — the check doesn't just catch errors, it forces the contract to become legible enough to check. Reified as a pipeline stage in `../verification/validated-seam-redispatch.md` (the checker stage).

**Every rung is external.** The producer prompted to judge its own output is not on the ladder: intrinsic self-correction degrades performance, self-critique approves invalid work at high false-positive rates, and models discriminate among their own candidates no better than they generate — a model can answer "15" and then judge "7 + 8 = 15" as false (see *Evidence*). The asymmetry the library leans on is between a producer and a *separate* check, at a seam.

### Coverage — how far down the ladder a task's intent reaches

The ladder measures per-clause checkability. The second quantity is **coverage**: what fraction of the *actual intent* the written clauses capture. A contract can be 100% deterministic and 40% of what you meant. The spectrum:

- **Sort a list** — `is_sorted(out) ∧ is_permutation(out, in)` is a complete, deterministic correctness check. Coverage ≈ 1 on the bottom rung; the output carries its own certificate.
- **Schema migration** — apply to a snapshot, diff, run the suite: deterministic checks reach most of correctness; residue like "won't lock the table in prod."
- **Refactor** — tests pin behavior deterministically; "more readable" is semantic residue.
- **Summarize a memo** — shape checks deterministically; faithfulness is nearly all residue.

How strongly the asymmetry holds *for a task* is where that task sits on this spectrum. Raising coverage — writing clauses that reach deeper (executable specs, property checks, golden tests) — is contract-side craft and lives with `contract-documentation/contract-documentation.md`; this node owns the boundary condition.

### Worked example — write the apology, count the words

The model has a real generation job:

> Write a friendly apology for a late package in exactly ten whitespace-separated words.

The first candidate reads naturally but misses the mechanical clause:

> Sorry your package arrived late; we appreciate your patience.

That is nine words, so the checker rejects it. A fresh attempt returns:

> Sorry your package arrived late; we truly appreciate your patience.

That is ten words, so the same checker passes it. The contract splits by clause:

| Clause | Check | Ladder placement |
| --- | --- | --- |
| exactly ten whitespace-separated words | split and count | deterministic |
| a friendly apology for a late package | read for meaning and tone | human gate |

The checker does not write another apology. It counts the words in the candidate the model already produced, then selects a different next action: reject and [re-dispatch](https://agentic-atlas.dev/glossary/re-dispatch) at nine; continue to the tone gate at ten. That deterministic check is cheaper and more reliable than asking another model to recreate the whole answer.

**Contract coverage is complete for the stated intent:** it names both exact length and friendly apology. The deterministic checker covers one of those two clauses; the human gate owns the semantic residue. The failure-mode call is *none* for that split. Coverage exhaustion begins if the [workflow](https://agentic-atlas.dev/glossary/workflow) replaces “friendly” with a cheap proxy such as “contains the word `sorry`” and then pretends the proxy captures the tone. The asymmetry holds for the mechanical clause, not for the whole answer.

### How the gap moved in studied setups

Three grounded facts govern how the gap moves, in place of an error-rate algebra (which assumes producer and verifier errors are independent — the one assumption the evidence most clearly refutes):

- **Scale can widen the measured gap.** Song et al.'s controlled self-improvement framework found a gap variant that scaled monotonically with pretraining compute. That is evidence for a design possibility, not a law for every task–contract–checker triple.
- **A producer of higher [capability class](https://agentic-atlas.dev/glossary/capability-class) can narrow verifier advantage.** Across Zhou et al.'s twelve benchmarks and generative-verifier setup, lower-class generators' errors were easier to detect and advantage was limited on harder cases. The design warning is conditional: coherent errors from producers at the highest class Zhou et al.'s setups covered can camouflage themselves.
- **False positives are a critical failure mode.** Several self-critique and planning studies found checkers approving bad work; that silently converts a validated seam into a rubber stamp. Report false-positive rate alongside agreement — do not infer one from the other.

## Scope and boundarieswhere the asymmetry fails

[](https://agentic-atlas.dev#scope-and-boundaries-where-the-asymmetry-fails)

scope-and-boundaries-where-the-asymmetry-fails.md

Three distinct modes — they fail differently and call for different remedies. (*Modes 1–2 are properties of the contract and the checker, not the task; only mode 3 is structural.*)

1. **Coverage exhaustion.** Clause-writing stops paying before intent is captured — the marginal clause adds no coverage ("make it moving"). The residue is inarticulable, not uncheckable. Two traps: *proxy clauses* substituted for inarticulable intent select for gaming (Goodhart — worse than no clause), and the *spec-authoring bottleneck* — delegating clause writing to an LLM relocates the coverage problem into the spec (Vikram et al.'s best setup produced valid, sound property tests efficiently but automatically covered only 21% of extractable API properties). Remedy: keep splitting until the true residue, then gate on a human or accept the risk — knowingly.
2. **Discrimination collapse.** The clause exists but the verifier can't discriminate: MT-Bench judges exceeded 80% human agreement on their studied comparisons, while position, verbosity, and self-preference biases remained; separate work found position bias strongest on near-ties. Strong-producer coherent errors can evade them (see *How the gap scales*). Panels rebuild discrimination only conditionally — verifier errors are correlated, so naive replication buys almost nothing (`../verification/panel-voting.md`). Remedy: diversity + reliability weighting, or push the clause down a rung instead.
3. **Quantifier inversion.** Absence claims — "no bug exists," "no failure mode," "no injection path." The clause is easy to *write* and universally quantified to *check*: verifying absence is categorically harder than producing the artifact, so checking ≫ doing and the premise inverts. The P-vs-NP intuition holds only for NP-shaped tasks, where a candidate carries a checkable certificate. Remedy: re-scope the clause to bounded, witnessed forms (this suite passes; this scanner finds nothing; these N properties hold on these inputs) and treat the unbounded remainder as mode-1 residue.

## Implicationsthe consequence map

[](https://agentic-atlas.dev#implications-the-consequence-map)

implications-the-consequence-map.md

A premise makes no tradeoff of its own; what it changes is what the reader does at every seam downstream. The teachable content is the boundary condition: knowing when the asymmetry holds is knowing when verification is worth its cost at all — and which of the three failure modes you are in decides what replaces it (more contract, a better-shaped checker, or the human gate).

## Evidencethe grounding pass

[](https://agentic-atlas.dev#evidence-the-grounding-pass)

evidence-the-grounding-pass.md

Qualitative model is the durable payload; the anchors below are evidence, dated because they rot. *(Research pass 2026-07-05.)*

- **The gap, formalized**: Song et al., *Mind the Gap* (ICLR 2025, [arXiv 2412.02674](https://arxiv.org/abs/2412.02674)) — defines the generation-verification gap; a variant in its controlled self-improvement framework scales monotonically with pretraining FLOPs. Practitioner framing: J. Wei, *Asymmetry of verification and verifier's law* (2025) — verifiability ∝ trainability; lists reverse-asymmetry cases (fact-checking an essay costs more than writing it).
- **Self-verification is off the ladder**: Huang et al. (ICLR 2024, arXiv 2310.01798) — intrinsic self-correction degrades reasoning without external signal; Valmeekam/Stechly/Kambhampati line (arXiv 2310.08118, 2310.12397, 2402.08115; ICML 2024 LLM-Modulo, 2402.01817) — self-critique collapses performance with high false-positive rates while *sound external verifiers* restore the gains; Jiang et al. (arXiv 2404.04298) — discrimination no better than generation intramodel; Li et al., *GV- consistency* (ICLR 2024, arXiv 2310.01846) — GPT-4 generator/validator consistent only 76%.
- **Trained/external verifiers work in the studied mathematical-reasoning setups**: Cobbe et al. 2021 (arXiv 2110.14168) — 6B generator + trained verifier ≈ 30× larger model; Lightman et al., *Let's Verify Step by Step* (ICLR 2024) — process supervision outperformed outcome supervision. Both require labeled correctness data, not prompting.
- **Discrimination collapse**: Zheng et al. (NeurIPS 2023, MT-Bench) — ~80% judge–human agreement, degrading as candidates converge; position/verbosity/ self-enhancement biases; Shi et al. (arXiv 2406.07791) — position bias is systematic, worst on near-ties; Wataoka et al. (arXiv 2410.21819) — self-preference is mechanistically low-perplexity preference; Zhou et al. (arXiv 2509.17995) — stronger generators' errors are harder to detect; verifier benefit saturates on hard problems.
- **Correlated panels**: Kohli (arXiv 2605.29800) — in its nine-model panel on three NLI datasets plus a pairwise-preference robustness check, 9 judges ≈ 2.2 effective votes (pairwise error correlation φ ≈ 0.39); unanimity was ~450× less reliable than independence predicted. Working mitigations: disjoint-family juries (Verga et al., arXiv 2404.18796), reliability-weighted weak-verifier ensembles (Weaver, NeurIPS 2025, arXiv 2506.18203).
- **Quantifier inversion**: Wentworth, *Verification Is Not Easier Than Generation In General* (2022) — the NP intuition fails on universally quantified checks and adversarial generators.
- **Spec-authoring bottleneck**: Vikram et al. (arXiv 2307.04346) — its best setup produced a valid and sound property-based test in 2.4 samples on average, while automatically covering only 21% of properties extractable from API documentation.

## Relationships

[](https://agentic-atlas.dev#relationships)

relationships.md

- **Premise of** `the-contract-keystone/the-contract-keystone.md` — stated there as the *affordability condition*, the contract's sibling premise (contract = possibility condition of checking; asymmetry = what makes checking worth doing). Settled 2026-07-05, foundations grilling.
- A well-written contract (`contract-documentation/contract-documentation.md`) is partly a device for *widening* the gap — coverage-raising craft lives there; the boundary condition lives here.
- Explains when `../verification/validated-seam-redispatch.md` converges — and which failure mode you are in when it can't. The checker stage is the ladder, reified.
- `../verification/panel-voting.md` — the mitigation when a semantic clause's gap is narrow; bounded by error correlation (failure mode 2).
- What `../verification/fresh-context-trials.md` leans on: the harness is itself probabilistic; "who tests the tester" dissolves only because the harness checks, it doesn't re-produce — and terminates fully only on the deterministic rung.
- The escalation target when all three modes exhaust: `../control-flow/human-in-the-loop-gate.md`.

## Lineage

[](https://agentic-atlas.dev#lineage)

lineage.md

Program result-checking (Blum and Kannan, "Designing Programs that Check Their Work", JACM 1995; surveyed in Wasserman and Blum, JACM 1997): verify one output instead of proving the program, under a little-o rule that bars the checker from recomputing the answer, so that its errors are not the producer's. "Every rung is external" is that rule. Coverage is what the classical version assumed away: a checker is defined against a known f.

The relationships ledger

Evidence-bearing references

## Relationships

Every connection keeps the section where it was found. The map above orients; this ledger carries the evidence.

### Outbound references 0

1. No outbound references.

### Inbound references 3

1. in-slice · occurrence 9
   [Foundations](https://agentic-atlas.dev/nodes/foundations#model-and-claims)
   why checking ≪ doing lets verification work at all; the ladder + coverage, and the three failure modes (coverage exhaustion / discrimination collapse / quantifier inversion)
   Evidence: [Model and claims](https://agentic-atlas.dev/nodes/foundations#model-and-claims) · occurrence 9
2. in-slice · occurrence 7
   [Foundations](https://agentic-atlas.dev/nodes/foundations#relationships)
   why checking ≪ doing lets verification work at all; the ladder + coverage, and the three failure modes (coverage exhaustion / discrimination collapse / quantifier inversion)
   Evidence: [Relationships](https://agentic-atlas.dev/nodes/foundations#relationships) · occurrence 7
3. in-slice · occurrence 2
   [Statelessness](https://agentic-atlas.dev/nodes/statelessness#relationships)
   why checking ≪ doing lets verification work at all; the ladder + coverage, and the three failure modes (coverage exhaustion / discrimination collapse / quantifier inversion)
   Evidence: [Relationships](https://agentic-atlas.dev/nodes/statelessness#relationships) · occurrence 2

[↑ back to the top](https://agentic-atlas.dev#content) [← the survey](https://agentic-atlas.dev/atlas)

Node verification-asymmetry · corpus 31de4cb · Catalog revision 35263c4c415da742953d0462804fb14424e2244dae4c63efd27e468988de70ab