GeLU is exp and division, so it is result-as-advice — a Lasso exp lookup plus range relations, with no polynomial approximation.

• GeLU decomposes into the ZKP-unfriendly trio (division, square root, exponentiation) that zkGPT handles uniformly: supply the result as advice, verify exp with a Lasso table and div/sqrt with a single range relation each.
• Contrast the philosophies. zkGPT proves the exact activation via advice + lookup; Jolt Atlas shrinks the table with lossy teleportation; DeepProve fuses the activation table into the preceding requantization. Same wall (a table must be addressable), three different moves.

Activations are tlookups. GeLU, ReLU, SwiGLU: build a two-column table (x, f(x)) and prove the input-output pairs lie in it with one tlookup.

• For elementwise $f: X\to Y$, build tables $T_X$ and $T_Y$. A random linear combination reduces "$Y=f(X)$" to one set-inclusion check $X+\alpha Y \subseteq T_X + \alpha T_Y$.
• Same primitive as the rest of zkLLM. DeepProve fuses the activation table into the preceding requantization; zkLLM keeps them separate.

Fuse GeLU into the preceding requantization: swap the range-check table for a GeLU table and adjust the recombination function's edge cases.

If a non-linear layer is followed after a linear one, then, instead of adding a separate and explicit requantization layer we can merge both the requantization and the non-linear layer operation as a unified layer. […] This not only reduces the proving time and proof size but also increases the accuracy since the nonlinear layer now takes the unclamped output of the linear layer as its input.

DeepProve · Appendix B.2

• Case 1 — input already $q$-bit. A plain lookup PIOP against $T_{\mathrm{GeLU}}$.
• Case 2 — input is $q'$-bit or wider. Run the requantization lookup argument, but replace table $T_{q'/q}$ with $T_{\mathrm{GeLU}}$, and replace the clamped edge values of $\mathrm{Comb}_y$ with $\mathrm{Quant}(\mathrm{DeQuant}(\pm 2^{q-1})\cdot \mathbb{P}[X \le \mathrm{DeQuant}(\pm 2^{q-1})])$.
• This is operator fusion: one lookup argument instead of two. Smaller proof, faster prover, and higher accuracy, because GeLU now sees the unclamped, un-rounded linear output.
• The same construction covers any tabulatable elementwise non-linearity: SiLU, GeGLU, tanh soft-capping.

Neural teleportation, in code: divide the input by τ into a prover-supplied quotient+remainder, then a single Read-RAF sumcheck proves output=Table[idx] AND idx=signed(quotient) at once. But the input clamp is where a real gap lives.

Jolt Atlas therefore uses a global, one-sided approximation: every pre-activation input to a selected activation is divided by a single factor τ > 1, with no compensating output multiplication and no weight rescaling. Concretely, the original computation y = σ(x) is replaced by y′ = σ(x/τ), which is a lossy approximation (i.e., y′ ≠ y in general) but it is not significant in practice.

Jolt Atlas · §4.2

With τ = 4, the effective input range shrinks by 4×, from [−R, R] to [−R/4, R/4], and the lookup table is bounded by $2^{16}$ entries. Empirical evaluation shows that τ = 4 introduces output differences of less than 55 units on a 128-scale fixed-point representation, acceptable for most inference tasks.

Jolt Atlas · §4.2

• Prefix-suffix decomposition. A table on two 64-bit inputs would need $2^{128}$ entries. Partition the input bits into $C$ segments of width $b$; for decomposable tables the MLE factors as $\tilde T(x) = \sum_i \prod_{j=1}^{C} s_{i,j}(x^{(j)})$, reducing table size from $2^{Cb}$ to $O(C\cdot 2^b)$.
• Worked example for ReLU: $\mathrm{ReLU}(x)=(1-b_0)\cdot x$ is determined entirely by the sign bit, so it splits into $p_{\mathrm{ReLU}}(x_{hi})s_{\mathrm{One}}(x_{lo}) + p_{\mathrm{NotMSB}}(x_{hi})s_{\mathrm{ReLU}}(x_{lo})$.
• Neural teleportation (adapted from TeleSparse). Replace $y=\sigma(x)$ with $y'=\sigma(x/\tau)$, a global one-sided transform with no compensating output multiplication and no weight rescaling — so no re-committing to modified weights.
• Why it works: saturating activations like $\mathrm{erf}$ and $\tanh$ spend most of their range in flat regions where $\sigma(x)\approx\pm 1$. For any input already saturated, $\sigma(x/\tau)=\sigma(x)$ exactly. Error concentrates in the narrow linear region near the origin.
• With $\tau = 4$ the effective input range shrinks 4×, bounding the table at $2^{16}$ entries, and introducing output differences of <55 units on a 128-scale fixed-point representation. It is lossy — unlike TeleSparse's two-sided form, which is exact.

// TODO: rm once clamp is implemented for tanh
provider.append_advice(VirtualPoly::DummyClampedTanhInput, clamped_eval);

// TODO: Pass these input in a clamping lookup table ...
assert!(clamped_tensor.iter().all(|&x| {
    let lower_bound = -(1 << (params.op.log_table - 1));
    let upper_bound = (1 << (params.op.log_table - 1)) - 1;
    x >= lower_bound && x <= upper_bound
}));

Not GeLU, and not a lookup: Mystique implements ReLU and Sigmoid (plus Max Pooling) as IEEE-754 single-precision floating-point Boolean circuits. The activation is computed exactly; you pay at the conversion boundary instead of in a table.

• The recipe is representation, not approximation. An arithmetic-to-Boolean conversion (zk-edaBits) followed by a Fix2Float conversion puts the value in a real IEEE-754 float, where the activation is evaluated by the standard single-precision circuits from EMP. Any elementwise nonlinearity -- ReLU, Sigmoid, and by the same recipe GeLU or tanh -- costs the same shape of circuit.
• No table, therefore no table domain, therefore no clamping and no range reduction. The entire problem that prefix-suffix decomposition and neural teleportation exist to solve simply does not arise: there is nothing whose domain has to stay addressable.
• The price is the conversion. Fix2Float and Float2Fix rest on private logical shifts, and the paper notes fixed-to-float is about 3x slower than float-to-fixed because the shift widths differ -- fixed by IEEE-754's 24-bit significand on one side and the 61-bit field on the other.
• The accuracy consequence is the point of the design: because the nonlinearity sees a true float, error does not compound through depth, which is what lets Mystique run 101 layers with a reported accuracy delta of 0.02% on CIFAR-10.

A real GeLU protocol, and the one operator here explicitly aimed at LLMs. GeLU is reduced to Tanh, Tanh to Sigmoid, and Sigmoid to digit-decomposed exponential and division -- all by table lookup, all inside the field.

GELU activation is used in LLMs.

Hao et al. · §5

• The reduction chain is explicit: $\mathrm{GELU}(x) = 0.5\,x\,[1 + \mathrm{Tanh}(\sqrt{2/\pi}\,x + 0.044715\,x^3)]$ with $\mathrm{Tanh}(x) := 2\cdot\mathrm{Sigmoid}(2x) - 1$, so the GeLU proof is an invocation of the Sigmoid proof.
• Sigmoid in turn rests on the exponential protocol, which decomposes the exponent into digits and uses $e^{-\sum_k 2^{d_k} x_k} = \prod_k e^{-2^{d_k} x_k}$ -- one small table per digit, products recombined with a truncation after each step. This is precisely zkLLM's zkAttn digit trick, independently rediscovered on a VOLE substrate.
• The comparison against Mystique is the paper's headline for this operator, and it is a fair one: they re-ran Mystique's own EMP implementation under identical network and hardware conditions rather than citing its printed numbers.
• But the approximation parameters are set to the cheapest setting and never validated. Division runs with $I = 0$ refinement iterations and reciprocal square root with $I = 1$, following prior work -- and no accuracy consequence is reported for GeLU, or for any function.