Proving inference · Operator atlas · Residual addition

Residual addition

x + sublayer(x)

$$Y = X_1 + X_2 \\[8pt] \text{but quantized, both addends must share a scale } s. \\[4pt] X_1 \text{ is a raw hidden state; } X_2 \text{ left a normalized block.} \\[2pt] \text{Their dynamic ranges differ by orders of magnitude.}$$

The algorithm

Add the block's output back to its input. Mathematically the simplest node in the graph.

Why it resists a proof

In quantized-land it is a trap. Rescaling the narrow-range tensor onto the wide-range tensor's grid at low precision destroys it. Residual connections are also a primary source of the outlier activations that break quantization globally. zkGPT's evaluation simply deletes them from GPT-2.

Cryptographic toolbox

  • Mixed precision: widen the bit-length locally
  • Scale-factor alignment before addition
  • Free in the PIOP: MLE addition checked at a random point

How each scheme proves it

DeepProve

Prove it for free; pay for it in bits, not in cryptography.

The authors prove the correctness of a modified version of GPT-2 that doesn't contain residual connections, attention masks, and the final projection layer. These relaxations significantly circumvent the outlier issues that we discussed in Section 1.

DeepProve · §6
  • The PIOP is a one-line check: sample $r$, verify $y_Y = y_{X_1} + y_{X_2}$ against the three oracles.
  • The engineering is entirely numeric: residual layers run at a larger bit-length than the rest of the model, chosen so the quantization grid is fine enough to represent both addends.
  • DeepProve keeps residuals, attention masks, and the final projection. zkGPT removes all three, which is how it avoids the outlier problem it never discusses.
Add: 1.03% of PIOP time.
Jolt Atlas

An elementwise Add over tensors, with NumPy broadcast semantics. Nothing to say, and nothing said.

  • Add, Sub, Mul, Div are supported elementwise ops; broadcasting is automatic.
  • Not "nothing said" in code. Each is a small degree-1/2/3 sumcheck whose 64-bit pre-clamp accumulation is re-executed into a ClampAcc virtual MLE (never committed), tied to the committed operands by a cheap linear equality, then clamped by the shared SatClamp lookup. Div proves the Euclidean identity right·q + R − left = 0 with a committed quotient and an UnsignedLessThan-range-checked remainder.
Audit surface

The pre-clamp acc is prover-supplied advice (re-executed, appended as ClampAcc, no separate commitment); its only anchors are the operand tie and the clamp lookup. The soundness-test harness (malicious_sub.rs) is worth teaching: a faithful attacker forges exactly one opening (proves left+1) to isolate which single check rejects — here, the operand tie. In ZK mode, Add/Sub/Sum are proved un-clamped and deliberately don't commit ClampRaD, so their saturating clamp is not range-checked under ZK.

← previousEmbedding lookup