# BERT Cross-Encoder Entailment Agent

[![Tests](https://img.shields.io/badge/tests-11%2F11%20passing-brightgreen)](tests/)
[![License: Tri](https://img.shields.io/badge/license-AGPL%20%7C%20BSL%201.1%20%7C%20MIT-blue)](LICENSE)
[![Model: DeBERTa-v3](https://img.shields.io/badge/model-DeBERTa--v3--base-orange)](https://huggingface.co/microsoft/deberta-v3-base)
[![Backend: TensorRT](https://img.shields.io/badge/backend-TensorRT%20FP16-76b900)](https://developer.nvidia.com/tensorrt)
[![Rust](https://img.shields.io/badge/daemon-Rust%20%2F%20Tokio-orange)](daemon/)
[![Audit: BLAKE3+ERE](https://img.shields.io/badge/audit-BLAKE3%20%2B%20ERE%20P5-blueviolet)](agent/ere_gate.py)
[![WORM](https://img.shields.io/badge/ledger-WORM%20chain-critical)](daemon/src/ledger.rs)
[![Lean 4](https://img.shields.io/badge/invariants-Lean%204%20proved-informational)](Invariants.lean)

**Authors:** Ahmad Ali Parr, Jessica L. Williams (SNAPKITTYWEST)  
**Stack:** DeBERTa-v3 · ONNX · TensorRT FP16 · Rust/Tokio · BLAKE3 · WORM ledger · ERE P1-P5

A production-grade entailment verification agent. Pass a retrieved source chunk and an
LLM-generated claim; get back a mathematically bounded entailment score, a verdict,
and a BLAKE3 cryptographic attestation sealed into an append-only WORM audit chain —
then passed through the ERE five-gate protocol before it leaves the system.

---

## What This Is

LLMs hallucinate. RAG systems retrieve chunks and generate claims against them. Without
a verification layer, a model can produce a plausible-sounding claim that contradicts
its own source — and no downstream system will catch it.

This agent is the verification layer. It does one thing:

> **Given a retrieved source and a generated claim, determine with
> cryptographic certainty whether the claim is entailed by the source.**

It is not a chatbot. It is not a general-purpose NLI system. It is a production daemon
that runs at the end of every RAG pipeline and refuses to propagate a claim until it
can prove the claim is entailed.

---

## How This Compares to Google BERT

| Property | Google BERT (2018) | This Agent |
|----------|-------------------|------------|
| Architecture | Bi-directional encoder | Cross-encoder (premise ++ hypothesis) |
| NLI task | Fine-tuned on MNLI only | ANLI + TrueTeacher + MNLI (3-source) |
| Hallucination detection | Not designed for it | Primary objective |
| Negation detection | Weak (symmetric embeddings) | Strong (joint self-attention) |
| Date/number flip detection | Fails | Catches (e.g. 1962 → 1926) |
| Runtime | Python / TF / PyTorch | Rust daemon, TensorRT FP16, GPU |
| Latency | ~100-300 ms (Python) | <5 ms batched (TRT) |
| Throughput | Single request | Dual-trigger continuous batching |
| Audit trail | None | BLAKE3 + WORM chain per inference |
| Security gates | None | ERE P1-P5 (5-gate sovereign protocol) |
| Formal invariants | None | Lean 4, zero sorry |
| License | Apache 2.0 | Tri-license (AGPL / BSL 1.1 / MIT) |

**Key difference:** BERT embeds premise and hypothesis *separately* and compares them
with cosine similarity. A cross-encoder concatenates them and runs joint self-attention.
That joint attention is what lets this agent catch subtle hallucinations — the model
can directly compare "born in 1962" against "born in 1926" at the token level.
BERT cannot do this. It sees two vectors, not two sentences in dialogue.

---

## Why Cross-Encoder, Not Bi-Encoder

A Bi-Encoder embeds premise and hypothesis separately. At inference, you compare
embeddings with cosine similarity. This works for semantic similarity, but it misses:

- Flipped dates: `"born in 1962"` vs `"born in 1926"` — both embed nearly identically
- Switched subjects: `"X defeated Y"` vs `"Y defeated X"` — same semantic field
- Negation: `"the vote passed"` vs `"the vote did not pass"`

A Cross-Encoder concatenates both and runs them through a single forward pass:

```
[CLS] retrieved_chunk [SEP] generated_claim [SEP]
```

Self-attention directly compares entities across the premise-hypothesis boundary at
every layer. The model learns to detect *contradiction*, not just *similarity*.
This is the architecture that makes hallucination detection tractable.

---

## Architecture

```
              Training Pipeline (Python)
                      │
        DeBERTa-v3-base + 3-label head
           Weighted CrossEntropyLoss
      (Contradiction=2.0, Neutral=1.5, Entailment=1.0)
            ANLI + TrueTeacher + MNLI
                      │
                      ▼
             ONNX export (dynamic axes)
                      │
          ORT graph optimization + FP16
                      │
                      ▼
            TensorRT engine (.plan cache)
                      │
              Rust Inference Daemon
         ┌────────────┴───────────────┐
         │   Dual-trigger batching    │
         │  MAX_BATCH or 5 ms timer   │
         │   Dynamic padding/ndarray  │
         │   TRT forward pass (GPU)   │
         │   Softmax → score          │
         │   BLAKE3 attestation seal  │
         │   WORM ledger append       │
         └────────────────────────────┘
                      │
               HTTP POST /verify
               { score, verdict, hash }
                      │
              ┌───────▼────────┐
              │  ERE P1-P5     │  ← agent/ere_gate.py
              │  Five gates    │
              │  P5 seal added │
              └───────┬────────┘
                      │
               Gated response
         { score, verdict, hash,
           ere_seal, ere_gates }
         OR { ere_halt: true }
```

---

## Milestones

| # | Milestone | Status |
|---|-----------|--------|
| M1 | DeBERTa-v3 cross-encoder + weighted 3-label loss | ✅ Done |
| M2 | ANLI + TrueTeacher + MNLI joint training dataset | ✅ Done |
| M3 | ONNX export + ORT FP16 graph optimization | ✅ Done |
| M4 | TensorRT engine with .plan caching | ✅ Done |
| M5 | Rust inference daemon (Tokio, Axum, dual-trigger batching) | ✅ Done |
| M6 | BLAKE3 attestation seal per inference | ✅ Done |
| M7 | WORM append-only audit chain (tamper-evident) | ✅ Done |
| M8 | FPR=0.0 PR-curve threshold calibration | ✅ Done |
| M9 | 11/11 tests passing (dataset, calibrate, ledger) | ✅ Done |
| M10 | Lean 4 formal invariants (zero sorry) | ✅ Done |
| M11 | ERE P1-P5 gate integration (`agent/ere_gate.py`) | ✅ Done |
| M12 | Tri-license (AGPL / BSL 1.1 / MIT) | ✅ Done |
| M13 | Sovereign Engine v2 gap integration (Gap 4 candidate) | 🔜 Planned |
| M14 | Rust daemon ERE gate enforcement (inline, pre-response) | 🔜 Planned |
| M15 | Benchmark vs NLI baselines (BERT, RoBERTa, DeBERTa-v2) | 🔜 Planned |

---

## ERE Gate Protocol

Every verdict produced by this agent passes through the **ERE (Expected Reasoning Error)**
five-gate protocol before leaving the system:

| Gate | Check | Failure means |
|------|-------|---------------|
| P1 | No secrets in payload | Credential leaked in model output |
| P2 | No eval / code injection | Adversarial input tried to inject code |
| P3 | Loop safety | Output contains infinite loop without exit |
| P4 | No telemetry beacons | Analytics SDK call in model output |
| P5 | SHA-256 audit seal | Commitment over `agent_id:intent:verdict` |

A verdict that fails any gate is suppressed. The caller receives `{ ere_halt: true }`.
The WORM ledger records the halt. The chain is not broken.

```python
from agent.ere_gate import gate_verdict

raw = {"score": 0.98, "verdict": "Entailment", "hash": "a3f8..."}
gated = gate_verdict(
    premise="The Battle of Hastings took place in 1066.",
    hypothesis="Hastings occurred in 1066.",
    raw_verdict=raw,
)

if not gated.allowed:
    raise RuntimeError(f"ERE halt: {gated.violations}")

print(gated.to_dict())
# { score, verdict, hash, ere_seal, ere_gates: {P1:T, P2:T, P3:T, P4:T, P5:T} }
```

---

## Full Pipeline

### 1. Install dependencies

```bash
pip install -r requirements.txt
```

### 2. Download datasets

```
data/
  anli/R1/{train,dev,test}.jsonl
  anli/R2/{train,dev,test}.jsonl
  anli/R3/{train,dev,test}.jsonl
  trueteacher/{train,dev}.jsonl      # Google, 1.4M records
  mnli/{train,dev}.jsonl
```

### 3. Fine-tune DeBERTa-v3

```bash
python -m bert.train \
  --data_dir data/ \
  --output_dir checkpoints/ \
  --backbone microsoft/deberta-v3-base \
  --epochs 5 \
  --batch_size 32 \
  --lr 2e-5
```

### 4. Export to ONNX + optimize FP16

```bash
python -m bert.export \
  --checkpoint checkpoints/best_model.pt \
  --output_dir onnx/ \
  --device cuda
```

### 5. Calibrate rejection threshold

```bash
python -m bert.calibrate \
  --checkpoint checkpoints/best_model.pt \
  --data_dir data/ \
  --output config/threshold.json
```

### 6. Build and run the Rust daemon

```bash
cd daemon
cargo build --release
RUST_LOG=info ./target/release/bert-daemon --config ../config/daemon.json
```

First startup: ~5 min for TensorRT engine compilation. Subsequent starts: instant from `.plan` cache.

### 7. Verify a claim

```bash
curl -X POST http://localhost:8080/verify \
  -H "Content-Type: application/json" \
  -d '{
    "premise": "The Battle of Hastings took place in 1066.",
    "hypothesis": "Hastings occurred in 1066.",
    "chunk_id": "chunk-001"
  }'
```

Response:

```json
{
  "score": 0.9812,
  "verdict": "Entailment",
  "hash": "a3f8d2c1...",
  "ere_seal": "7f3c8a19...",
  "ere_gates": { "P1": true, "P2": true, "P3": true, "P4": true, "P5": true }
}
```

The `hash` is the BLAKE3 attestation over the inference. The `ere_seal` is the P5 SHA-256
commitment over `agent_id:intent:verdict`. Both are recorded in the WORM ledger.

---

## File Structure

```
bert-agent/
├── agent/
│   ├── __init__.py      # Exports BERTEREGate, GatedVerdict, gate_verdict
│   └── ere_gate.py      # ERE P1-P5 gate adapter for BERT verdicts
├── bert/
│   ├── dataset.py       # ANLI + TrueTeacher + MNLI cross-encoder dataset
│   ├── model.py         # DeBERTa-v3 cross-encoder + weighted loss
│   ├── train.py         # Fine-tuning loop (AdamW + cosine LR)
│   ├── export.py        # ONNX export + ORT FP16 graph optimization
│   ├── trt_session.py   # TensorRT ORT session with optimization profiles
│   └── calibrate.py     # PR curve threshold calibration
├── daemon/
│   ├── Cargo.toml
│   └── src/
│       ├── main.rs        # Startup, channel wiring
│       ├── types.rs       # VerifyRequest, Attestation, Config
│       ├── session.rs     # TRT ORT session init
│       ├── inference.rs   # Dual-trigger continuous batching loop
│       ├── ledger.rs      # WORM append-only audit chain
│       └── server.rs      # Axum HTTP /verify handler
├── config/
│   └── daemon.json
├── tests/
│   ├── test_dataset.py
│   ├── test_calibrate.py
│   └── test_ledger.py
├── Invariants.lean        # Lean 4 formal invariants, zero sorry
├── LICENSE                # Tri-license: AGPL-3.0 | BSL 1.1 | MIT
└── requirements.txt
```

---

## Design Decisions

| Decision | Why |
|----------|-----|
| DeBERTa-v3 over BERT/RoBERTa | Disentangled attention handles positional reasoning — critical for detecting reordered events |
| Cross-Encoder over Bi-Encoder | Cannot cache embeddings, but self-attention compares entities across premise-hypothesis directly |
| Weighted loss (2.0/1.5/1.0) | False-positive Entailment is the worst failure mode — weight Contradiction higher |
| ANLI + TrueTeacher | Standard NLI is too easy; TrueTeacher mirrors actual LLM hallucination patterns |
| FPR=0.0 threshold calibration | In a verification engine, precision > recall — never cite a hallucinated claim |
| Dual-trigger batching (batch size OR 5ms) | Bounded latency guarantee without sacrificing GPU throughput |
| Dynamic padding per batch | Pad to longest sequence in the batch, not global max — avoids wasted compute |
| BLAKE3 + bincode attestation | Memory-bandwidth hashing speed; deterministic binary serialization (no JSON ordering ambiguity) |
| WORM ledger as chain | Every record links to previous hash — tamper detection is immediate |
| ERE P1-P5 gate layer | Every verdict inspected for secrets, injection, loops, telemetry before propagation |
| Lean 4 invariants | Formal proof that well-formed agents satisfy trust and entropy bounds — not just assertions |

---

## Theoretical Foundation

This agent is a component of the **Sovereign Stack**. Its cryptographic and formal
foundations are documented in the following published papers:

| DOI | Contribution |
|-----|-------------|
| [10.5281/zenodo.21443609](https://doi.org/10.5281/zenodo.21443609) | Jordan Spectral Transformer — phi-weighted routing |
| [10.5281/zenodo.21132094](https://doi.org/10.5281/zenodo.21132094) | Sovereign Compute Architecture |
| [10.5281/zenodo.20678420](https://doi.org/10.5281/zenodo.20678420) | Attention Exhaustion Attacks — 0% detection rate |
| [10.5281/zenodo.21268911](https://doi.org/10.5281/zenodo.21268911) | GKN I4 Quartic Invariant and E7 Symmetry |

Unified paper: [The Sovereign Stack](https://snapkittywest.github.io/hyperkitty/papers/sovereign-stack-unified.pdf)

---

## License

Tri-license — choose any one:

- **AGPL-3.0** for open source / community use
- **BSL 1.1 → MIT** for commercial / production use (< 5 servers free; converts to MIT 2029-01-01)
- **MIT** after 2029-01-01

See [LICENSE](LICENSE) for the full text and list of six protected inventions.

Copyright (C) 2026 Ahmad Ali Parr, Jessica L. Williams / SNAPKITTYWEST  
Bel Esprit D'Accord Irrevocable Trust

---

*Built to catch what BERT cannot see.*  
*Every claim sealed. Every halt recorded. Nothing propagates without proof.*