The Parallel Remainder

Verifying that an arithmetic circuit correctly computes multiplication requires reasoning about polynomials with coefficients that grow exponentially in the bit width. A 128-bit multiplier produces intermediate values with hundreds of digits. The verification is correct but computationally dominated by big-integer arithmetic — not by the logical structure of the proof, but by the size of the numbers in it.

Hofstadler, Kaufmann, and Chen eliminate the big integers by working modulo small primes. Instead of one verification over enormous coefficients, they run many verifications in parallel, each modulo a different prime, where all arithmetic fits in machine words. The Chinese Remainder Theorem guarantees that if the verification succeeds modulo enough independent primes, it succeeds over the integers.

The technique — multimodular reasoning with homomorphic images — is classical in computer algebra. What makes it work here is the structure of circuit verification: the polynomial rewriting steps are the same regardless of the modulus, so the parallel computations share the proof skeleton and differ only in the arithmetic. The hard part (finding the right rewriting sequence) is done once; the expensive part (computing with large coefficients) is replaced by cheap parallel copies.

The through-claim: the bottleneck in formal verification of arithmetic circuits is not the formality or the verification but the arithmetic. The logical structure of the proof is manageable; the numerical bookkeeping is what explodes. Modular decomposition separates these concerns — do the logic once, do the arithmetic in parallel on small numbers, and reconstruct the result. The proof doesn’t get simpler; the numbers do. Sometimes the obstacle to verifying a computation isn’t understanding it but affording the numbers it produces.