PaperlayerView exact revision on arXiv

Source-linked AI summary

Time-Optimal Interactive Proofs for Circuit Evaluation

Justin Thaler

arXiv:1304.3812v4cs.CRcs.CCcs.DS

TL;DR

Existing GKR implementations impose substantial prover overhead, limiting practical verifiable computation. This paper removes the logarithmic overhead for circuits with regular wiring patterns, reports major prover speedups, and develops protocols for matrix multiplication and data-parallel computation.

  • Problem

    Prior GKR prover implementations require O(S(n)logS(n)) time, with the logarithmic factor creating a substantial practical overhead over circuit evaluation.

  • Method

    The paper refines the GKR protocol to achieve O(S) prover time for circuits with regular wiring patterns and develops protocols for matrix multiplication and general data-parallel computation.

  • Results

    The prover is 200x-250x faster than the previous state-of-the-art GKR implementation, while communication costs and rounds are 2x-3x smaller.

  • Takeaways & Limitations

    The refinements substantially advance practical general-purpose interactive proofs, producing a prover less than 10x slower than straightforward C++ circuit evaluation and amenable to parallelization.

  • Takeaways & Limitations

    Theorem 1 does not apply to every circuit layer: its applicability is constrained by the layer's wiring pattern, although Appendix B extends the ideas to the cited arithmetic-indexing pattern.

Abstract

from arXiv · show

Recently, researchers have been working toward the development of practical general-purpose protocols for verifiable computation. These protocols enable a computationally weak verifier to offload computations to a powerful but untrusted prover, while providing the verifier with a guarantee that the prover performed the computations correctly. Despite substantial progress, existing implementations are not yet practical. The main bottleneck is typically the extra effort required by the prover to return an answer with a guarantee of correctness, compared to returning an answer with no guarantee. We describe a refinement of a powerful interactive proof protocol originally due to Goldwasser, Kalai, and Rothblum. Cormode, Mitzenmacher, and Thaler show how to implement the prover in this protocol in time O(S log S), where S is the size of an arithmetic circuit computing the function of interest. Our refinements apply to circuits whose wiring pattern is sufficiently "regular"; for these circuits, we bring the runtime of the prover down to O(S). That is, our prover can evaluate the circuit with a guarantee of correctness, with only a constant-factor blowup in work compared to evaluating the circuit with no guarantee. We argue that our refinements capture a large class of circuits, and prove some theorems formalizing this. Experimentally, our refinements yield a 200x speedup for the prover over the implementation of Cormode et al., and our prover is less than 10x slower than a C++ program that simply evaluates the circuit. Along the way, we describe a special-purpose protocol for matrix multiplication that is of interest in its own right. Our final contribution is a protocol targeted at general data parallel computation. Compared to prior work, this protocol can more efficiently verify complicated computations as long as that computation is applied independently to many pieces of data.

1 Introduction

Verifiable-computation protocols let weak verifiers outsource computation to untrusted provers, but prior implementations imposed substantial prover overhead and wiring restrictions. This paper removes the logarithmic overhead for regular circuits, develops protocols for data-parallel and matrix computations, and reports large practical speedups.

  • Verifiable-computation protocols let weak verifiers outsource computation while obtaining guarantees that untrusted provers computed answers correctly.
  • Prior interactive-proof implementations were theoretically powerful but too inefficient for practical deployment, with prover runtime remaining a major bottleneck.
  • The data-parallel protocol efficiently verifies computations applied independently to many pieces of data without significant assumptions about the sub-computation’s wiring.
  • Theorem 1 reduces prover runtime from O(S(n)logS(n)) to O(S(n)) for circuits with sufficiently regular wiring patterns.
  • 200x-250x speedups over the prior GKR implementation were observed, while the serial prover was less than 10x slower than sequential C++ circuit evaluation.
  • The matrix-multiplication protocol gives the prover runtime T(n)+O(n2) and space s(n)+o(n2), while avoiding circuit evaluation entirely.

2 Preliminaries

The preliminaries define interactive-proof correctness, the paper’s finite-field cost model, streaming inputs, and the MATMULT and DISTINCT problems used as focal applications.

  • 2.1 Definitions: An interactive proof consists of prover-verifier message exchange for computing f, with completeness for an honest prover and soundness against dishonest provers.
  • 2.1.1 Cost Model: The paper measures finite-field computation by machine operations, so prover time O(S(n)) denotes O(S(n)) additions and multiplications.
  • Input Representation: Inputs may be general data streams of tuples (i,δ), with negative updates allowed and m=Θ(n) assumed throughout.
  • Input Representation: The verifier makes one pass over the input stream, regardless of update ordering, while storing at most s(n) finite-field elements.
  • Problems: MATMULT computes A·B from two n×n matrices, while DISTINCT computes the number of items with non-zero frequency in a stream.
  • Notation: The notation [n] denotes {1,...,n}, [[n]] denotes {0,...,n−1}, and multilinear extension denotes the unique multilinear polynomial agreeing with a Boolean function.

3 Overview of the Ideas

The paper refines GKR by choosing polynomials that enable prover work reuse, achieving linear runtime for sufficiently regular circuits and efficient verification for data-parallel computations.

  • Regular circuits: O(S(n)) prover runtime is achieved for a large class of sufficiently regular circuits while preserving prior GKR verifier runtime.Theorem 1 formalizes this result.
  • Core approach: The protocol applies sum-check iteratively from circuit outputs toward inputs, as in GKR, but uses carefully chosen polynomials at each iteration.These choices allow the prover to reuse work from prior rounds.
  • Regular circuits: The GKR polynomial is sparse, which supports Cormode et al.’s O(S_i log S_i) runtime but prevents reuse of work across prior iterations.The refinement instead uses a denser polynomial representation.
  • Regular circuits: Grouping gates by the sum-check terms they contribute to removes the remaining logarithmic factor from prover work.Each group is treated as a single unit during the rounds.
  • Data-parallel computation: Theorem 1 is limited to regular wiring, while the data-parallel protocol targets repeated independent sub-computations and is most useful when B ≫ S.Its overhead depends minimally on the number of data pieces but necessarily on sub-computation complexity.
  • Matrix multiplication: The matrix-multiplication protocol avoids circuit evaluation and adds only O(n^2) prover work after computing the correct output.It uses a higher-degree extension of gate-value functions.

4 Technical Background

A polynomial over a finite field cannot vanish on too large a fraction of a finite grid unless its degree is large.

  • Schwartz-Zippel property: For a nonzero m-variate polynomial of total degree d, a uniformly random point in S^m is a root with probability at most d/|S|.Equivalently, two distinct degree-d polynomials agree on at most that fraction of grid points.

4.2 Sum-Check Protocol

The sum-check protocol lets a verifier check a Boolean-hypercube sum through a sequence of polynomial claims and random challenges, without evaluating the full sum.

  • Verifier requirement: The verifier requires an evaluation of g at a randomly chosen field vector to execute the protocol.This is the verifier’s key evaluation assumption.
  • Protocol steps: The protocol runs for v rounds, with the prover sending one univariate polynomial per round and the verifier randomly binding variables.The verifier checks successive polynomial consistency relations and degree bounds.
  • Protocol steps: After the final consistency check, the verifier evaluates the last polynomial at the random point and accepts when all checks succeed.This establishes the claimed Boolean-hypercube sum.
  • Purpose: The sum-check protocol verifies H = ∑b1∈{0,1} ... ∑bv∈{0,1} g(b1,...,bv) for a v-variate polynomial g.It is the paper’s main technical tool.
  • Costs: O(v) field elements are communicated when every variable degree is O(1), and verifier time equals communication plus evaluating g at the random point.The verifier’s total runtime is therefore proportional to these two costs.
  • Prover cost: O(2^v) total terms are evaluated because the number of terms decreases geometrically across rounds, provided the prover can evaluate g at needed points.The paper identifies this point-evaluation capability as the key application-specific challenge.

4.3 The GKR Protocol

GKR reduces circuit-output verification to input-layer verification through layer-by-layer sum-check applications, with costs governed by circuit depth, size, and wiring access.

  • Circuit representation: GKR represents a layered fan-in-two arithmetic circuit using gate-value extensions and wiring predicates for addition and multiplication gates.These objects encode gate values and the connections between adjacent layers.
  • Layer reduction: Each of the d(n) iterations reduces a claim about ˜V_i(z) to a claim about ˜V_i+1(ω) using sum-check and wiring-related polynomials.The verifier does not receive all intermediate layer values.
  • Layer reduction: A line restriction reduces two claimed evaluations at the next layer to one randomly checked evaluation, allowing the protocol to continue with a single-point claim.Schwartz-Zippel provides the corresponding safety guarantee.
  • Input layer: The final iteration checks the multilinear extension of the input layer, which the verifier can compute directly from the input.Prior methods provide O(n log n) streaming evaluation or an O(n) approach outside the general streaming model.
  • Costs: O(d(n) log S(n)) field elements are communicated, while verifier time is O(n log n + d(n) log S(n)).The n log n term comes from evaluating the input-layer extension in the described method.
  • Prover cost: A naive prover may require Ω(2^{s_i+2s_i+1}) time per iteration, potentially reaching Ω(S(n)^3), motivating structured implementations.Cormode, Mitzenmacher, and Thaler exploit the fact that each gate contributes to only one sum term.

5.1 Protocol Outline and Section Roadmap

The protocol follows GKR’s layer-by-layer sum-check structure but replaces its polynomial with a smaller-domain polynomial that lets the prover reuse work and remove a logarithmic runtime factor.

  • Protocol Outline: Each iteration reduces a claim about layer i to a claim about layer i+1 using sum-check on a specially chosen polynomial.The protocol proceeds from the output layer toward the input layer, as in GKR.
  • Protocol Outline: The refinement replaces f^(i)_z with g^(i)_z, defined over s_i variables instead of s_i + 2s_i+1 variables.The smaller domain is the basis for the prover’s work reuse.
  • Protocol Outline: Using g^(i)_z allows the prover to reuse work across sum-check rounds, reducing runtime by a logarithmic factor relative to prior work.Theorem 1 formalizes the resulting improvement.
  • Section Roadmap: The section roadmap develops the construction through a preliminary lemma, three circuit examples, and the algorithmic ideas behind work reuse.The examples include addition and multiplication trees and a circuit counting non-zero vector entries.

5.2 A Preliminary Lemma

A preliminary lemma represents the multilinear extension of circuit-layer values using any polynomial that agrees with those values on Boolean inputs.

  • Preliminary Lemma: For any polynomial W extending V_i on Boolean inputs, the lemma gives an expression for V~_i(z) suitable for sum-check verification.The expression applies for every z in F^s_i.
  • Preliminary Lemma: The proof establishes that the expression is multilinear in z and agrees with V_i on all Boolean inputs, so it equals V~_i.Uniqueness of the multilinear extension completes the argument.

5.3 Polynomials for Specific Circuits

The paper instantiates its polynomial construction for multiplication and addition trees and for a DISTINCT circuit that computes whether vector entries are non-zero over a Mersenne-prime field.

  • Binary Trees: A binary multiplication tree labels each layer’s gates so that a gate p receives inputs from labels (p,0) and (p,1) at the preceding layer.The labeling exposes the circuit’s regular wiring pattern.
  • Binary Trees: For multiplication trees, the multilinear extension is expressed as a sum over Boolean gate labels using g^(i)_z.The corresponding polynomial has degree three in each variable and requires four field elements per sum-check round.
  • Binary Trees: For addition trees, the construction is analogous to the multiplication-tree case, with a corresponding expression for V~_i(z).The paper also notes a degree-two variant in the relevant proposition.
  • DISTINCT: The DISTINCT circuit has k + 1 relevant multiplication layers, with regular connectivity determined by the binary representation and low-order bit of each gate number.The field choice supports extremely fast arithmetic, and the construction is tailored to Mersenne-prime cardinality.

5.4 Reusing Work

The prover reuses structured evaluations across sum-check rounds by grouping gate contributions and maintaining intermediate arrays, yielding linear work in adjacent layer sizes per iteration.

  • Work Reuse: Across all rounds, the prover needs only O(2^s_i) evaluations of g^(i)_z, and these can be organized to achieve O(2^s_i + 2^s_i+1) work.This equals O(S_i + S_i+1) for iteration i.
  • Work Reuse: The optimization applies to the listed circuit polynomials because each g^(i)_z evaluation takes constant time given β(z,p) and values of V~_i+1 at a constant number of points.The required V~ evaluations are computed using analogous intermediate arrays.
  • β Evaluation: The prover computes β(z,p) values with dynamic programming, constructing the initial array in O(2^s_i) time rather than the naive O(s_i2^s_i) time.The total number of multiplications across the stages is O(2^s_i).
  • β Evaluation: During round j, intermediate C(j) arrays support the required β evaluations and can be updated from C(j−1) in O(2^s_i−j) time.The method reuses one computed inverse per round; the total inverse cost is O~(s_i).
  • Work Reuse: Each gate at layer i+1 contributes to at most one required evaluation point, reducing the naive total to O(S_i+1 log S_i) before grouping.Grouping gates by their contribution point removes the remaining logarithmic factor because the required point set shrinks geometrically.

5.5 A General Theorem

The theorem identifies layered arithmetic circuits with regular wiring patterns for which the refined protocol achieves linear prover time while retaining efficient verification. It also applies to selected application circuits, including matrix multiplication and DISTINCT, and can benefit circuits with only some regular layers.

  • General theorem: The prover’s sum-check work is O(S_i+S_i+1) on regular layers, while reducing to verification at one point requires an additional similarity condition.The protocol processes the circuit through one sum-check-based iteration per layer.
  • General theorem: Theorem 1 applies when the circuit’s wiring functions and gate-type function are regular, with the first and second in-neighbor functions similar on all but O(1) layers.Regularity requires constant-time evaluation, limited input-bit influence, and at most one input bit per output bit.
  • General theorem: The refined protocol has prover time O(S(n)), verifier time O(nlogn+d(n)logS(n)), and communication O(|O|+d(n)logS(n)) field elements.The verifier makes one streaming pass while storing O(log(S(n))) field elements.
  • General theorem: The protocol’s costs match Cormode et al.’s implementation except that prover time improves from O(S(n)logS(n)) to O(S(n)).The verifier and communication asymptotics remain unchanged relative to that implementation.
  • Applications: For n × n matrix multiplication, the theorem yields prover time O(n^3) and verifier time O(n^2 logn), with n^2 output communication.The circuit has size O(n^3), using product gates followed by addition trees.
  • Applications: The refinements apply layer by layer, so circuits can still gain speedups when some, but not all, layers have sufficiently regular wiring.Appendix B extends the ideas to a layer whose labels encode integer addition, a pattern outside the theorem’s basic regularity condition.

6 Experimental Results

Experiments evaluate the refined protocols on matrix multiplication and DISTINCT, showing large prover speedups and reduced communication and rounds. GPU parallelization further accelerates the matrix-multiplication prover, while verifier time remains comparable to prior work and below local computation time.

  • Summary of Results: 200x-250x faster prover runtime was observed than in the previous state-of-the-art GKR implementation when Theorem 1 applies.The verifier’s runtime and communication improvements were also measured against prior implementations.
  • Summary of Results: 2x-3x reductions in communication costs and rounds were achieved relative to the previous state of the art.For 512 x 512 MATMULT, the protocol uses 236 rounds and 5.48 KBs of extra communication, versus 767 rounds and close to 18 KBs previously.
  • Summary of Results: The verifier took essentially the same time as in prior GKR implementations and much less time than performing the computation locally.The MATMULT verifier’s runtime was more than an order of magnitude below the 1.03 seconds required for serial integer multiplication.
  • Serial Implementation: 250x faster MATMULT prover runtime was measured than the comparison implementation for 512 x 512 matrices.The prover took about 38 seconds, versus over 2.5 hours for the comparison implementation, and was less than 7x slower than unverifiable circuit evaluation.
  • Serial Implementation: 200 times faster DISTINCT prover runtime was measured than the comparison implementation, while the prover was roughly 10x slower than unverifiable circuit evaluation.For a vector of length 2^20, the prover took about 17 seconds versus about 57 minutes for the comparison implementation.
  • Parallel Implementation: 30x speedup was obtained for the MATMULT prover relative to the serial implementation using GPU parallelization.Excluding circuit-evaluation runtime, the parallel prover was faster than sequential circuit evaluation for 512 x 512 matrix multiplication.

7 Verifying General Data Parallel Computations

The paper develops a protocol for verifying data-parallel computations, where the same sub-computation is applied independently to many data pieces. By exploiting noninteraction between sub-computations, it reduces verifier preprocessing and controls prover overhead as batch size grows.

  • Motivation: Existing circuit-verification implementations either require highly regular wiring or impose substantial prover and verifier overhead.The batching approach of prior work also makes verifier work and total communication grow linearly with batch size.
  • Problem setting: Data-parallel computation applies the same sub-computation independently to many pieces of data, possibly followed by aggregation.The protocol does not require the sub-computation itself to have regular wiring.
  • Applications: The protocol supports arbitrary counting queries by applying a function independently to database rows and aggregating the results.Its overhead depends minimally on database size but necessarily depends on the complexity of the queried property.
  • Protocol overview: For a super-circuit containing B independent copies of a size-S circuit, naive GKR preprocessing requires Ω(B·S), while the proposed protocol requires O(S).The protocol uses polynomials derived from one sub-computation’s wiring predicate because the copies do not interact.
  • Protocol overview: The prover runs in O(B · S · logS), so its correctness-guaranteeing slowdown is only logS, matching basic GKR on one sub-computation.This combines the data-parallel structure with the paper’s circuit-evaluation methods.
  • Efficiency guarantees: Theorem 2 gives verifier preprocessing O(S), online verification O(n∗logn∗+d·log(B·S)), prover time O(S · B · logS), and communication O(d ·log(B·S)) field elements.The verifier’s preprocessing is independent of the number B of data pieces.

8 Extensions

The paper presents specialized extensions for addition trees and matrix multiplication. These refinements reduce prover cost, communication, and space, including a matrix-multiplication protocol whose overhead is additive rather than multiplicative.

  • 8.1 Binary Tree of Addition Gates: The addition-tree optimization applies to multiple outputs and permits a binary tree of addition gates anywhere in the circuit.This contrasts with an earlier optimization restricted to a single-output circuit ending in an addition tree.
  • 8.1 Binary Tree of Addition Gates: The addition-tree optimization appears in circuits for MATMULT, DISTINCT, pattern matching, and counting queries.The same construction can verify multiple independent single-output instances whose circuits end with binary sum-gate trees.
  • 8.1 Binary Tree of Addition Gates: A single sum-check protocol directly reduces a claim about the output extension to a claim about the input extension at a random point.This replaces one sum-check invocation per circuit layer for the targeted addition-tree structure.
  • 8.2 Matrix Multiplication: Theorem 3 gives matrix multiplication communication n2 + O(logn), prover time T(n)+O(n2), and prover space s(n)+o(n2).Here T(n) and s(n) are the time and space of any unverifiable n×n matrix-multiplication algorithm.
  • 8.2 Matrix Multiplication: The verifier’s runtime can be reduced to O(n2) while preserving streaming when input matrices are presented in row-major order.The general theorem reports O(n2 logn) verifier time, while the optimization trades space or exploits input ordering.
  • 8.2 Matrix Multiplication: The prover’s matrix-multiplication runtime is within an additive low-order term of any unverifiable algorithm, avoiding the need to tolerate even a 2x slowdown.This also avoids the much larger space requirements that can arise in circuit-checking protocols.
  • 8.2 Matrix Multiplication: The matrix-multiplication protocol requires only the input and output matrices, without explicitly sending intermediate matrices.This supports repeated uses of matrix multiplication when the desired final output is smaller than the intermediate matrices.

9 Conclusion

The paper argues that its refinements make interactive proofs substantially more practical by removing logarithmic prover overhead for regular circuits and exploiting structure in real-world computations. It identifies compiler and systems support for data-parallel verification as future work.

  • Conclusion: The refinements remove the O(logS(n)) prover overhead for circuits with regular wiring patterns.The paper presents this as a step toward practical general-purpose interactive-proof implementations.
  • Future work: A full-fledged system for data-parallel computation remains future work.The proposed direction combines the protocol with a high-level language and automatic circuit compilation.

A Proof of Theorem 1

The proof establishes efficient prover evaluation for circuits satisfying a regularity condition. It represents wiring-related polynomials with constant individual degree and constructs the required sum-check messages using arrays updated after verifier challenges.

  • Regularity condition: Regularity requires that, after fixing a constant-size subset of input bits, each remaining input bit affects only O(1) output bits.This structural condition enables efficient evaluation of the wiring extensions.
  • Regularity condition: For each fixed assignment to the exceptional variables, every nonconstant output-bit extension depends on a single remaining input variable.Such extensions are either that variable or one minus that variable.
  • Polynomial construction: At each layer, the prover evaluates the sum-check polynomial using the multilinear extension of the layer values and the wiring-related function.The relevant β values can be computed in O(Si) total time across the sum-check iteration.
  • Polynomial construction: The protocol forms a polynomial g(i)_z(p)=β(z,p)·W(i)(p) whose degree is O(1) in every variable.The constant-degree property yields the stated verifier and communication costs after summing over circuit layers.
  • Prover evaluation: The prover initializes an array of gate values and updates it after each verifier challenge using a recurrence tied to the affected output variables.Each update from V(j−1) to V(j) takes O(2si+1−aj−1) time.
  • Prover evaluation: One layer’s entire sum-check execution takes O(Si +Si+1) prover time.Summed over all layers, this gives O(S(n)) prover time for the regular circuit class.
  • Prover evaluation: Skipping single-point reduction at only a constant number of layers increases the number of checked points and runtime by at most a constant factor.At most 2c=O(1) points need to be checked at each layer.

B Analysis for Pattern Matching

The pattern-matching analysis reduces a claim about one circuit layer to the next while preserving O(nm) prover time. It uses carry-aware polynomials and an ordered sum-check protocol to make required evaluations geometrically shrink.

  • B Analysis for Pattern Matching: The protocol reduces a claim about ˜Vℓ(z) to a claim about ˜Vℓ+1(r) while keeping the prover runtime O(Sℓ) = O(nm).The reduction uses a sum-check protocol for the layer adjacent to the input.
  • B Analysis for Pattern Matching: Introducing dummy carry variables makes each output bit depend on at most three input bits, restoring local wiring structure.Each carry variable is forced to equal the corresponding binary-addition carry bit.
  • B Analysis for Pattern Matching: The polynomial Φ(i,k,c) equals 1 exactly when c contains the carry bits produced by adding i and k.The local polynomial ˜φ enforces each carry transition, and Φ multiplies these constraints across bit positions.
  • B Analysis for Pattern Matching: The prover evaluates only O(2^(logn+logm−j)) terms in rounds 3j, 3j+1, and 3j+2 because invalid carry assignments vanish.The number of necessary evaluations decreases geometrically with j.
  • B Analysis for Pattern Matching: An ordering that binds each triple (ij,kj,cj) sequentially lets the V^(j) arrays halve in size every three rounds.Each newly bound ˜γ value feeds into ˜T without affecting later positions.
  • B Analysis for Pattern Matching: Maintaining prior carry-factor products and evaluating the current factor in constant time makes all Φ evaluations take O(1) time per necessary point.The accumulated maintenance costs O(logn) over the protocol.
Loading 1304.3812v4…