An interactive proof for matmul chains

Checkpoint: CP-017 · Status: COMPLETE, run 2026-09-02 Question: can a sumcheck protocol remove the bandwidth cost that E016 found dominates everything?

Answer: yes for matmul chains, no for our transformer

A two-layer chain, verified without the verifier ever receiving the intermediate:

Communication grows logarithmically while the data it replaces grows quadratically, so the advantage improves with scale. Honest runs accepted, corruptions rejected, soundness 2.3 × 10⁻¹⁸.

Applied to the E015 transformer layer, the saving is zero. All three matmul outputs — 49.1 MB, exactly E016's figure — feed lookup-table non-linearities that the verifier checks by recomputation, so it needs the values anyway. The chain breaks at the first non-linearity, and there is one after every matmul.

The tension this exposes

NC-9 makes non-linearities lookup tables, because a gather has no arithmetic and so cannot diverge between backends. That is what made E015 and E018 bit-exact.

A sumcheck only passes through low-degree arithmetic. A lookup table is not.

The property that gives us cross-backend determinism is the property that blocks the interactive proof.

It also explains SafetyNets' restriction to quadratic activations, which had looked like an arbitrary 2017 compromise. y = x² is arithmetic, so the chain passes through it. They changed the model because the protocol demanded it — and paid for it in accuracy.

Files

Raw records: ../../benchmarks/results/019-interactive-proof.jsonl

Two implementation bugs worth knowing about

Both produced silently wrong results rather than errors:

1. Dot products overflowed int64. With residues near 2^31 a single product already fills int64, so a sum of any length is wrong. dotmod now reduces every 2^62 / p² terms, and the prime was dropped below 2^25 to make that chunk large.
2. Hypercube variable order was reversed. eq_vector puts variable 0 in the low bit; the sumcheck was splitting on the high bit, so the challenges came back in the wrong order. Splitting on the low bit fixes it.

Status: complete. Positive result on pure linear algebra, negative result on our own architecture. Date: 2026-09-02. Apple M5; NumPy 2.5.2. Field p = 33554393 (< 2^25). Raw records: ../../benchmarks/results/019-interactive-proof.jsonl

---

1. The protocol works, and the reduction is enormous

A two-layer chain C2 = (X·W1)·W2, verified without the verifier ever receiving C1:

Honest runs accepted and single-entry corruptions rejected at every size. Communication grows logarithmically — 22 rounds at n=2048 against 16 at n=256 — while the data it replaces grows quadratically. The reduction therefore improves with scale.

This is exactly what E016 said was needed, and it is why SafetyNets reports under 8 KB. The bandwidth objection, for a chain of matmuls, is answered.

2. And it saves nothing on our transformer layer

Applied to the E015 layer (s=1024, d=2048), the realisable saving is zero.

49.1 MB — the exact figure E016 measured. Nothing changes.

A sumcheck removes the need to send a matmul output by replacing it with a claim about that output at one random point. That only helps if nothing downstream needs the actual values. In our layer every matmul output is consumed by a lookup-table non-linearity, which the verifier checks by recomputation, which needs the values.

The chain breaks at the first non-linearity, and there is a non-linearity after every matmul.

3. The tension, stated plainly

Two of our own design decisions turn out to pull against each other:

NC-9 specifies non-linearities as integer lookup tables, because a gather has no arithmetic and therefore cannot diverge between backends. That is what made E015 and E018 bit-exact.

A sumcheck can only pass through operations that are low-degree arithmetic. A lookup table is not.

The property that gives us cross-backend determinism is the property that blocks the interactive proof.

This also explains a choice in SafetyNets that had looked arbitrary. They restrict networks to quadratic activations and sum pooling — and take a real accuracy hit for it (TIMIT 25.7% against an 18.5% ensemble baseline). That is not a quirk of 2017 hardware. y = x² is arithmetic, so the sumcheck chain passes through it. They changed the model because the protocol demanded it.

4. Where that leaves the architecture

Four ways forward, and they are genuinely different bets:

Option (d) is what this experiment tested, and it is measured at zero benefit for a transformer. Option (c) remains the design E016 arrived at and is still the cheapest thing that works end to end.

Correction added after E020. Option (a) is stated above as "adopt SafetyNets' quadratic activations". That is incomplete. SafetyNets' networks had no attention, and their only softmax was the final classification layer, which they explicitly exclude from the proof. In a transformer softmax sits mid-chain and stops a sumcheck exactly as a lookup table does — so swapping GELU for x² is not sufficient. E020 measured both halves: the activation change is free (-0.5%), and replacing attention costs +4.2%.

The honest summary: we built the mechanism that fixes the bandwidth problem and discovered our own contract is incompatible with it. That is a better outcome than not knowing, and it converts a vague "GKR might help" into a specific, measured incompatibility with a named cause.

5. What a malicious provider can still get away with

• Everything from E013 — the proof constrains the answer, not the work.
• The intermediate is never checked directly. The sumcheck only establishes that C1 is consistent with the layers on either side of it. That is sufficient for correctness of the final output and is worth stating precisely, because it is a weaker-sounding property than "we verified C1".
• If challenges are predictable, or if Fiat-Shamir is used without a sound transcript binding, the prover can search for a passing transcript.

6. Limitations

• Two-layer chains of square matrices. Real shapes are rectangular and deeper.
• p < 2^25 was chosen so every dot product stays inside int64; soundness comes from 3 independent repetitions rather than one large field. A 2^61 field with 128-bit arithmetic would need one run, and would be the right production choice.
• Interactive. Making it non-interactive needs Fiat-Shamir, which adds a random-oracle assumption and is not implemented or measured here.
• Prover overhead is not measured. SafetyNets reports 5%; we report only communication and correctness. That gap should be closed before the comparison in §4 is used for a decision.

1. Price option (a): polynomial activations

The only route that keeps the sumcheck's ~800-byte transcript through a whole network. It costs a model change, and SafetyNets shows the accuracy hit is real (TIMIT 25.7% against an 18.5% ensemble baseline).

The measurement we can make ourselves, cheaply, reusing E018's harness: retrain the char transformer with quadratic activations in place of GELU, and compare perplexity. If the gap is small on our workload, option (a) becomes the leading architecture. If it is large, (c) — layer audit plus stake — stands.

This is the highest-value next experiment: it is a straight fork in the architecture and we already have both halves of the apparatus.

2. Measure prover overhead

E019 reports communication and correctness but not prover cost. SafetyNets claims 5%; our folding is O(n²) per sumcheck against an O(n³) matmul, so it should be small, but "should be" is not a measurement and the §4 comparison table needs it before it drives a decision.

3. Fiat-Shamir, and what it costs in assumptions

The protocol as implemented is interactive — 22 round trips. Production needs it non-interactive, which means hashing the transcript to derive challenges and adopting a random-oracle assumption. Cheap to implement, and it changes the trust set, so it belongs in the taxonomy row rather than being waved through.

4. A larger field

p < 2^25 was chosen so int64 never overflows, and soundness comes from three repetitions. A 2^61 field with 128-bit arithmetic gives the same soundness in one run and a third of the transcript. Right choice for production, irrelevant to the finding.

5. Read the lookup-argument literature before building anything

Option (b) — keeping lookup tables and proving them with a lookup argument — is exactly what ZIP does with Caulk. Its measured cost (37 hr for mini-BERT) makes it look unaffordable, but ZIP was proving everything; a lookup argument used only at non-linear boundaries, with sumcheck carrying the linear layers, is a different and much smaller proposition. Nobody appears to have measured that combination — it is gap G6/G7 in docs/literature.md and may be the interesting one.