16-bit affine quantization inherited from zkCNN — the clearest-documented quantization in the LLM-proving literature, and the one DeepProve measures itself against.

• Affine, per-layer/per-tensor scale and zero-point, all parameters and intermediates as Q-bit integers with q ∈ [0, 65536] (16-bit). It states its bit width, its scheme, and its accuracy cost — the reference point when normalizing everyone else.
• The 16-bit choice is on the high end. Lower precision is cheaper on the range-check and lookup side, so part of the gap between zkGPT and, say, DeepProve's 12-bit is quantization, not just protocol.
• Fixed scale factors, powers of two — the restriction DeepProve contrasts against (it allows real-valued scales). Combined with the alleged model relaxations, this is the accuracy-versus-speed trade the debate turns on.

Fixed-point discretization into the field via scaling factors, rescaled around each product. Documented but not the focus; C4 perplexity moves <0.01 at 13B.

the increase of perplexity is less than 0.1, and the impact diminishes to less than 0.01 as the sizes of the models scale to 13B.

zkLLM · §8, Evaluation

• Tensors are scaled and rounded into $\mathbb{F}$; products carry scaling factors that must be rescaled. No calibration study or bit-width sweep — the accuracy claim is the measured perplexity delta.
• Quantization error is bounded to about $10^{-2}$ L1 on the attention output, comparable to half-precision float rounding.

Standard symmetric affine PTQ — with one correction from the code: the outlier smoothing is DuQuant (Hadamard rotations), not generic orthonormal matrices, and the default width is 12-bit, not 8.

Deep learning practitioners already quantize model weights for reduced memory footprint and faster inference, but typically keep activations in floating-point format during the inference to mitigate lossiness due to quantization and accuracy degradation. However, to cryptographically prove the correctness of inference, both weights and activations must be in integers as well as all operations between them. Therefore, an accurate integer-only inference algorithm is necessary for efficient proof generation.

DeepProve · §1.1

• The ScalingFactor stores {min, max, scale, quantized_domain} and sets scale = (max−min)/(domain span). For a symmetric domain that is $2a/(2^b-1)$ — the integer domain is the asymmetric $[-2^{b-1}, 2^{b-1}-1]$, so the denominator is $2^b-1$, not the $2^{b-1}-1$ our old page (following the paper) printed.
• The requant multiplier is m() = S₁·S₂/S₃ (three scale factors), and the right-shift is shift() = ⌈−log₂ m⌉. Bit-width defaults to 12 (env ZKML_BIT_LEN), not 8; special LLM nodes override it (embeddings 23-bit, residual Add up to 24-bit).
• The calibration statistic is selectable — MinMax, Quantiles(p,q), or NSigmas(n) — and LLM inputs specifically use NSigmas(2) (mean ± 2σ), not raw min/max.
• Outlier smoothing is DuQuant. The rotation is not a generic orthonormal matrix — it is a Hadamard matrix built by the Sylvester recursion (every source file cites arXiv 2406.01721). It is model-specific: Gemma 3's extra RMSNorms block free absorption, so gemma3.rs chases the scale into dedicated scaling-EinSum rotation steps that gpt2.rs does not need.
• Accuracy is nearly free: 12-bit gives GPT-2 perplexity 49.49 vs a 49.22 float baseline (0.54% off); going 8→12 bits costs only 0.8% extra prover time, because the lookup table count barely changes.

    /// M = S1 * S2 / S3
    pub fn m(&self, s2: &Self, s3: &Self) -> f32 {
        self.scale() * s2.scale() / s3.scale()
    }

    /// M = S1 * S2 / S3 = 2^-n * eps ; n is the number of bits to shift right
    pub fn shift(&self, s2: &Self, s3: &Self) -> usize {
        (-self.m(s2, s3).log2()).ceil() as usize
    }

/// Generates a Hadamard matrix of size 2^k that has not been normalised.
pub fn get_hadamard_matrix_no_normalisation(k: usize) -> Result<Tensor<f32>> {
    ensure!(k >= 1, "k must be at least 1, got {}", k);
    if k == 1 {
        let data = vec![1.0f32, 1.0f32, 1.0f32, -1.0f32];
        Tensor::<f32>::new(vec![2, 2].into(), data)
    } else {
        let prev_hadamard = get_hadamard_matrix_no_normalisation(k - 1)?.into_data();

The paper is vague, but the code is concrete and rigid: power-of-two symmetric fixed-point over i32, no zero-point, no clamp on quantize — it panics on overflow rather than saturating.

• quantize_float(x, scale) is pure fixed-point: round(x · 2^scale) stored as i32, dequantized as fixed / 2^scale. The scale is always a power of two and the zero-point vanishes — exactly the restriction DeepProve contrasts itself against (it allows real-valued scales for finer table steps).
• There is no clamp in quantization: quantize_tensor panics if an element exceeds $\pm\,\texttt{i32::MAX}/2^{scale}$. Range control happens later, at the lookup boundary, via fused rebase and teleportation — not here.
• The same file derives the causal-mask sentinel (⌈(scale+1)·ln2⌉+1, giving -45056 at scale 12), tying quantization directly to how masking is represented.
• What is still absent — and this is the real gap — is any calibration procedure or model-level accuracy evaluation. DeepProve's own conclusion is that quantization nuances determine whether a reported accuracy number survives an end-to-end trace, and Jolt Atlas reports none.

Fixed-point in the field for linear layers only. Every non-linear layer converts out to IEEE-754 single-precision float, so quantization error never reaches a nonlinearity -- and there is no calibration story because there does not need to be one.

• A signed fixed-point $x$ at precision $s$ is encoded as $\mathrm{Encode}(\lfloor 2^s\cdot x\rfloor)$ over the Mersenne prime $p = 2^{61}-1$, negatives mapping to the top of the field. Fixed-point addition and multiplication are then just field addition and multiplication.
• The implementation fixes $s = 16$ and confines values to a 30-bit range, deliberately leaving slack. Matrix multiplication has multiplication depth 1, so a product cannot overflow the field before the next conversion pulls it back out.
• There is no calibration set, no bit-width sweep, and no outlier smoothing. The values that would wreck a quantization grid -- the ones DuQuant rotations and clamping exist to tame -- are handled in float, not in the field.
• This is the road DeepProve and Jolt Atlas did not take. Their requantization, clamping and lookup-domain machinery all exists to keep activations inside an integer grid. Mystique pays a representation conversion instead, and keeps the grid out of the nonlinearity entirely.

Fixed-point over the same 61-bit Mersenne prime as Mystique, at a default scale of 12 -- but here the fixed-point digits are the table addresses, so the precision choice and the lookup cost model are the same knob.

• Values are fixed-point over $p = 2^{61}-1$ with scale $s$ (default 12), $\lambda = 128$, $\rho \ge 40$ -- inherited wholesale from Mystique so the comparison is like-for-like.
• Digit decomposition is the substrate. A wide input is split into a constant number of digits of 5-12 bits, each of which addresses its own small table. A faithful table over the full field would need about $2^{61}$ entries; a 12-bit digit needs $2^{12}$.
• The scale is therefore not a free parameter: it is the truncation bitlength, and the paper reports a step change in runtime once the scale crosses 12, because a second lookup table is then required.
• No calibration procedure and no accuracy evaluation. Unlike Mystique -- which chose float circuits precisely to protect accuracy through depth -- this design puts the nonlinearity back into fixed point and never measures what that costs, on any model.