arborist/docs/benchmarks.md
russell@unturf.com b6bb31a836
docs+code: ground §12 judge pipeline in the actual judge_code.py
The §12.1 pipeline I added was second-hand from benchmark-matrix.md
and got several things wrong against the code:
- listed 4 verdicts; actual is 5 (missing FABRICATED — the
  fabrication-vs-WRONG split that energy-cogs §5.5 leans on for the
  qwen-fabricates / hermes-abstains finding)
- "θ=0.85" was right by accident — but it's the code-judge-pinned
  _CODE_JUDGE_THETA_CONTRA constant, raised from the manifest 0.5
  default after measuring 114 FPs in the 0.5-0.75 band
- omitted the short-answer entity-grounding fast path (which runs
  BEFORE NLI per the 2026-05-19 Poland-Tusk smoke)
- omitted the HYBRID rescue ladder (NLI entail / entity rescue /
  2026-05-21 verbatim-quote-on-topic rescue)
- conflated WRONG and FABRICATED (the subject-in-gold split is what
  distinguishes "source has the topic but a different value" from
  "source silent on the topic")

Rewrote §12.1 grounded in `bench/judge_code.py:judge()` (its own
docstring at line 501-528 is the truth on rule order), with file:line
citations and the verdict-mapping in full.

Also fixed a real artifact-vs-doc drift INSIDE the judge: the
module-top docstring still claimed θ_contra default 0.5 and omitted
the short-path and the WRONG/FABRICATED split. Updated to match the
authoritative judge() docstring + current code.

No behavior change — docstring + benchmarks doc only.
2026-05-22 19:17:28 -04:00

25 KiB
Raw Permalink Blame History

Benchmarks — orientation, harnesses, fixtures, discipline

Arborist ships two bench harnesses, four question fixtures, and a signal-floor discipline pinned across the substrate. This doc is the canonical entry point. Three companion docs cover specifics:

File Purpose
docs/bench-maxing.md Discipline rules (5pp signal floor, etc.)
docs/qa-modes-bench.md Historical journal — running addendum log
docs/bench-emergent-design.md Random-word stress-test design rationale
docs/qa-modes-bench-2026-04-30.md Frozen point-in-time bench (Apr-30 baseline)
docs/energy-cogs-benchmark.md qwen vs hermes — GPU energy COGS + quality-per-dollar (Dav1d-audience report)
docs/benchmark-matrix.md Control-arm (solo vs substrate) A/B matrix + the deterministic code judge

Read those when you need the why or the long-form data. This file covers the what, where, and how.

1. Three harnesses, three purposes

1.1 bench/qa_sweep.py — curated QA-quality bench

Runs a fixture file × answer modes × n samples. Persists a JSONL of per-row results plus a markdown summary. Used for:

  • Regression checks before merging substrate changes.
  • A/B cycles on policy knobs (cap on/off, reminder on/off, preflight enabled/disabled).
  • Per-mode strict-rate tracking over time.

Run via make bench-qa or bench/qa_sweep.py directly. Bench rows carry ~25 fields per cell, including the four-rung label (audit_mode), the verifier-method, the violation kinds, the preflight QuestionState projection (preflight_logical_statuses, preflight_question_shape, etc.), the quantifier classifier output (quantifier_intensity, scope_bound_hint, claim_cap_applied), the preflight stage hash 12-char prefix (#000009 §7.2), and a per-stage timing breakdown (preflight_ms, soft_preflight_ms, search_ms, context_ms, llm_ms, persist_ms, total_ms).

1.2 scripts/bench_emergent.py — random-word stress test

Picks three random words from /usr/share/dict/words, asks Hermes (at temp 0.8) to weave them into a creative question paragraph, then sends that paragraph to arborist. Logs every cycle to bench/emergent_log.jsonl as one JSONL line. Designed for blue-moon cadence, not every-commit benching — the combinatoric word space surfaces failure shapes the curated bench doesn't reach.

The teacher review step is intentionally not automated. Fox brings interesting log entries to a teacher model (Claude Opus 4.7 in the current setup) and asks for guidance: did the answer match the question? Novelty class (known_truth_grounding / emergent_synthesis / novel_claim / no_signal)? Which hyperparam to tune next?

Run via make bench-emergent (default EMERGENT_N=10) or make bench-emergent EMERGENT_N=100 for a longer cycle. See docs/bench-emergent-design.md for the design rationale.

1.3 bench/control_ab.py + watt_* — cross-model cost & quality-per-dollar

This is how we benchmark qwen vs hermes with arborist, on two axes that multiply into quality-per-dollar. Full living report (and the Dav1d-facing writeup) in docs/energy-cogs-benchmark.md; this is the orientation.

Two rigs, run on the same harness (the GPU work happens on the producer box, never in arborist's python+sqlite3 core):

rig A rig B
model Qwen3.6-27B UD-Q4_K_XL (llama.cpp) Hermes-3-8B FP8 (vLLM)
GPU RTX 4090, ai.foxhop.net (isolated for the bench) RTX 3090, 3090-ai.foxhop.net (live/public)

Value axis — bench/control_ab.py. Runs the same model two ways: solo (question only, no retrieval/verifier) vs substrate-ON (full query() — 4-route FTS5 → context → LLM → verifier), n=30 per fixture, grades each answer with the judge (§12). Headline finding: the substrate lifts both models 213× and they nearly converge (an 8B and a 27B reach similar grounded quality — grounding comes from retrieval+verify, not parametric size).

Cost axis — bench/watt_bench.py / watt_calibrate.py / watt_probe.py. Measures GPU joules per token by slope calibration (prefill J/input-tok and decode J/output-tok measured separately — they differ 3540×), times the real token mix per query, at a site --price-per-kwh. Power states are measured at runtime, never hardcoded; cache-miss is forced so we time generation not a SQLite lookup. Result: a grounded answer costs **$0.070.16 per 1,000 queries** of GPU electricity (hermes-8B cheaper than qwen-27B — but that's a 4-way confound: params × quant × engine × card, not "8B vs 27B" alone). The dominant cost is prefilling the retrieved context (~⅔ of substrate GPU energy), not generating the answer.

Run the value axis via make control-ab (N=… FIXTURE=…); the watt instruments run directly — bench/watt_calibrate.py / watt_bench.py, with make rapl-access first for CPU-package power. Invocations and raw artifacts are in docs/energy-cogs-benchmark.md §8. All value-axis grading is done by the deterministic code judge (§12) — an Opus LLM-judge was attempted for #000057 and abandoned (too expensive per call, ~79.5 % JUDGE_ERROR rate-limited, burned coding quota); it never produced usable verdicts at scale and is gated off so it can't re-burn.

2. Four question fixtures

bench/qa_questions.txt                                — 75 questions
bench/qa_questions_smoke.txt                          —  smoke test
bench/qa_questions_quantifier_subset.txt              —  9 questions
bench/qa_questions_quantifier_baseline.txt            —  1 question
bench/qa_questions_metacog_subset.txt                 — 28 questions
Fixture Use case Cell size at n=3 × 3 modes
qa_questions.txt Full regression bench. Run before merging substrate changes. Wide coverage + corner cases. 675 runs, ~3-3.5h
qa_questions_smoke.txt Smoke test on 1-2 questions. Use to confirm a CLI flag wires through correctly. 3-6 runs, ~30s
qa_questions_quantifier_subset.txt 9 broad-quantifier questions (7 unbounded + 2 bounded). Use for A/B cycles on #000008 knobs. 81 runs, ~7-15min
qa_questions_quantifier_baseline.txt Single broad question for narrow n=3 baseline measurement. 9 runs, ~2-4min
qa_questions_metacog_subset.txt 28 questions targeting each #000010 detector (temporal, contradiction, false-premise, out-of-corpus) plus mixed multi-trigger + well-formed controls. 252 runs, ~25-35min

When choosing a fixture: ask whether you're measuring the substrate as a whole (full bench), a specific feature (broad-quantifier subset, metacog subset), or just wiring correctness (smoke).

3. The signal floor — n=3 × 9 = 27 sample minimum, 5pp delta floor

Per docs/bench-maxing.md:

  • 5pp floor for STRICT-rate deltas at n=3 × any-fixture sample size. Differences below this are Hermes nondeterminism, not signal. Quote-mode often jitters ±10pp on 27-sample cells.
  • Mean-ratio + UNGROUNDED-rate are tighter signals at the same sample size — they aggregate per-row values rather than counting discrete verdicts.
  • n=5 verification when an A/B cell sits within the noise band (e.g. 0.30 vs 0.33 STRICT-rate is 3pp — within noise; n=5 on the closer cell tightens the variance).
  • vLLM concurrency saturates at c=3-4. Going higher slows per-call latency without parallelizing harder. Default c=4.

Don't tune to a single bench cycle. Always have a baseline + an A/B cell + (sometimes) a verification cell.

4. Make targets cheat sheet

# Curated QA bench (default: bench/qa_questions.txt × 3 modes × n=3)
make bench-qa

# Same but with limit / different file
.venv/bin/python bench/qa_sweep.py \
    --questions bench/qa_questions_quantifier_subset.txt \
    --shards-dir ~/.arborist/shards --n 3 --concurrency 4 \
    --out-dir bench/qa_results

# A/B cycle: flip a policy knob for one bench cell
.venv/bin/python bench/qa_sweep.py \
    --questions bench/qa_questions_quantifier_subset.txt \
    --shards-dir ~/.arborist/shards --n 3 --concurrency 4 \
    --policy quantifier_guard_apply_caps=true \
    --policy quantifier_reminder_enabled=true

# Resume an interrupted bench (same --seed, append to existing JSONL)
.venv/bin/python bench/qa_sweep.py \
    --resume bench/qa_results/2026-05-03T19-30-13Z.jsonl \
    --seed 0

# Smoke test — quick sanity of the wiring
.venv/bin/python bench/qa_sweep.py \
    --questions bench/qa_questions_smoke.txt --n 1 --concurrency 1

# Random-word stress test (blue-moon cadence)
make bench-emergent              # n=10 default
make bench-emergent EMERGENT_N=100

5. The bench-row schema

Every row in bench/qa_results/<stamp>.jsonl carries (current shape — fields are additive across versions):

Identity & verdict:

  • question, answer_mode, audit_mode, verifier_method
  • n_quotes, n_verified, ratio
  • cache_key (12-char prefix)
  • preflight_hash (12-char prefix; see #000009 §7.2)
  • model_profile_id

Diagnostics:

  • format_collapsed (pointer-mode only signal; #000008)
  • violation_kinds (sorted list of unique kinds)
  • lazy_anchor_ratio, pointer_id_distribution
  • answer_brackets, answer_pointer_count, answer_chars_with_brackets, raw_meaningful_line_count
  • deflection_kind, subject_anchor, subject_in_answer
  • metaphor_deflection_kind, metaphor_cue_count, metaphor_overlap_count

Preflight projection (#000010):

  • preflight_logical_statuses (list)
  • preflight_question_shape, preflight_result
  • preflight_temporal_sensitivity
  • preflight_has_false_premise, preflight_has_contradiction
  • preflight_corpus_requirement

Quantifier classifier (#000008):

  • quantifier_intensity, quantifier_matched_token
  • scope_bound_hint, quantifier_explicit_count
  • claim_cap_applied

Capacity:

  • prompt_chars_total, prompt_chars_evidence, prompt_chars_system, prompt_chars_question
  • answer_chars

Directive compliance (per-row pass/fail for the seven-point program directives observable from a single bench row):

  • directive_compliance dict keyed on D2/D3/D4/D6/D7

Time:

  • elapsed_s, iso_ts, error

The markdown summary alongside the JSONL renders aggregate views (per-mode strict-rate, format-collapse + violation kinds table, strict-rate-by-prompt-size buckets, directive coverage).

6. The journal — where headlines live

docs/qa-modes-bench.md is the rolling research log for the QA bench. Each substantial bench cycle adds a new addendum (or refines an existing one). The 2026-05-02 baseline is the frozen authoritative state of the substrate before #000008/9/10/11 landed; subsequent addenda compare against it.

Current addenda:

  • 2026-05-02 baseline — pre-preflight authoritative state.
  • Addendum 1 (broad-quantifier A/B from #000008 §12.6).
  • Addendum 2 (preflight on vs off, 9-question broad subset).
  • Addendum 3 (full 75-question regression check post-flip).
  • Addendum 4 (metacog-trigger detector validation, 6 → 28 question fixture).

When a new bench cycle produces a substantive finding, add an addendum or refine an existing one. Bench artifacts (JSONL + markdown) live in bench/qa_results/ and are gitignored — only headlines + cross-references go in the journal.

Per-ticket bench data lives in the relevant ticket file's §12 or §13 (e.g. docs/tickets/ticket-000008-...md §12 carries the four-cell A/B; #000010 §13 has three sub-validations; #000006 has the rolling-amend pattern across multiple cycle counts).

7. The bench-emergent log

bench/emergent_log.jsonl is a long-running append-only log of random-word stress cycles. Each entry has:

{
  "ts": <unix>, "iso_ts": "2026-05-04T...",
  "words": ["dismally", "heats", "Jamaicans"],
  "question": "<model-generated question paragraph>",
  "answer": "<arborist's answer>",
  "audit_mode": "STRICT|HYBRID|UNGROUNDED",
  "verifier_method": "claim_lattice",
  "n_quotes": 3, "n_verified": 0,
  "violation_kinds": ["CITATION_MISMATCH", "TOO_MANY_EVIDENCE_IDS"],
  "metaphor_deflection_kind": "no_signal",
  "metaphor_cue_count": 2, "metaphor_overlap_count": 2,
  "sources": [{"title": "...", "uri": "...", "used": false}, ...],
  "answer_seconds": <float>, "total_seconds": <float>,
  "teacher": <reserved for human review>
}

Findings live in docs/tickets/ticket-000006-bench-emergent-findings.md as rolling amends — each new cycle batch produces a new amend with the verdict shift, violation profile, and tuning candidates.

8. How to run a focused A/B

Pattern from #000008 §12 (broad-quantifier four-cell A/B):

  1. Pick a fixture matching the feature under test (broad-subset for quantifier work; metacog-subset for metacognition work; smoke for wiring sanity).
  2. Run the baseline — same fixture, default policy.
  3. Run the cell — same fixture, one policy knob flipped via --policy KEY=VALUE. Repeat for each independent knob.
  4. Compare — STRICT-rate, mean-ratio, UNGROUNDED-rate, FORMAT_COLLAPSED rate, dominant violation kinds. Apply the 5pp floor to STRICT-rate; mean-ratio and UNGROUNDED tend to be tighter.
  5. Verify with n=5 if a cell sits within the noise band.
  6. Document — add an addendum to docs/qa-modes-bench.md or a new §12.x / §13.x to the relevant ticket file.

The four-cell A/B in #000008 (preflight off / reminder only / cap only / cap+reminder) is the canonical pattern for measuring multi-knob features.

9. How to interpret results

STRICT-rate = the fraction of cells where the verifier could prove every claim grounded against cited evidence. Most direct quality metric, but noisy at small sample sizes.

HYBRID-rate = mixed verdicts (some claims grounded, some not). Often more informative than STRICT-rate when a feature's job is to rescue UNGROUNDED → HYBRID rather than HYBRID → STRICT.

UNGROUNDED-rate = honest "the verifier could not ground." Lower is generally better, but UNGROUNDED on questions the corpus genuinely can't answer is the correct outcome — the substrate preferring UNGROUNDED to fabricated STRICT is the architectural win named in docs/seven-point-program.md D7.

Mean ratio = mean of n_verified / n_quotes across rows. Aggregates per-row values rather than counting verdicts; tighter at small sample sizes than STRICT-rate.

FORMAT_COLLAPSED rate = pointer-mode-specific gauge of whether the model is following the [E\d+] citation protocol. Zero is the goal; non-zero means the model emitted free prose without pointer tags.

Violation kind distribution = per-mode tallies of which hard checks fired most often. Gives the operator a per-failure-mode view of the substrate's weaknesses.

Directive compliance = per-row pass/fail for the seven-point-program directives (D2/D3/D4/D6/D7). Substrate-level hygiene check; should be ~100% on lattice modes.

Audit-line tails (rendered by arborist/cli.py:_render_warrant_tail):

  • Hard tails: · warrant missing, · title mismatch, · format collapsed, · broad cap N, · broad rejected, · broad unbounded, · broad runaway, · false premise, · contradictory, · stale risk, · out of corpus, · frame ambiguous.
  • Soft tails (advisory): · soft: <label> (#000011 sidecar output; SOFT_DISABLED / SOFT_PARSE_FAIL / SOFT_WELL_FORMED suppress).

A row with multiple tails composes them: EVIDENCE-WARRANTED · via claim_lattice · false premise · soft: time sensitive is a verdict the substrate reached but with two distinct preflight warnings worth the operator's attention.

10. Operator commands cheat sheet

# Inspect preflight stage payload from any cache row
arborist providence --show-preflight CACHE_KEY_PREFIX

# Single query with all preflight knobs flipped
arborist query "winners of all major sports?" \
    --apply-quantifier-caps --reject-broad --soft-preflight

# Dry-run — assemble context but skip LLM
arborist query "..." --dry-run

# Force fresh inference (delete prior cache row first)
arborist query "..." --burn

# Show raw JSON record instead of human render
arborist query "..." --json

The Makefile exposes most of these via shorthand:

make query Q="..." BROAD=1 REJECT_BROAD=1 ALLOW_BROAD=1 \
    BURN=1 JSON=1 ANSWER_MODE=claim_lattice

See the Makefile directly for the full set.

11. Deterministic retrieval instruments (no-LLM)

The bench-maxing rule (CLAUDE.md): when a lever's failure class is below the n=3 / 5pp noise floor, fix the instrument — mine ground-truth-carrying questions and grade by deterministic retrieval, not by the LLM verifier. These instruments take query --dry-run output only: no LLM, no verifier, no judge, no noise floor, scalable to the corpus. They measure retrieval surfacing — necessary-not-sufficient for STRICT, and they complement, never replace, the curated adversarial set (the verifier-honesty gate).

  • bench/mine_questions.py — mines questions whose target article is known by construction (surface-variant of a corpus title). Classes: numeral (Roman↔ordinal), accent, hyphen, honorific (Mt↔Mount), amp (&↔and), brit (US↔UK spelling), stale (temporal fabrication-bait, control_ab only).
  • bench/recall_at_k.py — recall@1/@3/@k of the known target on a mined fixture. Returns rank, so recall at every k is free from one retrieval (a too-lenient k hides a rank-only lift — report @1/@3/@k).
  • bench/jaggedness.py (make bench-jaggedness, #000060) — does retrieval surface the SAME target for a question's canonical phrasing (title verbatim) AND its surface-perturbed phrasing? A non-jagged retriever agrees; a jagged one finds "Henry VIII" but misses "Henry the eighth". Reuses recall_at_k.probe + mine_questions._surface_variant.
    • J_norm (binary) = fraction of titles where canonical & perturbed DISAGREE on surfacing the target @k (XOR). Lower = more non-jagged.
    • graded mean |Δrank| over titles where both surfaced — rank instability the binary metric can't see.
    • Distinguishes a true recall-miss (both phrasings miss = not jagged) from jaggedness (one surfaces, one doesn't). Feeds #000012's ForkScore ΔJaggednessReduction: a retrieval fold that lowers J_norm without lowering recall is a non-jagged win.
    • The A-vs-C answer-quality jaggedness delta (does the substrate make answers more consistent across variants than the bare model?) is the LLM+judge version — rides bench/control_sweep.py over variant groups, gated v2.

12. The judge — how bench answers are graded

A grading judge appears only in the cross-model value bench (§1.3) — deciding whether a model's answer is correct-and-grounded. It is external bench science and must not be confused with arborist's in-system verifier (arborist/qa/verify.py), which decides audit_mode on the proof path and is bound by the "no LLM-as-judge in the verifier" rule. The bench judge sits outside both arms (solo and substrate) and grades post-hoc; it never touches either system's internals.

Verdict vocabulary (closed, so aggregation is deterministic): CORRECT_GROUNDED / WRONG / ABSTAINED / JUDGE_ERROR.

The judge is the deterministic code judge. Every value-axis number in docs/energy-cogs-benchmark.md was graded by it. There is no LLM-judge running on this path.

12.1 Code judge — bench/judge_code.py

Deterministic, no LLM, no quota. Five verdicts: CORRECT_GROUNDED / WRONG / FABRICATED / ABSTAINED / JUDGE_ERROR. The WRONG-vs-FABRICATED split is what powers the bare-model failure-style finding in energy-cogs §5.5 (bare qwen fabricates, bare hermes abstains; the substrate fixes both).

Authoritative source: bench/judge_code.py judge() at line 493 — its own docstring (line 501-528) is the truth on rule order. Pipeline, first hit decides:

  1. Empty / no-gold guards. Empty answer → ABSTAINED; empty gold → JUDGE_ERROR.
  2. Explicit abstention phrases — broad lexical regex including the "I do not have access to information / context" Hermes family that the original narrow patterns missed. Match → ABSTAINED.
  3. Short-answer entity-grounding fast path. When the answer is short, asserts at least one specific, every specific is in gold, AND the question's subject anchor is in gold → CORRECT_GROUNDED. Runs before NLI (since the 2026-05-19 Poland-Tusk smoke): NLI's clause-level aggregation can mis-fire as contradiction on multi-PM lists even when the answer is right; positive lexical evidence wins.
  4. Strong NLI contradictionarborist.qa.nli.shadow_check, θ_contra = 0.85 (code-judge-pinned _CODE_JUDGE_THETA_CONTRA, raised from the manifest's 0.5 default after measuring 114 FPs in the 0.5-0.75 band). max_contradiction ≥ 0.85WRONG.
  5. Lexical verifier vs goldarborist.qa.verify.verify_quotes (the existing quote → span → entity → paraphrase ladder), then map:
    • STRICTCORRECT_GROUNDED
    • HYBRID + NLI entail ≥ 0.55 (_CODE_JUDGE_THETA_ENTAIL_CORROBORATE) → CORRECT_GROUNDED
    • HYBRID + subject-anchor-in-gold + every specific in gold → CORRECT_GROUNDED (entity-grounding rescue)
    • HYBRID + ≥1 verbatim quote verified + on-topic + no unsourced numeric specific + not NLI-contradicted → CORRECT_GROUNDED (2026-05-21 relaxed rescue, 2d31866: unsourced proper-nouns treated as aliases / paraphrase, but a wrong date/count is held back)
    • HYBRID otherwise → JUDGE_ERROR ("code judge ambiguous … residue for LLM judge")
    • UNGROUNDED + specifics-not-in-gold + subject-in-gold → WRONG (source has the topic but a different value)
    • UNGROUNDED + specifics-not-in-gold + subject-not-in-gold → FABRICATED (source silent on the topic)
    • UNGROUNDED + no asserted specifics → ABSTAINED (thin / non-answer, not a fabrication)

Claim-lattice JSON envelopes are unwrapped to prose (_unwrap_claim_lattice_json) before any rule runs, so substrate-CL grades on equal terms with solo-prose. Each Verdict carries a decision trace (rules_fired, NLI probabilities, subject anchor, specifics, audit_mode) — fully replayable. JUDGE_ERROR is reserved only for the HYBRID-without-corroboration class (the ~10 % residue after the 2d31866 HYBRID-rescue strengthening; energy-cogs §5.5); everything else lands on a concrete verdict.

Self-test: bench/judge_code.py:self_test() (make judge-self-test), gating before any control-ab run. The pipeline cross-reference (older, shorter) is docs/benchmark-matrix.md "## The judge"; used in context in docs/energy-cogs-benchmark.md §5.5.

12.2 Why there is no LLM judge in active use — bench/judge.py (abandoned)

An Opus headless judge (claude -p) was attempted for #000057 as "external bench science." It did not work in practice:

  • ~79.5 % of its verdicts came back JUDGE_ERROR — rate-limited by the Anthropic API on a huge-N sweep, per docs/qa-modes-bench.md.
  • Each call was expensive enough that completing a real sweep would have consumed the coding-agent's quota for unrelated work; the experiment burned Opus quota and wasted dev time wiring it up (f63b00d9dc02e4, the wakeup call for the CLAUDE.md "Budget discipline" rule).
  • It is now fail-closed gated off by an env flag (ARBORIST_JUDGE_ENABLE=1) so a stray re-run can't re-burn the budget — a guardrail, not a feature flag a reviewer should treat as available.

The intended methodological hygiene (hermetic / blinded / grounded / structured / audited; stated same-family threat-to-validity) is preserved in the bench/judge.py module docstring as a record of what would be required of any future external SOTA judge — it is not a description of an active grading path. Re-introducing it needs a different-family SOTA model (per the same-family threat note) AND fox's explicit go on spend.

To forward to a reviewer (Dav1d): docs/energy-cogs-benchmark.md (qwen-vs-hermes, already Dav1d-audience — shows the code judge grading in §5.5/§8) + this §12. The separate docs/relevance-and-veto-synthesis-for-dav1d.md covers the in-system verifier / veto layer (proof-path; a different thing from bench grading) and should not be confused with this section.