Operator atlas — zkAI

Proving inference · Operator atlas

Operator atlas

Every algorithm inside an LLM forward pass that a zkSNARK must prove, and how each proving scheme handles it. Matmul is not the bottleneck; the nonlinearities are.

Operator	zkGPT	zkLLM	DeepProve	Jolt Atlas	Mystique	Hao et al.
QuantizationNumeric substrate	●	●	●	●	●	●
RequantizationNumeric substrate	●	○	●	●	○	●
ClampingNumeric substrate	○	○	●	●	○	○
Matrix multiplicationLinear algebra	●	●	●	●	●	○
Embedding lookupLinear algebra	○	○	●	●	○	○
Residual additionLinear algebra	○	○	●	●	○	○
Absolute positional encodingPositional information	○	○	●	●	○	○
Rotary positional embeddingPositional information	○	○	●	●	○	○
Attention scoresAttention	○	●	●	●	○	○
Causal maskingAttention	○	○	●	●	○	○
SoftmaxAttention	●	●	●	●	●	●
Multi-head attentionAttention	○	●	●	●	○	○
RMSNormNormalization & activation	●	○	●	●	○	○
LayerNormNormalization & activation	○	○	●	●	○	●
GeLU activationNormalization & activation	●	●	●	●	●	●
Unembedding → logitsOutput & decoding	○	○	●	●	○	○
Argmax / greedy decodeOutput & decoding	○	○	●	○	○	○
Autoregression & certificationOutput & decoding	○	○	●	●	○	○
Memory & read consistencySystems-level obligations	○	○	●	●	○	○
Zero-knowledgeSystems-level obligations	●	●	○	●	●	●
The memory wallSystems-level obligations	○	●	●	●	●	○
Proof of non-hallucinationSystems-level obligations	○	○	●	○	○	○
The sumcheck protocolCryptographic machinery	●	●	●	○	○	○
Lookup arguments & range checksCryptographic machinery	●	●	●	○	○	●
Claims & the backward passCryptographic machinery	○	○	●	○	○	○
Model transforms & fusionCryptographic machinery	○	○	●	○	○	○

● = the paper describes a protocol for this operator. ○ = it does not. An empty column is not a criticism — most systems are explicit about their scope — but an empty row is a gap in the field.

Numeric substrate

Accuracy-critical

Quantization

float32 → q-bit signed integer

6 schemes address it

DeepProve's #1 cost

Requantization

rescale · round · shift · clamp

4 schemes address it

Table-size sensitive

Clamping

saturating out-of-range activations

2 schemes address it

Linear algebra

SNARK-friendly

Matrix multiplication

QKV projections, FFN, logits

5 schemes address it

Cheap if you're clever

Embedding lookup

token id → vector · ONNX Gather

2 schemes address it

Trivial — except for scales

Residual addition

x + sublayer(x)

2 schemes address it

Positional information

Nearly free

Absolute positional encoding

GPT-2

2 schemes address it

Needs a structural trick

Rotary positional embedding

Gemma 3, Llama, most modern LLMs

2 schemes address it

Attention

A matmul in disguise

Attention scores

Q·Kᵀ / √dₖ

3 schemes address it

O(s), not O(s²)

Causal masking

the −∞ upper triangle

2 schemes address it

DeepProve's #2 cost

Softmax

the exponential problem

6 schemes address it

Composition + padding pain

Multi-head attention

and GQA for Gemma 3

3 schemes address it

Normalization & activation

Square roots and inverses

RMSNorm

Gemma 3, Llama

3 schemes address it

A separate layer (keeps ε)

LayerNorm

GPT-2

3 schemes address it

DeepProve's #3 cost

GeLU activation

and Erf, Tanh, SiLU by the same recipe

6 schemes address it

Output & decoding

A matmul, then an argmax

Unembedding → logits

h · Wᵀ over the vocabulary

2 schemes address it

Two checks, one grand product

Argmax / greedy decode

and the sampling problem

1 schemes address it

DeepProve's best idea

Autoregression & certification

KV caching, sequence certification — the trick that kills the quadratic

2 schemes address it

Systems-level obligations

Or: avoid it entirely

Memory & read consistency

KV cache, tensor reads — what a read owes you

2 schemes address it

Usually not implemented

Zero-knowledge

hiding the weights and the prompt

5 schemes address it

The real binding constraint

The memory wall

scale out, or scale down

4 schemes address it

Nearly free

Proof of non-hallucination

an unexpected freebie

1 schemes address it

Cryptographic machinery

Foundational

The sumcheck protocol

the workhorse under every page

3 schemes address it

Foundational

Lookup arguments & range checks

how non-linearity is discharged

4 schemes address it

Foundational

Claims & the backward pass

how operators compose into one proof

1 schemes address it

Foundational

Model transforms & fusion

the graph rewrite before proving

1 schemes address it