The flagship of constraint fusion. Where prior work spends three range relations proving a normalization, zkGPT algebraically merges them into one.

• Same starting move as DeepProve — the square root and reciprocal are proven by result-as-advice, supplying qσ as a witness and checking it with a single range relation instead of an arithmetic square root. This alone turns Hao et al.'s >4000 s of norm proving into <30 s.
• Constraint fusion goes further. Proving σ naively needs three rounded quantities (mean, then variance, then √), each costing a range relation. zkGPT substitutes the mean and variance analytically into the final constraint, collapsing to one range relation: $n(2q_\sigma-1)^2 \le \sum_i(nq_{x_i}-\sum_j q_{x_j})^2 < n(2q_\sigma+1)^2$.
• Range relations are zkGPT's stated bottleneck (costlier than arithmetic relations), and fusion preserves the original precision, so this is pure win. Automatic rules pick the optimal merge per layer.

Never prove a square root. Guess the inverse norm, multiply by it, and prove the result is normalized.

The "standard" approach of proving the above, which was also adopted by all prior works, is to first construct a circuit that directly computes the RMSNorm layer and subsequently invoke a PIOP for proving the correct computation of that circuit. Unfortunately, this approach not only incurs significant prover overheads since it contains many "SNARK-unfriendly" operations such as square roots and inverses, but also leads to a significant accuracy loss.

DeepProve · §4.3.3

Proving norms is challenging because small errors accumulate during the sum on the variance and expected value. This, in turn, drastically reduces the accuracy.

DeepProve · Appendix C

• The idea is the paper's: never prove a square root. Supply the inverse norm as a witness, multiply by it, and prove the result is normalized. But three details from the code correct our old page.
• The witness is not $\mathrm{Quant}(1/\mathrm{rms})$. It is a per-row fixed-point multiplier fract_mul (the mantissa of $nws=\sqrt{\text{target}/\sum x^2}$) plus a single shared right-shift, and ε is deliberately dropped — the factor targets the centre of the check-table range, not the true $1/\sqrt{\mathrm{mean}(x^2)+\epsilon}$.
• Applying it is not a bare $Y=X\cdot d$. It is multiply → add rounding constant → shared right-shift → clamping table lookup. The lookup handles clamping internally.
• Well-formedness is not a separate "Phase 2." The normalized-output bound is carried as parameters of a single LookupVariant::Normalisation, verified inside one LogUp argument — not a second proof phase. The verifier recomputes the target sum-of-squares and error bound from public context.
• Appendix C's error bound still holds in spirit: $\sum_j Y[i,j]^2$ must land within error_bound of the target, so the output really is normalized up to a bound set by the output scale.

        // Apply the fixed point multipliers, rounding and right shift
        let rescaled_input = input
            .mul(self.normalisation.clone())?
            .add_scalar(self.rounding_constant())
            .bitwise_right_shift_scalar(self.right_shift() as Element);
        // Perform the lookup, the table will handle clamping internally
        table.lookup_tensor(rescaled_input)

Rsqrt is a first-class ONNX op, proven by lookup. The rounding-error accumulation DeepProve engineers around is not analysed.

• Rsqrt (reciprocal square root) appears directly in the supported "Math Functions" set, so the whole normalisation is Mul ∘ Rsqrt ∘ Div ∘ ReduceSum of squares.
• This is precisely the "standard approach" DeepProve rejects — quantizing the inverse square root introduces rounding error at each row, of each layer, and the errors accumulate through the variance sum.
• Whether that matters for Jolt Atlas depends on its fixed-point precision, which the paper does not report. With 16-bit activations it may well be fine; with 8-bit it would not be.