Technical detail

The design has four parts ¹:

• tlookup is a parallel lookup argument for non-arithmetic tensor operations. The authors state it adds no asymptotic overhead in memory or running time (§4).
• zkAttn proves softmax attention by splitting the exponentiation into K segments, each checked with tlookup (§5).
• The commitments use Hyrax, a Pedersen variant, over BLS12-381 under discrete-log hardness (§3).
• Tensors are scaled by 2^16 and rounded into the field. The resulting total L1 error on the output is about 10^-2 (§7–8).

The paper's security analysis is in §7.2 ¹:

• Theorems 7.2 and 7.3 give tlookup a completeness error of O(N/|F|). They show that a cheating probabilistic polynomial-time prover succeeds only with negligible probability. The rest of the protocol applies the sumcheck protocol and proofs of opening for committed tensors.
• Theorem 7.4 covers zero knowledge. It states that a simulator with only oracle access to the output produces a view indistinguishable from the real one. The theorem assumes zero-knowledge variants of sumcheck and Pedersen commitments. The threat model assumes a semi-honest verifier (§3.6).

Table 1 reports these costs on an A100 40 GB GPU at sequence length 2,048 ¹:

• OPT-13B took 1,270 s to commit and 713 s to prove. The proof was 160 kB, verified in 3.71 s and used 22.9 GB of memory.
• LLaMa-2-13B took 986 s to commit and 803 s to prove. The proof was 188 kB, verified in 3.95 s and used 23.1 GB of memory.

The public code covers LLaMa-2 7B and 13B, runs prover and verifier side by side, and is interactive ².