9 Interactive proofs and PCPs
This chapter covers interactive proof systems (\(\mathsf{IP}\), \(\mathsf{MA}\), \(\mathsf{AM}\)) and probabilistically checkable proofs. Verifiers are machine-free: a verifier is a polynomial-time function or a language in \(\mathsf{P}\) applied to an encoded view, and its coins are a uniformly random point of \(\{ 0,1\} ^t\). Formalized so far: the three interactive classes with completeness \(2/3\) and soundness \(1/3\), \(\mathsf{P} \subseteq \mathsf{MA}\) and \(\mathsf{P} \subseteq \mathsf{AM}\), \(\mathsf{IP} \subseteq \mathsf{PSPACE}\) by evaluating the protocol’s game tree, the one-variable multilinear extension, and the PCP theorem \(\mathsf{NP} = \mathsf{PCP}(O(\log n), O(1))\) (completeness \(1\), soundness \(1/2\)) with a constructible randomness bound, proved along Dinur’s gap-amplification route. The main open direction is \(\mathsf{PSPACE} \subseteq \mathsf{IP}\) (hence \(\mathsf{IP} = \mathsf{PSPACE}\)) through sum-check and arithmetization, followed by hardness of approximation built on the PCP theorem.
9.1 Interactive protocols
A transcript is a list of messages (bit strings); the verifier speaks at even positions and the prover at odd ones. A prover strategy is an arbitrary function from the visible transcript to the next message; it never sees the verifier’s coins, and it is bounded by \(m\) if the message it returns on every transcript has length at most \(m\). A protocol consists of a round count, a coin count \(c\) and a message-length bound (functions of the input length), a next-message function in \(\mathsf{FP}\) applied to the encoded view \(\mathrm{pair}(\mathrm{pair}(x, r), \langle \tau \rangle )\) of the input \(x\), the private coins \(r\) and the transcript \(\tau \) (where \(\langle \tau \rangle \) is the rose-tree serialization of \(\tau \)), a proof that for every \(x\), \(r\) and \(\tau \) the verifier’s message has length at most the message bound at \(|x|\), and a verdict language in \(\mathsf{P}\). Each round appends the verifier’s message, computed from the current view, and then the prover’s reply to the transcript extended by that message. The verifier accepts if the view of the transcript after the round count at \(|x|\) many rounds lies in the verdict language, and the accept event is the set of coin strings \(r \in \{ 0,1\} ^{c(|x|)}\) on which it accepts.
\(L \in \mathsf{IP}\) if some protocol whose round count, coin count \(c\) and message bound \(m\) are given by polynomials with natural-number coefficients satisfies: for \(x \in L\) some strategy bounded by \(m(|x|)\) is accepted with probability at least \(2/3\), and for \(x \notin L\) every strategy bounded by \(m(|x|)\) is accepted with probability at most \(1/3\), the probability being over uniform \(r \in \{ 0,1\} ^{c(|x|)}\). The counts are required to be polynomials, not merely polynomially bounded, so that the verifier can compute them.
\(L \in \mathsf{MA}\) if there are a polynomial \(p\) with natural-number coefficients and \(V \in \mathsf{P}\) such that for \(x \in L\) some proof \(w\) with \(|w| \le p(|x|)\) makes \(\mathrm{pair}(\mathrm{pair}(x, w), r) \in V\) for at least \(2/3\) of the \(r \in \{ 0,1\} ^{p(|x|)}\), and for \(x \notin L\) every such proof does so for at most \(1/3\) of them. \(L \in \mathsf{AM}\) if the coins \(r\) come first and are public: the fraction of \(r \in \{ 0,1\} ^{p(|x|)}\) admitting some reply \(w\) with \(|w| \le p(|x|)\) and \(\mathrm{pair}(\mathrm{pair}(x, r), w) \in V\) is at least \(2/3\) for members and at most \(1/3\) for non-members.
\(\mathsf{P} \subseteq \mathsf{MA}\) and \(\mathsf{P} \subseteq \mathsf{AM}\).
Take \(p = 0\), so there are no coins and the proof or reply is empty; the verifier decides the input it recovers from the encoded view, so the acceptance probability is \(1\) on members and \(0\) on non-members.
The transcript after \(n\) rounds has length exactly \(2n\). If two strategies agree on all transcripts of length at most \(2n\), then for every input and every coin string the transcripts after \(n\) rounds coincide. Hence acceptance and the accept event on input \(x\) depend on the strategy only through its values on transcripts of length at most twice the round count at \(|x|\).
Induction on the number of rounds; the transcript after \(n\) rounds has length exactly \(2n\).
Fix a protocol, an input \(x\), a coin count \(t\) and a message bound \(m\). A coin string \(r \in \{ 0,1\} ^t\) is consistent with a transcript \(\tau \) if every verifier message recorded in \(\tau \) is the one the verifier sends on coins \(r\). Define \(\mathrm{gval}\) at a transcript \(\tau \) by recursion on the number of remaining rounds: with none left it counts the coin strings consistent with \(\tau \) on which the verdict accepts the view of \(\tau \), and otherwise it sums, over the verifier messages that the consistent coin strings produce next, the maximum over replies of length at most \(m\) of the value one round down. Let \(\mathrm{gval}(x)\) be its value at the root: coin count \(c(|x|)\), message bound and round count at \(|x|\), and the empty transcript. Then every strategy bounded by the message bound at \(|x|\) has at most \(\mathrm{gval}(x)\) accepting coin strings, and a bounded strategy chosen for \(x\) (a maximizing reply at every node) has exactly \(\mathrm{gval}(x)\).
Induction on the remaining rounds; the maximizing reply is chosen node by node.
If a protocol and a language \(L\) satisfy the completeness and soundness conditions of \(\mathsf{IP}\) (no polynomial bound on the counts is needed), then for every \(x\), \(x \in L\) if and only if \(2^{c(|x|)} {\lt} 2\, \mathrm{gval}(x)\), where \(c\) is the coin count and \(\mathrm{gval}(x)\) is the root value of Lemma 360. In particular, for every \(L \in \mathsf{IP}\) there is a protocol with this property.
By the lemma, the root value is the largest accepting count of a bounded strategy. Completeness puts it at least two thirds of the coin space on members and soundness at most one third on non-members, so comparing it with half the coin space separates them.
\(\mathsf{IP} \subseteq \mathsf{PSPACE}\).
The game value is written as nested counter loops and walked depth-first on a stack with one frame per round; one step of the walk is a polynomial-time function, and Lemma 217 turns the iteration into a polynomial-space machine.
If \(\mathsf{PSPACE} \subseteq \mathsf{IP}\), then \(\mathsf{IP} = \mathsf{PSPACE}\). The hypothesis is also recorded, unproved, as the proposition PSPACESubsetIP, and the conclusion is stated from either form.
Antisymmetry with Theorem 362.
\(\mathsf{IP}(c, s)\), \(\mathsf{MA}(c, s)\) and \(\mathsf{AM}(c, s)\): the classes with completeness \(c\) and soundness \(s\) as parameters, together with monotonicity in both thresholds and the identification of the hard-wired classes with \(c = 2/3\), \(s = 1/3\).
For constants \(0 \le s {\lt} c \le 1\) and every polynomial \(q\), \(\mathsf{IP}(c, s) = \mathsf{IP}(1 - 2^{-q(n)}, 2^{-q(n)})\): run the protocol sequentially polynomially many times and accept by a threshold vote.
Soundness against an adaptive prover needs the conditional per-run bound across rounds, not only independence of the coins; strategy extensionality lets each run’s strategy be read off the combined one.
\(\mathsf{NP} \subseteq \mathsf{MA}\).
Merlin sends the NP witness and Arthur ignores his coins.
\(\mathsf{MA} \subseteq \mathsf{IP}\).
A one-round protocol with an empty verifier message; the prover’s reply is Merlin’s proof, which cannot depend on the private coins.
\(\mathsf{NP} \subseteq \mathsf{IP}\).
Compose the two inclusions.
9.2 Algebraic tools and IP = PSPACE
For \(f : \{ 0,1\} \to R\) with \(R\) a commutative ring, let \(\widetilde{f} : R \to R\) be \(\widetilde{f}(x) = f(0)(1 - x) + f(1)\, x\). Then \(\widetilde{f}(0) = f(0)\) and \(\widetilde{f}(1) = f(1)\), so \(\widetilde{f}\) agrees with \(f\) at both Boolean points.
Direct computation.
For \(f : \{ 0,1\} ^m \to \mathbb {F}\), the multilinear extension \(\widetilde{f}(x) = \sum _{b \in \{ 0,1\} ^m} f(b) \prod _i (b_i x_i + (1 - b_i)(1 - x_i))\), with the facts that it agrees with \(f\) on the cube and is the unique multilinear polynomial doing so.
If \(p\) is a nonzero polynomial over a finite field \(\mathbb {F}\) of total degree at most \(d\) in \(m\) variables, a uniformly random point of \(\mathbb {F}^m\) is a root with probability at most \(d / |\mathbb {F}|\); in particular a nonzero univariate polynomial of degree \(d\) has at most \(d\) roots. Mathlib provides the counting statement for MvPolynomial (MvPolynomial.schwartz_zippel_totalDegree, over an integral domain with points drawn from \(S^m\) for a finite set \(S\)); nothing in this node is formalized in the library yet, and what remains is the bridge to the library’s finite probability over encoded coin strings.
For a polynomial \(g\) in \(m\) variables over \(\mathbb {F}\) with individual degree at most \(d\), given by an evaluation oracle, and a claimed value \(v\) of \(\sum _{b \in \{ 0,1\} ^m} g(b)\): in round \(i\) the prover sends a univariate polynomial \(h_i\) of degree at most \(d\), the verifier checks \(h_i(0) + h_i(1)\) against the current claim, and replaces the claim by \(h_i(r_i)\) for a random \(r_i \in \mathbb {F}\); at the end it checks \(g(r_1, \dots , r_m)\) against the last claim.
If the claim is correct, the honest prover is accepted with probability \(1\). If it is incorrect, every prover is accepted with probability at most \(m d / |\mathbb {F}|\).
Round-by-round invariant: a false claim stays false unless the verifier hits a root of the difference between the prover’s polynomial and the true one.
Map a QBF to an expression over \(\mathbb {F}\): \(\neg a \mapsto 1 - a\), \(a \wedge b \mapsto ab\), \(\forall x\, \varphi \mapsto \varphi |_{x=0} \cdot \varphi |_{x=1}\), \(\exists x\, \varphi \mapsto 1 - (1 - \varphi |_{x=0})(1 - \varphi |_{x=1})\), interleaved with linearization operators \(L_{x}\, p = (1 - x)\, p|_{x=0} + x\, p|_{x=1}\) that keep every intermediate polynomial of individual degree at most \(2\).
On Boolean points the arithmetized expression takes the value \(1\) exactly on true formulas and \(0\) otherwise, linearization does not change values on Boolean points, and with linearization every polynomial the protocol handles has individual degree at most \(2\) and total size polynomial in the formula.
\(\mathsf{TQBF} \in \mathsf{IP}\), with polynomial verifier time, polynomial communication, perfect completeness and soundness error bounded away from \(1\), over a field whose size dominates the degree and soundness parameters and admits a polynomial-size encoding.
Run a sum-check-style round for each quantifier and linearization operator, from the outside in. Naive arithmetization without degree reduction has exponential degree, which is why the degree-control lemma is a separate node.
\(\mathsf{PSPACE} \subseteq \mathsf{IP}\). The statement is recorded, unproved, as the proposition PSPACESubsetIP of Proposition 363.
Compose a polynomial-time reduction to TQBF with the TQBF protocol; \(\mathsf{IP}\) is closed under polynomial-time many-one reductions.
\(\mathsf{IP} = \mathsf{PSPACE}\).
Apply Proposition 363.
9.3 Probabilistically checkable proofs
A PCP verifier is non-adaptive: it has a list of proof positions (natural numbers) for each input \(x\) and coin string \(r\), together with an \(\mathsf{FP}\) function mapping \(\mathrm{pair}(x, r)\) to the rose-tree serialization of that list, and a verdict language in \(\mathsf{P}\) that decides \(\mathrm{pair}(\mathrm{pair}(x, r), a)\), where \(a\) lists the bits of the proof (a finite bit string) found at those positions. A position past the end of the proof reads as \(0\). The verifier is query-bounded by \(q\) if it reads at most \(q(|x|)\) positions for every \(x\) and every coin string \(r\).
For arbitrary functions \(r, q : \mathbb {N} \to \mathbb {N}\), \(L \in \mathsf{PCP}(r, q)\) if some verifier query-bounded by \(q\), using exactly \(r(|x|)\) uniformly random coins, accepts some proof of each \(x \in L\) with probability \(1\), and accepts every proof of each \(x \notin L\) with probability at most \(1/2\).
A function \(r\) is constructible if \(x \mapsto 1^{r(|x|)}\) is in \(\mathsf{FP}\).
\(\mathsf{P} \subseteq \mathsf{PCP}(r, q)\) for all \(r\) and \(q\), and \(\mathsf{PCP}(r, q) \subseteq \mathsf{PCP}(r, q')\) whenever \(q \le q'\) pointwise.
For the first, a verifier that reads nothing, ignores its coins and decides the input it recovers from the encoded view. For the second, the same verifier meets any pointwise larger query bound. Monotonicity in the coin count is not formalized.
For every set \(A \subseteq \mathbb {N}\), computable or not, the language \(\{ x : |x| \in A\} \) lies in \(\bigcup \mathsf{PCP}(r, q)\) over all \(r = O(\log n)\) and \(q = O(1)\), with no constructibility requirement on \(r\).
Use the indicator of \(A\) as the coin count, the zero query bound, and a verifier that reads nothing and accepts exactly when it received one coin. Since there are uncountably many sets \(A\) and \(\mathsf{NP}\) is countable, the unrestricted union is not \(\mathsf{NP}\); this consequence is argued in the documentation, not stated in Lean.
For a rational \(s\), let \(\mathsf{PCP}_s(r, q)\) be the class with soundness error \(s\) in place of \(1/2\), so \(\mathsf{PCP}_{1/2}(r, q) = \mathsf{PCP}(r, q)\). If \(r\) is constructible and \(0 \le s\), then \(\mathsf{PCP}_s(r, q) \subseteq \mathsf{PCP}_{s^2}(2r, 2q)\). Consequently, if \(r\) is constructible and \(0 \le s {\lt} 1\), every language in \(\mathsf{PCP}_s(r, q)\) is in \(\mathsf{PCP}(2^j r, 2^j q)\) for some \(j \in \mathbb {N}\).
Running the verifier twice on independent coins squares the error and keeps perfect completeness; the coin string is split at the constructible per-run count, and doubling keeps the bound constructible. After \(j\) doublings the error is \(s^{2^j} \le s^j\), which is below \(1/2\) for large \(j\).
A constraint graph over an alphabet \(\Sigma \) has vertices \(\{ 0, \dots , V - 1\} \) and finitely many indexed directed edges (parallel edges and self-loops allowed), each carrying a Boolean-valued binary constraint on the labels of its tail and head. It is satisfiable if some labelling of the vertices satisfies every edge. For finite nonempty \(\Sigma \), its unsatisfiability value is the least, over all labellings, of the fraction of edges left unsatisfied (taken to be \(0\) for an edgeless graph); it is \(0\) exactly when the graph is satisfiable.
There are a fixed finite alphabet, constants \(0 {\lt} \gamma \le 1\) and \(c\), and a map \(\varphi \mapsto G_\varphi \) from CNF formulas to constraint graphs over that alphabet such that: for every CNF \(\varphi \) with \(m\) clauses, \(G_\varphi \) has at most \((6m + 2)^{c} \cdot 3m\) edges; and for every \(\varphi \) in which every clause has exactly three literals, \(G_\varphi \) is satisfiable if \(\varphi \) is, and the unsatisfiability value of \(G_\varphi \) is at least \(\gamma \) if \(\varphi \) is unsatisfiable. The map is defined as a noncomputable mathematical reduction; the polynomial-time counterpart used for the PCP theorem is built from the same amplifier inside the proof of Theorem 387.
An amplifier is a transformation of constraint graphs over a fixed alphabet that multiplies the edge count by at most a constant, preserves satisfiability, and maps unsatisfiability value \(v\) to at least \(\min (\gamma , 2v)\). Dinur’s round (expander preprocessing, graph powering, and alphabet reduction through a Hadamard-code assignment tester, over an explicit expander family) is one. Iterating it \(k\) times on a graph with at most \(2^k\) edges gives the dichotomy: satisfiable graphs stay satisfiable and unsatisfiable ones reach value at least \(\gamma \). Apply it to the \(3m\)-edge constraint graph of the formula with \(k = \lfloor \log _2 3m \rfloor + 1\).
For every \(L \in \mathsf{NP}\) there are a constructible \(r\) with \(r = O(\log n)\) and a \(q\) with \(q = O(1)\) such that \(L \in \mathsf{PCP}(r, q)\). Here \(f = O(g)\) means \(f(n) \le C\, g(n)\) for some constant \(C\) and all sufficiently large \(n\), and \(\log n\) is \(\lfloor \log _2 n \rfloor \); the \(q\) produced is a constant function.
Map each input, by an \(\mathsf{FP}\) function, to an exact-3CNF that is satisfiable exactly when the input is in \(L\) (Cook–Levin followed by Tseitin splitting). Pad its constraint graph to a size fixed by the input length and compute the gap constraint graph by a polynomial-time implementation of every round of Dinur’s amplifier (the amplifier of Theorem 386, over its explicit expander family). The verifier picks a random edge from logarithmically many coins and reads the fixed-width labels of its two endpoints, so members are accepted with probability \(1\) and non-members with probability bounded away from \(1\); Lemma 384 brings the soundness error below \(1/2\).
If \(r\) is constructible, \(r = O(\log n)\) and \(q = O(1)\) (in the sense of Theorem 387), then \(\mathsf{PCP}(r, q) \subseteq \mathsf{NP}\).
The verifier’s behaviour on all \(2^{r(n)} = \mathrm{poly}(n)\) coin strings is determined by a polynomial-size table listing, for each coin string, the answers to its constantly many queries. The witness is such a table; a polynomial-time check, which uses constructibility to write out \(2^{r(n)}\), verifies its length, its consistency (a position queried under two coin strings gets the same answer), and acceptance on every coin string. A member has such a table by perfect completeness; a non-member has none, since a consistent table gives a proof accepted with probability \(1 {\gt} 1/2\).
\(\mathsf{NP} = \bigcup \mathsf{PCP}(r, q)\), the union over all constructible \(r\) with \(r = O(\log n)\) and all \(q\) with \(q = O(1)\) (in the sense of Theorem 387; no constructibility is required of \(q\)).
The two inclusions. The constructibility requirement on \(r\) cannot be dropped, by Proposition 383.
9.4 Hardness of approximation
For \(0 \le s {\lt} c \le 1\) and fixed arity and alphabet, \(\mathrm{Gap}_{c,s}\)-CSP is the promise problem whose yes-instances are encoded constraint systems with value at least \(c\) and whose no-instances have value less than \(s\). \(\mathrm{Gap}\)-MAX-3SAT\(_{1,s}\) separates satisfiable 3CNFs from those in which every assignment satisfies fewer than an \(s\) fraction of the clauses.
There is \(\varepsilon {\gt} 0\) such that \(\mathrm{Gap}\)-MAX-3SAT\(_{1, 1 - \varepsilon }\) is NP-hard under polynomial-time reductions to the promise problem.
Turn each random string of the PCP verifier into a constant-size CNF over the proof bits, then convert to 3CNF; the constant soundness gap becomes a constant fraction of violated clauses. The equivalence between PCP characterizations and gap-CSP hardness is the reusable statement.
A label-cover instance is a bipartite constraint graph with label sets \(\Sigma _A\), \(\Sigma _B\) whose constraints are projections \(\pi _e : \Sigma _A \to \Sigma _B\); its value is the largest fraction of edges satisfied by a labelling.
For some constant \(\delta {\lt} 1\) and constant-size label sets, distinguishing label-cover instances of value \(1\) from those of value at most \(\delta \) is NP-hard.
The clause–variable game on a gap-3SAT instance.
For every label-cover instance of value at most \(\delta {\lt} 1\), its \(k\)-fold parallel repetition has value at most \(\delta '^{\, k}\) for a constant \(\delta ' {\lt} 1\) depending only on \(\delta \) and the label-set sizes. Hence gap label cover with arbitrarily small constant soundness is NP-hard.
Raz’s theorem, or a simpler projection-game variant with a weaker exponent.