Here are two graphs. Same number of vertices, same number of edges, but not the same graph: no relabeling of vertices turns one into the other. Can you prove it?
With a short classical proof, you're stuck. Proving two graphs the same is easy, just show the mapping; that is an NP certificate. But proving them different? There is no short certificate anyone knows how to write. And yet a five-minute conversation can do what no short written proof can.
The quiz#
The verifier has two graphs, and . The prover claims they are not isomorphic, and the verifier doesn't trust the prover. So the verifier secretly picks one at random, , shuffles its vertices with a random permutation, sends the scramble over, and asks: which graph did I start from?
This is a quiz. The verifier already knows the answer. The question is whether the prover does too. If the graphs really are non-isomorphic, the scrambled graph is isomorphic to exactly one of them, and an all-powerful prover can check both and answer correctly every time. But if the graphs are actually isomorphic, a random permutation of has exactly the same distribution as a random permutation of . The prover has no information about , and any strategy succeeds with probability at most . Repeat: ten rounds, and a cheating prover's odds fall below one in a thousand.
The verifier used two things classical proofs don't have. Randomness created a challenge it already knew the answer to. Interaction forced the prover to demonstrate knowledge instead of handing over a certificate.
The definition#
Goldwasser, Micali, and Rackoff introduced the model in 1985. The prover is computationally unbounded; the verifier is a probabilistic polynomial-time machine; they exchange messages for some number of rounds. Completeness: on a yes-instance, the honest prover makes the verifier accept with probability at least . Soundness: on a no-instance, no prover, however powerful, makes the verifier accept with probability more than . As with BPP, the constants are arbitrary; any gap amplifies by repetition. The definition is asymmetric, and the asymmetry is the point. Completeness needs one specific prover to succeed; soundness must hold against every possible prover. IP is the class of languages with interactive proofs over polynomially many rounds.
After the definition came a consensus about its limits. Babai independently introduced Arthur-Merlin games, where the verifier's coins are public, and proved that any constant number of rounds collapses to AM; Goldwasser and Sipser showed hiding the coins doesn't help. So constant-round interaction gives AM, believed to sit inside the polynomial hierarchy, not far above NP. Most researchers expected that was the whole story: IP was probably just AM.
In 1990, Lund, Fortnow, Karloff, and Nisan shattered that expectation. With a technique called the sum-check protocol, they proved that counting the satisfying assignments of a Boolean formula, a sharp-P-complete problem, has an interactive proof; co-NP is therefore inside IP, and if the polynomial hierarchy doesn't collapse, IP extends far beyond AM. Within weeks, Shamir pushed the technique to the full answer: IP equals PSPACE. Every problem solvable in polynomial space, a class containing NP, co-NP, and the entire polynomial hierarchy, has an interactive proof.
Arithmetization#
The proof rests on one algebraic idea: lift Boolean formulas into polynomials. A Boolean formula lives on the hypercube, just zeros and ones, and checking every point would take exponential time. But over a larger domain, two distinct low-degree polynomials can agree on only a few points, so evaluating at a random point exposes a fake almost surely. That is the crack the verifier exploits.
Work over a finite field , the integers modulo a large prime. Translate the formula: becomes , becomes , and becomes . On zero-one inputs these agree with the logic, but the polynomial is defined over all of . Quantifiers translate too: an existential becomes a sum over , a universal becomes a product. A quantified Boolean formula becomes nested sums and products of a polynomial over a finite field.
The sum-check protocol#
Now the engine. Think of it as an audit: the prover claims a huge sum, far too large for the verifier to compute directly. The verifier forces the prover to break the sum down one variable at a time, checking a random spot at each step; any fudged line is almost certainly caught.
Both parties know a polynomial in variables over . The prover claims a value for
a sum of terms. In round one, the prover sends a univariate polynomial , claimed to equal the sum of with the first variable set to and the rest summed over the Boolean cube. The verifier checks , which must hold because summing both values of accounts for every term; if it fails, reject. Then the verifier picks a random field element , reducing the claim to the value of , a statement of the same shape in one fewer variable. Each round pins down one more variable, until after rounds the verifier checks the final claim by evaluating itself.
Why is this sound? A lying prover has sent a polynomial different from the true one, and two distinct polynomials of degree agree on at most points. The chance the random challenge lands on a point of agreement is at most , so over rounds the total cheating probability is at most . Choose much larger than and the protocol is sound.
Pause and try: why do two distinct degree-d polynomials agree on at most d points?
Let and be distinct univariate polynomials of degree at most . Their difference is nonzero with degree at most , so it has at most roots, and every point of agreement is a root. A uniformly random challenge from a field of size hits one with probability at most .
Taming the degree#
One direction of IP equals PSPACE is straightforward: the whole interaction can be simulated in polynomial space, computing the optimal prover strategy by exhaustive search over responses. The hard direction is giving an interactive proof for TQBF, true quantified Boolean formulas, the PSPACE-complete problem of deciding sentences like: for all , there exists , for all , and so on.
Arithmetize, and the quantifiers become alternating sums and products. The sum-check protocol handles sums beautifully, but products are a wall. Taking the product over multiplies two polynomials, doubling the degree in the remaining variables; after many quantifiers the degree grows exponentially, and sum-check soundness needs degree small compared to the field size.
Shamir found the way through; Alexander Shen soon simplified it to the version everyone teaches. After each quantifier, apply a linearization operator: for variable , replace with the unique polynomial linear in that agrees with at and , namely
On Boolean inputs this changes nothing, but the degree in drops to one. Checking the linearization at a random point reduces to evaluating at two points, and those evaluations are sums, exactly what sum-check handles. So the protocol interleaves: a quantifier via sum-check, then linearize and verify via more sum-check rounds, then the next quantifier. Each new quantifier also relinearizes every variable before it, so the round count is , still polynomial. TQBF has an interactive proof, so IP equals PSPACE.
What it means#
A polynomial-time verifier, a machine that cannot solve NP-hard problems on its own, can verify any computation a polynomial-space machine could perform, just by having a conversation. Interaction and randomness together give verification power far beyond either alone.
The result connects outward. In 1988, Ben-Or, Goldreich, Goldwasser, and others proved that if one-way functions exist, every language in IP has a computational zero-knowledge proof: every PSPACE problem can be verified without revealing anything about how the answer was found. The proof also broke a barrier. Fortnow and Sipser had constructed an oracle relative to which co-NP is not in IP, so the theorem cannot hold in all oracle worlds; by exploiting algebraic structure instead of treating computation as a black box, Shamir's proof became the first major theorem to provably break through relativization. Related algebraic techniques underlie the PCP theorem and hardness of approximation. And because sum-check is public-coin, the Fiat-Shamir transform can make it non-interactive, the pipeline from Shamir's 1990 result to modern SNARKs, which underpin real-world verifiable computation today.
Computation, proof, and interaction: three ideas that turn out to be the same idea.
If you remember three things#
- Randomness plus interaction verifies what no short certificate can: the graph non-isomorphism quiz catches a cheating prover with probability per round, amplified by repetition.
- Arithmetization lifts Boolean claims to low-degree polynomials over , where the sum-check protocol audits a -term sum in rounds with cheating probability at most .
- Linearization tames the degree blowup from universal quantifiers, proving IP equals PSPACE: the first major non-relativizing theorem, and the ancestor of modern SNARKs.
Discussion
No comments yet. Be the first.