Claim verification¶

Architecture

A generated draft is not trusted because it cites sources; it is trusted because each atomic claim inside it was independently checked against the exact evidence the generator was allowed to see, using a scoring formula an F7 math review specifically hardened against plausible-looking fabrication. This page documents that formula and the pipeline around it, as built in core-engine/src/verify/.

Overview & purpose¶

Generation without verification is confident hallucination with citations attached. core-engine/src/verify/ runs after a draft is generated and before it is delivered: it decomposes the draft into atomic claims, embeds each claim and every candidate evidence span under one consistent model, scores each (claim, span) pair by combining semantic and lexical evidence, and bands the best score into a verdict. The result, plus the evidence plan and prompt, is persisted as an immutable trace so an answer's grounding remains inspectable after the fact.

The central engineering problem the F7 review solved: how do you score a claim so that genuine paraphrase is rewarded but a topically-similar fabrication is not? A pure embedding-similarity score cannot tell them apart. The answer landed on is a geometric fusion of a semantic signal and a lexical signal, plus a hard numeric gate for figures, both discussed below.

Design¶

Pipeline¶

flowchart LR
    DRAFT["Draft"] --> DECOMP["Decompose<br/>(LLM, constrained JSON)"]
    DECOMP --> EMBED["Embed claims + spans<br/>under ONE model"]
    EMBED --> MATCH["Match: candidates =<br/>cited spans ∪ top-m by cosine"]
    MATCH --> SCORE["Score each pair:<br/>geometric fusion + numeric gate"]
    SCORE --> BAND["Band: supported/partial/unsupported"]
    BAND --> POLICY["Policy: flag or redact"]
    POLICY --> TRACE["Persist trace"]

Decomposition¶

core-engine/src/verify/decompose.rs calls the same LlmProvider used for generation, with a fixed system prompt instructing constrained JSON output: a list of {claimText, draftSpan: [start, end], citedMarkers: ["S1"]} objects. The prompt explicitly instructs splitting compound sentences into one claim each and omitting hedges, transitions, and questions as non-factual. Temperature is pinned to 0.0 (determinism-leaning, though the spec notes the LLM step remains the recorded nondeterministic boundary regardless).

Parsing (parse_claims) tolerates code-fence wrapping (``json fences, plain fences, or none) but nothing else, and validates every claim'sdraftSpanis in-bounds and non-empty before accepting it. On malformed output,decompose()retries **up to 2 more times** (3 attempts total); if all three fail, the caller receives aDecomposeErrorand the whole generation degrades toverification: unavailable` rather than being silently treated as verified.

Lexical matching: IDF-weighted token coverage¶

core-engine/src/verify/lex.rs tokenizes claim and span text through a pinned, language-agnostic pipeline: NFC normalize, then unicode_words() (UAX-29 word segmentation), then char-wise Unicode lowercase, then drop any token with no alphanumeric character. There is no stopword list: function words survive tokenization but are downweighted by IDF instead.

idf(t) = ln(1 + N / df(t))     df floored at 1
lex(claim, span) = Σ_{t ∈ claim ∩ span} idf(t) · min(count) / Σ_{t ∈ claim} idf(t) · count

N and df are computed over the plan's spans only (PlanIdf), so the IDF table is self-contained and deterministic given the plan. A term appearing in zero plan spans still gets a defined (maximal) weight because df is floored at 1, not zero. The intersection is a multiset: a claim needing "beta" twice against a span containing it once gets partial credit for that token, not full credit. This is coverage, not F1: a long span that fully contains the claim's vocabulary scores 1.0 regardless of its own length, so verbose evidence is never penalized for its verbosity.

The numeric gate¶

Also in lex.rs, numerics() extracts normalized numeric atoms from a token list: English month names map to their numeric component (an explicit 12-entry table); any token containing a digit is split on -, /, : (so ISO dates and prose dates decompose to the same components, e.g. both 2026-03-05 and 5 March 2026 yield ["2026", "3", "5"] in some order); digit-group commas are stripped; every surviving numeric string parses through f64 so 500, 500.0, and 0500 all canonicalize identically.

pub fn numeric_gate_trips(claim_numerics: &[String], span_numerics: &[String]) -> bool {
    if claim_numerics.is_empty() { return false; }
    claim_numerics.iter().any(|n| !span_numerics.contains(n))
}

The gate is universal coverage: it trips if any numeric in the claim is absent from the candidate span's numerics, the strictest reading of "figures require figure evidence." A claim asserting two numbers where the span only confirms one still trips the gate.

The matcher: geometric fusion¶

core-engine/src/verify/matcher.rs fuses the two signals:

match = clamp01(cos)^β × lex^(1−β)          β = 0.65 default

pub fn fuse(cos: f64, lex: f64, beta: f64) -> f64 {
    let beta = beta.clamp(0.0, 1.0);
    let cos = cos.clamp(0.0, 1.0);   // raw cosine spans [-1, 1]; clamp BEFORE fusion
    let lex = lex.clamp(0.0, 1.0);
    if beta == 0.0 { return lex; }   // fast-paths precede pow: 0^0 never evaluated
    if beta == 1.0 { return cos; }
    cos.powf(beta) * lex.powf(1.0 - beta)
}

Cosine is clamped to [0, 1] before it enters the formula, and β ∈ {0, 1} short-circuits before any powf call, the same guard pattern as the approved confidence-decay formula (../architecture/confidence-decay.md).

The numeric gate caps the whole pair score, not just the lexical term:

pub fn pair_score(cos: f64, lex: f64, beta: f64, numeric_gate_tripped: bool) -> f64 {
    let fused = fuse(cos, lex, beta);
    if numeric_gate_tripped { fused.min(0.2) } else { fused }
}

Capping only the lexical term was tried and rejected during the F7 review: a near-verbatim span with a wrong number would still fuse to 0.65·1 + 0.35·0.2 = 0.72 (arithmetic) or similarly high under geometric fusion with a lexical-only cap, both reading "partial" for a claim with the wrong figure. Capping the whole score forces it deep into unsupported (0.2, well under the 0.50 partial floor) regardless of how strong the semantic and un-gated lexical match are.

Candidate selection¶

For each claim, candidates are the union of:

1. Every plan span its citedMarkers resolve to (citation markers are hints, never proof, per the concept page).
2. The top-m (verify.candidates_m, default 8) plan spans by raw cosine similarity to the claim's embedding.

Only truth-class spans participate; cache-class spans (derived summaries from the memory planner) can accelerate planning but can never themselves support a claim. Ties on score keep the first span in canonical plan order (strictly-greater comparison), so verification is deterministic given fixed inputs.

Data model¶

Trace record¶

pub struct GenerationTrace {
    pub kind: String,               // "generation"
    pub query_id: String,
    pub request: serde_json::Value, // sanitized request
    pub plan_hash: String,
    pub prompt_hash: String,
    pub models: TraceModels,
    pub plan: TracePlan,
    pub draft: String,              // pre-redaction
    pub claims: Vec<ClaimVerdict>,
    pub verification: String,       // "verified" | "unavailable: <reason>"
    pub usage_input_tokens: u64,
    pub usage_output_tokens: u64,
    pub ts: u64,
}

pub struct TraceModels {
    pub gen: String,
    pub decompose: String,
    pub embed: String,       // empty when verification was unavailable
    pub score_model: String, // "v1", bumps on formula/threshold changes
    pub plan_model: String,
    pub prompt_model: String,
}

ClaimVerdict¶

pub struct ClaimVerdict {
    pub text: String,
    pub draft_span: (u64, u64),
    pub verdict: Verdict,               // Supported | Partial | Unsupported | EvidenceRedacted
    pub score: f64,                     // max over candidate pairs
    pub best_span: Option<TraceSpanRef>,
    pub candidates_considered: u32,
    pub cited_markers: Vec<String>,
    pub numeric_gated: bool,
}

EvidenceRedacted is a fourth verdict, distinct from the three the spec's §3 defines: when a claim's best-matching span overlaps a range a GDPR erasure has masked, verification reports this explicitly rather than a confusing low-score mismatch (see the GDPR erasure spec §3.2 step 5).

Verdict bands¶

Algorithms & invariants¶

flowchart TB
    DRAFT{draft empty?} -->|yes| VNOCLAIM["Verified: 0 claims"]
    DRAFT -->|no| DECOMP[Decompose]
    DECOMP -->|fails after 3 attempts| UNAVAIL["Unavailable"]
    DECOMP -->|ok, 0 claims| VNOCLAIM
    DECOMP -->|ok, N claims| TRUTH{any truth-class<br/>plan spans?}
    TRUTH -->|no| ALLUNSUP["Every claim Unsupported<br/>by construction, no embedding round-trip"]
    TRUTH -->|yes| EMBEDCHECK{embedder configured<br/>AND model resolvable<br/>AND registered?}
    EMBEDCHECK -->|no| UNAVAIL
    EMBEDCHECK -->|yes| MATCH[Embed + match + band]

Redaction policy¶

fn redact(draft: &str, claims: &[ClaimVerdict]) -> Option<String> {
    // collects Unsupported claims' draft_span ranges, sorts, merges overlaps,
    // replaces each merged range with "[unsupported claim removed]"
}

Under verify.policy = redact, overlapping unsupported ranges merge into one before substitution, so two adjacent unsupported claims produce one omission notice, not two. The trace always stores the original, pre-redaction draft; only the delivered response text is redacted. Under flag (the default), nothing is rewritten; the caller annotates verdicts in place.

Configuration¶

As-built notes¶

From the spec's §14 v0.3 changelog, reconciled against core-engine/src/verify/:

• Casefold is char-wise Unicode lowercase, an approximation of full Unicode simple casefolding, recorded as a deliberate approximation; edge cases like ß/İ keep their simple-fold behavior rather than a dedicated casefolding table.
• The numeric gate is ∀-coverage: every numeric token in the claim must find a match in the candidate span, the strictest reading available of "figures require figure evidence." English month names normalize into the same component space as ISO date digits.
• Embedding-space consistency is structural, as described above: claims and spans are both embedded at verification time under one resolved model, with the model recorded in trace.models.embed.
• Verdict ties keep the first span in canonical plan order via a strictly-greater score comparison, making the matcher deterministic given fixed inputs.
• Redact policy merges overlapping ranges; per-tenant policy override is deferred alongside the cap-override follow-up noted in generation orchestration.
• Traces persist as kind: "generation" named-msgpack rows in the traces CF; GET /v1/trace decodes either the generation trace shape or the older query-trace shape generically.
• Zero-evidence drafts skip the embedding round-trip, as shown in the flow diagram above.
• The adversarial test suite (tests/verify_adversarial.rs) measures number-swap and topical-fabrication classes at 100% unsupported (spec floor 0.95) and paraphrase at ≥ 0.90 supported. Entity-swapped claims (one name changed in otherwise-verbatim text) are a recorded v1 limitation: they are lexically and semantically near-identical to their source and defeat any cosine/lexical matcher by construction, requiring NLI-class entailment deferred to Phase 4. The suite still measures this class with an assertion that flags if the gap ever closes, but it does not gate v1 releases.

Related¶

• Concepts › Verified answers
• Architecture › Generation orchestration
• Architecture › Memory planner
• Architecture › Eval harness
• Architecture › GDPR erasure