What does the sumcheck prover actually pay?
Overview
README.md ↗Status: hypotheses recorded before the run.
Why
docs/paper-readiness.md has carried B4 — "sumcheck prover overhead
unmeasured" since the assessment was written, and it is the last unquantified
number in the paper.
It matters more than it looks. The paper's §2 states SafetyNets' prover overhead as 5% and concedes that figure is better than anything we build. §10 then argues sumcheck does not transfer to a transformer — but that argument is made entirely on bandwidth grounds. We never measured what the prover pays, so the comparison rests on their number and none of our own.
E025 is the reason this is worth doing rather than assuming. The accuracy figure also looked settled, and measuring it moved the headline by a full point and showed the original sample could not have supported its own conclusion. A number that has never been measured should be assumed to be in the same state.
The gap in E019
E019 implemented the protocol and measured communication (792 bytes against
16.8 MB) and verifier cost. It could not measure prover cost, because
sumcheck() interleaves both parties in one loop: the prover's round polynomial,
the verifier's check, the verifier's challenge and the prover's fold all happen
in the same iteration.
E026 splits them so each side's work can be timed on its own.
What is being measured
For C = A @ B over F_p, the prover's cost decomposes as:
| cost | who | |
|---|---|---|
C = A @ B |
O(n³) | the native computation — the baseline, not overhead |
| reduce A, B into residues | O(n²) | prover |
a = A~(r1, ·), b = B~(·, r2) |
O(n²) | prover |
| v = log₂n sumcheck rounds, halving each time | O(n) | prover |
| forming the claim from C, and the final MLE openings | O(n²) | verifier |
So the structure predicts prover overhead O(n²)/O(n³) = O(1/n): asymptotically free, and dominated in practice by constant factors, because the native matmul rides float64 BLAS while every field operation is modular numpy.
Reported against the same baseline as everything else in this repository:
R_prove = (prover total with proof) / (prover cost without proof)
Hypotheses, recorded before looking
H1. Prover overhead falls with n, approximately as 1/n. If it is flat or rising, the implementation is doing something of the wrong order and the measurement is invalid before it is interesting.
H2. At the largest n tested, single-matmul prover overhead lands in single digit percent, i.e. consistent with SafetyNets' 5% being real rather than a result of a friendlier setting. Confidence: moderate. The arithmetic: at n = 2048 the O(n²)/O(n³) ratio is 1/2048 ≈ 0.05%, and modular numpy is perhaps 50–200× slower per element than BLAS float, which lands near 5%. That is a prediction from two independently-known constants, so it is a real test rather than a fitted one.
H3. The MLE vectors dominate the prover's overhead (O(n²)), not the sumcheck rounds (O(n)). If the rounds dominate, our model of where the cost sits is wrong and §10's reasoning needs re-examining.
H4. Verifier compute is O(n²) and so R_verify also falls with n, staying
far below 1 — sumcheck beats re-execution on compute as well as on bandwidth.
H5. The two-layer chain costs the prover more than twice a single matmul, because the second sumcheck needs the MLE of the intermediate C1, which a single matmul never has to form.
What would change the paper
If prover overhead is large and does not fall with n, then §10's conclusion ("sumcheck does not transfer, on bandwidth grounds") is understated — it would not transfer on prover cost either, and the paper should say so.
If it is small and falls as predicted, then the honest statement is that the only thing blocking sumcheck for transformers is the non-linearity structure, which is what §10 already argues. That strengthens the paper without changing its conclusion, and it means the 5% we quote from SafetyNets is a number we can now speak to rather than merely cite.
Analysis
analysis.md ↗B4 is cleared. The sumcheck protocol itself costs the prover 0.5% of its overhead. Everything else is the machinery around it, and most of that turned out to be our own implementation rather than the protocol.
| prover overhead at n = 4096 | |
|---|---|
| our first implementation | 36.1% |
| after two fixes the measurement itself exposed | 10.4% |
| SafetyNets (2017), reported | 5% |
Scaling as n^−0.92, against the n^−1 the structure predicts. Extrapolating, this implementation reaches 5% at n ≈ 8,800.
The result
Square matmuls over F_p (p = 2^25 − 39), 7 repetitions, fastest run kept.
native is the same product computed with no proof at all.
Single matmul, optimised prover
| n | native | R_prove |
fall per doubling | R_verify |
transcript |
|---|---|---|---|---|---|
| 256 | 0.2 ms | 145.5% | — | 312.8% | 96 B |
| 512 | 1.0 ms | 58.2% | 2.50× | 245.3% | 108 B |
| 1024 | 6.7 ms | 33.4% | 1.75× | 165.6% | 120 B |
| 2048 | 45.2 ms | 20.1% | 1.66× | 113.3% | 132 B |
| 4096 | 339.8 ms | 10.4% | 1.93× | 63.4% | 144 B |
The two-layer chain tracks it almost exactly: 10.2% at n = 4096, with
R_verify 46.5%.
The measurement found its own bug, twice
The first run said 36.1%, and the breakdown said two thirds of that was forming the multilinear extensions. Chasing why turned up two defects that were ours, not the protocol's:
1. dotmod multiplies int64 arrays, and numpy has no BLAS path for int64.
It falls back to a scalar loop. Measured directly: a modular vector-matrix
product runs at 733× the per-element cost of a float64 BLAS multiply-add,
while a plain modular reduction runs at 144×. E019's own matmul_mod documents
this trap and splits operands into 13-bit limbs to avoid it; the MLE path never
got the same treatment. Applying it: 6.6× faster, bit-identical output, with
the exactness bound (2^49 against float64's 2^53) asserted rather than assumed.
2. Two of the three field reductions were on data already in the field.
Under the numeric contract the operands are bounded at 2^11, and p is 2^25, so
A and B are residues as they stand. Only the product needs reducing.
That is NC-3b paying for itself somewhere it was never designed to: the operand bound that makes heterogeneous hardware agree also makes entering the proof field nearly free.
Together, a 3.5× speedup at n = 4096:
| n | naive | optimised | speedup |
|---|---|---|---|
| 1024 | 101.8% | 33.4% | 3.05× |
| 2048 | 61.7% | 20.1% | 3.08× |
| 4096 | 36.1% | 10.4% | 3.47× |
The lesson generalises past this experiment: our first number was a measurement of our own code, not of the protocol. It is the same failure mode as E017, where a broken integer pipeline scored at chance and looked like evidence against the approach.
Hypotheses
H1 — overhead falls with n, as ~1/n: confirmed. Measured n^−0.92 against a predicted n^−1. (The naive implementation gave n^−0.71; the residual gap there was the int64 fallback, whose cost grows with the data rather than staying a constant factor.)
H2 — single-digit percent at the largest n: narrowly falsified. 10.4%, not under 10. But the substantive claim behind it holds: this is within 2× of SafetyNets' 5%, and reaches 5% by n ≈ 8,800. My stated reasoning was wrong in both directions and happened to nearly cancel — I estimated a 50–200× slowdown against one pass over n² data; the truth is 144–733× against five passes.
H3 — the MLE dominates, not the rounds: confirmed, emphatically.
| n | entering the field | multilinear extensions | sumcheck rounds |
|---|---|---|---|
| 1024 | 50.5% | 44.2% | 5.3% |
| 4096 | 50.5% | 48.9% | 0.5% |
The sumcheck protocol is free. At n = 4096 it is half a percent of the prover's overhead. The cost is entirely the multilinear extensions and field entry, split almost exactly evenly once both are optimised.
H4 — verifier stays below re-execution: falsified below n = 4096. R_verify
exceeds 1.0 for a single matmul at every size up to 2048 — verification costs
more than just recomputing the product — and only drops below at n = 4096
(63.4%). The chain does better, crossing 1.0 near n = 1024. Sumcheck's advantage
is bandwidth; below n ≈ 2048 it has no compute advantage at all.
H5 — chain costs more than twice a single: falsified. Measured 1.67–2.02, averaging just under 2. A chain amortises very slightly rather than compounding.
What this changes in the paper
§10 argues sumcheck does not transfer to a transformer on bandwidth grounds: every matmul output feeds a lookup-table non-linearity the verifier must recompute, so the chain breaks at the first non-linearity. That argument is unaffected, and this experiment strengthens the paper by removing a weaker one we might have been tempted to make.
The prover is not the obstacle. At 10.4% and falling as 1/n, sumcheck's prover cost is affordable, and our measurement is consistent with SafetyNets' 5% being a real number rather than an artefact of a friendlier setting. We can now say that from our own data instead of citing theirs.
So the honest conclusion is sharper than before: the only thing blocking sumcheck for transformers is the non-linearity structure. Not prover cost, not communication. That is a cleaner claim, and a more falsifiable one.
What this does not settle
- Still numpy, not an optimised field implementation. Montgomery multiplication, SIMD or a C prover would move the constant further. 10.4% is an upper bound on what the protocol requires, not a floor.
- Square matmuls only. A transformer's are rectangular, and cost depends on the contracted dimension differently from the output dimensions. Qwen2.5-0.5B contracts over 896 and 4864, and at n = 1024 the measured overhead is 33%.
- Single-threaded prover against multi-threaded BLAS. The native baseline
gets more hardware than the prover does, which inflates
R_proveby an unmeasured factor — so the true figure is likely better than reported. - No commitment scheme. A deployed protocol needs the verifier to hold commitments to A and B rather than the matrices themselves. That cost falls on the prover and is not measured here.