Most of times the pattern of proving and verifying it is like this $prove \to verify$, that is: there is an entity that generates the solution, andPo then another that tries to verify it. But more expressive algorithms could be possible if there is interaction between the two entities, ones that try to prove it, and others try to verify it. From some point of view, this is similar from what AlphaGo does when searching, there is a part that guides the search, another that actually searches for it. Or the modern alpha geometry in modern times.
Deterministic Interactive Theorem-provers
Def: deterministic interactive theorem provers
We have $k$ rounds of exchange, at the end the prover produces something. Let’s formalize it: Given $V, P : \left\{ 0, 1 \right\}^{*} \to \left\{ 0, 1 \right\}^{*}$ a verifier and a prover, and and input $x$ (a problem), a $k$ round interactive proof is defines as following:
$$ a_{1} = V(x), a_{2} = P(x, a_{1}), \dots, a_{2i + 1} = V(x, a_{1}, \dots, a_{2i}), a_{2i + 2} = P(x, a_{1}, \dots, a_{2i + 1}) $$We write
$$ out^{k}_{V}\langle V, P \rangle (x) \in \left\{ 0, 1 \right\} \text{ as the output of the k-round interactive proof} $$Languages in $dIP(k)$
Given a language $L$ we say that it is in $dIP(k)$ if in $k$ rounds we have:
- Completeness: that is there exists a prover that produces a correct result for a given verifier, if the solution is correct.
- Correctness: if a solution is correct, every interactive proof gives a false result.
More formally, given a deterministic TM acting as verifier, working in polynomial time: Completeness:
$$ x \in L \to \exists P: out^{k}_{V}\langle V, P \rangle = 1 $$Correctness:
$$ x \not\in L \to \forall P : out^{k}_{V}\langle V, P \rangle = 0 $$We also define the deterministic interactive prover class as
$$ dIP = \bigcup_{k \geq 1} dIP(k) $$3SAT in $dIP$
This can be prooven quite easily. But I am tired to write this down. But the takeaway is the following: This follows that $dIP = NP$, which essentially says that you don’t have any advantage using this method.
Probabilistic Interactive Theorem-Provers
The definition is very similar to the above. Note: interactive theorem provers, intuitively, seem to be very similar to a conversation between two agents, that try to work together to reach to a solution.