Proving inference · Operator atlas · Absolute positional encoding
Absolute positional encoding
GPT-2
$$Y = X + W[1:s], \qquad W\in\mathbb{F}^{s'\times d},\quad s\le s'
\\[8pt]
\text{problem: the verifier's random point } r\in\mathbb{F}^{\log(sd)} \text{ doesn't "fit" the MLE of the taller } W.$$
The algorithm
Add a learned position matrix, row-truncated to the actual sequence length.
Why it resists a proof
Only a shape mismatch: the committed $W$ has $s'$ rows (max context) but you need its first $s$. You cannot just evaluate $\tilde f_W$ at $r$.
Cryptographic toolbox
- Prefix-restriction of an MLE by zero-padding the challenge point
How each scheme proves it
Evaluate the truncated W by prepending zeros to the challenge point.
- Observe $\tilde f_{W,\le s}(x) = \tilde f_W(\mathbf{0}\,\|\,x)$ with $\mathbf{0}\in\mathbb{F}^{\log(s'/s)}$. The prover sends $y_W = \tilde f_W(\mathbf{0}\|r)$ and the verifier queries the existing oracle there.
- Whole protocol: verifier samples $r$, prover sends three evaluations, verifier checks $y_Y = y_X + y_W$. $O(1)$ proof and verification; soundness error $3\log(sd)/|\mathbb{F}|$.
GPT-2's learned absolute encoding is not a bespoke op in Jolt — it decomposes into a Gather of the position table plus an Add, both already proven.
- GPT-2 (nanoGPT, the repo's actual target) uses learned position embeddings, so APE =
Gather(position table) +Add. Both have dedicated protocols above; there is nothing new to prove. - Sinusoidal APE would instead route through the
sin/cosneural-teleport path — but no sinusoidal-APE model ships in the repo.