IP = PSPACE using Error Correcting Codes

by Or Meir (see ECCC's TR10-137)

Oded's comments

This work may interest only those who know the proof of the fact that PSPACE has interactive proof systems, and wonder "why does this fundamental fact hold" (and/or what makes it possible). Or's answer is that an interactive proof of QBF (or un-SAT) may proceed by considering two different encodings of the underlying formula, where both encodings use rather arbitrary tensor codes (i.e., high-dimensional tensor products of some very simple and rather general codes). One tensor code is used to directly encode the truth-table of the formula, and the other codeword is consistent with the said truth-table on the Boolean subcube but is locally computable (i.e., given the formula one can easily compute the value of the codeword at any coordinate). Indeed, the codewords in both codes are of exponential length, and the interactive proof refers to claims regarding these codewords (e.g., the sum of the values of certain sub-cubes). The celebrated sum-check is used to translate claims regarding the value of the first code at any coordinate into claims on the value of the second code at other coordinates.

Thus, Or's answer is that it is all about tensor codes; indeed, the notion of a tensor code and some basic properties of it are all that one needs in order to estbalish IP=PSPACE. Specifically, tensor codes are the natural setting for the application of the sum-check, and they allow to enforce equality amoung auxiliary variables (copies of a variable), which in turn is the source of discrepancy between the two aforementioned encodings.

Being among the researchers that were most annoyed at the mysterious role of polynomials in the original proof of IP=PSPACE, I find the replacment of polynomials by tensor codes and the way in which the latter are used in Or's proof most pleasing. In particular, the reference to the partial (sub-cubes) sums of the values of the corresponding codewords is most natural, since Boolean sub-cubes correspond to partial assignments whereas non-Boolean coordinates are merely parity check values.

The original abstract

The IP theorem, which asserts that IP = PSPACE (Lund et. al., and Shamir, in J. ACM 39(4)), is one of the major achievements of complexity theory. The known proofs of the theorem are based on the arithmetization technique, which transforms a quantified Boolean formula into a related polynomial. The intuition that underlies the use of polynomials is commonly explained by the fact that polynomials constitute good error correcting codes. However, the known proofs seem tailored to the use of polynomials, and do not generalize to arbitrary error correcting codes. In this work, we show that the IP theorem can be proved by using general error correcting codes. We believe that this establishes a rigorous basis for the aforementioned intuition, and sheds further light on the IP theorem.
Back to list of Oded's choices.