Probabilistic Verification of Proofs

Madhu Sudan

Abstract. Recent research in the theory of computing has led to the following intriguing result. “There exists a probabilistic verifier for proofs of mathematical assertions that looks at a proof in only a constant number of bit positions and satisfies the following properties: (Completeness) For every valid theorem there exists a proof that is always accepted. (Soundness) For invalid assertions every purported proof is rejected with some positive probability that is independent of the length of the theorem or proof.” This result sheds insight into the fundamental complexity class NP and shows that it is equivalent to a seemingly smaller class of languages with efficient probabilistically checkable proofs. This result is especially significant to combinatorial optimization. For many combinatorial optimization problems it demonstrates that the task of finding even nearly-optimal solutions is computationally intractable. In this article we describe some methods used to construct such verifiers.

1991 Mathematics Subject Classification: 68Q10, 68Q15. Keywords and Phrases: Computational complexity, Algorithms, Combinatorial optimization, Logic, Probability, Approximation.

1 Introduction

The notion of efficient verification of proofs has been a central theme in the theory of computing. The computational view of this notion abstracts the semantics of the proof system into a verification procedure or verifier, i.e., a polynomial time computable Boolean function described by a Turing machine. A purported theorem T and proof π are then just a sequence of bits; π proves T if the verifier accepts the pair (T, π). The purported theorem T is true if such a proof π exists. The class NP [15, 32] represents the class of all theorems with “short” proofs; and allows for very simple combinatorial descriptions of theorems and proofs. As an example, we describe the problem 3-SAT.

A 3cnf formula ϕ is described by N “clauses” C_{1}, …, C_{N} on n Boolean variables x_{1}, …, x_{n}. A clause consists of up to 3 literals (i.e., a variable or its negation) and the clause is satisfied by some Boolean assignment to the variables if at least one literal is assigned a true value. The formula ϕ is said to be satisfiable, if there exists an assignment to the n variables which simultaneously satisfies all clauses. 3-SAT is the language of all satisfiable 3cnf formulae.

The NP-completeness of 3-SAT may be interpreted as follows: For any system of logic, there exists a polynomial time computable function f such given an assertion T in this system of logic and an integer n, f(T, 1^{n}) computes a 3cnf formula that is satisfiable if and only if T has a proof of length at most n. Thus, under the equivalence class of polynomial time computation, the satisfying assignment to f(T, 1^{n}) is a proof for the theorem T, and the statement f(T, 1^{n}) ∈ 3-SAT is itself the theorem. While this method of describing theorems and proofs is equivalent to any other system of logic it has some conceptual simplicity. One formal effect that captures this simplicity is that an incorrect proof has a very local error: Such an incorrect proof is an assignment that fails to satisfy at least one clause. Hence the three bits corresponding to the assignment to the variables participating in this clause point give the explicit error in the proof. In other words every incorrect proof has a witness of the error that is at most 3 bits long. This example demonstrates some of the power of the computational view of proofs.

Over the course of the last decade a number of new computational notions of proofs have been proposed and analyzed. The common theme in these definitions is a probabilistic verifier who is allowed some small probability of making an error. One of these notions, known as a probabilistically checkable proof (PCP), is motivated by the following informally stated question: “How fast can the verifier be compared to the size of the proof?” It is easy to establish that a deterministic verifier must at the very least “look” at the whole proof. This however need not be true for probabilistic ones. The notion of “looking at a bit of the proof”. can be formalized by providing the verifier with oracle access to the proof, i.e., the verifier can specify the address of a location of the proof and gets back the bit written in that location and this entire process takes only as much time as required to write the address. The number of bits of the proof that are “looked” at is now the number of oracle queries. To contrast such a verifier with the traditional verifier, one also quantifies the amount of randomness used by such a verifier. Thus we define (r(·), q(·))-restricted PCP verifier to be a probabilistic verifier with random access to a proof oracle, such that on input x of length n, the verifier tosses at most r(n) coins and accesses the oracle at most q(n) times, where the locations accessed are a function of the random coins. A language L is said to be in class PCP(r, q) if there exists an (r(·), q(·))-restricted PCP verifier V satisfying the following: If x ∈ L there exists an oracle π such that the verifier V accepts x with probability 1 on oracle access to π. If x ∉ L, for every π, V accepts x with probability at most 1/2. Notice that the verifier can make mistakes when x ∉ L. (The definition of a PCP as defined above is from [6]. Many components in this definition come from earlier works: The notion of probabilistic verifiers was first proposed in [25, 10], as part of a larger definition. The notion of oracle machine verifiers was proposed in [22]. The parameters of interest. i.e., r(·) and q(·), were implicit in [19]. A closely related definition focusing on different parameters, termed transparent proofs, was also studied by [9].)

It is immediate from the definition of PCP that NP = ∪_{c>0}PCP(0, n^{c}) (the verifier is not randomized, but is allowed unlimited access to the proof). The results of [8, 9, 19] showed that by allowing the verifier small amounts of randomness, the query complexity can be reduced dramatically and in particular NP ⊆ ∪_{c>0}PCP(c log n log log n, c log n log log n). Subsequently [6, 5] showed that it is possible to restrict the verifier even more significantly to just a constant number of queries (independent of the theorem, the proof or the system of axioms). They also reduce randomness to strictly logarithmic in input size. Specifically, they show

Theorem 1 ∃q < ∞ such that NP = ∪_{c>0}PCP(c log n, q).

The consequences to combinatorial optimization may be described informally as follows: The notion of a PCP verifier allows one to formalize the notion of an “approximately” correct proof; and the strong results obtained above show that such a proof exists if and only if a perfectly correct proof exists. Thus the task of finding an approximately correct proof is as hard as the task of finding a perfectly correct proof. The traditional connection between proofs and optimization [15, 29, 32] now indicates that for some optimization problems (unfortunately, not necessarily natural ones) finding near-optimal solutions should be as hard as finding optimal ones. The statement can actually be formalized and made applicable even to natural optimization problems. This connection was discovered by [19] and its applicability was further extended in [5] to apply to a large number of optimization problems considered in [34].

In this article we describe some of the methods used in the construction of probabilistically checkable proofs, from a very high level. In particular, we describe some of the properties that a probabilistically checkable proof must have. We also give a hint of how such properties are effected. The primary hope is to motivate the reader to read more detailed descriptions. The concluding section includes pointers for further reading as well as to more recent work.

2 Construction and verification of PCPs

In this section we will describe from a high-level the construction of a probabilistically checkable proof. Using the completeness of 3-SAT we will assume that we restrict our attention to theorems of the form ϕ ∈ 3-SAT, where ϕ is a 3cnf formula. It will be useful to think of ϕ as a function mapping {0, 1}^{n} to {0, 1}, using the association that 0 represents the Boolean false and 1 represents the Boolean true. ϕ(a⃗) = 1 if ϕ is satisfied by the assignment a⃗ ∈ {0, 1}^{n}. We will switch between 3 possible views of a, the proof of the theorem ϕ ∈ 3-SAT. a may be thought of as a string, as a vector (over some appropriate field containing 0 and 1), or as an oracle that on query i responds with the ith coordinate of a.

Recall that our goal is to describe an alternate proof for ϕ ∈ 3-SAT. More importantly we wish to describe a new probabilistic verifier V for proofs of satisfiability of 3cnf formulae. The verifier will make “few” queries to the new proof, an oracle A, and then cast a verdict. If ϕ ∉ 3-SAT, then no oracle satisfies the verifier with probability 1/2, while if ϕ ∈ 3-SAT, then there exists an oracle A such that V always accepts. In the latter case there exists a effective transformation T which transforms the proof a ∈ {0, 1}^{n} satisfying ϕ(a) = 1 into the the oracle A. It is this transformation that will be our primary focus. For reasons of space, we will focus on the weaker goal of describing a verifier V that makes only q = q(n) = (log n)^{O(1)} queries and the transformation T for such a verifier.

2.1 Motivation

We start by examining some properties such a transformation T necessarily exhibits. The first interesting property exhibited by A = T (a) is its redundancy. Let us view A as a string, and suppose Ã is a string obtained by randomly choosing a small fraction of the bits of A and changing them (from 0 to 1 and vice versa). A PCP verifier making q queries still accepts with probability the proof Ã with high probability, where this probability tends to 1 as the fraction of errors in the proof tend to 0. Furthermore it is possible to determine the acceptance probability of the verifier on string Ã in polynomial time. Thus even though Ã is far from A, it preserves its “meaning” (i.e., continues to prove the statement ϕ ∈ 3-SAT.) The easiest conceivable way to achieve such an effect is to insist that Ã preserves the original proof. i.e., a⃗ itself (despite the fact that 1% of its bits are erroneous). This leads us to the first property of the transformation T (·) that we will try to achieve. T is an \underline{error-correcting code}, i.e., for any two strings a_{1} and a_{2}, T (a_{1}) and T (a_{2}) differ in a constant fraction of the bits.

In particular this implies that T is an expansive mapping i.e., maps {0, 1}^{n} → {0, 1}^{N} for N > n and hence there are many strings in the range that T does not map to. Given a formula ϕ ∉ 3-SAT and a string Ã, the PCP verifier has to reject the offered proof with probability at least ϵ > 0 after reading just q bits in such a proof. Furthermore, when the verifier rejects the proof, it must offer an explicit error in the proof in the three bits it reads. The error described may either claim (1) Ã is not describing any string in the image of T; or (2) Ã may be the encoding of some string a⃗; but ϕ(a⃗) ≠ 1 for any such string.

To use error of the form (1) above with some string A, it must be that there exist indices i_{1}, …, i_{q} ∈ [N] such that for any string T (a⃗), the projection to the coordinates i_{1}, …, i_{q} does not agree with the projection of A to the same coordinates. We say that an error-correcting code T is \underline{q-locally checkable} if for every string A that is not in the range of T, there exist indices i_{1}, …, i_{q} ∈ [N] with this property. It will be our goal to come up with an appropriate q-locally checkable code T, for relatively small q.

Finally, T will need to have a “semantic” part: i.e., somehow T must be dependent on ϕ, in order for it to exploit the error condition in (2) above. Summarizing, in the next sections we will describe a transformation T that is an error-correcting code, with good local checkability, that will somehow reveal the truth of the statement ϕ ∈ 3-SAT.

2.2 The transformation

We start with a simple transformation which leads to some error-correction properties. (Here and later we use [n] to denote the set {1, …, n}.) The simplest method for adding some error-correcting feature to any information string is to encode it using the Reed-Solomon code. Specifically, to encode the information string a_{1}, …, a_{n} we pick a finite field F of order Ω(n) and an injective map b : [n] → F.

We then pick a polynomial P_{a} : F → F of degree at most n such that P_{a}(b(i)) = a_{i} for i ∈ [n] and our first transformation, denoted T_{1} is given by T_{1}(a) = (P_{a}(z))_{z∈F} be the encoding of a. Notice that the encoding does not give us a string in {0, 1}^{N}, but rather an element of F^{|F |} that we view as a string over F. Using the elementary property that two distinct degree n polynomials can agree in at most n places, we find that this transformation is very redundant. Specifically T_{1}(a_{1}) and T_{1}(a_{2}) have a Hamming distance of at least |F | − n when viewed as strings over F.

The above transformation has the right error-correcting property, but lacks local checkability. To get this additional property, we use the idea of encoding using multivariate polynomials. Specifically, we pick an integer m, and field F (whose size will be determined shortly), a set H ⊂ F, such that |H|^{m} ≥ n and an injective function b : [n] → H^{m}. To encode a string a⃗, we pick an m-variate polynomial P_{a} : F^{m} → F of degree |H| in each variable such that P_{a}(b(i)) = a_{i} for every i ∈ [n]. (It is easy to prove that such a polynomial P_{a} always exists.) The total degree of such a polynomial is at most m|H|. The encoding of a is then simply the string T_{2}(a) = (P_{a}(z_{1}, …, z_{m}))_{z_{1},...,z_{m}∈F}. Thus T_{2} : {0, 1}^{n} → F^{|F |^{m}} and satisfies the following distance property. For any pair of strings a_{1} and a_{2}, T_{2}(a_{1}) and T_{2}(a_{2}) agree in at most m|H|/|F | fraction of all indices, when viewed as strings over F. This property follows from a well-known extension of the distance property of polynomials to the multivariate case, which states that a (multivariate) polynomial of total degree d can be zero on at most d/|F | fraction of the domain.

The advantage in using the multivariate polynomials is that they exhibit significantly better local checkability properties. In particular, for every function Q : F^{m} → F that is not a polynomial of degree d, there exist d + 2 points that “prove” this property. We are now ready to describe some useful choices of m, |H| and |F |. (Incidentally, the choice of the function b : [n] → H^{m} does not affect the performance of the transformation T_{2} in any way.) To get a good locally checkable code one would like to minimize the degree which is at most m|H|. However, the choice has to satisfy |H|^{m} ≥ n. To ensure that T_{2}(a) is not too long compared to a, one needs to ensure that |F |^{m} is only polynomially larger |H|^{m}, which implies |F | should be a polynomial in |H|. Furthermore, to get a constant distance, |F | better be larger than the total degree (by at least a constant factor). One such choice of parameters is (we omit floors and ceilings in the following choices): m = \frac{log n}{log log n}, |H| = log n, and |F | = (log n)^{2}. This creates a transformation T_{2} which maps n bits to n^{2} elements from a field of size log^{2} n, with degree and hence q-local checkability for q ≤ log^{2} n.

We now bring in the semantic element to the error correcting code. This will take some development, so we first outline the plan for this stage. In the final construction T (a) = T_{ϕ}(a) will be a sequence of polynomials f_{0} : F^{m} → F and f_{1}, …, f_{k} : F^{m′} → F, described by their value at every input in F^{m′}. (k, m′ will be specified later.) The value of the polynomial f_{i} at some point u ∈ F^{m′}will be determined by a simple formula — or “construction rule” — applied to the value of the polynomial f_{i−1} at some l places ψ_{i,1}(u), …, ψ_{i,l}(u). (Again, l will be determined shortly.) The polynomial f_{0} will be T_{2}(a). The rules will be constructed so that f_{k} is identically zero if and only if a satisfies ϕ.

To get such a sequence, we start by “arithmetizing” the notion of a 3-SAT formula and the notion of satisfiability of a clause. Recall that a variable is specified by an index in [n] and thus a literal can be specified as an element of [n] × {0, 1}. A clause is a triple of literals and thus an element of [n]×[n]×[n]×{0, 1}^{3}. A 3cnf formula ϕ can thus be described by a function ϕ′ mapping [n] × [n] × [n] × {0, 1}^{3} to {0, 1}. ϕ′(i, j, k, b_{1}, b_{2}, b_{3}) = 1 iff the clause with literals (i, b_{1}), (j, b_{2}) and (k, b_{3}) occurs in ϕ. Using the function b : [n] → H^{m}, we can identify a clause with an element of H^{3m+3}. We say that a polynomial ϕ̂ : F^{3m+3} → F of degree less than |H| in each variable is the arithmetization of ϕ if ϕ′(i, j, k, b_{1}, b_{2}, b_{3}) = ϕ̂(b(i), b(j), b(k), b_{1}, b_{2}, b_{3}) for any i, j, k ∈ [n] and b_{1}, b_{2}, b_{3} ∈ {0, 1}. We will fix ϕ̂(u) = 0 for all other u ∈ H^{3m+3}. As claimed earlier, it can be shown that such a polynomial ϕ̂ does exist and that it can be computed in polynomial time from ϕ.

We now move on to the task of arithmetizing the notion of satisfiability. Given a clause C on literals (i, b_{1}) (j, b_{2}) and (k, b_{3}), and an assignment a_{1}, …, a_{n} that has been transformed by the transformation T_{2} into the polynomial f_{0} : F^{m} → F, notice that the formula (f_{0}(b(i)) − b_{1}) · (f_{0}(b(j)) − b_{2}) · (f_{0}(b(k)) − b_{3}) is 0 if and only if the clause C is satisfied. This leads us to the definition of the polynomial f_{1} : F^{3m+3} → F to be

f_{1}(u, v, w, b_{1}, b_{2}, b_{3}) = ϕ̂(u, v, w, b_{1}, b_{2}, b_{3})(f_{0}(u) − b_{1})(f_{0}(v) − b_{2})(f_{0}(w) − b_{3}) (1)

where u, v, w ∈ F^{m} and b_{1}, b_{2}, b_{3} ∈ F. By construction it is clear that f_{1} is a polynomial on m′ = 3m + 3 variables having degree at most 2|H| in each variable; and furthermore is identically zero on the domain H^{m′} if and only if ϕ is satisfied by the assignment a.

This is close in spirit to what we desire. In what follows, we will develop a sequence of polynomials which will move the condition on f_{1} being zero on the domain H^{m} to the condition that f_{m′+1} being zero on F^{m′}. This will be achieved inductively: specifically we will define f_{i} : F^{m′} → F to be such that f_{i+1} is zero on the domain F^{i} × H^{m−i} if and only if f_{i} is zero on the domain F^{i−1} × H^{m−i+1}. This is achieved by the following rule.

f_{i+1}(r_{1}, …, r_{i}; z_{i+1}, …, z_{m′}) = ∑_{j=1}^{|H|} r_{i}^{j} · f_{i}(r_{1}, …, r_{i−1}; ζ_{j}; z_{i+1}, …, z_{m′}), (2)

where ζ_{1}, …, ζ_{|H|} is any enumeration of the elements of H. It is easy to argue that the polynomials f_{i+1} satisfies the desired property by an inductive argument on i. This concludes the transformation T, that we summarize as follows: given ϕ, a, we pick a field F, a subset H, an integer m, an injective map b : [n] → H^{m} and an enumeration ζ_{1}, …, ζ_{|H|} of the elements of H. We then let f_{0} = T_{2}(a), f_{1} be as defined by (1), f_{2}, …, f_{m′+1} be as defined by (2) and let T (a) = (f_{0}, …, f_{m′+1}).

2.3 The verification

We now describe the verifier for the transformation T. The verifier will be given oracles for functions f_{0}, …, f_{m′+1} and needs to verify that (a) The oracles f_{i}, i ∈ {0, m′+1} describe polynomials of the correct degree. (b) For every i ∈ [m′+1], the polynomial f_{i} is constructed from p_{i−1} using (1) or (2) (as appropriate). (c) The polynomial f_{m′+1} is identically zero. Assuming that the functions f_{0}, …, f_{m′+1} are indeed polynomials of the correct degree, (b) and (c) can be verified very easily, probabilistically. To verify (c) the verifier queries the oracle f_{m′+1} at a randomly chosen input u ∈ F^{m′}. By the distance property of polynomials, if f_{m′+1} is not identically zero then f_{m′+1}(u) ≠ 0 with high probability. To check (b) the verifier checks that the appropriate rule (1) or (2) holds for the oracles f_{i+1} and f_{i} for randomly chosen u. If the polynomial f_{i+1} is not identical to the polynomial obtained by applying the rule to f_{i}, then this difference will be witnessed by the point u with high probability. (Once again the distance property of polynomial is being used here.)

Thus the entire verification process reduces to the task of checking condition (a). A test for this condition is termed a “low-degree test” and has been a subject of active investigation recently. Specifically a low-degree test probabilistically queries q locations in an oracle Q and behaves as follows: If Q is a polynomial of total degree d, then the test accepts with probability 1. If the test accepts with probability 1−δ, then there is a polynomial P : F^{w} → F such that Q and P agree in all but at most ϵ fraction of the inputs, where ϵ, δ are parameters associated with the test.

To test that Q is a polynomial of degree at most d, one exploits the geometry of the space F^{m} as follows: For u, v ∈ F^{m} and t ∈ F, let l_{u,v}(t) = u + tv and let the line through u with slope v, denoted l_{u,v}, be the parameterized set of points {l_{u,v}(t)|t ∈ F }. It is immediate that for any polynomial P : F^{m} → F of degree at most and a line l = l_{u,v}, the function P |_{l} : F → F given by P |_{l}(t) = P (l_{u,v}(t)) is a univariate polynomial of degree at most d. Based on this observation a low-degree test was proposed in [37]: “Pick u, v uniformly and independently at random from F^{m} and verify that the points {(t, Q(l_{u,v}(t))|t ∈ F } are described by a univariate polynomial of degree at most d.” It is clear that the tester makes |F | queries to the oracle for Q and accepts all degree d polynomials. The “converse” is harder to prove and we will not attempt to hint at the proof here. A sequence of results [37, 6, 5, 36, 7] concludes showing that this test works for every ϵ < δ < 1, provided |F | is polynomially larger that d/(1 − δ).

We are still not done, since the low-degree test does not guarantee that the oracle Q is always equal to a low-degree polynomial, but only close to one. To patch this problem, we again resort to the error-correcting nature of polynomials; by using a probabilistic (and highly-efficient) error-correcting algorithm C for lowdegree polynomials, due to [11]. C will have oracle access to some function Q : F^{w} → F and behave as follows on input u ∈ F^{w}: If Q is a degree d polynomial, it will return Q(u). If Q is ϵ-close to a degree d polynomial P, it will return P (u) or “error” with high probability (over its internal coin tosses). Again C uses the property of lines in F^{m}. “Given u⃗ ∈ F^{w} C picks at random v⃗ ∈ F^{w} and considers the function q(t) = Q|_{l_{u⃗,v⃗}}(t). If q is a polynomial in t of degree at most d, then outputs q(0) else outputs error.” A simple probabilistic argument shows that C has the desired properties for every ϵ < 1, provided F is large enough.

We are now ready to specify the complete PCP verifier for verifying ϕ ∈ 3-SAT. The verifier has access to the oracles f_{0}, …, f_{m′+1}. It performs a lowdegree test on every oracle f_{i}, i ∈ {0, …, m′ + 1}. If all low-degree tests pass, it then picks a random u ∈ F^{m′} and verifies that for every i that the oracles C^{f_{i+1}} satisfies the appropriate rule (1 or 2) w.r.t C^{f_{i}}. (Notice that we are now working with the oracles C^{f_{i}} rather than f_{i}. This is the right choice, since C^{f_{i}} is a polynomial — not merely close to one.) Finally it checks that C^{f_{m′+1}}(u) = 0. If all checks pass, then it accepts the proof, else it rejects the proof. Thus for the choices of m, |F | etc. as made above, the construction yields a verifier making a total of O(log^{c} n) queries to all the oracles, for some absolute constant c. A formalization of the arguments above yields (modulo the analysis of the low-degree test) that the verifier accepts incorrect proofs with probability o(1), as n → ∞. Thus we conclude:

Theorem 2 NP ⊆ PCP(O(log n), log^{c} n).

Notes The result from Theorem 2 is essentially due to [8, 9], though the randomness efficiency was not reduced to O(log n) until the work of [6]. To get the full effect of Theorem 1 a number of new ideas are required. A central theme is a paradigm to compose proof systems, developed by [6]. In addition [5] present two new PCP constructions to prove Theorem 1. The interested reader may read the original papers for further details. Additional details may be found in [1, 38].

Subsequently there has been a significant amount of work improving the constant q of Theorem 1. This quest was initiated in [13] and further pursued in [20, 14, 35, 12]. Recently, a surprisingly sharp result, essentially showing q = 3, has been obtained by [27] (see also [23] for a variant of this result). This work introduces novel techniques to analyze the soundness of verifiers and while the result does rely on some prior work, may be read completely independently.

The consequences to optimization problems have also improved significantly since the initial works of [19, 5]. In particular, a number of new optimization problems have been related to PCPs and sharp results obtained in [33, 3, 21, 18, 26, 39]. Detailed surveys of such connections are available in [4, 17]. The connections have also motivated some new systematic study of combinatorial optimization problems — see [16, 31, 30].

The renewed interest in the approximability of optimization problems has also resulted, surprisingly, in a new spurt in algorithmic results. Particularly striking results in this direction are [24, 2]. Some of these algorithmic results, in particular [28, 40], are needed to analyze the tightness of the new PCP constructions of [27].

References

[1] S. Arora. Probabilistic Checking of Proofs and Hardness of Approximation Problems. PhD thesis, U.C. Berkeley, 1994. Available from

    http://www.cs.princeton.edu/~arora.

[2] S. Arora. Polynomial-time approximation schemes for Euclidean TSP and other geometric problems. Proc. 37th Symposium on Foundations of Computer Science, IEEE, 1996.

Probabilistic Verification of Proofs 469

[3] S. Arora, L. Babai, J. Stern, and Z. Sweedyk. The hardness of approximate optima in lattices, codes, and systems of linear equations. J. Computer and System Sciences, 54(2):317-331, April 1997.

[4] S. Arora and C. Lund. Hardness of approximations. In Approximation Algorithms for NP-hard problems, D. Hochbaum, ed. PWS Publishing, 1996.

[5] S. Arora, C. Lund, R. Motwani, M. Sudan, and M. Szegedy. Proof verification and the hardness of approximations. To appear J. ACM, 45(3), 1998.

[6] S. Arora and S. Safra. Probabilistic checking of proofs: a new characterization of NP. J. ACM, 45(1):70-122, 1998.

[7] S. Arora and M. Sudan. Improved low degree testing and its applications. Proc. 29th Annual Symposium on Theory of Computing, ACM, 1997.

[8] L. Babai, L. Fortnow, and C. Lund. Non-deterministic exponential time has two-prover interactive protocols. Computational Complexity, 1:3-40, 1991.

[9] L. Babai, L. Fortnow, L. Levin, and M. Szegedy. Checking computations in polylogarithmic time. Proc. 23rd Annual Symposium on Theory of Computing, ACM, 1991.

[10] L. Babai and S. Moran. Arthur-Merlin games: a randomized proof system, and a hierarchy of complexity classes. J. Computer and System Sciences, 36(2):254-276, 1988.

[11] D. Beaver and J. Feigenbaum. Hiding instances in multioracle queries. Proc. Symposium on Theoretical Aspects of Computer Science, 1990.

[12] M. Bellare, O. Goldreich and M. Sudan. Free bits, PCPs and nonapproximability — towards tight results. SIAM J. Computing, 27(3):804-915, 1998.

[13] M. Bellare, S. Goldwasser, C. Lund, and A. Russell. Efficient probabilistically checkable proofs. Proc. 25th Annual Symposium on Theory of Computing, ACM, 1993.

[14] M. Bellare and M. Sudan. Improved non-approximability results. Proc. 26th Annual Symposium on Theory of Computing, ACM, 1994.

[15] S. Cook. The complexity of theorem-proving procedures. Proc. 3rd Annual Symposium on Theory of Computing, ACM, 1971.

[16] N. Creignou. A dichotomy theorem for maximum generalized satisfiability problems. J. Computer and System Sciences, 51(3):511-522, 1995.

[17] P. Crescenzi and V. Kann, A compendium of NP optimization problems. Technical Report, Dipartimento di Scienze dell’Informazione, Università di Roma “La Sapienza”, SI/RR-95/02, 1995. Available from

http://www.nada.kth.se/ viggo/problemlist/compendium.html.

[18] U. Feige. A threshold of ln n for Set Cover. Proc. 28th Annual Symposium on Theory of Computing, ACM, 1996.

[19] U. Feige, S. Goldwasser, L. Lovasz, S. Safra, and M. Szegedy. Interactive proofs and the hardness of approximating cliques. J. ACM, 43(2):268-292, 1996.

[20] U. Feige and J. Kilian. Two prover protocols — Low error at affordable rates. Proc. 26th Annual Symposium on Theory of Computing, ACM, 1994.

[21] U. Feige and J. Kilian. Zero knowledge and chromatic number. Proc. 11th Annual Conference on Structure in Complexity Theory, IEEE, 1996.

[22] L. Fortnow, J. Rompel, and M. Sipser. On the power of multi-prover interactive protocols. Theoretical Computer Science, 134(2):545-557, 1994.

470 Madhu Sudan

[23] V. Guruswami, D. Lewin, M. Sudan and L. Trevisan. A tight characterization of NP with 3 query PCPs. ECCC Tech. Report TR98-034, 1998. Available from

http://www.eccc.uni-trier.de/eccc/.

[24] M. Goemans and D. Williamson. Improved approximation algorithms for maximum cut and satisfiability problems using semidefinite programming. J. ACM, 42(6):1115-1145, 1995.

[25] S. Goldwasser, S. Micali, and C. Rackoff. The knowledge complexity of interactive proof-systems. SIAM J. Computing, 18(1):186-208, 1989.

[26] J. Håstad. Clique is hard to approximate within n^{1−ϵ}. Proc. 37th Symposium on Foundations of Computer Science, IEEE, 1996.

[27] J. Håstad. Some optimal inapproximability results. Proc. 29th Annual Symposium on Theory of Computing, ACM, 1997.

[28] H. Karloff and U. Zwick. A 7/8-approximation algorithm for MAX 3SAT? Proc. 38th Symposium on Foundations of Computer Science, IEEE, 1997.

[29] R. Karp. Reducibility among combinatorial problems. In R. E. Miller and J. W. Thatcher, editors, Complexity of Computer Computations, Advances in Computing Research, pp. 85-103. Plenum Press, 1972.

[30] S. Khanna, M. Sudan and L. Trevisan. Constraint satisfaction: The approximability of minimization problems. Proc. 12th Annual Conference on Structure in Complexity Theory, IEEE, 1997.

[31] S. Khanna, M. Sudan, and D. P. Williamson. A complete classification of the approximability of maximization problems derived from Boolean constraint satisfaction. Proc. 29th Annual Symposium on Theory of Computing, ACM, 1997.

[32] L. Levin. Universal’nyĭe perebornyĭe zadachi (Universal search problems : in Russian). Problemy Peredachi Informatsii, 9(3):265-266, 1973.

[33] C. Lund and M. Yannakakis. On the hardness of approximating minimization problems. J. ACM, 41(5):960-981, September 1994.

[34] C. Papadimitriou and M. Yannakakis. Optimization, approximation and complexity classes. J. Computer and System Sciences 43(3):425-440, 1991.

[35] R. Raz. A parallel repetition theorem. SIAM J. Computing, 27(3):763-803, 1998.

[36] R. Raz and S. Safra. A sub-constant error-probability low-degree test, and a subconstant error-probability PCP characterization of NP. Proc. 29th Annual Symposium on Theory of Computing, ACM, 1997.

[37] R. Rubinfeld and M. Sudan. Robust characterizations of polynomials with applications to program testing. SIAM J. Computing 25(2):252-271, 1996.

[38] M. Sudan. Efficient Checking of Polynomials and Proofs and the Hardness of Approximation Problems. ACM Distinguished Theses, Lecture Notes in Computer Science, no. 1001, Springer, 1996.

[39] L. Trevisan. When Hamming meets Euclid: The approximability of geometric TSP and MST. Proc. 29th Annual Symposium on Theory of Computing, ACM, 1997.

[40] U. Zwick. Approximation algorithms for constraint satisfaction problems involving at most three variables per constraint. Proc. 9th Annual Symposium on Discrete Algorithms, ACM-SIAM, 1998.

Madhu Sudan

LCS, MIT, 545 Technology Square Cambridge, MA 02139, U.S.A.

                  email:  madhu@lcs.mit.edu