Verifiable Compute Needs a Numeric Contract

A distributed compute network routes a job to a stranger's machine and settles payment when a result comes back. The result carries a signature. That signature establishes origin — this came from the holder of that node's key, unmodified — and nothing else. A provider holding a valid key can fabricate an output, sign it, and be paid.

The obvious response is a cryptographic proof of correct execution. We began there and abandoned it on measurement: proving y = 3x + 5 in a modern zkVM costs 11.19 s against 0.69 ns of native computation, and the asymptotic overhead settles at 7 × 10⁴× for the friendliest possible workload (§4). That is not a tuning problem.

The metric. Throughout, we report

        cost of obtaining trustworthy evidence
  R  =  ──────────────────────────────────────
             cost of the native computation

against the option every verifier already has: re-execute the job, for which R_verify = 1 by definition. A mechanism costing more than re-execution must justify itself with something re-execution cannot provide — succinctness for a third party, or privacy of the weights. For a coordinator that holds the model and could simply re-run it, neither applies.

What we found instead. The interesting constraint turned out not to be cryptographic at all. It is that a verifier cannot distinguish a cheating provider from an honest one running different hardware, because honest hardware does not agree with itself.

ZIP (CCS 2025) is a commit-and-prove SNARK for inference with native IEEE-754 semantics. Its mini-BERT experiment reports 37.06 prover-hours and 0.85 verifier-hours. Notably, 93% of the proving cost is the linear layers (34.53 of 37.06 hr) even though the paper's contribution optimises the non-linear ones — which is what directed our attention to matrix multiplication.

SafetyNets (NeurIPS 2017) applies an interactive proof (sumcheck/GKR) to neural inference: 5% prover overhead, under 8 KB of communication, verification 8–82× faster than re-executing, for a whole CNN. Two of those beat what we build here: our prover is 10.4% at n = 4096 (§10) and our verification is 1.6× faster than re-execution at that size. Communication is not comparable, since their figure covers an entire network and ours covers a matmul chain. Its restriction to quadratic activations and sum pooling is usually read as a dated compromise; §10 argues it is load-bearing.

EigenAI (Jan 2026) ships deterministic inference plus optimistic re-execution plus slashing. It achieves determinism by controlling the environment — fixed GPU architecture, pinned drivers, canonical reduction orders — and states as future work: "Cross-Architecture Reproducibility. Determinism currently holds only within fixed GPU families. Future work includes portable numeric normalization to enable heterogeneous verifier sets." That sentence describes the problem this paper addresses.

Proof of useful work. Forcing a prover to expend work is not an open problem: constructions exist, including one for matrix multiplication at 1 + o(1) overhead. But every one rests on an unproven hardness conjecture — there are no unconditional superlinear lower bounds, and ω is still falling (< 2.371177). A 50-scheme systematisation concludes proof-of-useful-work "is actually not as useful as expected". Proof-of-Learning, the direct ML analogue, was published and then broken by spoofing attacks.

Verification produces evidence for specific claims, and mechanisms are routinely credited with claims they do not support. We separate:

A signed receipt establishes O. A SNARK establishes A. Neither establishes D, and a proof carries no information about the machine that produced it.

Adversary. The provider is untrusted and rationally malicious: it cheats when expected profit is positive and invests effort proportional to the payoff. A rational model is more useful than a worst-case one here, because it makes the defence a question of expected value.

Trusted. The coordinator, throughout. Removing that assumption is out of scope and we flag where it matters (§8.3).

General zkVM. SP1 6.5.0, CPU prover, Apple M5.

The cost is almost entirely a fixed charge per proof: the marginal and fixed costs are equal only at ~9.7 × 10⁵ zkVM cycles. Compressed proofs verify in a flat ~37 ms with a byte-identical 1.27 MB proof across a 965× range of job sizes — genuinely succinct — but reaching the point where that beats re-execution costs ~28 minutes of prover time to verify 35 ms of computation.

This is a lower bound for inference: u64 arithmetic in a register-resident loop is the friendliest workload a RISC-V zkVM will see.

Freivalds (1977). Verifying A·B = C for n = 8192:

Nine orders of magnitude separate these two mechanisms on the same claim. The difference is not implementation quality: a zkVM proves a RISC-V execution trace and pays for every load and branch, while Freivalds exploits the algebraic structure of the statement.

Measured caveat: the theoretical k/n advantage is eroded ~4.7× because matmul is the most heavily optimised kernel in computing while the check is memory-bandwidth bound. Quote measured ratios, not asymptotic ones.

Freivalds' soundness argument assumes exact arithmetic. Floating-point matmul rounds, so an honest prover produces a nonzero residual, so the verifier needs a tolerance — and any tolerance is an attacker's budget.

We measured how large that tolerance must be. On real-valued operands:

Crossing vendors costs 4.8 × 10⁻⁷. Crossing from CPU to GPU costs 1,600× more. The accurate statement is not "heterogeneous hardware diverges" but "heterogeneous CPUs agree; GPUs diverge, because their matmul paths round operands."

A 5,900× separation is a threshold anyone can set. 3.7× is not. And admitting GPUs is precisely what a compute network exists to do.

We note the sharper form of this: a backend advertising float32 may not be computing in float32, and TF32 is enabled by default in many frameworks because it is faster. A provider "running float32" very often is not — the same behaviour as an attacker, with no intent to cheat.

If inexact arithmetic is the problem, the fix is to remove it from the specification rather than tolerate it in the verifier.

The GPU's imprecision was never about the GPU. It was about representing real numbers. We expected a supply/security trade-off — a stricter contract excluding honest hardware — and measured the opposite: the strictest contract admits every honest backend tested.

NC-0.5, the resulting specification, in brief:

NC-4 deserves emphasis: once arithmetic is exact, reduction order needs no constraint. Float contracts must pin an order that is effectively impossible to pin across hardware; exactness deletes the requirement rather than satisfying it.

6.1 The binding constraint is the operand, not the accumulator

Our first draft bounded the float32 accumulator at 2²⁴. That bound was never the binding one. Apple's Metal matmul is exact on integer operands only to 2¹¹, and inexact from 2¹², regardless of accumulator magnitude — 13 bits tighter. Every earlier experiment satisfied the real bound by accident, because int8 operands are ≤ 127. Attention probabilities carried at 2¹⁵ were the first to exceed it, and the contract failed silently mid-generation.

From the Metal measurement we predicted, and recorded before any NVIDIA hardware was available:

NVIDIA's TF32 carries a 10-bit explicit mantissa — 11 with the implicit bit — so a TF32 path should show an operand bound of 2¹¹, the same figure as Metal, arrived at from a different vendor's design.

Measured on an NVIDIA L4 (Ada, compute 8.9), with the reduction length held short so the accumulator kept ~19 bits of headroom throughout:

Exact to 2¹¹, inexact from 2¹². Precisely the Metal figure. Two vendors sharing no design lineage land on the same 11-bit effective mantissa. The bound is a property of accelerator matmul, not of one framework.

7.1 A real model, five backends

Qwen2.5-0.5B — 24 layers, hidden 896, GQA, RMSNorm, SwiGLU, RoPE, vocab 151,936 — under NC-0.5, first 96 tokens of wikitext-2:

Byte-identical on all five, every next-token prediction matching, across two CPU vendors, two GPU vendors, three operating systems and three Python versions.

TF32 was left enabled deliberately. int8 operands are four bits inside NC-3b's bound, so the reduced-precision tensor-core path cannot lose anything. The contract never asks a provider to disable a hardware feature — which is the difference between a specification that can be complied with and one that demands crippled hardware.

8.1 Compute

Verification of matmul under exact field arithmetic: R_verify = 0.046 at n = 8192, soundness 9.1 × 10⁻¹³, no tolerance and no tuning parameter. Exact arithmetic costs 2× the floating-point check and buys back the entire guarantee.

For a whole transformer layer, verification splits: matmuls checked by Freivalds at 0.33% of their multiply-accumulates, everything else recomputed at 1.0× with zero soundness error. The governing relation is

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

8.2 Accuracy

Measured like for like on Qwen2.5-0.5B, wikitext-2: 120 disjoint 128-token chunks spread across the whole test set, 15,240 scored positions, with intervals by bootstrap over chunks (20,000 resamples).

Those intervals are wide, and they are the uninteresting half. Perplexity is dominated by which chunks are drawn — per-chunk values here span 8.6 to 43.3, a 5× range against pipeline differences of a few percent. Every pipeline saw identical chunks, so the differences are paired, and pairing cancels chunk difficulty:

Quantisation costs +6.67%; full integer determinism adds +2.43% [1.63, 3.23] on top. The gap's interval is 1.6 points wide against ~5 on either endpoint — the payoff of the paired design.

That +2.43% is plausibly close to intrinsic: a float-accumulation pipeline keeps accumulators exact between steps, and a fully-integer one cannot, so it has more rounding boundaries by construction. The per-chunk view supports that reading rather than a stronger one — the gap holds its sign in only 83 of 120 chunks, so the contract is worse on average by a little, not worse on every input.

A defect only scale revealed. Our contract originally specified per-tensor quantisation, written from a 2-layer character model where it was harmless. On a real model, per-tensor int8 gives perplexity 70.39 against a float baseline of 16.77; per-channel gives 17.36. The clause was wrong, and no toy could have shown it.

8.3 Bandwidth — the constraint we did not anticipate

Verifying a layer requires the verifier to hold that layer's intermediate tensors. Measured, for one layer at s = 1024, d = 2048:

Every configuration loses, including rented-GPU compute with intra-datacentre transfer. Compute was never the binding cost.

(SafetyNets states the direction of this effect in one sentence in 2017. We rediscovered it by construction before reading them, and record that here rather than claim priority.)

The audit protocol. Bandwidth for auditing one layer is flat; compute saved scales with depth. We implement: the provider Merkle-commits to every layer output, submits root and answer, and the coordinator challenges one layer drawn uniformly after the commitment. Measured on Qwen2.5-0.5B, 24 layers:

Two details of the paper design were wrong and building it corrected them. The opening does not need to carry the layer's output: the verifier recomputes it and checks its own digest against the root, which halves the traffic and is strictly more secure, since the provider never states what the output was. And layer 0 is free — its input is the embedding the verifier derives itself, so the opening is two Merkle paths and 160 bytes.

This is not a proof. A single-layer cheat escapes with probability 1 − 1/L = 0.958 at 24 layers. The defence is the stake. For a provider skipping m of L layers, the saving is m/L of the job value V and the detection probability is m/L, so cheating is negative-expected-value when penalty·(m/L) > V·(m/L) — the m and L cancel:

A stake equal to the job's compute value suffices, at any depth and any level of greed.

8.4 A conclusive fraud proof, when someone will pay for one

The audit's verdict is economic, not evidential: it establishes that cheating loses money, never that a particular provider cheated. Where a conclusive ruling is wanted, the same Merkle commitment supports an Arbitrum-style bisection. Two parties who disagree binary-search to the first layer whose committed digest differs, and an arbiter recomputes that layer alone.

Measured on the same 24-layer model:

Five rounds (⌈log₂24⌉), 1.9 KB of digests and Merkle paths, and the arbiter recomputes exactly one layer whether the provider cheated on one layer or on twenty-one. A challenger that disputes an honest job is ruled against by the same machinery, so a false dispute is as slashable as a false result.

Two properties are worth drawing out. Both scale the right way with depth — rounds grow as log₂L while the arbiter's share is 1/L, so deeper models make adjudication cheaper. And the search lands on the actual cheated layer in 24 of 24 cases, because under exact integer semantics a perturbation propagates rather than being rounded away. The exactness that makes heterogeneous verification possible is also what makes the fraud proof name the right layer.

This construction is standard in rollups and has not previously transferred to neural inference, for the reason this paper is about: it requires two honest parties to produce identical bytes. It does not reduce the cost of verification — the challenger still re-executes — it reduces the cost of adjudication, and makes the verdict conclusive.

Correctness is not expenditure. A compute market pays for work, and almost all of the verifiable-computation literature addresses answers. We ran seven provider strategies against our strongest checker. Every strategy that changes the answer is rejected — including the reduced-precision cheat. Exactly one strategy is accepted while doing materially less work: returning a cached correct answer, and no checker of any strength can object, because the answer is right. It is a pricing bug, closed by deduplicating on the input commitment.

The other low-work strategy that passes is Strassen's algorithm — 67% of the arithmetic, exactly correct, accepted. Correctly accepted: a verifier cannot distinguish "cleverer" from "lazier", because at the level of the output there is no difference.

A shortcut is only an attack if you are paying for effort rather than output.

We therefore argue that Claim C and Claim D should be removed from the settlement path rather than solved: price the job from its specification, verify the output, deduplicate repeats, and let efficient providers keep the margin.

Sumcheck answers the bandwidth problem for linear algebra. We implement it: a two-layer chain of 2048² matmuls verified without the verifier ever receiving the intermediate, in a 792-byte transcript against 16.8 MB — a 21,183× reduction that improves with scale, because communication grows logarithmically while the data it replaces grows quadratically.

Applied to a transformer layer it saves nothing. All three matmul outputs — 49.1 MB, the same figure as §8.3 — feed lookup-table non-linearities the verifier checks by recomputation, so it needs the values regardless. The chain breaks at the first non-linearity, and there is one after every matmul.

This is a tension between two requirements: NC-9 makes non-linearities lookup tables because a gather has no arithmetic and so cannot diverge; a sumcheck passes only through low-degree arithmetic. The property that buys determinism blocks the proof.

It is worth being precise about what does not block it. We measured the prover, on square matmuls over F_p:

falling as n^−0.92 against the n^−1 the structure predicts, and reaching 5% by n ≈ 8,800. Within that, the sumcheck rounds themselves are 0.5% of the overhead: the protocol is free, and the cost is entirely the multilinear extensions and reducing operands into the field, split about evenly.

Two details are worth reporting because they nearly misled us. Our first implementation measured 36.1%, and the breakdown showed why: numpy has no BLAS path for int64, so the extension products were running at 733× the per-element cost of a float64 multiply-add, and two of three field reductions were being applied to operands already inside the field — NC-3b bounds them at 2^11 and p is 2^25. Fixing both gave 3.5×. The first number measured our code, not the protocol.

So the prover is not the obstacle, and our measurement is consistent with SafetyNets' reported 5% being real rather than an artefact of a friendlier setting. The obstacle is the non-linearity structure alone.

Making a transformer sumcheck-compatible therefore means changing the model. We measure the cost:

Replacing GELU with x² is free (−0.5%, inside seed noise). Replacing softmax is the entire cost, and it grows with depth: softmax improves with depth while squared attention stops improving and regresses. The gap is a divergence, not a fixed tax a larger model amortises.

We therefore read SafetyNets' restriction to quadratic activations as load-bearing rather than dated. Their networks were CNNs and fully-connected nets with no attention to lose; a transformer's inductive bias lives in exactly the operation a sumcheck cannot pass through.

• Not deployed. No production node runs the contract. This is a measurement study, not a systems-deployment paper.
• One model, one corpus, one context length. Qwen2.5-0.5B on wikitext-2 at 128 tokens. Nothing here establishes the gap for a larger model, for code, or at long context. The bootstrap also assumes chunks are exchangeable; they are disjoint and spread across the corpus, but adjacent chunks share an article.
• The int8 ceiling is our own W8A8 implementation, not a tuned production quantiser. A stronger ceiling would widen the determinism gap, not narrow it.
• Sumcheck's compute advantage arrives late. Verification costs more than recomputing a single matmul at every size up to n = 2048, and only drops below re-execution at n = 4096 (63%). Its advantage is bandwidth, not compute.
• The prover figures are numpy, single-threaded, against multi-threaded BLAS, on square matmuls. 10.4% is an upper bound on what the protocol needs, not a floor, and a transformer's matmuls are rectangular.
• Empirical, not proved. No security proofs. All claims are measurements under stated assumptions.
• One model family. Qwen2.5-0.5B. Larger models, and architectures with different non-linearity profiles, are untested.
• Coordinator trusted throughout, though no longer for the audit challenge. That draw is now a commit-reveal two-party coin — the coordinator publishes H(nonce) before the provider runs, and challenge = H(nonce ‖ root ‖ answer) mod L is reproducible by the consumer, at 32 bytes per job. The residual assumption is publication: the commitment must reach the consumer before the job runs, or a colluding coordinator can backdate it and grind nonces, which we measure at 17 guesses to reach a chosen layer out of 24.
• Stake and slashing are unimplemented. §8.3's economics are derived.

Corrections

We made eight documented errors and record them because a measurement paper with no retractions is usually one that was not checking. Four that changed conclusions:

1. We bounded the accumulator when the binding constraint is the operand mantissa — 13 bits tighter, and the contract failed silently until we found it.
2. We predicted honest CPU/GPU greedy decoding would diverge "within tens of tokens". It usually does not: 9 of 10 prompts were identical over 300 tokens. Argmax has a margin. The conclusion survived; the reasoning was wrong.
3. We reported an unexplained ~7-point accuracy gap that was an artefact of comparing a 256-token measurement against a 128-token one.
4. We reported the determinism cost as +3.5% from 4–6 chunks with no stated uncertainty. Re-measured over 120 chunks it is +2.43% [1.63, 3.23] — the old estimate falls outside the new interval, and resampling at the original sample size gives [−1.36%, +6.47%], which contains zero. The conclusion was right and the evidence did not establish it; those are different things. The correction moves in the contract's favour, which is not a reason to have been less careful.

The question we set out to answer was which verification mechanism a compute market should adopt. The answer is that the choice of mechanism is downstream of a decision most systems never make explicit: what arithmetic the network requires.

Three independent lines of work arrive at the same requirement for three unrelated reasons — SafetyNets needed field arithmetic for its proof system, EigenAI needed reproducibility for optimistic re-execution, and we needed cross-backend agreement for probabilistic checking. That convergence is the strongest evidence we have that constraining arithmetic is the right lever.

Once it is constrained, verification is cheap by classical means and needs no cryptography at all. Left unconstrained, no mechanism helps: a proof of the wrong circuit is a valid proof.

Artefacts. The full repository, every raw measurement record, and a conformance kit that reproduces the cross-vendor determinism result with numpy alone and no GPU.