Proving inference · Operator atlas · Attention scores
Attention scores
Q·Kᵀ / √dₖ
$$T_p = Q\cdot K^\top, \qquad\text{then scale by } 1/\sqrt{d_k}
\\[8pt]
\text{the scale is absorbed into the claim:}\qquad y_{T_p} \leftarrow y_{T_p}\cdot \mathrm{Quant}(1/\sqrt{d_k})^{-1}$$
The algorithm
The $s\times s$ score matrix, before masking and softmax.
Why it resists a proof
Nothing special — a matmul with a transposed operand and a scalar. The transpose is handled by permuting the challenge point rather than materialising $K^\top$.
Cryptographic toolbox
- Batched matmul sumcheck
- Challenge-point permutation for the transpose
- Scalar folding into the evaluation claim
How each scheme proves it
Q·Kᵀ is step 1 of zkAttn: a dedicated matmul sumcheck. Nothing separate.
- The score matrix $Z = QK^\top$ is proven by the tensor matmul sumcheck, then fed straight into the digit-decomposition softmax (zkAttn). Scaling by $1/\sqrt{d}$ is folded into the quantization scale factor.
Batched matmul; the transpose costs nothing.
- Given $r_{K^\top}=(r_1,r_2)$, set $y_K = y_{K^\top}$ and $r_K = (r_2,r_1)$. Free.
- The $1/\sqrt{d_k}$ scaling is undone on the verifier's evaluation claim before entering the matmul PIOP, rather than proven as its own layer.
An Einsum with an attention contraction pattern — and in code that reuse is the point: Q·Kᵀ runs the same folding engine as a feed-forward matmul, so there is no bespoke scores protocol to give.
- Einsum explicitly "supports patterns like
mk,kn->mn,bmk,bkn->bmn, and attention patterns". - In code,
Q·Kᵀis literally the sameeinsum/dot.rsengine as a feed-forward matmul — the attention contraction is one moreEqSchedule, not a bespoke protocol. The transpose is a choice offoldaxes; the $1/\sqrt{d_k}$ scale rides the fused-rebase seam.