In computational complexity theory, an interactive proof system is an abstract machine that models computation as the exchange of messages between two parties: a prover and a verifier. The parties interact by exchanging messages in order to ascertain whether a given string belongs to a language or not. The prover is assumed to possess unlimited computational resources but cannot be trusted, while the verifier has bounded computation power but is assumed to be always honest. Messages are sent between the verifier and prover until the verifier has an answer to the problem and has "convinced" itself that it is correct.

All interactive proof systems have two requirements:

The specific nature of the system, and so the complexity class of languages it can recognize, depends on what sort of bounds are put on the verifier, as well as what abilities it is given—for example, most interactive proof systems depend critically on the verifier's ability to make random choices. It also depends on the nature of the messages exchanged—how many and what they can contain. Interactive proof systems have been found to have some important implications for traditional complexity classes defined using only one machine. The main complexity classes describing interactive proof systems are AM and IP.

Every interactive proof system defines a formal language of strings ${\displaystyle L}$. Soundness of the proof system refers to the property that no prover can make the verifier accept for the wrong statement ${\displaystyle y\not \in L}$ except with some small probability. The upper bound of this probability is referred to as the soundness error of a proof system. More formally, for every prover ${\displaystyle ({\tilde {\mathcal {P}}})}$, and every ${\displaystyle y\not \in L}$:

for some ${\displaystyle \epsilon \ll 1}$. As long as the soundness error is bounded by a polynomial fraction of the potential running time of the verifier (i.e. ${\displaystyle \epsilon \leq 1/\mathrm {poly} (|y|)}$), it is always possible to amplify soundness until the soundness error becomes negligible function relative to the running time of the verifier. This is achieved by repeating the proof and accepting only if all proofs verify. After ${\displaystyle \ell }$ repetitions, a soundness error ${\displaystyle \epsilon }$ will be reduced to ${\displaystyle \epsilon ^{\ell }}$.

The complexity class NP may be viewed as a very simple proof system. In this system, the verifier is a deterministic, polynomial-time machine (a P machine). The protocol is:

In the case where a valid proof certificate exists, the prover is always able to make the verifier accept by giving it that certificate. In the case where there is no valid proof certificate, however, the input is not in the language, and no prover, however malicious it is, can convince the verifier otherwise, because any proof certificate will be rejected.

Although NP may be viewed as using interaction, it wasn't until 1985 that the concept of computation through interaction was conceived (in the context of complexity theory) by two independent groups of researchers. One approach, by László Babai, who published "Trading group theory for randomness", defined the Arthur–Merlin (AM) class hierarchy. In this presentation, Arthur (the verifier) is a probabilistic, polynomial-time machine, while Merlin (the prover) has unbounded resources.