in N) such that f is satisfiable if and
only if A has a proof of length at most N
(in V ). Thus the deep logical question
0
about the truth of A seems to reduce to
a merely combinatorial question about
the satisfiability of f. The natural evidence for the satisfiability of f would
be an assignment and this is what we
refer to as a “format” for proofs. The
advantage of this format is that in order
to reject an “erroneous proof,” that is,
an assignment x that fails to satisfy f,
one only needs to point to one clause
of f that is not satisfied and thus only
point to the three bits of the proof of
x that this clause depends on to reveal
the error. Thus errors are easily localized in this format.
Can one go further and even “find”
this error efficiently? This is where
PCPs come in. In what follows, we will
attempt to describe verifiers that can
verify proofs of satisfiability of 3CNF
formulae (noticing that by the discussion above, this is as general as verifying
proofs of any mathematical statement
in any formal system).
probabilistically checkable proofs. We
start by formalizing the notion of the
number of bits of a proof that are “read”
by the verifier. In order to do so, we allow
the verifier to have random access (
oracle access) to a proof. So while the proof
may be a binary string p = áp [ 1] . . . p []
ñ Î {0, 1} , the verifier gets to “read” the
ith bit of p by querying an “oracle” for
the ith bit of p and get p[i ] in response,
and this counts as one query.
PCPs are motivated by the question:
“how many bits of queries are really essential to gain some confidence into
the correctness of a theorem?” It is easy
to argue that if the verifier hopes to get
away by querying only a constant number of bits of the proof, then it cannot
hope to be deterministic (else a constant time brute force search would find
a proof that the verifier would accept).
So we will allow the verifier to be probabilistic, and also it to make mistakes
(with low probability). This leads us to
the notion of a PCP verifier.
Definition 2. 1. A PCP verifier of query
complexity q(n), and gap e (n) is a probabilistic algorithm V that, given as input
an assertion A Î {0, 1}n, picks a random
string R Î {0, 1}*, makes oracle queries
to a proof oracle p : { 1,…,} ® {0, 1} and
produces an accept/reject verdict.
Running time: V always runs in time
polynomial in n.
Query complexity: V makes q(n) queries
into the proof p.
proof size: grows polynomial in n.
Completeness: If A is a true assertion,
then there exists a proof p that the verifier
accepts on every random string R.
Soundness, with gap e (n): If A is not true,
then for every proof p , the probability, over
the choice of the randomness R, that the
verifier accepts at most 1 − e (n).
The above definition associates two
parameters to a PCP verifier, query
complexity, and gap. The query complexity is the number of bits of the
proof that the verifier “reads.” The gap
is related to the “error” probability of
the verifier, that is, the probability of
accepting false assertions. The larger
the gap, the smaller the error. Since the
definition above introduces several notions and parameters at once, let us use
a couple of simple examples to see what
is really going on.
The classical proof of satisfiability
takes a formula of length n, on up to n
variables and gives a satisfying assignment. The classical verifier, who just
reads the entire assignment and verifies
that every clause is satisfied, is also a
PCP verifier. Its query complexity q(n) is
thus equal to n. Since this verifier makes
no error, its gap is given by e (n) = 1.
Now consider a probabilistic version
of this verifier who chooses to verify
just one randomly chosen clause of the
given 3CNF formula. In this case the
verifier only needs to query three bits of
the proof and so we have q(n) = 3. How
about the gap? Well, if a formula is not
satisfiable, then at least one of the up
to n clauses in the formula will be left
unsatisfied by every assignment. Thus
once we fix a proof p, the probability that
the verifier rejects is least 1/n, the probability with which the verifier happens
to choose a clause that is not satisfied by
the assignment p. This corresponds to a
gap of e (n) = 1/n. (Unfortunately, there
do exist (many) unsatisfiable 3CNF formulae which have assignments that
may satisfy all but one clause of the formula. So the gap of the above verifier is
really Q(1/n).)
Thus PCP verifiers are just extensions of “classical verifiers” of proofs.
Every classical verifier is a PCP verifier
with high query complexity and no error
(that is, high gap), and can be converted
into one with low (constant!) query complexity with high error (tiny gap). Indeed
a smooth trade-off between the parameters can also be achieved easily. To
reduce the error (increase the gap) of a
PCP verifier with query complexity q and
gap e , we could just run this verifier several, say k, times on a given proof, and
reject if it ever finds an error. The new
query complexity is now kq and if the
theorem is not true then the probability
of detecting an error is now ( 1 − e )k. The
new error is approximately 1 − ke if k <<
1/e and thus the gap goes up by a factor
of roughly k.
The fundamental question in PCP
research was whether this trade-off was
essential, or was it possible to get high
gap without increasing the number
of queries so much. The PCP theorem
states that such proof systems can be
constructed!
Theorem 2. 2 (PCP Theorem3, 4, 12).
3SAT has a PCP verifier of constant query
complexity and constant positive gap.
There are two distinct proofs of this
theorem in the literature and both are
quite nontrivial. In Section 4 we will
attempt to give some idea of the two
proofs. But before that we will give a
brief history of the evolution of the notion of a PCP, and one of the principal
applications of PCPs in computer science. The exact constants (in the query
complexity and gap) are by now well
studied and we will comment on them
later in the concluding section.
history of definitions. The notion
of a PCP verifier appears quite natural
given the objective of “quick and dirty”
verification of long proofs. However,
historically, the notion did not evolve
from such considerations. Rather the
definition fell out as a byproduct of investigations in cryptography and computational complexity, where the notion of a PCP verifier was one of many
different elegant notions of probabilistic verification procedures among
interacting entities. Here we attempt
to use the historic thread to highlight
some of these notions (see Goldreich18
for a much more detailed look into
these notions). We remark that in addition to leading to the definition of
PCPs, the surrounding theory also
influences the constructions of PCP