Non-linearities under an exact contract

Checkpoint: CP-013 · Status: COMPLETE, run 2026-09-01 Question: can softmax, GELU and layernorm be pinned exactly — and what does verifying a whole layer cost?

Result

Yes. A transformer-shaped layer — three matmuls, softmax, GELU, layernorm, requantisation, all in exact integer arithmetic — produced bit-identical output on numpy-cpu, mlx-cpu and mlx-gpu at every shape tested.

The trick is specification, not arithmetic: non-linearities are specified as integer lookup tables rather than as formulas. A gather is memory indexing, so there is nothing to round and divergence is structurally impossible rather than merely unlikely. Reductions (max, sum) are exact integer operations, so they stay order-independent and no backend has to agree with any other about reduction order.

NC-0.1's scope limit is lifted — the numeric contract now covers a whole layer.

Verification cost, and the rule

R_verify ≈ the fraction of the layer that is non-linear.

Scope qualifier added after E016: this is a compute ratio and assumes the verifier already holds the layer's intermediate tensors. E016 measured the cost of transmitting them — 49 MB per layer, 3,010× the answer — and found it dominates every configuration. See ../016-verification-bandwidth/.

The linear half is nearly free; the non-linear half is paid in full. That is a design rule: to make verification cheaper, make non-linearities cheaper to recompute — not cleverer to check.

A side benefit worth noting: the recomputed half has zero soundness error. It isn't sampled, it's redone. The layer's whole probabilistic gap is the matmul term.

Where the prediction failed

We predicted R_verify under 10%. Measured 47–96%. Two causes, one real:

1. Our Freivalds runs 112× slower than its own arithmetic — 36.3% of the matmuls' wall time against 0.33% of their operations — because int64 numpy has no BLAS path. An int8/int32 GEMM (which every inference accelerator has) removes most of it. Implementation artefact.
2. The non-linear share is inflated — 23–41% here versus the ~1/d ≈ 0.02% predicted from operation counts. The prediction assumed both op classes run at the same throughput; numpy integer elementwise is ~100× slower per element than BLAS is per MAC. How much survives on fused kernels is UNKNOWN.

The structure is confirmed and favourable. The absolute overhead is not yet established: it lies somewhere between 0.5% and 20% depending on a number we have not measured.

Files

Raw records: ../../benchmarks/results/015-nonlinearities.jsonl

Bug found

Our Freivalds helper built its random matrix with A.shape[1] rows instead of B.shape[1]. Every matrix in E003 was square, which hid it; rectangular layer shapes did not. Fixed here and in E003's implementation — E003's results are unaffected, since its operands were square throughout.

Checkpoint CP-013

Can a whole transformer-shaped layer — matmuls and softmax, GELU, layernorm — be put under an exact numeric contract, and what does verifying it cost?

Why this is the experiment that decides NC-0.1

E014 produced a numeric contract that makes linear algebra bit-exact across heterogeneous hardware, and flagged its own scope limit: linear layers only. Softmax, layernorm and GELU involve division, exponentials and inverse square roots. If they cannot be pinned exactly, a full inference pipeline is partly contractable and partly not, and the security measured in E014 does not survive to anything Nodus actually sells.

Hypotheses

H15a. Non-linearities can be specified exactly, if they are specified as integer lookup tables over a quantised domain rather than as formulas. A gather is memory indexing, not arithmetic — there is nothing to round, so divergence is structurally impossible rather than merely unlikely.

H15b. The reductions inside softmax and layernorm (sum, max) are exact and order-independent in integer arithmetic, so NC-4 continues to hold and no backend needs to agree on a reduction order.

H15c (the cost hypothesis). Non-linearities do not need a clever verification scheme, because they are cheap enough for the verifier to simply redo. In a transformer layer the matmuls are O(s·d²) and the elementwise and reduction operations are O(s·d), so the non-linearities are roughly 1/d of the work — 0.02% at d = 4096.

• Falsified if recomputing the non-linearities costs a material fraction of the layer.

Predicted verification structure

   matmuls        ->  Freivalds        ->  ~0.5% of their cost
   everything else->  just recompute   ->  100% of their cost
   ------------------------------------------------------------
   layer total    ->  R_verify ~= 0.5% + (non-linear share of the layer)

If H15c holds, the second term is negligible and R_verify stays near the 4.6% measured for pure matmul in E003-D.

Prediction recorded before running

R_verify for the whole layer will be under 10%.

H15c is the one the research lead expected to be comfortably true and it is the one that needs the most care in interpretation — see analysis.md.

Implementation: implementation/intlayer.py.

The layer

Transformer-shaped, not a real transformer — no multi-head split, no residual connections, no positional encoding. It exists to exercise every op class a real layer contains, at realistic shapes:

  scores = Wq @ Wk           matmul, attention-shaped
  attn   = softmax_int(scores)
  H      = X @ W1            matmul (s x d) @ (d x 4d)
  H8     = requantise(H)     arithmetic shift + clip
  G      = gelu_int(H8)      LUT gather
  Y      = G @ W2            matmul (s x 4d) @ (4d x d)
  N      = layernorm_int(Y)  integer mean/variance/isqrt

All operands int8; all intermediates exact integers.

How each non-linearity is made exact

Backends

numpy-cpu, mlx-cpu, mlx-gpu. The whole layer runs on each, and outputs are compared for bit-identity — not closeness.

Verification

• matmuls — Freivalds over F_p (p = 1048573, k = 2), soundness 9.1 × 10^-13.
• everything else — recomputed by the verifier and compared exactly. Soundness for these is zero error: they are not sampled, they are redone.

Metrics, and the distinction that matters

Two costs are reported for the matmul check and they differ by two orders of magnitude:

• arithmetic cost — k·(1/m + 1/n + 1/k) of the matmul's multiply-accumulates. Implementation-independent. This is the real number.
• wall-clock cost — what our implementation took. Our Freivalds runs on int64 numpy, which has no BLAS path, while the native matmul runs on tiled float32 BLAS.

Per-op-class timings inside the native layer are collected so the layer can be split into its linear and non-linear halves.

Limitations

• Not a real transformer; no multi-head, no residuals, no attention masking.
• numpy integer elementwise throughput is far below BLAS matmul throughput, which inflates the measured non-linear share of the layer. A fused inference kernel would not have this profile.
• One machine. Single run per shape.
• LUT-based non-linearities are appropriate for int8 activations. Higher-precision activations would need piecewise-polynomial approximation instead (this is what ZIP does; see docs/literature.md).

Status: complete. H15a and H15b confirmed. H15c confirmed in arithmetic, but the prediction "R_verify under 10%" is NOT met by this implementation, and the reason is instructive. Date: 2026-09-01. Apple M5; NumPy 2.5.2 + Accelerate; MLX 0.32.2. Raw records: ../../benchmarks/results/015-nonlinearities.jsonl

---

1. The result that matters: exactness holds for the whole layer

Bit-identical, not close — across CPU and GPU, for a layer containing three matmuls, a softmax, a GELU, a layernorm and a requantisation.

H15a confirmed. Specifying non-linearities as integer lookup tables rather than as formulas removes the failure mode entirely. A gather is memory indexing; there is no arithmetic, so there is nothing to round and nothing to diverge. This is stronger than "the backends happened to agree" — divergence is structurally impossible.

H15b confirmed. The reductions inside softmax and layernorm (max, sum) are exact integer operations, so they are order-independent and NC-4 continues to hold: no backend has to agree with any other about reduction order.

The one genuine arithmetic hazard — inverse square root in layernorm — is handled by computing an exact integer sqrt with an explicit ±1 correction, using float64 sqrt only as a seed. That makes it FPU-independent.

NC-0.1's scope limit is lifted. The numeric contract now covers a whole layer.

2. Verification cost, and the rule that generalises

Verification decomposes cleanly, because the two halves are checked by different means:

So the governing relation is:

R_verify ≈ 0.005 × (linear share) + 1.0 × (non-linear share) ≈ the fraction of the layer that is non-linear.

The linear term is nearly free; the non-linear term is paid in full. This is a useful design rule: the verification overhead of an exactly-specified layer is essentially its non-linear fraction, and the way to reduce it is to make non-linearities cheaper to recompute, not to invent a cleverer check for them.

Measured:

3. Why the prediction was missed, and which part is real

The prediction was R_verify under 10%. Measured 47–96%. Two separate causes, and only one of them is fundamental.

Cause 1 — our Freivalds runs 112× slower than its own arithmetic

At s=1024, d=2048 the matmul check costs 36.3% of the matmuls it verifies, while its arithmetic is only 0.326% of theirs — a 112× penalty.

The cause is not the algorithm. It is that our check runs on int64 numpy, which has no BLAS path, while the native matmul runs on tiled float32 BLAS. This is the same effect recorded in E003 variant D, and the same remedy applies: an int8/int32 GEMM — which every inference accelerator already has, because it is what quantised inference runs on — would remove most of it.

We attempted a fix here (smaller prime p = 65521, all products on float64 BLAS) and it was slower, because reducing the operands mod p costs a full O(n²) pass per matrix and dominated the saving. The right version pre-reduces the weights once and amortises them across jobs; that is engineering we have not done, and we are not claiming its result.

This term is an implementation artefact. The 0.33% is the real number.

Cause 2 — the non-linear share is inflated, and this one is partly real

The rule in §2 says R_verify tracks the non-linear share. Here that share is 23–41%, which is far above the 1/d ≈ 0.02% that H15c predicted from operation counts.

H15c's arithmetic was right and its assumption was wrong. It assumed both op classes run at the same throughput per operation. They do not: numpy integer elementwise operations are roughly two orders of magnitude slower per element than BLAS matmul is per multiply-accumulate. The non-linearities are ~1/d of the operations and ~1/3 of the time.

How much of this survives on real hardware is UNKNOWN and not measured here. Fused inference kernels run non-linearities at memory bandwidth and typically spend a much smaller fraction of layer time on them — but that is an expectation, not a measurement, and it is the obvious thing to check next.

Honest summary: the fundamental structure is confirmed and favourable; the absolute overhead we measured (47–96%) is dominated by two implementation choices; and the true figure lies somewhere between 0.5% and 20% depending on a number we have not yet measured.

4. Security

Recomputation is worth noting as a feature: for the non-linear part there is no probabilistic gap at all. The layer's overall soundness error is the matmul term alone.

Trust set: the verifier holds the weights and the layer's intermediate tensors; randomness is chosen after the outputs are fixed; the numeric contract is part of the job specification.

5. What a malicious provider can still get away with

• Everything from E013 — caching, sub-contracting, being legitimately efficient. Verification constrains the answer, not the work.
• Anything the contract does not pin. We pinned dtype, accumulator, tiling, LUT contents and rounding. A real deployment must pin the LUTs by hash, or a provider can be "correct" against its own cheaper table.
• Bandwidth. The provider must transmit intermediate tensors for the verifier to recheck. We did not model that cost, and at O(s·d) per op it is not obviously negligible next to the compute being saved. This is the largest unmodelled cost in the scheme.

6. Limitations

• Not a real transformer: no multi-head, no residuals, no masking.
• The non-linear share depends heavily on implementation quality; ours is numpy.
• Single run per shape, one machine.
• LUT specification suits int8 activations. Higher precision needs piecewise-polynomial approximations — which is exactly what ZIP does, and its measurements are the reference point (docs/literature.md).
• The accuracy cost of integer inference remains UNKNOWN, and remains the price of this entire direction.

1. Bandwidth — the largest unmodelled cost [do first]

To recheck the non-linearities, the verifier needs the layer's intermediate tensors. That is O(s·d) per operation transmitted over a network, against compute the verifier is trying to avoid doing. We did not model it, and it could plausibly dominate everything measured in this experiment.

Concretely: does the coordinator need the full activations, or can it re-derive them from the layer's inputs plus the (already verified) matmul outputs? For a deterministic contract the answer looks like yes — it can recompute the non-linearities from the matmul outputs it already checked, which would make the transmitted set just the matmul outputs. That should be verified, because if true it changes the cost model substantially, and if false the scheme has a network bill nobody has counted.

2. Measure the non-linear share on a real inference stack

R_verify tracks the non-linear fraction of the layer, so that fraction is now the single most important unknown. Ours is 23–41% and is a numpy artefact. A fused kernel (llama.cpp, MLX's own transformer ops) would give the real figure. Until then the headline overhead is a range, not a number.

3. Remove the 112× Freivalds penalty

Use an int8/int32 GEMM path, or pre-reduce weights once into F_p and amortise across jobs, then run the check on BLAS. We tried the naive version of this and it was slower because the reduction pass dominated; the amortised version is straightforward and untested.

4. Pin the LUTs by hash in NC-0.2

A contract that says "GELU via a lookup table" without fixing which table lets a provider be correct against its own cheaper one. The tables are small (256 and 2048 entries) — commit to them by hash in the job specification.

5. The accuracy question, still unanswered

Everything since E014 assumes integer semantics are acceptable. The end-to-end task accuracy cost of int8 inference against a float baseline is still UNKNOWN, and it is the price of the whole direction. It needs a real model, which is the same setup as the deferred cross-backend decoding experiment.

6. Multi-layer, then a real model

A single layer is not a pipeline. Errors do not compound in exact arithmetic — that is the point — but the bandwidth and intermediate storage costs do, which is another reason item 1 comes first.