Verification Methodology

4 min read#methodology

What "verified" means on this site — the re-implemented pipelines, the standard probe, the metrics, and the verified/attested boundary.

Contents

Verification Methodology

Every load-bearing number on this site is either verified — recomputed by the site build from the pipelines in this repository — or explicitly attested — captured from a run too expensive to repeat inside the build, with the raw log committed. Nothing is transcribed by hand: verified numbers are injected into the page at build time from the check's actual stdout, so a fabricated value is not merely detectable, it is impossible to type.

The re-implemented pipelines

  • Inference: the Java engine at code/attention/src/ — see The Engine. Every check compiles it from source (javac, JDK 21+) in a clean staging directory and runs it on the stories15M checkpoint and tokenizer, fetched by URL from their public homes and content-hashed.
  • Training: the PyTorch pipeline at code/attention/python/ — model port, streaming cluster attention, tokenizer, trainer, and llama2.c exporter. The train-pipeline check runs a seeded 20-step fine-tune end-to-end, including the export → Java round trip.
  • Data: prepare.py re-derives tokens.npy from the public dataset (prefix-verified continuously; full file reproduced in the authoring environment).

The standard probe

Short-range fidelity numbers teacher-force one fixed 70-token prompt (the "Shoggoth probe", defined verbatim in each check's run script) through the candidate implementation and exact causal attention, sharing one set of weights, and count positions whose argmax token agrees. The original experiment used a 56-token probe whose text was not preserved; the counts here are therefore re-measurements under a documented probe, not transcriptions of the historical table — rankings, not raw counts, are the comparable quantity, and the rankings reproduce.

Stream health

The --stream harness generates 2048 tokens (8× the trained context, BOS treated as a story separator) with fixed seeds and reports the per-128-token window distinct-token ratio — a collapsing ratio is "mush" made measurable. The engine's exact port of llama2.c's xorshift RNG makes these runs bit-reproducible for a given seed, which is what lets a sampled generation be a verifiable quantity at all. First/last/min ratios per seed are in the stream-health check; three seeds each.

What is attested, not verified

  • Speed (tok/s): timing is machine-dependent and nondeterministic, so every throughput figure is an attested measurement. Check scripts strip timing from their output for exactly this reason.
  • The 300-step fine-tunes: hours of CPU, far over the build's 20-minute per-check budget. Committed logs: experiment.log, tune-tiered.log. The same pipeline is verified at 20 steps.
  • Historical numbers from the original experiment (the 56-token-probe fidelity table, occupancy statistics, ablations not re-run here) are reported as findings with their original values and marked by context.

Trust model

Checks execute where the site is authored; each successful run is recorded in evidence/attestations.json keyed by the content hash of the check script, its inputs manifest, and every input's bytes. CI runs a trust-mode verification: it executes nothing but re-resolves and re-hashes every input, so edited code, changed data, or a drifted upstream checkpoint all invalidate the attestation and fail the build until someone re-verifies locally. Determinism caveat: floating-point results are reproduced on the authoring machine class; a different BLAS/CPU may produce trailing-digit differences, which surface as check failures to re-attest rather than silent drift.

One such caveat was discovered by the checks: on JDK 24 the "bit-identical" exactness diffs came back at ~1.6e-5, not zero — the newer JIT compiles the two implementations' shared kernels differently (inlining and auto-vectorization decisions are made per call site), so identical Java source no longer implies identical floating-point results across implementations. The check scripts pin JDK 21, where the identities hold exactly at 0.000000. This is the evidence discipline working as intended: a claim of bit-identity is only as strong as the toolchain it names.