Testing
How this project establishes that it computes the right thing, and how each of those checks was shown to be capable of failing.
The short version: a differential harness against the PyTorch reference, a byte-for-byte comparison against the reference C engine, and two mutation checks that prove both halves of the test suite can actually fail.
Results
All numbers below were produced by the commands in this file on the machine measured in performance.md. Nothing here is quoted from anywhere else.
Differential test, random weights
python reference/diff_test.py — pass requires |err| <= 1e-4 + 1e-4*|ref| at every logit and argmax agreement at every position.
| config | dim | heads / kv | layers | vocab | seq | classifier | max |err| | max |ref| | err/tol | top-1 |
|---|---|---|---|---|---|---|---|---|---|---|
tiny | 64 | 4 / 4 | 2 | 97 | 32 | tied | 3.87e-06 | 4.22 | 0.030 | 32/32 |
gqa-2x | 64 | 8 / 4 | 3 | 128 | 48 | tied | 4.17e-06 | 4.17 | 0.028 | 48/48 |
gqa-4x | 96 | 8 / 2 | 2 | 200 | 64 | tied | 5.72e-06 | 4.98 | 0.046 | 64/64 |
mqa | 64 | 4 / 1 | 2 | 64 | 40 | tied | 2.87e-06 | 4.57 | 0.026 | 40/40 |
untied-cls | 128 | 4 / 4 | 4 | 512 | 64 | untied | 9.66e-06 | 5.23 | 0.071 | 64/64 |
full-context | 48 | 2 / 2 | 1 | 50 | 128 | tied | 5.01e-06 | 4.50 | 0.029 | 128/128 |
6/6 pass. Worst case uses 7.1% of the allowed budget. Top-1 agreement is 100% everywhere.
max|ref| is printed on purpose. It is the evidence that the weights were re-randomised: llama2.c initialises matrices with std=0.02, which makes the logits nearly flat, and a flat output lets a whole family of genuinely wrong implementations land inside the tolerance. A max logit of ~5 rather than ~1e-3 means the test is measuring the arithmetic and not the tolerance.
Differential test, real weights
python reference/diff_test.py --checkpoint stories15M.pt -n 200
| model | max |err| | max |ref| | err/tol | top-1 | result |
|---|---|---|---|---|---|
| stories15M (15M params, vocab 32000) | 3.34e-05 | 26.2 | 0.192 | 200/200 | PASS |
The 200-token sequence is chosen by the reference greedy decoder, so the engine is being compared on a sequence an independent implementation produced.
Mutation check
python reference/mutation_check.py
| mutant | caught by |
|---|---|
RoPE exponent 2i → i | all six |
| RoPE skipped on keys | all six |
GQA mapping h / kv_mul → h % n_kv_heads | gqa-2x, gqa-4x only |
Attention window pos + 1 → pos.max(1) | all six |
| Attention scale removed | all six |
RMSNorm eps 1e-5 → 1e-27 | all six |
| SwiGLU gate and up swapped | all six |
| Untied classifier ignored | untied-cls only |
Residual x += d → x = d | all six |
| RoPE theta 10000 → 500000 | all six |
"all six" means tiny, gqa-2x, gqa-4x, mqa, untied-cls, full-context, the order the harness reports them in.
10/10 caught. The whole run takes roughly 20-30 seconds, dominated by rebuilding the crate ten times; every mutant shares one CARGO_TARGET_DIR and runs with LTO disabled, since LTO is the slowest part of the build and has no bearing on which mutants get caught.
The per-mutant column is the useful part, and it is why the configurations are chosen the way they are. gqa-modulo-mapping is caught by the two GQA configurations and nothing else, because modulo and division agree when kv_heads == n_heads — the other four configurations cannot see that bug at all. ignore-untied-classifier is caught by untied-cls alone, for the mirror-image reason. If every mutant had been caught by all six configurations, that would have looked like thoroughness and actually meant the suite had no discrimination.
Two guards keep that number honest:
- Each mutation's replacement snippet must occur exactly once in the source. Otherwise a refactor turns the mutant into a no-op, the harness correctly reports a pass, and "the test passed" becomes indistinguishable from "the bug slipped through".
- The unmutated source is checked first. "10/10 caught" would otherwise be consistent with "10/10 failed for an unrelated reason".
Rust tests, and proof they can fail
75 tests, passing in both release and debug (debug matters: it enables integer overflow checks, which is where a wrapping size computation in the loader would show up).
| suite | tests | what it covers |
|---|---|---|
src/ops.rs | 23 | kernels against hand-computed answers, RoPE invariants and its frequency schedule, causality of the attention window, dot across every length mod 8 |
tests/loader.rs | 18 | totality over hostile input, 2000 pseudo-random buffers, overflow, tensor ordering |
tests/tokenizer.rs | 16 | exact conformance to Meta's published token ids, byte fallback, round trips |
tests/engine.rs | 18 | causality, determinism, BOS termination, State::reset equivalence, argmax totality on NaN |
But a passing suite only says the tests agree with the code. It does not say they can notice disagreement, so reference/mutation_check_tests.py injects 21 realistic bugs one at a time and requires cargo test to fail on every one. 21/21 caught. It is the same discipline as mutation_check.py, pointed at the other half of the project: that one proves the differential harness can fail, this one proves the Rust tests can.
Running it found two genuine blind spots, both of which were real holes in the suite rather than in the mutants:
- The RoPE tests could not see the RoPE frequencies. All four were structural invariants — identity at pos 0, pair-norm preservation, no head mixing, the relative-position property — and every one of them is satisfied by a rotation through any angle. So
2 * i→iproduced angles that are wrong everywhere and passed the lot. The differential harness caught it; the unit suite on its own could not. There is now a test that computes the expected angle from the documented schedule and compares. - Nothing covered generation's BOS termination. That is the bug the byte-identity check found by hand, and the differential harness cannot see it because it never looks at text. There is now an engineered checkpoint whose first greedy step emits BOS, plus its mirror so the first test cannot pass for the wrong reason.
A third finding was subtler and worth naming: state_rejects_a_config_whose_cache_would_overflow was using i32::MAX as dim, which is odd, so State::new rejected the odd head size and returned InvalidHeader. The test passed without ever reaching the arithmetic it is named after. It now uses an even dim, asserts the config is structurally valid, and asserts the specific Overflow { what: "kv cache" } error rather than merely that some error occurred.
Every check, and how it was shown to fail
A check that has only ever been observed passing is consistent with a check that cannot fail. So each one was also exercised in a state where it had to go red. This is the inventory:
| check | how it was shown to fail |
|---|---|
diff_test.py (6 configs) | 10 injected bugs, mutation_check.py, 10/10 |
cargo test (75 tests) | 21 injected bugs, mutation_check_tests.py, 21/21 |
| byte-identical greedy output | a RoPE-less mutant binary: bench.py reports DIFFERENT and exits 1 |
| zero-dependency assertion | a Cargo.lock with a second package, with zero packages, and naming a package that is not proofinfer — all three rejected |
verus/check_citations.py | GQA mapping mutated in place, nine lines inserted to shift every citation, attention window changed, a cache write deleted; plus a missing source file, an unregistered citation, and a rotted table entry |
| CI workflow wiring | every steps.<id>.outputs.<name> resolves to a step that writes it, every run: block parses as bash, no || true outside comments |
| Verus itself | --no-cheating rejects assume / admit / external_body; the unmutated baseline is run first so "24 verified" cannot mean "the file does not parse" |
The full-run commands are in the repository, not just in a shell history: reference/mutation_check.py, reference/mutation_check_tests.py, and verus/check_citations.py all exit non-zero on failure and all run in CI.
Why the differential test is worth anything
The two implementations share nothing but the file format.
| reference (PyTorch) | proofinfer (Rust) | |
|---|---|---|
| forward pass | batched over the whole sequence | one token at a time |
| attention | scaled_dot_product_attention(is_causal=True) | explicit loop over the KV cache |
| RoPE | precomputed freq_cis table in the file | computed from theta and pos in ops::rope |
| GQA heads | torch.repeat_interleave | h / kv_mul index division |
| weights | f32 tensors via numpy | f32 slices read by a bounds-checked cursor |
Two consequences worth spelling out.
RoPE is computed, not read. The checkpoint file contains a freq_cis table, and reading it would have been easier. But then the differential test would compare two programs sharing a precomputed constant, and a bug in our RoPE would be invisible. Computing it means the test genuinely exercises our angle arithmetic. The loader skips those bytes on purpose.
The tolerance is a statement about summation order, not about the model. Both sides sum the same products in different orders, and floating-point addition is not associative, so a bitwise comparison would be testing matmul's inner loop rather than the transformer. Hence 1e-4 + 1e-4*|ref|: the absolute term covers logits near zero, where a relative bound is meaningless because the reference itself is working in f32 and has no significant digits left, and the relative term covers large logits where accumulated rounding grows with magnitude. For fp16 the relative term would have to be around 1e-2, because fp16 carries about three decimal digits.
Source: https://github.com/blackdragoon26/proofinfer/blob/main/docs/testing.md in the repository.