Proving inference · Operator atlas · Proof of non-hallucination
Proof of non-hallucination
an unexpected freebie
$$\mathrm{Ker}(Q,K) = \mathrm{softmax}\!\left(\frac{Q K^\top}{\sqrt{d}}\right) \qquad \text{— already computed as } T_s
\\[10pt]
\text{attention score} = \log\det \mathrm{Ker}(Q,K) = \sum_{i=0}^{s-1} \log \mathrm{Ker}_{i,i}
\\[6pt]
\text{(lower-triangular after masking} \Rightarrow \det = \text{product of the diagonal)}$$
The algorithm
Prove that the generated response passed a white-box hallucination detector (LLM-Check), alongside the proof of inference itself.
Why it resists a proof
Not hard — and that is the point. The detector's core quantity is the log-determinant of the attention kernel, which the inference proof already contains as the softmax output $T_s$. Masking makes the kernel triangular, so the determinant is the diagonal product, so the log-det is a sum of logs.
Cryptographic toolbox
- Lookup table to approximate log₂
- Sumcheck to aggregate the diagonal
- Reuse of the existing softmax witness
How each scheme proves it
First cryptographic proof of LLM non-hallucination. A lookup for log, a sumcheck for the sum, riding on witnesses that already exist.
- Detection algorithm: LLM-Check's Attention Score, aggregated across heads by averaging (a summation, since shapes are fixed).
- Chosen because it is white-box (the prover has all internal states anyway), needs no external database, and needs no second LLM for post-processing — the three properties that make a detector provable.
- Measured: 68.69% AUROC / 67.96% accuracy on GPT-2 (Fava annotation dataset, 460 samples), 65.84% / 64.16% on Gemma 3. Quantization slightly improved GPT-2's detection and slightly degraded Gemma 3's.
- Prover overhead for the gadget: 98 ms (GPT-2), 21 ms (Gemma 3) at sequence length 512 — a rounding error against a multi-minute proof.
98.1 ms (GPT-2) / 21.1 ms (Gemma 3), seq 512.