Spec: Claim Verification — Decomposition, Span Matching & Scoring (F7 math)¶

File: .ai/specs/core-engine/2026-07-02-claim-verification.md Status: Approved (F7 math review complete 2026-07-04 — conditions incorporated in v0.2, incl. a review-mandated change from arithmetic to geometric fusion; see Changelog) Owners: Planner lane Related: PR-052; memory-planner spec (evidence plan), generation-orchestration spec (draft + markers), ingestion-provenance spec (spans), eval-harness spec (measures this)

1. Overview¶

Defines how a generated draft decomposes into atomic claims, the hybrid matcher that scores each claim against the evidence plan's spans, the verdict bands, unsupported-claim policy, and the trace record that makes every answer auditable.

2. Problem Statement¶

Generation without verification is confident hallucination with citations. The hard parts needing pinned math: what counts as one claim; how "supported" is computed such that paraphrase matches but fabrication does not; what happens to unsupported text; and how the whole judgment is recorded reproducibly.

3. Proposed Solution¶

Decomposition: the draft is decomposed by an LLM call (same LlmProvider, constrained JSON output: list of {claim_text, draft_span, cited_markers[]}) — claims are atomic declarative statements; non-factual text (hedges, transitions, questions) is classed non_claim and skipped. Matching: for each claim, candidate spans = cited markers' spans ∪ top-m (m=8) plan spans by embedding similarity to the claim. Per (claim, span): match = clamp01(cos(emb(claim), emb(span)))^β × lex(claim, span)^(1−β), β = 0.65 — geometric fusion, review-mandated (same form and same guards as the approved confidence-decay §5): cos is clamped to [0,1] BEFORE use (raw cosine spans [−1,1]), and β ∈ {0,1} takes fast-paths before any pow evaluation. Rationale for geometric over the drafted arithmetic blend: arithmetically, a topically-similar fabrication (cos ≈ 0.8, lex ≈ 0.2) scores 0.65·0.8 + 0.35·0.2 = 0.59 → "partial", which makes §12's planted-falsehood metric unachievable; geometrically the same inputs give ≈ 0.49 → unsupported, while a genuine paraphrase (cos ≈ 0.9, lex ≈ 0.6) still clears "supported" at ≈ 0.78. Both signals must be present; neither can outvote the other's absence. lex is pinned (review condition) as IDF-weighted token coverage: tokenize claim and span (NFC normalize → UAX-29 word segmentation → Unicode simple casefold → drop pure-punctuation tokens; NO stopword lists — language-agnostic), idf(t) = ln(1 + N/df(t)) computed over the plan's spans only (self-contained and deterministic given the plan), lex = Σ_{t ∈ claim∩span} idf(t) / Σ_{t ∈ claim} idf(t) with multiset intersection. Coverage rather than F1 so a long span containing verbatim support is not punished for its length; IDF so function words cannot inflate the score. Numeric gate (OQ-1 resolved): if the claim contains ≥1 numeric token (numbers, dates, percentages — normalized: digit-group separators, currency symbols and % stripped; dates to ISO components; exact match after normalization, v1) and the span contains no matching normalized numeric, the WHOLE pair score is capped at 0.2 — capping only the lexical term was insufficient (0.65·1 + 0.35·0.2 = 0.72 would have read "partial" with the wrong figure). Doctrine: figures require figure evidence — a claim asserting a number no span states is unsupported by construction. Claim score = max over candidates; truth-class spans only (cache-class never supports a claim — memory-planner spec). Bands: supported ≥ 0.75; partial ∈ [0.50, 0.75); unsupported < 0.50 (defaults, config-bounded ±0.1). Policy: flag (default — annotate) or redact (replace unsupported sentences with an omission notice). Citation markers are hints only: an [S3] citation whose span does not actually match does not rescue the claim.

4. Architecture¶

draft → decompose (LLM, constrained) → embed claims (EmbeddingProvider) → match against plan spans → verdicts → policy application → trace persist (plan_hash, prompt_model, score_model, claims, matches, verdicts) → response annotation.

5. Data Models¶

Trace record (traces CF): {query_id, request, plan_hash, prompt_hash, models: {gen, embed, score_model: v1, plan_model: v1}, claims: [{text, draft_span, verdict, score, best_span_ref, candidates_considered}], stats, ts}. Deterministic given fixed (draft, plan, embeddings) — the LLM steps (generation, decomposition) are the nondeterministic boundary, recorded by hash.

6. API Contracts¶

Runs inline in /v1/generate (SSE verification event carries per-claim verdicts). GET /v1/trace/:queryId returns the full record; MCP getTrace returns the claim-grouped shaped form (mcp-tools spec). Decomposition failure (malformed LLM JSON after 2 retries) → response delivered with verification: unavailable flag, never silently unverified-as-verified. Embedding-space consistency (review condition): claims MUST be embedded with the same embedding model id recorded for the plan's spans (trace models.embed); a mismatch → verification: unavailable (fail loud — cosine across mixed embedding spaces is meaningless).

7. UI/UX¶

Trace viewer: claims listed with verdict badges; clicking a claim highlights its best span's text slice (ingestion-provenance slice API). score_parts shown for operator trust calibration.

8. Configuration¶

verify.beta (0.65; validated (0,1) — literal 0/1 are the fast-paths, not config values), verify.bands {supported: 0.75, partial: 0.50} (±0.1 override bounds AND supported ≥ partial + 0.10 enforced after overrides — no band inversion or collapse; review condition), verify.candidates_m (8), verify.policy (flag|redact, per-tenant overridable), verify.decompose_model (may differ from gen model — smaller/cheaper works).

9. Alternatives Considered¶

NLI entailment models (attractive; rejected v1: adds a model-serving dependency to the core binary; the hybrid lexical+embedding matcher is dependency-free given EmbeddingProvider — eval harness will tell us if NLI is worth the weight, revisit Phase 4). Pure lexical F1 (rejected: paraphrase-blind). Pure embedding cosine (rejected: fabricated-but-topical claims score deceptively high; the lexical term anchors specifics like numbers and names). Sentence-as-claim without decomposition (rejected: compound sentences hide half-true claims; atomic decomposition is the point). Verifying against the whole corpus (rejected: verification is against what was planned — an answer citing evidence outside its plan is a planning failure to surface, not to paper over).

10. Implementation Approach¶

PR-052 commits as planned: this spec (F7 sign-off) → decomposition stage → matcher (pure function, unit tables) → verdicts + policy → trace persistence + endpoints → adversarial suite (planted falsehoods, number-swapped claims, topical-but-fabricated claims must land unsupported).

11. Migration Path¶

Greenfield. Threshold/formula changes bump score_model; historical traces immutable (they record the model that judged them).

12. Success Metrics¶

Adversarial suite — v1 classes are number-swapped and topical-but-fabricated claims: unsupported ≥ 0.95 of cases. Entity-swapped claims (one name changed in otherwise-verbatim text) are a recorded v1 limitation (review finding): they are lexically and semantically near-identical to their source, defeat any cosine/lexical matcher by construction, and require NLI-class entailment — Phase-4 revisit per §9; the eval harness should still measure the class so the gap is quantified, but it does not gate v1. Paraphrase suite: true restatements supported ≥ 0.90 (fixture corpora; eval harness extends with labeled data and sets the release-gate floor per PR-057). Determinism given fixed inputs. Trace completeness: every response's trace resolves fully (claims → spans → text slices).

13. Open Questions¶

• OQ-1: Resolved at F7 review (2026-07-04) — yes, but the drafted mechanism was insufficient: capping only the lexical term still yields 0.72 ("partial") for a wrong-figure claim on a near-verbatim span. The gate applies to the WHOLE pair score (cap 0.2, deep in unsupported). Numeric matching is exact after normalization in v1; tolerance/rounding semantics ("about 5 million") are recorded as a known limitation for the eval harness to size. Unit tables must cover: wrong number/right text, right number/paraphrased text, dates in different formats, numbers absent from both.

14. Changelog¶

• 2026-07-04 — v0.3: as-built record (PR-052). Implemented as core-engine/src/verify/ (pinned lexical pipeline in lex.rs over unicode-normalization + unicode-segmentation, pure matcher in matcher.rs, constrained-JSON decomposition in decompose.rs, orchestration + trace model in mod.rs); [verify] config with band-bound validation; GET /v1/trace/:queryId; MCP generate + getTrace activated (tools.json regenerated). As-built decisions, none weakening a review condition: (1) casefold is char-wise Unicode lowercase (≈ simple fold; ß/İ keep simple-fold behavior) — recorded approximation; (2) numeric gate is ∀-coverage (EVERY claim numeric needs a span match — the strictest reading of "figures require figure evidence"), with English month-name→component normalization and ISO dates decomposing through UAX-29 token splits; numbers canonicalize through f64 so 500/500.0/0500 collide; tolerance semantics remain the recorded limitation; (3) embedding-space consistency is STRUCTURAL: claims and spans are both embedded at verification time under one model (verify.embed_model → request's semantic model → embedding.model); no endpoint or unregistered model → verification: unavailable, and the model used is recorded in trace models.embed; (4) verdict ties keep the first span in canonical plan order (strictly-greater comparison); (5) redact policy merges overlapping unsupported ranges; the delivered draft is redacted, the trace preserves the original; per-tenant policy override deferred with the cap-override follow-up; (6) traces persist as kind: "generation" named-msgpack rows in the traces CF — GET /v1/trace decodes either trace shape generically; (7) zero-evidence drafts skip the embedding round-trip: every decomposed claim is unsupported by construction. Adversarial suite (tests/verify_adversarial.rs): number-swap and topical-fabrication classes at 100% unsupported (spec floor 0.95), paraphrase ≥ 0.90 supported, and the entity-swap limitation is MEASURED with an assertion that flags if the gap ever closes; verifier e2e incl. redaction + trace completeness in tests/generate_e2e.rs.
• 2026-07-04 — v0.2 countersigned by J. Porter (jp@densops.com) — approval final (incl. the geometric-fusion change and the entity-swap §12 rescope).
• 2026-07-04 — v0.2: F7 math review complete — Approved with conditions, all incorporated (reviewer: Claude, acting F7 reviewer by J. Porter's delegation). Conditions: (1) cos clamped to [0,1] before fusion; (2) fusion changed arithmetic → geometric clamp01(cos)^β · lex^(1−β) with β∈{0,1} fast-paths (mirrors approved decay §5) — arithmetic blending let topical similarity outvote lexical absence and made §12 unachievable; (3) lexical term pinned as IDF-weighted token coverage (NFC/UAX-29/casefold, no stopwords, plan-local IDF) — raw token-F1 was undefined, punished long spans, and was inflatable by function words; (4) numeric gate applies to the whole pair score (cap 0.2), not the lexical term; (5) embedding-model consistency enforced fail-loud; (6) β validated (0,1), band overrides validated supported ≥ partial + 0.10; (7) §12 adversarial metric rescoped to achievable v1 classes — entity-swap recorded as a limitation requiring NLI (Phase 4). Max-over-candidates confirmed for v1 (multi-span composite claims land ≤ partial; atomic decomposition mitigates). OQ-1 resolved.
• 2026-07-02 — v0.1: initial draft. Awaiting F7 sign-off.