PaperlayerView exact revision on arXiv

Source-linked AI summary

Practical Verified Computation with Streaming Interactive Proofs

Graham Cormode, Michael Mitzenmacher, Justin Thaler

arXiv:1105.2003v5cs.DScs.CCcs.CR

TL;DR

The paper asks how users can verify outsourced computations when recomputation and local storage are impractical. It engineers a general-purpose interactive proof construction and develops specialized streaming protocols, finding that practical delegation is closer to reality while fine-tuned methods achieve strong scalability for key problems.

  • Problem

    Users need to verify outsourced computation without recomputing results or storing the full input locally.

  • Method

    The paper combines an engineered Goldwasser–Kalai–Rothblum implementation with specialized protocols using Fast Fourier Transforms and polynomial linearization.

  • Results

    The general-purpose protocol is significantly closer to practical use, while specialized protocols scale to streams with billions of updates and use low space and communication.

  • Takeaways & Limitations

    Fine-tuned protocols remain valuable for key real-world problems even if general-purpose methods improve.

  • Takeaways & Limitations

    The general-purpose implementation is not yet practical for everyday use, and prover runtime remains its chief limitation.

Abstract

from arXiv · show

When delegating computation to a service provider, as in cloud computing, we seek some reassurance that the output is correct and complete. Yet recomputing the output as a check is inefficient and expensive, and it may not even be feasible to store all the data locally. We are therefore interested in proof systems which allow a service provider to prove the correctness of its output to a streaming (sublinear space) user, who cannot store the full input or perform the full computation herself. Our approach is two-fold. First, we describe a carefully chosen instantiation of one of the most efficient general-purpose constructions for arbitrary computations (streaming or otherwise), due to Goldwasser, Kalai, and Rothblum. This requires several new insights to make the methodology more practical. Our main contribution is in achieving a prover who runs in time O(S(n) log S(n)), where S(n) is the size of an arithmetic circuit computing the function of interest. Our experimental results demonstrate that a practical general-purpose protocol for verifiable computation may be significantly closer to reality than previously realized. Second, we describe techniques that achieve genuine scalability for protocols fine-tuned for specific important problems in streaming and database processing. Focusing in particular on non-interactive protocols for problems ranging from matrix-vector multiplication to bipartite perfect matching, we build on prior work to achieve a prover who runs in nearly linear-time, while obtaining optimal tradeoffs between communication cost and the user's working memory. Existing techniques required (substantially) superlinear time for the prover. We argue that even if general-purpose methods improve, fine-tuned protocols will remain valuable in real-world settings for key problems, and hence special attention to specific problems is warranted.

1 Introduction

The paper addresses trust in outsourced computation by developing streaming verification protocols that use limited verifier space and communication. It combines an engineered general-purpose construction with scalable specialized protocols for important streaming problems.

  • Motivation: Cloud users need ways to verify outsourced computations without recomputing results or storing massive inputs locally.Faulty implementations, disk failures, and memory errors can produce incorrect results even without a malicious provider.
  • Motivation: Streaming verifiers process inputs in one pass with small space, matching cloud workflows where data is uploaded incrementally.The model supports data too large for the user to store in memory.
  • General-purpose protocols: The paper engineers Goldwasser–Kalai–Rothblum circuit checking and modifies it to make general-purpose delegation more scalable.The implementation aims to make reliable delegation of arbitrary computations closer to practical use.
  • Specialized protocols: Specialized protocols use Fast Fourier Transforms and polynomial linearization to improve scalability for important streaming and database problems.The protocols include non-interactive designs with one prover-to-verifier message and interactive protocols for specific problems.
  • Empirical findings: Five orders of magnitude separate empirical prover speeds across techniques and problems, supporting continued value for fine-tuned protocols.Many protocols use at most a few megabytes of space and communication on terabyte inputs, while prover and verifier costs scale linearly or almost linearly.
  • Conclusion: The authors conclude that engineering has made interactive proof systems suitable for everyday delegated computation, while specialized methods remain important.The paper reports empirical scaling to streams with billions of updates and protocols for problems including F0 and matrix-vector multiplication.

2 Fast Non-interactive Proofs via Fast Fourier Transforms

The section develops FFT-based non-interactive protocols that reduce prover bottlenecks to near-linear computation while preserving streaming verifier tradeoffs. These improvements extend to several important vector, optimization, and graph problems.

  • FFT methods reduce the cost of evaluating low-degree extensions at many locations, addressing the prover bottleneck in non-interactive proofs.The approach targets multi-point evaluation, which previously required computing each value independently.
  • The protocols retain an (n^α, n^(1−α)) communication-space tradeoff for F2, including the described α = 1/2 instantiation.The verifier treats the input as a √n × √n array and checks a polynomial identity at a random field point.
  • 2.1 Breaking the bottleneck: O(n log n) arithmetic operations suffice for the honest prover in the F2 protocol, improving over the prior Θ(n3/2)-time implementation.The implementation previously failed to scale beyond n > 10^7, while the FFT-based protocol scales to streams with billions of items.
  • 2.1 Breaking the bottleneck: The Prime Factor Algorithm enables fast finite-field DFTs by decomposing transforms into smaller coprime-length DFTs when suitable roots of unity exist.The method requires transform lengths whose factors divide p − 1, with padding used when the desired length is unavailable.
  • 2.1 Breaking the bottleneck: N = 90090 supports inputs exceeding 10^9, with transform cost 47N instead of naive convolution time Θ(N^2).The chosen length factors as 2×5×7×9×11×13, enabling the stated finite-field transform cost.
  • For MVMULT, the prover cost falls from O(mn^(3/2)) to O(mn log n), while related protocols obtain nearly linear prover time and stated verifier bounds.The resulting corollaries cover inner product, Hamming distance, linear programming, triangle counting, connectivity, and bipartite perfect matching.

3 A General Approach: Multi-round Protocols Via Circuit Checking

The paper instantiates the Goldwasser–Kalai–Rothblum circuit-checking framework for streaming verification and develops specialized arithmetic-circuit protocols. The general construction achieves nearly linear prover time, but circuit representation remains a practical constraint.

  • General construction: The implementation targets the Goldwasser–Kalai–Rothblum protocol for verifying arbitrary computations with streaming users.The verifier processes the input under severe space constraints while the protocol checks a layered arithmetic circuit.
  • General construction: O(S(n) log S(n)) prover time and O(log S(n)) verifier space are achieved for log-space uniform circuits.The result applies over the entire protocol execution.
  • General construction: Theorem 3.3 shifts the verifier’s time-consuming, data-independent work into offline preprocessing before the stream is observed.Online verification then uses O(d(n) log S(n)) space and time O(n log n+d(n) log S(n)).
  • General construction: Under efficient wiring-predicate evaluation, the verifier uses O(log S(n)) space and time O(n log n + d(n)poly(log S(n))).The additional assumption is a O(log S(n))-space, poly(log S(n))-time algorithm for evaluating the wiring predicate’s multilinear extension.
  • Circuit design issues: Boolean-circuit encoding can make simple arithmetic operations unnecessarily deep, while direct arithmetic circuits reduce addition to a single depth-1 gate.The direct approach nevertheless appears limited for functions such as testing whether x > y over Fp.
  • Efficient protocols for specific problems: For specific problems, carefully chosen arithmetic circuits instantiate interactive protocols, including a first protocol of its kind for PMWW.One example achieves prover time O(n log n log p) with a (log n log p, log n) protocol.

4 Multi-Round Protocols via Linearization

Linearization keeps polynomial degrees low in multi-round protocols for F0 and PMWW, trading additional interaction for improved scalability. The resulting protocols achieve logarithmic-round complexity with logarithmic communication and verifier costs.

  • Linearization motivation: Two orders of magnitude: the new F0 protocol improves the prover’s runtime over existing protocols while retaining similar asymptotic costs.Linearization avoids high-degree polynomials by adding more rounds of interaction.
  • Linearization set-up: The ⨿ and Π operators arithmetize OR and AND, reducing k-variate degree-j polynomials to k −1-variate polynomials of degree at most 2j per variable.Their Boolean behavior matches OR and AND when the two input values are Boolean.
  • Linearization set-up: Linearization controls polynomial degree by making each Li operation linear in Xi while preserving agreement with g on Boolean inputs.This enables low-degree polynomial verification without changing values on {0, 1}^k.
  • F0 and PMWW protocols: F0 is computed by columnwise OR operations followed by adjacent summations, with linearization applied to keep the resulting polynomial degrees controlled.The input is represented as a matrix whose entries indicate item occurrences in stream positions.

5 Experimental Evaluation

The experiments show that specialized protocols can substantially outperform general-purpose circuit checking, while verifier costs remain low. The main limitation is prover runtime in the general-purpose implementation, whereas specialized methods achieve high throughput and favorable scalability across several problems.

  • F2 protocols: Over 20 million items per second was processed by the F2 verifier, while interactive protocols used less than 1 kilobyte for space and communication.
  • F2 protocols: 350,000–750,000 items per second was achieved by the FFT-based non-interactive F2 prover, even for streams with billions of updates.
  • F2 protocols: Nearly 20,000 items per second was sustained by the circuit-checking prover across all stream lengths for F2.
  • MVMULT protocols: For MVMULT, the (n, n) protocol reached 30–50 million items per second when the verifier could use O(n) space.
  • F0 protocols: For F0, the bounded protocol dropped from about 80,000 to 1,600 items per second as F∞ increased from 30 to 200, while linearization was preferable beyond very small F∞.

6 Conclusion and Future Directions

The paper shows that engineered interactive-proof protocols can support practical delegated computation, while specialized protocols provide greater scalability. Future progress must address circuit-representation requirements and superlinear prover costs.

  • Interactive proof systems, combined with significant engineering, can yield protocols suitable for everyday use.
  • The verifier’s runtime is dominated by evaluating the input’s LDE at a point r, comparable to solving low-complexity problems directly with sufficient memory.
  • For superlinear computations, the verifier would save significant time and space compared with solving without a prover.
  • Reusing the same evaluation point can amortize LDE costs across non-interactive queries while maintaining soundness when the prover cannot observe acceptance outcomes.
  • The main obstacle to broader practicality is circuit representation together with the prover’s superlinear dependence on circuit size.

A Details for Theorems 3.2-3.4

The appendix provides an efficient instantiation of the cited construction, with efficient prover implementation and very efficient verification for a broad circuit class.

  • The instantiation makes the prover efficient and the verifier very efficient for a large class of arithmetic circuits.

A.1 Notation and Background

This section sets up layered arithmetic-circuit notation and the multilinear extensions used in the protocol’s sum-check polynomial.

  • The circuit is layered, has fan-in 2 over a field F, and is characterized by size S(n), depth d(n), and n input wires.
  • V_i(j) denotes the value of gate j at layer i, while ˜V_i is its multilinear extension over F^v.
  • At protocol iteration i, the sum-check protocol is applied to a 3v-variate polynomial f_i.
  • The polynomial combines wiring predicates with sums and products of multilinear gate-value extensions, plus a polynomial β(p) depending only on p.
  • The appendix first outlines how to engineer an efficient prover before giving the construction precisely.

A.2.1 High-level Outline

The high-level outline exploits multilinear wiring extensions so that circuit gates contribute sparsely and predictably during intermediate sum-check rounds.

  • A.2.1 High-level Outline: In each sum-check round, the prover sends a univariate polynomial derived from f_i.
  • A.2.1 High-level Outline: When wiring predicates are multilinear extensions, each gate at adjacent layers contributes to exactly one term in the sum.
  • A.2.1 High-level Outline: The multilinear wiring extension decomposes into variable-wise indicator functions, one for each relevant gate.
  • A.2.1 High-level Outline: During intermediate rounds, each current-layer gate contributes to the unique term matching its trailing binary-representation bits.

A.2.2 Decomposing

The multilinear extensions of the wiring predicates are decomposed into sums of indicator polynomials, with each gate contributing to the appropriate term.

  • χ_y is the unique multilinear polynomial that equals 1 on Boolean vector y and 0 on every other Boolean vector.It is constructed as a product of coordinate-wise factors χ_0(x_k)=1−x_k and χ_1(x_k)=x_k.
  • For fixed Boolean suffix x, χ_y evaluates to a product over the randomized prefix when y agrees with x on all remaining coordinates, and to 0 otherwise.This gives χ_y a variable-wise indicator interpretation on the Boolean-valued variables.
  • The multilinear extensions of add_i and multi_i are sums of χ_y terms, with each gate y at layer i−1 contributing one term.The resulting expressions agree with the original predicates on Boolean inputs, so they equal their multilinear extensions.
  • The construction introduces x* by replacing the first j Boolean coordinates with r_1,...,r_j while retaining the remaining coordinates of x.The associated set S_x contains layer i−1 gates whose final coordinates match x.

A.2.3 Completing the Calculation

The sum-check messages can be computed by aggregating gate contributions, allowing the prover to process adjacent circuit layers in single passes.

  • At round j, the prover computes the message polynomial g_j and needs only its evaluations at 0, 1, and 2.Because g_j has degree three under multilinear extensions, these three evaluations uniquely determine it.
  • Each gate at layer i−1 belongs to exactly one suffix class x, so it contributes to exactly one term in the sum defining g_j(r_j).The class x(y) is determined by the final 3v−j bits of the gate’s binary representation.
  • The evaluation combines the gate contributions with values of the multilinear extension at the points determined by the randomized prefix.The relevant points are partitioned into p*, ω_1*, and ω_2* components.
  • The prover can compute g_j(0), g_j(1), and g_j(2) in a single pass over the gates at layer i−1.The corresponding multilinear-extension values needed for each message can likewise be computed in one pass over layer i.

A.3 Finishing the Proofs of Theorems 3.2 and 3.3

Instantiating the protocol with multilinear wiring extensions yields a near-linear-time prover, while the verifier evaluates wiring predicates using logarithmic space.

  • O(S(n) log S(n)) prover time follows when the circuit uses multilinear extensions of its wiring predicate and gate-value function.The verifier can evaluate the required extensions through an implicit pass over each circuit layer using O(log S(n)) space.
  • The verifier can precompute wiring-extension evaluations before the online phase because they do not depend on the input or verifier randomness after the random points are fixed.Online verification then requires O(1) time per protocol round, for total time O(d(n) log S(n)).
  • The stronger implementation theorem reduces verifier space and time costs beyond the baseline guarantee, although greater time may be acceptable when streaming verification is more space-constrained.This trade-off is explicitly framed for streaming contexts.

A.4 Discussion and Formal Statement of Theorem 3.4

Theorem A.1 makes circuit checking practical when wiring extensions are efficiently evaluable, and the appendix shows this condition for the paper’s motivating circuits and space-bounded computations.

  • A.4 Discussion and Formal Statement of Theorem 3.4: O(S(n) log S(n)) prover time and O(log S(n)) verifier space are guaranteed for suitable log-space uniform circuits.The verifier time is O(n log n + d(n)poly(log S(n))), assuming small-space, polylog-time evaluation of each wiring extension.
  • A.4 Discussion and Formal Statement of Theorem 3.4: The theorem’s key assumption is that the multilinear wiring extensions can be evaluated quickly using small space, a condition argued to hold for many regular circuits.The appendix applies it to all four circuits considered in the paper.
  • A.4 Discussion and Formal Statement of Theorem 3.4: F2 uses one multiplication layer to square inputs followed by a binary addition tree that sums the squared frequencies.At the bottom multiplication layer, mult_d is true exactly when the two input gates and their parent have the same index, while add_d is zero.
  • A.4 Discussion and Formal Statement of Theorem 3.4: The F2 wiring predicate for addition connects each parent to consecutive children, with ω1=2p and ω2=2p+1 on Boolean inputs.The multilinear extension encodes parity and agreement of the higher-order bits and is evaluable in O(v)=O(log n) time and space.
  • A.4 Discussion and Formal Statement of Theorem 3.4: F0 computes a_i^(p−1) using repeated squaring and multiplication, then sums the results through a binary addition tree over the field with p=2^61−1.The special field value gives the exponent circuit a particularly regular structure used in the experiments.
  • A.4.3 More Efficient Protocols for Space-Bounded Computation: Theorem A.1 also applies to space-bounded computations whose circuits construct the transition matrix and obtain progressively shorter reachability matrices by repeated squaring.The wiring for these matrix layers resembles naive matrix-vector multiplication.
  • A.4.3 More Efficient Protocols for Space-Bounded Computation: For these circuits, intermediate wiring extensions use O(log S(n)) memory and poly(s(n)) time, while the final layer uses O(n·s(n) log n) time.This yields a prover running in O(S(n) log S(n)) time and a verifier using O(log S(n)) space.
  • A.4.3 More Efficient Protocols for Space-Bounded Computation: The improvement removes the superlinear-in-circuit-size prover overhead from the prior construction, reducing it to a logarithmic factor while retaining efficient verification.The circuit representation itself can still introduce overhead compared with the original uniform computation.
Loading 1105.2003v5…