verifier-completeness

name	verifier-completeness
description	Run when auditing or writing a reward/eval verifier — BEFORE you trust a pass rate, a reward signal, or a "the verifier is sound" claim. The reflexive check is for FALSE-ACCEPTS (soundness: a wrong answer must never be accepted). This skill forces the OTHER direction, which soundness gates structurally cannot see: COMPLETENESS — is every CORRECT answer accepted? A correct answer rejected by the verifier (a reward UNDER-count) does not merely mislabel one eval row; in an RL loop it is a training-reward signal that pushes the policy AWAY from correct behavior. An under-count poisons the POLICY, not just the eval. Use this skill to build a fixed known-correct notation battery, run it through every verifier entry point, and gate the correct→accept direction in CI. Triggered by the verifier-integrity-sprint-2026-07-11 finding: the math verifier was LaTeX-blind, under-counted base passAt1 0.5167→1.0, and trained 27 adapters on poisoned reward.
metadata	{"short-description":"Audit verifiers for FALSE-NEGATIVES (completeness), not just false-accepts; a reward under-count poisons the policy, not just the eval"}

Verifier-completeness audit

The lesson (why this skill exists)

Auditing a verifier for soundness (wrong→accept) is necessary but not sufficient. The #908 bug was a completeness failure (correct→reject): the math verifier's parser had no LaTeX handling and read a bare e as a free symbol, so mathematically-correct answers like -2x \sin(x^2) (vs gold -2*x*sin(x**2)), \frac{1}{2} e^{2x} (vs exp(2*x)/2), and e^x (Euler) were scored reward=-1.

Two things made this worse than a mislabeled eval row:

1. It under-counted base capability by ~48 points. Base passAt1 read 0.5167; under the fixed verifier it is 1.0. A result that was read as "SEED_NOISE_DOMINATED / reward unreachable" was actually "the task is at CEILING — there is nothing for GRPO to improve."
2. It poisoned the policy. GRPO samples rollouts, and LaTeX is likelier in sampling than in greedy eval. Every correct-LaTeX rollout scored -1, which actively pushed the policy away from correct formatting. A re-score corrects eval numbers but cannot undo weight updates — poisoned adapters must be RE-TRAINED. The smoking gun: one math run regressed on all 3 seeds (0.5167→0.35/0.38/0.42), exactly the poison mechanism's prediction.

The one-line durable lesson: audit verifiers for FALSE-NEGATIVES (completeness), not just false-accepts (soundness); a reward under-count poisons the policy, not just the eval.

A soundness gate — by construction — can never catch this class, because a correct-answer rejection mints no false accept. You need a completeness gate.

When to run this

• You wrote or are auditing a verifier (symbolic, execution, semantic, judge-based).
• A pass rate looks suspiciously low OR suspiciously uniform across arms (a verifier ceiling reads as "noise-dominated" / "no headroom").
• An RL/GRPO run REGRESSED capability (adapter worse than base) — a signature of a poisoned reward.
• Before promoting any adapter trained under a verifier that has not been completeness-audited.
• A verifier parser was changed (add a notation class to the battery; never assume "parse" means "parse correctly").

How — the completeness battery

The guard is a FIXED suite of canonical golds, each rendered in EVERY equivalent notation the verifier might receive, asserted ACCEPTED through EVERY verifier entry point.

1. Pick canonical golds that exercise the notation classes your domain hits. For symbolic math: plain sympy, LaTeX (\sin, \frac{a}{b}, e^{x}), unicode/prose (e^x, 2x, caret superscripts), fraction-vs-division, and exp-vs-e^. Six golds × ≥5 notations = 36 pairs is a usable floor.
2. Assert through EVERY entry point. A verifier with two doors (e.g. an RL reward function AND an eval oracle) can be sound at one door and incomplete at the other. The #908 bug backed BOTH provenance_bench.math_reward.reward_for_problem and agent.math_verifier.verify through one shared parser — test both.
3. Make it SOUND-aware. Every gold and every notation in a case must be GENUINELY, symbolically equal, so "accept" is always the correct verdict. The battery can only ever detect an under-accept; it can never license an over-accept. Do NOT add wrong-answer cases here — that direction stays owned by the soundness tests.
4. Wire it into CI, fail-closed when the verifier's dependency (e.g. sympy) is absent — a missing dependency means the run is not verifiable, so skip cleanly rather than mint a false green.

Reference implementation: tools/verifier_completeness_battery.py + tests/test_verifier_completeness.py, wired into .github/workflows/ci.yml.

The sibling: numeric-equality soundness

If your verifier falls back to numeric sampling to decide equality (common when a symbolic residue is transcendental), the sample points are a soundness hole. A FIXED small sample set can be colluded against: a wrong answer whose gold-difference is a polynomial with roots exactly at the sample points reads "equal". (The pre-#908 code sampled 4 fixed points; the exploit sin(x)+(x-0.5)(x-1.5)(x-2.5)(x+1.3) passed.)

Fix: decide polynomial residues EXACTLY (sympy.Poly(...).is_zero — a nonzero degree-d polynomial has ≤d roots, so no finite point sample can read "equal") BEFORE any sampling. Only a genuinely transcendental residue reaches the numeric probe, which should be a FIXED-SEED random battery of many points (≥32) over a wide domain requiring agreement at all decidable points — deterministic, byte-reproducible, no wall-clock/entropy nondeterminism. One-directional: a true-equal is zero everywhere, so this adds zero false-rejects.

Honesty rules (do not bypass)

• A completeness audit that finds nothing is a VALID result (a clean bill of health). Do not invent a notation class to justify the skill. State the clean result plainly.
• A re-score corrects EVAL numbers; it does NOT clear a trained adapter. Adapters trained on a poisoned reward must be RE-TRAINED. Record this distinction; do not let a re-score be read as "the adapter is now fine".
• candidateOnly:true, canClaimAGI:false. A verifier fix is measurement infrastructure, not a capability claim.
• Record the outcome (including a clean NULL) in agi-proof/failure-ledger.md with the numbers and what is NOT yet proven.