This is of course a consequence of $NP \subset PSPACE = IP$. But it can also be proven directly for UNSAT.

The basic idea is reducing the problem to zero-testing a sum over a polynomial in a suitable finite field. It's a bit too technical to repeat neatly here, but I can give you an informal idea of how it is done.

Let's consider a formula $\phi$, define $p_\phi$ to be the polynomial where you think of $x_i$s as variables, replacing $\neg x_i$ by $(1 - x_i)$, each $\wedge$ by $\times$ and each $\vee$ by $+$. Notice that the formula is unsatisfiable iff $p_\phi(x_1, \dots, x_n) = 0$ for all $x \in \{0, 1\}^n$ or equiavalently if

$$ \sum_{x_1 \in \{0, 1\}}\sum_{x_2 \in \{0, 1\}} \dots \sum_{x_n \in \{0, 1\}} p(x_1, x_2, \dots, x_n) = 0 $$

This follows from the fact that $p_\phi \geq 0$ for any $0/1$ assignement.

The interaction is essentially the prover trying to convince the verifier that the sum is indeed zero. The interaction is done on the sum above modulo a suitable prime to keep computations manageable for the verifier. The full details are explained here. The main proof that you need to follow and convince yourself of, is that the prover cannot fool the verifier with large probability.

This is of course a consequence of $coNP \subset PH \subset PSPACE = IP$. But it can also be proven directly for UNSAT.

The basic idea is reducing the problem to zero-testing a sum over a polynomial in a suitable finite field. It's a bit too technical to repeat neatly here, but I can give you an informal idea of how it is done.

Let's consider a formula $\phi$, define $p_\phi$ to be the polynomial where you think of $x_i$s as variables, replacing $\neg x_i$ by $(1 - x_i)$, each $\wedge$ by $\times$ and each $\vee$ by $+$. Notice that the formula is unsatisfiable iff $p_\phi(x_1, \dots, x_n) = 0$ for all $x \in \{0, 1\}^n$ or equiavalently if

$$ \sum_{x_1 \in \{0, 1\}}\sum_{x_2 \in \{0, 1\}} \dots \sum_{x_n \in \{0, 1\}} p(x_1, x_2, \dots, x_n) = 0 $$

This follows from the fact that $p_\phi \geq 0$ for any $0/1$ assignement.

The interaction is essentially the prover trying to convince the verifier that the sum is indeed zero. The interaction is done on the sum above modulo a suitable prime to keep computations manageable for the verifier. The full details are explained here. The main proof that you need to follow and convince yourself of, is that the prover cannot fool the verifier with large probability.