Result-as-advice plus a single exponentiation table. The prover supplies the softmax output; each exp is one Lasso lookup, and the division is one range relation.

• The exponentials are proven against one precomputed table of all possible exp results — a single Lasso query per exponentiation, no simulation of $e^x$ in the field.
• The normalizing division is result-as-advice checked by one range relation. So softmax reduces to a batch of exp lookups plus one range check, not a bespoke shift-and-normalise protocol like zkLLM's zkAttn or DeepProve's log-sum-exp shift.
• Note the model caveat that colours the whole comparison — DeepProve alleges zkGPT's evaluated GPT-2 omits the causal attention mask (which zkGPT's paper does not state). If so, the softmax being proven is over unmasked scores.

zkAttn — the softmax proof DeepProve inherits. Shift each row so exp sums to 1, then decompose into base-b digits and run one tlookup per digit.

Exploit the shift-invariance property of Softmax to adjust each row of Z by a constant, represented as a vector ẑ, so that exp(Z − ẑ1⊤) sums to 1 row-wise.

zkLLM · §2, zkAttn

• Shift-invariance. Subtract a per-row $\hat z$ so $\exp(Z-\hat z\mathbf{1}^\top)$ sums to 1. The exp output is then the normalised probability. DeepProve's log-sum-exp shift is the same idea, generalised.
• Digit decomposition. Rather than one giant exp table, write $Z'$ in $K$ base-$b$ digits and use $\exp(-\sum_k b^k Z^{(k)}) = \prod_k \exp(-b^k Z^{(k)})$ — one small tlookup per digit. This is the memory win over listing all input-output pairs.
• $\hat z$ is never verified directly; instead the rowwise sums of $Y$ are checked to equal 1. DeepProve extends zkAttn to batch across heads and to allow real-valued, not power-of-two, scale factors.

zkLLM's protocol batched across heads — but the code corrects two paper-level framings: the shift Z is the log-sum-exp (not a max), and the normalisation check is a tolerant range check (not exact Quant(1.0)).

The main difference between our protocol and that of zkLLM is that their protocol only uses scaling factors of the form $2^k$ with $k \in \mathbb{Z}$ whereas we allow for $k \in \mathbb{R}$ to allow for smaller step sizes between table entries for the same table size.

DeepProve · Appendix B.7

• Z is not a max-subtraction stability shift. The committed witness is the quantised log-sum-exp: the row max plus $\log\sum_k e^{\text{scalar}\cdot(X-\max)}$. Subtracting it means the single exp lookup emits already-normalised probabilities — the normaliser is folded into the exponent, so no division is ever proven.
• Exponentiation is a lookup against a TableType::Exp whose domain is $[-(2^b)+1, 0]$ (the shifted input is always ≤ 0). A value ≤ the min maps to 0, which is also how the masked −∞ sentinel cleanly yields $e=0$.
• Row-sum well-formedness is a tolerant range check, not exact equality. The code emits offset + (Quant(1.0) + error_bound) − row_sum and range-checks it in the 16-bit ShiftCheck table, enforcing $|\text{row\_sum} - \mathrm{Quant}(1.0)| \le \text{error\_bound}$.
• The "real-valued scale factors vs zkLLM" advantage is half the story: the exp input scale is a general f32, but the output scale output_sf is deliberately a power of two (capped at 16 bits). The flexibility is on the input side.
• The SoftmaxProof bundles four LogUp proofs (exp, range, error/shift-check, zero) plus one sumcheck; it commits the shift tensor per row and has no weight commitments. Batched across heads, it is what makes multi-head attention tractable.

        let dim_maxes = input.clone().max_dim(-1);
        let log_sum_exp = (input.clone().sub(dim_maxes.clone())?)
            .float()
            .mul_scalar(scalar)
            .mask_fill(input_mask, f32::NEG_INFINITY)?
            .exp()
            .sum_dim(-1)
            .log();

Not "just a lookup" — the code has a dedicated 4-stage batched-sumcheck protocol. It decomposes softmax into a max-indicator, a two-sub-table exponentiation, a complementary-slackness clamp, and a reciprocal-multiply, and never proves a division.

Non-linear operations like Softmax cannot be expressed as polynomial relations. Jolt Atlas uses lookup arguments to verify these operations: the prover demonstrates that each input-output pair appears in a precomputed lookup table.

Jolt Atlas · §4

• The paper is terse; the code is not. SoftmaxLastAxisProver::prove drives four SoftmaxStage sumchecks: (1) reciprocal-multiply + exp-sum + range-check; (2) exp-mult + max-indicator + remainder checks + slackness; (3) two Shout exp lookups + range-checks; (4) the Shout one-hot provers.
• Exponentiation by two tiny tables. Using $e^{a+b}=e^a\!\cdot\!e^b$, the centered logit $z=\max_k-x$ is clamped to $z_c=\min(z, z_{bound}-1)$, split into digits $z_c=z_{hi}\!\cdot\!B+z_{lo}$, each a Shout lookup into lut_hi/lut_lo (~401 entries vs a flat ~65k table), recombined as $\exp_q=\lfloor \exp_{hi}\exp_{lo}/S\rfloor$ with a range-checked remainder.
• The max is pinned without a comparator. A MaxIndicator sumcheck forces $\max_k = x$ at the one-hot argmax; an operand link then reconstructs $x = \max_k - z_c - \mathrm{sat\_diff}$ so the non-negativity of $z_c$ (Shout table membership) and $\mathrm{sat\_diff}$ (range check) forces $\max_k \ge x$ everywhere.
• The clamp is made unique by a complementary-slackness sumcheck (input claim 0) proving $\mathrm{sat\_diff}\cdot(z_{bound}-1-z_c)=0$ — either the slack is zero or the clamp is saturated. A reusable pattern for any saturating quantized op.
• No division is proven. The three per-row scalars $\max_k$, $\exp\_sum_q$, $\mathrm{argmax}_k$ are sent as uncommitted transcript advice, and the verifier recomputes $\mathrm{inv\_sum}=\lfloor S^2/\exp\_sum_q\rfloor$ itself. Normalization is then $\exp_q\cdot\mathrm{inv\_sum}=\mathrm{softmax}_q\cdot S + R$.

//! The prover sends three auxiliary vectors (`max_k`, `exp_sum_q`, `argmax_k`) to the
//! verifier via the transcript. These let the verifier derive `inv_sum[k]` without a
//! committed polynomial, but they add O(F) field elements to the proof size.
//!
//! TODO(#218): Remove auxiliary vectors and derive them inside the protocol.

let max_k_eval = MultilinearPolynomial::from(self.max_k.clone()).evaluate(&r2_lead.r);
let z_hi_eval = accessor.get_advice(VirtualPoly::SoftmaxZHi).1;
let z_lo_eval = accessor.get_advice(VirtualPoly::SoftmaxZLo).1;
let z_c_eval = z_hi_eval * F::from_u64(lut.base) + z_lo_eval;
let sat_diff_eval = accessor.get_advice(VirtualPoly::SoftmaxSatDiff).1;
let x_r2 = max_k_eval - z_c_eval - sat_diff_eval;
let prover_x_r2 = accessor.get_nodeio(Target::Input(0)).1;
if prover_x_r2 != x_r2 {
    return Err(ProofVerifyError::InvalidOpeningProof(
        "Operand link failed: prover's X(r2) does not match max_k - z_c - sat_diff".to_string(),
    ));
}

Softmax is just another float circuit -- exponentiation and division evaluated in IEEE-754 inside the Boolean domain. No shift-invariance trick, no exp lookup table, no tolerant row-sum check, because none of those is needed once you have real floats.

• SoftMax is listed among the non-linear layers implemented directly (with ReLU, Sigmoid, Max Pooling and Batch Normalization). It inherits the generic path: convert to Boolean, convert to float, evaluate the circuit, convert back.
• The division is genuinely computed, not avoided. Every other system here contorts to eliminate the normaliser -- zkLLM and DeepProve subtract a per-row shift so the exponential emits already-normalised probabilities; Jolt Atlas has the verifier recompute a reciprocal. Mystique just does the division, in float, because in float division is a circuit like any other.
• This is the cleanest illustration of the paper's whole bet: the operator that costs the sum-check lineage its single largest prover slice is, here, unremarkable -- and the cost has moved to Batch Normalization and to the conversions instead.

A genuine softmax protocol, and it independently reinvents the shift: subtract the row max (via the maxpool protocol), exponentiate by digit-decomposed lookup, then divide -- with the input range bound exploited to make the division narrow.

• $\Pi_{\mathrm{Softmax}}$ first invokes $\Pi_{\mathrm{Maxpool}}$ to obtain $x_{\max}$, then computes $e^{x_i - x_{\max}}$ by the digit-decomposed exponential, sums, and divides. Subtracting the max is exactly zkLLM's and DeepProve's shift-invariance move, and for exactly the same reason: it bounds the exponent's range so the table can be small.
• The division is then made cheap by a range argument rather than by elimination: the summed input is bounded by $n$, so the divisor's bitlength is only $s + \lceil\log n\rceil$. The paper notes that for $n = 256$ and $s = 12$ this means dividing on just 20 bits.
• Unlike DeepProve, the normaliser is not folded into the exponent -- a real division is proven, using the division building block. That building block runs with zero refinement iterations by default, which is where softmax's accuracy risk actually lives.
• Softmax is the operator where the improvement over Mystique is largest, which is unsurprising: it is the one that most punished Mystique's arithmetic-to-Boolean round trip, needing exponentiation and division in a Boolean circuit.