as “Coke and Pepsi taste different”—irrespective of that example’s informality. Rather, as is done in the theory of NP-completeness, interactive proof systems are connected to computational decision problems where input strings are to be classified as yes-inputs and no-inputs. A particular decision problem is said to have an interactive proof system if there exists a computationally efficient verification procedure (called the verifier) with two properties that capture the essence of what it means to be a proof:

 

1. Completeness. This property represents the requirement that true statements can be proved. Here, the requirement is that for any yes-input string x, there exists a behavior of the entity the verifier interacts with (called the prover) that causes the verifier to believe that x is indeed a yes-input. This situation may be indicated by the verifier outputting 1 (or accept) after interacting with the prover.

2. Soundness. This property represents the complementary requirement to completeness, which is that false statements cannot be proved. In the current situation, the requirement is that the probability that the verifier will be convinced to output 1 given a no-input is negligible, regardless of the prover’s actions. Instead, the verifier outputs 0 (or reject) with probability very close to 1, indicating the prover’s failure to convince it otherwise.

 

While the verifier is restricted to be computationally efficient (or more formally to be describable as a polynomial-time probabilistic Turing machine), no such restriction is placed on the prover. These assumptions serve to place an emphasis on efficient verification, as opposed to efficient construction of proofs.

It must be stressed that there is an inherent asymmetry between the completeness and soundness conditions: when the verifier outputs 0 (or reject), it is not necessarily convinced that the input is a no-input, but only that the prover has failed to convince it that the input is a yes-input. This is analogous to the traditional notion of a proof: one would not be convinced that a particular mathematical statement is false by seeing an incorrect proof claiming it is true.

The most fundamental question, from the viewpoint of complexity theory, about the interactive proof system model is: which computational decision problems have interactive proof systems? The answer is known: a decision problem has an interactive proof system if and only if it is solvable by an ordinary computer (or deterministic Turing machine) that requires an amount of memory that scales at most polynomially in its input length. A more succinct expression of this fact is given by the equation IP = PSPACE. In this equation, IP denotes the set of decision problems having interactive proof systems, PSPACE represents the set of decision problems solvable using polynomial memory (or space), and of course the equality expresses the fact that the two sets are equal, meaning that the two descriptions give rise to precisely the same set of problems.

Like all set equalities, there are two subset relations represented by the equation IP = PSPACE. One of the two

relations, IP  PSPACE, is easy to prove: the typical proof involves a fairly straightforward recursive traversal of a game tree whose edges represent messages exchanged between the prover and verifier, which can be performed in a space-efficient way. The other relation, PSPACE  IP, was proved by Adi Shamir14 in 1990, based on work of Carsten Lund et al. 10 It is a landmark result that established the powerful proof technique of arithmetization as a standard tool in computational complexity.

1. 2. Quantum computation in proofs

The idea of quantum computation was born in the early 1980s when Richard Feynman7 asked a brilliant question: If quantum mechanics is so hard to simulate with a classical computer, why not build a computer based on quantum mechanics to simulate quantum mechanics more directly? Feynman’s ideas on the subject led David Deutsch6 to define the quantum Turing machine model and to investigate its computational power. Driven in large part by Peter Shor’s subsequent discoveries of polynomial-time algorithms for factoring and computing discrete logarithms on a quantum computer, 15 quantum computation has developed into an active field of study within theoretical computer science and both theoretical and experimental physics.

Large-scale quantum computers do not currently exist, and it is universally agreed that at the very least their realization will be an enormous technological challenge. However, it must also be appreciated that quantum mechanics is a remarkably accurate theory that has never been refuted— and with the theory suggesting that quantum computing should be possible, scientists are naturally compelled to test the theory by attempting to build a quantum computer. Efforts to do this are underway in many laboratories around the world.

Within the theoretical study of quantum computation, it is natural to consider quantum computational variants of interesting classical models, including those based on the notion of proofs. The quantum interactive proof system model, which was first introduced in 1999, 17 represents a natural quantum computational analog to the (classical) interactive proof system model. In simple terms, the quantum model allows the verifier and prover in an interactive proof system to perform quantum computations and exchange quantum information, but is otherwise similar to the classical model.

The potential advantages of quantum computation in the setting of interactive proof systems are not limited to the fact that the verifier is able to perform a potentially wider range of computations. The nature of quantum information is such that it has striking benefits in a variety of information-processing tasks, such as secret key exchange3 and distributed computational tasks allowing limited communication. 13 A known benefit of quantum computation in the interactive proof system model is that it allows for a major reduction in the number of messages that must be exchanged: quantum interactive proof systems allowing just three messages to be exchanged between the prover and verifier have the full power of those allowing any polynomial number of messages. 9