Proofs & hallucination firewall

Two mechanisms turn derived facts into a verifiable answer: proofs explain why a fact holds (down to stored hyperedges), and the firewall ensures the LLM can only repeat what the proofs support.

build_proof

from hypermesh.rag.symbolic import build_proof, Fact

proof = build_proof(
    Fact("coordinated_threat", (42,)),
    fact_base,
    proof_id="proof-1",
    provenance_resolver=None,   # optional hook, see below
)
proof.status          # "proved" | "unproved"
proof.confidence      # root confidence
proof.as_dict()       # JSON-serialisable DAG

A proof tree is a DAG: the root is the derived conclusion, internal nodes are rule applications, and leaves are ground evidence bound to provenance. Shared sub-proofs reference a single node id (a true DAG, not a duplicated tree). If the goal isn’t in the fact base, the returned tree has status: "unproved" and no nodes.

ProofTree

Field	Meaning
`proof_id`	Caller-supplied id.
`goal`	`{predicate, args, root?}` — the fact being proved.
`status`	`"proved"` or `"unproved"`.
`confidence`	Root fact confidence.
`depth`	Longest premise chain.
`rules_fired`	Rule ids used, in first-seen order.
`nodes`	List of node dicts (see below).
`edges`	`{from, to, role: "premise"}` links.

proof.evidence_tags returns the set of all citation tags in the tree (HEDGE-N, RULE-N, STEP-N).

Node shapes

Conclusion node (a derived fact):

{
  "id": "S1",
  "kind": "conclusion",
  "fact": "coordinated_threat(42)",
  "predicate": "coordinated_threat",
  "args": [42],
  "rule": "rule:coordinated_threat",
  "rule_tag": "RULE-0",
  "step_tag": "STEP-1",
  "confidence": 0.9,
  "premises": ["L1", "L2"]
}

Evidence node (a leaf bound to a stored hyperedge):

{
  "id": "L1",
  "kind": "evidence",
  "evidence_type": "hyperedge",
  "fact": "member(42, 7)",
  "predicate": "member",
  "args": [42, 7],
  "confidence": 1.0,
  "hedge_tag": "HEDGE-42",
  "provenance": {
    "source": "hyperedge",
    "table": "DRONES",
    "edge_idx": 42,
    "event_ts": 1700000000,
    "verified": true
  }
}

The provenance.verified: true is the crux: the leaf is bound to a concrete hyperedge in the retrieved set, so the proof bottoms out in real, stored data.

Provenance resolver

By default each leaf is marked verified against the live store. To enrich provenance (e.g. attach a source document id or content digest from your ingest index), pass a provenance_resolver:

def resolver(edge_ref: dict) -> dict:
    # edge_ref = {table, edge_idx, event_ts, member_ids, hedge_tag}
    return {"source_id": lookup_source(edge_ref["edge_idx"]),
            "digest": lookup_digest(edge_ref["edge_idx"])}

proof = build_proof(goal, fb, provenance_resolver=resolver)

The returned dict is merged into the leaf’s provenance. If the resolver raises, the leaf is marked verified: false rather than failing the proof. RAGPipeline forwards its own provenance_resolver here.

Confidence propagation

A conclusion’s confidence is rule_confidence × min(premise_confidence). It therefore only ever degrades along a chain, never inflates — a five-hop derivation is never more confident than its weakest input.

Hallucination firewall

After generation, the firewall gates the answer against the set of allowed citation tags (everything in the proofs/evidence/context).

from hypermesh.rag.symbolic import HallucinationFirewall

fw = HallucinationFirewall()   # optional: HallucinationFirewall(abstain_message="...")
result = fw.check(
    answer,
    allowed_tags={"HEDGE-42", "RULE-0", "STEP-1"},
    proved=True,             # was a symbolic conclusion actually derived?
    require_proof=False,     # if True and not proved → abstain outright
)
result.answer     # sanitized text
result.outcome    # "supported" | "stripped" | "abstained"

How it decides

The answer is split into sentences. For each:

Short / connective sentences (< 20 chars) are kept as glue.
Sentences containing an honest [UNVERIFIED…] marker are kept.
Other sentences are factual and must cite a tag ([HEDGE-N], [RULE-N], [STEP-N], [PATTERN-N]) that is in allowed_tags. If they do, they’re kept and counted as supported. If not, they’re stripped.

Outcomes

Outcome	When
`supported`	Every factual sentence cited an allowed tag.
`stripped`	Some factual sentences were unsupported and removed.
`abstained`	`require_proof and not proved`, or every factual sentence was unsupported (nothing left to say).

When the firewall abstains it returns the abstain message (“Insufficient verifiable evidence to answer this question.” by default) and sets abstained=True.

FirewallResult

Field	Meaning
`answer`	Sanitized answer (or abstain message).
`outcome`	`supported` / `stripped` / `abstained`.
`abstained`	bool.
`coverage`	supported ÷ factual sentences (`1.0` if no factual sentences).
`supported`	Kept factual sentences.
`stripped`	Removed sentences.

result.as_dict() returns {outcome, abstained, coverage, supported_count, stripped_count, stripped[:10]} — this is what surfaces in RAGResult.firewall.

Why this is the safety boundary

The firewall runs after any model, on its raw text, using only tags that trace to proofs. So the guarantee — no unsupported sentence reaches the user — holds no matter which LLM wrote the text, including a cheap or local one. The model cannot smuggle a claim past it, because a claim without a provable tag is simply deleted.

Next: Pipeline, modes & LLMs.