Intuition says the FLOP-heavy matmuls dominate a zkML proof. Multiple 2024-2026 systems show the opposite: linear layers are cheaper to prove than to compute, and the bill is set by activations multiplied by their bit-width.
Ask an engineer new to zkML where a neural network’s proving cost goes, and the answer is almost always the same: the matrix multiplies. It is the obvious guess. A transformer’s FLOPs are dominated by the big GeMMs — the query, key, value, and output projections, the feed-forward matrices — and a proof has to account for every operation, so surely the proof is dominated by the same arithmetic that dominates the forward pass. Spend the optimization budget on the matmuls and the rest is rounding error.
The guess is backwards. Across the specialized zkML systems built between 2024 and 2026, the FLOP-heavy linear layers turn out to be the structurally cheap part of the proof — cheap enough, in some systems, that proving a matrix multiply costs less than computing it. The expensive part is everything that is not a matrix multiply: the ReLU, the softmax, the GELU, the layer normalization. Every non-arithmetic operation has to be forced through a lookup argument whose cost grows with the precision — the bit-width — you demand of the activation. A network’s proving cost is set by its activations and their bit-width, not by its parameter count.
This is a claim about the per-layer arithmetic inside a single inference step: given one forward pass, which layer type costs the most to prove. It is a different question from how a whole proof scales by model and library — that ground is the zkML cost curve — and different again from binding the witness to the committed weights. It is the matmul-versus-activation split itself, and the literature adjudicates it with surprising consistency.
Start with the part everyone expects to be expensive, because the surprise is load-bearing for everything after it.
A matrix multiplication has enormous structure, and structure is exactly what a proof system can exploit. The sumcheck protocol — the workhorse of modern zkML provers — lets you prove that a claimed matrix product is correct without re-doing the multiplication constraint by constraint. zkLLM, the first specialized zero-knowledge proof system tailored for large language models, states the position bluntly: zkLLM: Zero Knowledge Proofs for Large Language Models (arXiv 2404.16109) notes that “dedicated sumchecks for matrix multiplications have achieved running times significantly lower than the computation itself.” Read that twice. The proof of the matmul runs faster than the matmul. The most FLOP-heavy part of the network is the part with the most efficient proving protocol.
That is why the parameter-count intuition fails. Parameters live in the linear layers, and the linear layers are precisely where a dedicated sumcheck beats naive recomputation. A bigger weight matrix is more numbers to commit to, but the proof of the product itself does not scale the way the multiply does. The FLOPs that dominate the forward pass are not the FLOPs that dominate the proof.
Jolt Atlas, a 2026 zkML framework built on the Jolt proving system, makes the same split visible in a single end-to-end measurement. Jolt Atlas: Verifiable Inference via Lookup Arguments in Zero Knowledge (arXiv 2602.17452) reports a GPT-2 (125M parameters) proof with an end-to-end total of about 38 seconds, of which the sum-check proving — the part covering the linear algebra — is roughly 16 seconds, with witness generation around 7.5 seconds and commitment time around 3.5 seconds. The linear-layer sumcheck, the term the intuition says should dominate, is under half of the total prover time. The rest of the clock is spent elsewhere, and “elsewhere” has a name.
The trouble with a neural network, from a proof system’s point of view, is that it is not made only of multiplications and additions. It is made of those plus a set of functions that arithmetic circuits cannot express natively: the exponential inside a softmax, the max inside a ReLU, the error function inside a GELU, the reciprocal square root inside a layer norm. A SNARK speaks the language of low-degree polynomials over a finite field, and none of those functions is one.
Jolt Atlas states the consequence in nearly the exact words of the thesis: modern models “rely heavily on non-linear operations such as softmax or ReLU whose faithful realisation in low-degree arithmetic constraint systems can blow up constraint counts and/or degrees, often making them the dominant cost unless specialized techniques such as lookup arguments are used.” That is the whole argument in one sentence. The matmuls have structure-exploiting protocols; the non-linearities do not, and absent a workaround they become the dominant cost.
The workaround is the lookup argument. Instead of expressing the function as polynomial constraints, you precompute a table of its input-output pairs and prove that each activation value appears in that table. zkLLM’s entire contribution is built around this: the paper introduces “tlookup, a parallelized lookup argument designed for non-arithmetic tensor operations in deep learning, offering a solution with no asymptotic overhead.” The framing is telling — the named, persistent challenge the system was built to address is “the persistent challenge of non-arithmetic operations in deep learning,” not the linear algebra. The linear algebra was never the problem. The activations were.
zkGPT, a non-interactive proof framework for LLM inference, points its optimizations at the same target. zkGPT: An Efficient Non-interactive Zero-knowledge Proof Framework for LLM Inference proposes “constraint fusion to reduce the overhead of proving non-linear layers and circuit squeeze to improve parallelism.” The non-linear layers are the named line item worth a dedicated optimization. And it pays: zkGPT “can prove GPT-2 inference in less than 25 seconds,” reporting “nearly 279x and 185x speedup” over two prior state-of-the-art systems, while the proof itself stays small at 101 KB. A two-orders-of-magnitude speedup that comes from handling the non-linear layers better — not from touching the parameter count — is exactly what you would expect if the cost lived in technique and layer-handling rather than in raw FLOPs. The small proof tells the same story: the heavy linear algebra compresses well, and the burden sits on the prover’s handling of the non-linearities.
A lookup table is not free, and the precise shape of its cost is the second half of the thesis. The size of the table is governed by the range of values the activation can take, and the range is governed by the bit-width — the precision — you assign to the activation. Wider range means more distinct values to tabulate means a bigger table means more prover work and a heavier argument. This is the mechanism by which “activations × bit-width” sets the bill, and the literature makes it literal.
Jolt Atlas spells out the dependence. Its neural-teleportation optimization shrinks the activation range to bound the table: with a teleportation factor of 4, “the effective input range shrinks by 4x, from [-R, R] to [-R/4, R/4], and the lookup table is bounded by 2^16 entries (sufficient for 16-bit fixed-point activations).” The paper is explicit that “the effective activation range after teleportation directly determines the required bit-width … the choice of tau implicitly controls the cost profile of the lookup argument.” The proof’s cost profile is controlled by a knob that does nothing but narrow the activation range. Not the matmul. The range of the activation.
Which functions need the biggest tables? The saturating ones. Jolt Atlas notes that “activation functions like erf (used in GELU) and tanh require lookup tables spanning the full input range, which increases the computational costs of both prover and verifier.” A clean ReLU is comparatively kind to a prover; a GELU or a tanh, with a curve that has to be tabulated across its whole domain, is not.
The Zhejiang group’s recursive-ZK framework confirms the precision dependence in a third independent design. Zero-Knowledge Proof Based Verifiable Inference of Models (arXiv 2511.19902) builds softmax and SiLU from a precomputed lookup table of length 2^l, where each entry is round(2^{-i/2^l} * 2^q) — a table whose length is two to the power of the fractional-bit count. The table size is exponential in the bit-width chosen for the activation. Three different systems, three different lookup constructions, one shared dependency: the precision you demand of the non-linearity is the dial that sets the proving cost.
If the per-layer split is real, it should show up as a fraction. TeleSparse, a ZK-friendly post-processing mechanism for deep networks, puts the single sharpest number on it. TeleSparse: Practical Privacy-Preserving Verification of Deep Neural Networks (arXiv 2504.19274) reports that “non-linear layers in models like ResNet-101 can consume up to 80% of the prover’s computational load due to extensive lookup table operations.” Up to 80% — on a convolutional network whose FLOPs are overwhelmingly in its convolutions and dense layers. Four-fifths of the prover’s work goes to the layers that hold almost none of the FLOPs.
TeleSparse traces that 80% to exactly the mechanism above. “Outlier values broaden the input range of activation functions, necessitating larger lookup tables,” the paper observes, and so it sets out to “identify symmetric neural network configurations that minimize the range of activation values, thereby reducing the size of the necessary lookup tables.” The tables themselves are named as the source of the prover’s pain — they “introduce considerable overhead, leading to slower proof generation, increased memory demands for the prover, and larger proof sizes.” Shrink the range and the pain recedes: TeleSparse “reduces prover memory usage by 67% and proof generation time by 46% on the same model,” with a concrete ResNet-20 on CIFAR-100 moving from 120.2 GB to 39.8 GB and from 564 seconds to 307 seconds, at an accuracy trade-off of roughly 1%.
Read those two numbers together and the thesis is hard to escape. A 46% time reduction and a 67% memory reduction, achieved by narrowing activation ranges and shrinking lookup tables — touching the non-linear handling and nothing about the parameter count — is the matmul-versus-activation split shown as a lever you can pull. The cost was in the activations; you remove it from the activations.
The same lever recurs across the systems for a reason: it is the only lever pointed at the dominant term. Jolt Atlas calls its version neural teleportation; TeleSparse calls its version neural teleportation too; zkGPT calls its constraint fusion. Different names, same target — the lookup-bound activation, narrowed to bound its table. This is also why folding schemes, which amortize a long repetitive computation step by step, are a complementary and not a competing optimization: folding attacks the cost of repetition across an autoregressive loop, while range-narrowing attacks the cost of the non-linearity within one step. A real system wants both, because they bite on different axes.
A thesis that survives only by ignoring the counter-evidence is not worth shipping, and there is a clean counter-example. The matmul-is-cheap claim is architecture-dependent, not universal — it is a claim about systems that pair a specialized matmul sumcheck with lookup-bound activations, and not every prover is built that way.
The Zhejiang recursive-ZK framework is the boundary case. Its design is recursively composed proofs with no trusted setup, supporting both linear and nonlinear layers, and in its measured breakdown the matrix-multiply component is the larger line item. Zero-Knowledge Proof Based Verifiable Inference of Models (arXiv 2511.19902) reports component proving times in which GeMM — the matrix multiplication — runs to roughly 204,138 seconds against softmax’s roughly 39,456 seconds. In that particular implementation the matrix operations dominate proving time, full stop. “Non-linearities always dominate” is therefore false as a universal law. It is true of systems that have already made their matmuls cheap with a dedicated sumcheck and are left with the activations as the residual; it is not true of a design whose matmul handling is itself the expensive part.
But notice what does not flip even at this boundary. The same paper still frames the non-arithmetic operations as the qualitatively hard part that transformers introduced, observing that “modern architectures rely extensively on nonlinear operations, which became central after the introduction of the transformer architecture in 2017.” The disagreement is about which term tops the wall clock in one specific recursive design, not about which class of operations is the awkward one to prove. Linear algebra has a known, efficient, structure-exploiting protocol; non-arithmetic operations do not, which is why every system here had to invent something — tlookup, constraint fusion, a teleportation pass, a precision-parameterized exponential table — to handle them. The qualitative claim is robust even where the quantitative ranking inverts.
So the honest statement is bounded, not absolute. Given a prover that exploits matmul structure with a dedicated sumcheck — the design the field is converging on — the residual cost concentrates in the activations and scales with their bit-width. If your prover has not made its matmuls cheap, the matmuls can still dominate. The intuition is not wrong about FLOPs; it is wrong about where an efficient prover spends its time.
The practical consequence is a reordering of the optimization budget that cuts against instinct.
If you are choosing a model to prove, the cheap axis is parameter count and the expensive axis is activation precision and the number of distinct non-linearities. A wider matrix is comparatively free; a higher-precision GELU is not. A network designed for cheap proving is not a small network — it is a network with narrow activation ranges, low-bit fixed-point activations, and a frugal palette of non-linearities, ideally the kind that tabulate cheaply rather than the saturating kind that need a table across the full range.
If you are choosing where to spend engineering effort on a prover, the answer is the lookup argument, not the matmul kernel. The matmul already has a sumcheck that beats recomputation; squeezing it further is a small return on a small term. The activations are the large term, and every published win here — the 46% and 67% from TeleSparse, the 17× Jolt Atlas reports for nanoGPT (about 14 seconds against ezkl’s about 237 seconds for a roughly 0.25M-parameter, 4-layer model), the two-orders-of-magnitude figures from zkGPT — came from attacking the non-arithmetic handling, not the arithmetic. The reason transformer proving moved from impossible toward merely expensive, as the first proven LLM describes, is precisely that the hard part was always the softmax and the layer norm — the parts the specialized arguments target.
And if you are scoping a system, do not budget by FLOPs. A FLOP count tells you what the forward pass costs to run; it says little about what it costs to prove, because the operations that dominate the FLOPs are the ones with the most efficient proof. Budget by activations and their bit-width — the number the prover actually pays.
The matmuls feel like they should be the bill because they are where the FLOPs are. They are not, in any prover worth using, because they are also where the cleanest protocol is: a dedicated sumcheck proves a matrix product faster than the product computes. The cost left over lives in the ReLU, the softmax, the GELU, the layer norm — the operations a finite field cannot speak, forced through a lookup table whose size grows with the precision you demand. Optimize the table, not the matmul, and you optimize the term that actually dominates.
A membership-inference attack that separates your book from a held-out one is usually reading the calendar, not the weights. A successful attack is not a sound proof — and the null it would need to test against cannot be sampled.
17 min →
Unlearning promises a model can forget specific data without a full retrain. What it delivers is output suppression: a small benign relearning set — or simply quantizing the model — brings the 'forgotten' knowledge back.
14 min →
The EU AI Act requires AI output to be marked in a robust, reliable way. A formal impossibility theorem says strong watermarking cannot exist. Five words in the statute carry the collision.
13 min →