Argmax / greedy decode
and the sampling problem
The algorithm
Pick the highest-scoring token. This is what makes inference deterministic, and therefore what makes the certification algorithm sound.
Why it resists a proof
$\max$ is a comparison, not arithmetic. Proving "this is the largest" requires both a range argument (nothing exceeds it) and an existence argument (something equals it). And if the model samples instead, the whole soundness statement evaporates.
Cryptographic toolbox
- Lookup range check for non-negativity
- Grand-product GKR circuit for the zero-existence check
- Claim-linking: f_D(r₁,r₂) = f_m(r₂) − f_X(r₁,r₂)
- De-randomization for top-k sampling
How each scheme proves it
Split max into 'upper bound' plus 'attained', and prove the second with a grand product.
In practice, this is not a limitation since any randomized algorithm can be "de-randomized" by providing a single purely random seed as additional input. […] The main challenge comes from actually showing that the initial random seed has been sampled correctly. […] We note that we do not include this in our implementation, same as all prior works on verifiable LLM inference.
DeepProve · §4.3.6
- The prover computes $D[i,j] = m[i]-X[i,j]$ and runs a lookup range PIOP to show $D \ge 0$ everywhere.
- Then a specialised GKR grand-product circuit shows $\prod_j D[i,j] = 0$ for each row — the max is actually achieved.
- $D$ is linked back to the committed $m$ and $X$ by $\tilde f_D(r_1,r_2) = \tilde f_m(r_2) - \tilde f_X(r_1,r_2)$, checked at both random points the two subprotocols produce.
- Sampling. If decoding is stochastic, de-randomize: take the seed as public input and prove the decode stage against it. Proving the seed was honestly sampled needs a randomness beacon or an interactive coin flip. Not implemented — nor in any prior work.