certhead

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

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.

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:

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.

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:

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:

(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

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

$ 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

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

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 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 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

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/mlx_traffic_cert.json

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

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

Datasets

Try it in a browser — no install, no GPU

Documentation

Everything above, explained in one place: https://nickharris808.github.io/evidence-docs/ — the tutorial, what this proves and what it does not, and a CLI reference 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.