Metadata-Version: 2.4
Name: certhead
Version: 0.1.0
Summary: An LLM output head that PROVES its token instead of guessing it, and falls back to dense rather than be wrong
License: Apache-2.0
Project-URL: Homepage, https://github.com/nickharris808/certhead
Project-URL: Issues, https://github.com/nickharris808/certhead/issues
Keywords: llm,inference,argmax,verification,exactness,quantization,certificate,bounds
Classifier: Development Status :: 4 - Beta
Classifier: Intended Audience :: Developers
Classifier: Intended Audience :: Science/Research
Classifier: License :: OSI Approved :: Apache Software License
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3.9
Classifier: Programming Language :: Python :: 3.10
Classifier: Programming Language :: Python :: 3.11
Classifier: Programming Language :: Python :: 3.12
Classifier: Topic :: Scientific/Engineering :: Artificial Intelligence
Classifier: Topic :: Software Development :: Quality Assurance
Requires-Python: >=3.9
Description-Content-Type: text/markdown
License-File: LICENSE
License-File: LICENSE-TAG
Requires-Dist: numpy>=1.21
Provides-Extra: dev
Requires-Dist: pytest>=7; extra == "dev"
Provides-Extra: signoff
Requires-Dist: signoff-cert>=1.0.0; extra == "signoff"
Dynamic: license-file

# certhead

**An output head that returns the token a dense head would have returned — and can show you why.**

[![License](https://img.shields.io/badge/license-Apache--2.0-blue.svg)](LICENSE)
[![Python](https://img.shields.io/badge/python-3.9%2B-blue.svg)](https://www.python.org/)
[![Dependencies](https://img.shields.io/badge/dependencies-numpy-brightgreen.svg)](pyproject.toml)
[![Claims](https://img.shields.io/badge/claims--map-CLEAN-brightgreen.svg)](CLAIMS-MAP.md)

A language model's output head is a big matrix. Reading less of it is easy; reading less of it and
still being **right every time** is the part that needs an argument.

certhead reads a coarse version of every vocabulary row, derives a *certified interval* for each
row's score, discards the rows that provably cannot win, and refines only the survivors. When the
intervals fail to separate, it computes the dense product rather than guess.

That last clause is the whole design. **certhead can be slow. It cannot be wrong.**

```bash
pip install git+https://github.com/nickharris808/certhead@v0.1.0
```

## The comparison that is actually the point

Reading 5 bits per row is not novel — that is just quantization. The claim is what the same bytes
buy you.

On the real `Qwen2.5-0.5B-Instruct` output head (V=151,936 × d=896), over 1,552 hidden states
captured from seven kinds of prompt, at an **identical byte budget**:

| | wrong tokens | can it tell you which ones? |
|---|---|---|
| quantized argmax | **151 / 1552 — 9.7%** `[8.3%, 11.3%]` 95% CI | no |
| **certhead** | **0 / 1552** | n/a — it returns the dense token |

The first token the quantizer got wrong: it said token `374` where the truth was `1887`. It had no
way to know, and neither did anyone downstream.

## HONEST SCOPE

Matched pairs. Each line says what is established and what is not.

| What certhead **does** establish | What it does **not** |
|---|---|
| Returns the identical token to `argmax(Wh)`, always | This is **structural, not measured** — it holds because of the dense fallback. The 0/1552 is a self-check on the implementation, not the source of the guarantee |
| At 5-bit coarse, reads a median **15.8%** of head bytes | **15.8% is essentially the closed form**, not a pruning result — see below. Read that section before quoting the number |
| A quantized head at the same budget is wrong on 9.7% of tokens | On **one model, one head, one 1,552-state corpus**. Nothing here generalises to another vocabulary or hidden size |
| 5 bits is the minimum coarse width at which the bound separates for this head | That minimum is a property of **this model's score-margin distribution**. It is the genuinely measured quantity, and it is model-specific |
| Wall time on an MLX microbenchmark fell to ~0.52× dense | **The proportionality test FAILED** and no speedup is claimed. See "Do the bytes become time?" |
| Bytes read are **counted**, exactly, deterministically | No FLOPs, no memory-bus counters, no end-to-end serving latency is measured anywhere |

## Read this before quoting "15.8%"

Every row must be read at least once, so the byte cost has a hard floor:

```
bytes / dense  ≈  coarse_bits/32  +  (survivors/V) × (refinement + dense)
```

At 5 bits the measured median is **0.1582** and the floor is **0.1574**. The excess is **+0.0009**.
In other words, at the width that works, the second term has almost vanished and the number you
get is the floor — which is computable in advance from `coarse_bits` and `d`, without a GPU and
without this library.

This is stated up front because **the previous version of this measurement was retracted for
exactly that defect.** v1.0 of the harness reported a median of 0.237 as though it were a pruning
result. It was not: at a 2-bit coarse stage the certified interval had half-width ~85 against a
score gap of ~21, so the coarse scan pruned **0 of 151,936 rows**. Reading 8 bits of every row and
eliminating nothing is not branch-and-bound; it is 8-bit quantization, and 8/32 = 0.25 was the
number being reported. The retraction is recorded in the harness's own docstring, and this
portfolio has retracted a headline for the same reason before.

**So what *is* measured?** The sweep, which is not predictable in advance:

| coarse bits | median bytes | floor | excess | fallback rate | certhead wrong | quantized wrong |
|---|---|---|---|---|---|---|
| 2 | 0.1898 | 0.0636 | +0.1262 | 23.9% | 0 | 1211 / 1552 |
| 4 | 0.2232 | 0.1261 | +0.0971 | 6.2% | 0 | 293 / 1552 |
| **5** | **0.1582** | 0.1574 | **+0.0009** | **3.4%** | **0** | **151 / 1552** |
| 6 | 0.1886 | 0.1886 | +0.0000 | 1.4% | 0 | 83 / 1552 |
| 7 | 0.2199 | 0.2199 | +0.0000 | 0.5% | 0 | 40 / 1552 |
| 8 | 0.2511 | 0.2511 | +0.0000 | 0.3% | 0 | 14 / 1552 |

The curve has a **minimum at 5 bits**, and that is the finding. Below it the bound is too loose and
fallbacks dominate (2-bit costs *more* despite reading a quarter the bytes). Above it you are
simply paying for a wider floor. Where that minimum sits is a fact about the model, discoverable
only by measuring.

The distribution is narrow — p90 0.1627, max 0.1998 — and flat across prompt kinds (median 0.1576
for code, 0.1591 for deliberately ambiguous text). A method whose cost varied wildly by input
would be more interesting; this one does not, and saying so is more useful than a mean.

## Do the bytes become time?

**Pre-registered answer: not proportionally.** `experiments/certhead/bench_mlx.py`, Apple Metal,
batch 1, the real head shape:

| | median time | bytes | effective bandwidth |
|---|---|---|---|
| dense fp16 | 1.47 ms | 272 MB | 185 GB/s |
| certhead (2% survivors) | 0.76 ms | 83 MB | 109 GB/s |

(Absolute times are one machine on one thermal day and drift ~10% between runs; the **ratios** are
what repeat, and they are what the verdict is decided on.)

Time fell to **0.52×** while bytes fell to **0.30×** — a proportionality gap of **1.70–2.01** across
5 independent repeats, against a threshold of **1.5 fixed before the benchmark was first run**.
Verdict: `BYTES_DID_NOT_BECOME_TIME`, decided on the *worst* repeat.

The diagnostic is the bandwidth column. Dense saturates the memory system; every certhead
configuration runs at roughly 60% of that rate, which is the signature of a step that costs time
without moving the counted bytes — here, the survivor compaction.

**This repository does not promote that 0.52× to a speedup claim,** and the threshold was not
retuned after the numbers came in. It is one matvec on one machine at batch 1; the one time this
portfolio measured serving end to end, it got 0.997×. The counting claim is the one meant to carry
weight, and it survives the negative intact.

## 30-second quickstart

```bash
certhead verify          # the oracles that establish the invariant
certhead demo            # one certified argmax, explained
```

```console
$ certhead demo
synthetic head: V=4,096 d=128, coarse=5 bits

winner ................. token 1701
exact score ............ 35.029769
established by ......... proven_by_bound
max pruned upper bound   34.355208
margin ................. 0.186021
refinement stages ...... 2
head bytes read ........ 346,036 of 2,097,152 (16.5%)
survivors per stage .... [29, 1]

matches dense argmax: True
```

## In your own code

```python
import numpy as np
from certhead import compile_head, argmax_certified, dense_argmax

W = np.random.default_rng(0).normal(size=(4096, 128))   # your output head
head = compile_head(W, n_stages=3, tile=8, coarse_bits=5)

h = np.random.default_rng(1).normal(size=128)           # a hidden state
cert = argmax_certified(head, h, W)

assert cert.winner == dense_argmax(W, h)                # always true, by construction
print(cert.method)          # 'proven_by_bound' or 'dense_fallback'
print(cert.byte_fraction)   # may exceed 1.0 — see below
print(cert.margin)          # None on a fallback: no claim the run did not earn
```

`byte_fraction` **can exceed 1.0** and is deliberately not clamped. A bound too loose to prune
anything costs the coarse scan, every refinement, *and* the dense read on top. At 1-bit stages that
is ~1.28× dense, measured. Hiding the method's worst case behind a clamp would be its own dishonesty.

## How the invariant is established

Not by sampling. A bound-based method fails exactly when two scores are nearly equal, and near-ties
are vanishingly rare under any natural distribution — so a sample is drawn from precisely the region
where the method cannot fail. (The sibling benchmark in this portfolio measured that effect: sampling
24% of a fully enumerable domain still admitted a one-input defect four times in five.)

So three oracles, in descending order of what they are worth:

1. **`whole_domain`** — enumerates a small head **exhaustively** (81 of 81 points) and asserts
   `n == domain_size` at the end, so a truncated sweep cannot report itself as complete.
2. **`adversarial`** — **constructs** the hard cases rather than waiting for them: exact ties solved
   from `h · (wᵢ − wⱼ) = 0`, then ties at 1 ULP, 1e-12, 1e-9, 1e-6, 1e-3 either side. The fallback
   must fire, and the suite fails if it never does.
3. **`random_probe`** — labelled in its own output as **NOT evidence of exactness**, and kept only
   because it exercises realistic shapes the tiny exhaustive head cannot.

If you insisted on reading the 1,552-state agreement as a statistic: 1,552 trials with 0 failures
rejects every rate at or above **0.0019** at the 95% level (Clopper–Pearson, exact). That bound is
weaker than the structural argument, which is why the structural argument is the one quoted.

## Exit codes

| code | meaning |
|---|---|
| `0` | checked, and the invariant holds |
| `1` | checked, and a disagreement was found |
| `2` | **not checked** — abstain, unreadable input, or a missing dependency |

`2` exists so that "we could not check" can never be misread as "it passed".

## Licence and the commercial boundary

Apache-2.0, and [`LICENSE-TAG`](LICENSE-TAG) is **CLEAN** — but for a different reason than the
other packages in this portfolio, which are clean because they only *measure*. certhead is clean
because **it computes the identical function**: an equivalence-preserving rewrite that admits
nothing, refuses nothing, and gates nothing. [`CLAIMS-MAP.md`](CLAIMS-MAP.md) makes that auditable
rather than asserted, including the strongest objection to it.

A certificate-carrying admission gate — one that withholds a physical resource when the evidence
does not support the bound — is a separate, commercially licensed product.

## Reproducing the numbers

```bash
pytest -q                                            # 17 tests
certhead verify                                      # the three oracles
python experiments/certhead/run_bytes.py             # the sweep table (~31 min, needs a GPU/MPS)
python experiments/certhead/bench_mlx.py             # the traffic verdict (Apple Metal)
```

`run_bytes.py` **refuses to pad**: an earlier version repeated hidden states to reach a requested
`--n`, which inflated every denominator with inputs carrying no new information. It now reports how
short the corpus actually is and stops.

Certificates: [`results/data/certhead/bytes_cert.json`](../../../results/data/certhead/bytes_cert.json)
· [`results/data/certhead/mlx_traffic_cert.json`](../../../results/data/certhead/mlx_traffic_cert.json)

<!-- PORTFOLIO -->
---

## The rest of the portfolio

25 artifacts, one idea: **a measurement you cannot check is a press release.** Every tool
here reports; none of them gates.

**Tools**

| | |
|---|---|
| [`abstain-bench`](https://github.com/nickharris808/abstain-bench) | how often does a verifier pass input it could not check? |
| [`evidence`](https://github.com/nickharris808/evidence) | run the whole portfolio over your repo — the weakest leg, never the mean |
| [`floorgen`](https://github.com/nickharris808/floorgen) | what must your system remember? an exact lower bound |
| [`formal-proof-mcp`](https://github.com/nickharris808/formal-proof-mcp) | a proof kernel for your coding agent |
| [`gatecount`](https://github.com/nickharris808/gatecount) | exactly how many states does removing this check admit? |
| [`gridlock`](https://github.com/nickharris808/gridlock) | certify a wait-for relation cannot wedge |
| [`honestbench`](https://github.com/nickharris808/honestbench) | measure your CI's escape rate |
| [`kvleak`](https://github.com/nickharris808/kvleak) | cross-tenant leak scanner |
| [`kvprobe`](https://github.com/nickharris808/kvprobe) | model-substitution detector with a measured FPR |
| [`preregister`](https://github.com/nickharris808/preregister) | refuses to seal a plan whose conclusion is already fixed |
| [`proof-carrying-ci`](https://github.com/nickharris808/proof-carrying-ci) | the whole portfolio as one CI check, with SARIF |
| [`proof-to-code-drift`](https://github.com/nickharris808/proof-to-code-drift) | fail the build when the proof stops matching |
| [`sf-verify`](https://github.com/nickharris808/sf-verify) | re-derive admission decisions offline |
| [`signoff-cert`](https://github.com/nickharris808/signoff-cert) | certificates that carry their own false-pass bound |
| [`tokencount`](https://github.com/nickharris808/tokencount) | a token count both parties can recompute |

**Benchmarks** — each recomputes one of our own published numbers from its certificate

| | |
|---|---|
| [`illusion-bench`](https://github.com/nickharris808/illusion-bench) | how many broken kernels does your oracle admit? |
| [`kv-reuse-econ-bench`](https://github.com/nickharris808/kv-reuse-econ-bench) | recompute our economics headline |
| [`llm-tenant-isolation-bench`](https://github.com/nickharris808/llm-tenant-isolation-bench) | recompute our isolation figures |

**Datasets**

| | |
|---|---|
| [`abstain-corpus`](https://huggingface.co/datasets/nickh007/abstain-corpus) | 32 inputs a verifier must NOT pass |
| [`kv-reuse-econ-traces`](https://huggingface.co/datasets/nickh007/kv-reuse-econ-traces) | per-workload reuse accounting + the closed form |
| [`kv-tenant-isolation-bench`](https://huggingface.co/datasets/nickh007/kv-tenant-isolation-bench) | isolation observations, uninterpretable rows included |
| [`llm-precision-fingerprints`](https://huggingface.co/datasets/nickh007/llm-precision-fingerprints) | precision-labelled logprobs with a negative control |

**Try it in a browser** — no install, no GPU

| | |
|---|---|
| [`negative-results-atlas`](https://huggingface.co/spaces/nickh007/negative-results-atlas) | ten claims we took back |
| [`tenant-leak-demo`](https://huggingface.co/spaces/nickh007/tenant-leak-demo) | the residency calculator |
| [`wait-for-visualiser`](https://huggingface.co/spaces/nickh007/wait-for-visualiser) | paste a wait-for graph, see the cycle |

### Documentation

Everything above, explained in one place: **<https://nickharris808.github.io/evidence-docs/>** —
the [tutorial](https://nickharris808.github.io/evidence-docs/start/tutorial/),
[what this proves and what it does not](https://nickharris808.github.io/evidence-docs/concepts/what-this-proves/),
and a [CLI reference](https://nickharris808.github.io/evidence-docs/reference/cli/) generated by
running `--help` on every published command.

### The commercial edition

Everything above is **measure-only** and Apache-2.0: it tells you what is true and never acts on
it. The **enforcement** side — binding a partition key at the admission decision, the compiled gate
corpus, and the certificate-*issuing* faucet — is covered by filed patents and licensed separately.

**Reading is free. Enforcing is licensed.**
<!-- /PORTFOLIO -->
