arborist/docs/verifier-semantic-gap-design.md

Closing the verifier's lazy-anchor semantic gap

Date: 2026-04-30 Scope: Design proposal for adding a soft semantic-entailment signal alongside the existing lexical claim-lattice verifier in aborist/qa/verify.py. Doc-only — no code in this commit. Successor to roadmap item #9 in docs/qa-modes-bench-2026-04-30.md. Audience: fox + future blackops shifts. Hard constraint: the soft signal is a demote-only sidecar. It never enters the proof path.

---

1. Problem statement

Today's verify_claim_lattice and verify_claim_lattice_json in aborist/qa/verify.py perform six deterministic, lexical checks on every (claim, pointer) pair. Check #5 is the topic of this proposal:

Claim's content tokens textually overlap the cited evidence span at coverage ≥ min_citation_coverage (default 0.30, lexical, case-insensitive substring).

This catches the shape of a citation mismatch but not its predicate. A claim and a span can share enough surface tokens to clear 30% coverage while the span never asserts the claim's relation. The model used training-data knowledge to write the claim, picked the topically-closest pointer the runtime offered, and the verifier said STRICT.

This is the long-tail "verifier semantic check (soft signal)" item from the bench journey doc:

"did the claim's predicate match the cited span's frame?"

1.1 Concrete failure cases

Case A — Great Wall elevation (surfaced live 2026-04-30 evening).

Question: "which side is the ground elevation highest throughout the span of the great wall of china, the north or south?" Mode: claim_lattice_pointer Verdict: STRICT, n_quotes=2, n_verified=2, lazy_anchor_ratio=0.5. Claim: "The ground elevation is higher on the northern side of the Great Wall of China." Cited span (E13): "...regions have traditionally been referred to as 'Outer China' because they are located beyond the Great Wall of China. ... China is bordered in the north, west and so..." Content tokens in claim ≈ {ground, elevation, higher, northern, side, great, wall, china}; tokens present in span ≈ {northern (stem-flexed), great, wall, china} → 4/8 = 50% coverage, well above the 0.30 floor. The cited span carries no elevation assertion at all. The model used training-time topology knowledge of the Wall and grabbed the topically-closest "north + Great Wall" chunk. The verifier had no way to detect that the predicate is_higher_than(north_side, south_side) is missing from the span.

Case B — JP-dinos / Triceratops & Operation Genesis (CLAUDE.md retrieval-pipeline & doc F5).

Question: "what dinosaurs were in the first jurassic park film?" Mode: claim_lattice (JSON). Several "verified" claims cite spans from Jurassic Park: Operation Genesis (a 2003 video game) rather than the 1993 film. The cited span genuinely contains Triceratops (the game indexed every dinosaur) and the claim text says "Triceratops appears in Jurassic Park" — coverage is 100%. Lexically perfect; semantically mis-rooted. The dinosaur token's the same; the claim's relation is appears_in(film=JP1, species=Triceratops); the span's relation is appears_in(video_game=Operation_Genesis, species=Triceratops). The current verifier cannot tell.

Case C — Boltzmann constant value.

Question: "what is the boltzmann constant?" Mode: claim_lattice_pointer. Inspected one STRICT run; the model emitted "The Boltzmann constant is approximately 1.380649×10^−23 joules per kelvin" cited to a chunk that mentions the constant by name and the unit "joule" but never states the numerical value. Coverage clears 0.30 because boltzmann, constant, joule, kelvin all appear; the value 1.380649×10^−23 does not. Same shape as case A: factually correct claim, partially-grounded citation, but the load-bearing predicate (the number) was emitted from training, not the span.

1.2 What these cases share

Across all three: claim and span talk about the same topic, so token overlap is high. The claim's load-bearing predicate (a relation, a number, a comparison) is absent from the span. This is the canonical NLI "non-entailment" pattern. Lexical coverage is the wrong instrument; entailment is the right one. We need to add an entailment-shaped check without compromising the determinism, content-addressability, or proof-path purity that v9.8 admissibility depends on.

The lazy_anchor_demote sidecar in verify_claim_lattice already proves the architectural pattern works: a soft signal computed at verify time, surfaced in the verdict for the renderer, and used to cap the audit_mode at HYBRID — never to invent STRICT. We extend that pattern.

---

2. Architectural constraints

Any design must hold every one of these. Violations are not negotiable.

1. Soft signals never enter the proof path. Per CLAUDE.md "Soft hash vs hard hash": SHA-256 is hard; embeddings/TF-IDF/entailment-scores are soft. The new score must NOT thread into cache_key, run_dag_root, the audit_events chain, or the canonical-JSON inputs of build_run_dag's verify_payload. Pattern to follow: existing pointer_id_distribution / lazy_anchor_ratio / lazy_anchor_demoted fields in the verdict — surfaced for the renderer, deliberately not folded into verify_hash.
2. Determinism: same inputs → same verdict. No PRNGs leaking through. ONNX/PyTorch with torch.use_deterministic_algorithms(True), fp32, model.eval(). Every model load from a pinned weights hash (sha256 of safetensors), with the hash logged but not in the proof path. Output thresholded to a boolean — same shape as lazy_anchor_demoted: bool.
3. Hermes is the only allowed external endpoint. https://hermes.ai.unturf.com/v1. No HuggingFace inference API, no OpenAI, no third-party hosted endpoints. Local model files are fine and preferred (CPU-runnable, sub-200M params).
4. Backward compatibility. Records under the current governance_policy_hash keep their verdicts. The new check is gated behind a new policy field (claim_lattice_semantic_check) with default false; flipping it on bumps the policy hash so new writes go under a fresh cache_key but old cached records still resolve under the old hash. Same migration pattern as the entity-policy and atomic-claim rollouts.
5. Demote-only. The semantic check may move STRICT → HYBRID. It may NEVER move HYBRID → STRICT, UNGROUNDED → HYBRID, or invent grounding the lexical path didn't find. STRICT remains earned, never inferred.
6. Latency budget. Current claim_lattice mean ~4.6s, claim_lattice_pointer ~4.4s. The semantic check must add < 1s typical, < 3s worst case for an answer with ≤ 12 claims.
7. Optional dependency. Same shape as mwparserfromhell: an extras group like aborist[semantic]. Installs without it set claim_lattice_semantic_check = False automatically; verdicts revert to today's behavior.

---

3. Candidate designs

Three options, each evaluated against constraints and the §1.1 cases.

3a. Lightweight NLI sidecar (cross-encoder)

A small NLI cross-encoder (cross-encoder/nli-MiniLM2-L6-H768 ≈ 80M, cross-encoder/nli-deberta-v3-small ≈ 184M, or MoritzLaurer/DeBERTa-v3-base-mnli-fever-anli ≈ 184M) loaded once at import time. Per-claim signature: score(premise=evidence_span, hypothesis=claim_text) → {entailment, neutral, contradiction}. Demote STRICT → HYBRID when all cited spans for a claim score entailment_prob < threshold.

• Accuracy on §1.1. High. NLI cross-encoders trained on MNLI+ANLI+FEVER reliably mark "Outer China beyond the Great Wall" / "north side higher" as neutral, and "Triceratops in JP1" / "Triceratops in Operation Genesis" as neutral or contradiction. Boltzmann numerical-value entailment is a known weak spot for small NLI models but the directional signal is right ("constant has unit joule per kelvin" entails "exists" but not "equals 1.380649e-23"); demotes correctly often enough.
• Latency. 80–184M-param cross-encoder on CPU, sequence length capped to ~512 tokens: ~30–80 ms per (claim, span) pair. With max 12 claims × 2 pointers/claim = 24 inferences, worst case ~1.9 s. Inside the < 3s budget. Typical (4–6 claims, 1 pointer each) is < 0.5 s.
• Dependency cost. New extra: aborist[semantic] adds transformers + torch-cpu + sentencepiece ≈ 250 MB install. Weights 70–700 MB; the smaller MiniLM variant fits in ~100 MB. Ship pinned by sha256.
• Determinism. fp32 with torch.use_deterministic_algorithms(True) and model.eval() is bit-exact across runs on the same hardware. Cross-hardware drift exists at the LSB; thresholding at 0.5/0.7 absorbs it. Same kind of "deterministic up to thresholding" the lazy-anchor demote already lives with.
• Integration. Drop-in extension of the verdict-construction tail of verify_claim_lattice and verify_claim_lattice_json. New helper _score_semantic_entailment(claim_text, evidence_span) -> (label, prob) gated on policy["claim_lattice_semantic_check"]. New verdict fields: semantic_entailment_scores (per-claim, render-layer only), semantic_demoted: bool, semantic_violations. The bool feeds the same demote pattern as lazy_anchor_demoted.

3b. TF-IDF predicate matching

Pure-Python heuristic: extract a (subject, predicate, object) triple from each claim using hand-rolled rules; same extraction on the cited span's nearest sentence to the claim's spotlight token. Score predicate similarity by cosine over TF-IDF vectors weighted toward verb/relation tokens; demote on score below threshold.

• Accuracy on §1.1. Mixed. Great Wall probably caught (claim's predicate is "is_higher_than" — the span has no elevation/comparison verb). Triceratops/Operation Genesis probably missed (both sides have "appears" — discriminator is the subject: film vs game). Boltzmann numerical fails fully (no verb-level distinction; missing element is a number). Catches maybe 1 of 3 named cases.
• Latency. Negligible.
• Dependency cost. Zero (aborist/distill/tfidf.py already implements pure-Python TF-IDF; reuse).
• Determinism. Trivially deterministic.
• Integration. Same hook point. Cheap to implement, but high false-negative rate on cases B & C, and the design pattern doesn't scale — every new failure shape needs new heuristics.

3c. Per-claim re-prompt to Hermes

Second LLM call per claim: "Does the following span support the following claim? Answer yes or no." temperature=0, max_tokens=4, single-token response.

• Accuracy on §1.1. Plausibly high. Hermes-3-8B is competent at narrow single-claim entailment. But: the same model that wrote the lazy-anchored claim is being asked to grade it. Self-evaluation bias is documented — confirms its own outputs.
• Latency. Doubles the LLM-call count. 12 claims = 12 extra round trips. Even with 4-way parallelism, ~1.5–3s, right at the ceiling. Also ties verifier latency to vLLM availability — when JSON-mode 5xx clusters hit (the 19-error morning), the semantic check would have also failed.
• Dependency cost. Zero new code dependencies; operational coupling to Hermes worsens.
• Determinism. temperature=0 necessary but not sufficient — vLLM batch-position effects + server-side prefix-cache can change tokenization. Reproducibility across days not guaranteed.
• Integration. Same hook point. Calls aborist.qa.client.ChatClient.complete per claim.

3d. Comparison summary

design	catches Wall	catches Tri/OpGenesis	catches Boltzmann	latency added	det.	dep. cost
3a NLI cross-encoder (MiniLM-class)	yes	yes	weak-yes	0.5s typ / 1.9s worst	high	+250MB install, +100MB weights
3b TF-IDF predicate	maybe	no	no	negligible	full	none
3c Re-prompt Hermes	yes	yes	yes	1.5–8s	medium	none, ops coupling

---

4. Recommendation: 3a (NLI cross-encoder), default off, opt-in by policy

3a wins on accuracy across all three named failure cases and stays inside the latency budget. 3b's miss rate on JP-dinos and Boltzmann is too high to justify even at zero cost — those are the cases that motivated this work. 3c's self-evaluation bias and operational coupling outweigh its zero-install cost.

Chosen model: cross-encoder/nli-MiniLM2-L6-H768 (≈80M params, ~100MB weights). Smallest CPU-runnable cross-encoder with serviceable MNLI/ANLI accuracy. Pinned by sha256 of the safetensors file. Threshold default entailment_prob < 0.50 triggers demote — tuned via §5.

4.1 Implementation plan (high-level, 8 steps)

1. Add optional dep. aborist[semantic] extras group in pyproject.toml pulling transformers>=4.40, torch>=2.2 --extra-index-url cpu, sentencepiece. Weights distributed out-of-band (pinned-revision download with sha256 verification at first load); cached under ~/.aborist/models/<sha>/.
2. New module aborist/qa/semantic_check.py. Single public function score_entailment(premise: str, hypothesis: str) -> tuple[str, float] returning (label, entail_prob). Module-level lazy-loaded model object. import semantic_check is cheap; first call pays the ~2s load. Soft-fails to (None, None) if transformers is not installed.
3. Policy fields. Add to DEFAULT_POLICY and DEFAULT_QUERY_POLICY:
   • claim_lattice_semantic_check: bool = False
   • claim_lattice_semantic_threshold: float = 0.50
   • claim_lattice_semantic_model: str = "cross-encoder/nli-MiniLM2-L6-H768"
   • claim_lattice_semantic_model_sha256: str = "<pinned hex>" These fold into governance_policy_hash automatically.
4. Wire into verify_claim_lattice and verify_claim_lattice_json. After the lexical six-check loop completes and audit_mode is determined, but before lazy_anchor_demoted is computed: if policy bool is set, run score_entailment over each verified (claim_text, evidence_span) pair. Aggregate per-claim: a claim is "semantically supported" iff at least one of its pointers entails. If audit_mode == "STRICT" and ANY claim fails semantic support, demote to HYBRID and append a SEMANTIC_NON_ENTAILMENT violation.
5. New verdict fields, render-layer only. semantic_entailment_scores: list[dict] (per claim: {claim_idx, pointer_id, label, prob}), semantic_demoted: bool, semantic_violations. None get folded into build_run_dag's verify_payload — same architectural choice as pointer_id_distribution / lazy_anchor_ratio. The violations list (which IS in the verify payload) carries only the kind tag (SEMANTIC_NON_ENTAILMENT) and the count, not the per-claim scores. Demote stays operator-visible in the audit chain without folding the soft probability values themselves into the hash.
6. Renderer surfaces the smell. When semantic_demoted == True, the human renderer prepends [non-entailment smell — N of M claims show low entailment] to the answer prefix, identical pattern to today's lazy-anchor smell prefix.
7. Tests. Three live fixtures matching §1.1 cases: Great Wall elevation must demote, Boltzmann constant numerical claim must demote, JP-dinos Operation-Genesis citation must demote. Plus a positive-control: "who painted the mona lisa" must NOT demote. Add to tests/test_qa_quality_live.py gated on semantic_check=true.
8. Bench impact, before/after. Run make bench-qa with claim_lattice_semantic_check=true and =false on the same question set. Compare strict-rate, grounded count, mean latency. Land the policy default at false with the bench numbers in the commit message; defer flipping the default to a separate doc + commit once we've seen the bench delta.

---

5. Bench impact estimate (speculative but disciplined)

Sampling current bench data at bench/qa_results/2026-04-30T21-35-04Z.jsonl:

• 75 claim_lattice_pointer rows total, ~16 STRICT in the post-stop-sequence run.
• 75 claim_lattice (JSON) rows total, ~37 STRICT.
• Across both lattice modes, an estimated 5–10 STRICT verdicts per 22-question bench (n=3) look like §1.1-shaped lexical-pass / semantic-fail cases.
• Expected demote: ~5–8 of the current ~53 STRICT verdicts move to HYBRID. That's roughly a 5–10pp drop in strict-rate, with zero drop in grounded count.
• Mean latency cost: +0.4s typical (4–6 claims × 1–2 pointers each × ~50ms per scoring call), +1.5–2s on broad-descriptive 12-claim tail.

This matches the honest-verdicts-beat-optimistic-ones principle in CLAUDE.md: each demoted verdict is one false-positive STRICT removed from the audit ledger. The strict-rate goes down; the substrate's claims about itself become more truthful.

Quote-mode is out of scope for this design (it's a separate verifier path with its own verbatim-substring contract). If the quote-mode false-STRICT problem (failure mode F4 in the bench journey) needs addressing later, the same NLI sidecar could be wired into verify_quotes post-classification, but that's a separate design.

---

6. Open questions for fox

1. Model choice. Default to cross-encoder/nli-MiniLM2-L6-H768 (~80M, fastest)? Or step up to cross-encoder/nli-deberta-v3-small (~184M, more accurate, ~2× slower)? Recommendation: smaller for now; revisit if accuracy disappoints.
2. Threshold tuning policy. Default entailment_prob < 0.50 triggers demote. Hardcoded constant (folds into source identity) or policy[...] field (folds into governance hash, lets per-deployment tuning bump cache-key cleanly)? Recommendation: policy field.
3. Persistence of the soft signal. lazy_anchor_ratio is render-layer only — never written to providence_cache. Should semantic_entailment_scores follow same pattern, or should the semantic_demoted boolean flag be persisted as a new column on providence_cache so an operator querying old records can tell why a HYBRID is HYBRID? Recommendation: bool stays in violations (already persisted via run_dag_blob), per-claim prob array does NOT persist. Easy migration, no schema bump.
4. Default-on vs default-off. Plan above is default-off, opt-in via policy. Alternative is default-on, which bumps everyone's governance_policy_hash and stales every record on next lookup. Recommendation: default-off until two clean benches under the new path confirm no regression on positive controls.
5. Hardware drift. If a deployment swaps CPU vendors (Intel BLAS vs AMD vs ARM), float arithmetic differs at the LSB, occasionally crossing the 0.50 threshold for marginal cases. Proof path doesn't care (soft signal), but two operators looking at the same record could see different semantic_demoted bits if their machines disagree. Acceptable? Recommendation: yes — soft signals are by definition not bit-stable across machines, and the v9.8 audit chain only commits to inputs that ARE bit-stable. Worth fox's explicit blessing.
6. JP-dinos Operation-Genesis case overlap with retrieval-side fixes. The JP-dinos case is also on the retrieval-side roadmap (extending noisy markers to catch "(NES game)"-style parens). If retrieval-side filtering lands first, the verifier-side semantic check would still catch any other topic-aliased citation that retrieval didn't filter. Complementary, not duplicative. Worth doing both?

---

100-word summary

The claim-lattice verifier passes any (claim, span) pair with ≥30% lexical token overlap, but topical overlap can mask predicate mismatch. Three live cases — Great Wall elevation, JP-dinos Triceratops/Operation-Genesis, Boltzmann constant value — landed STRICT despite the cited span never asserting the claim's load-bearing relation. Recommended fix: a small NLI cross-encoder (~80M params, CPU-runnable, deterministic at fp32) computing entailment per (claim, span), gated behind a default-off policy field. Soft signal demotes STRICT→HYBRID only — never inverts UNGROUNDED, never enters the proof path, mirrors today's lazy_anchor_demoted pattern. Estimated ~5–8 STRICT demotes per 66-run bench, +0.4s typical latency.