The celebrated $\mathbf{IP}=\mathbf{PSPACE}$ Theorem gives an efficient interactive proof for any bounded-space algorithm. In this work we study interactive proofs for non-deterministic bounded space computations. While Savitch's Theorem shows that nondeterministic bounded-space algorithms can be simulated by deterministic bounded-space algorithms, this simulation has a quadratic overhead. We give interactive protocols for nondeterministic algorithms directly to get faster verifiers.

More specifically, for any non-deterministic space $S$ algorithm, we construct an interactive proof in which the verifier runs in time $\tilde{O}(n+S^2)$. This improves on the best previous bound of $\tilde{O}(n+S^3)$ and matches the result for deterministic space bounded algorithms, up to $\mathrm{polylog}(S)$ factors.

We further generalize to alternating bounded space algorithms. For any language $L$ decided by a time $T$, space $S$ algorithm that uses $d$ alternations, we construct an interactive proof in which the verifier runs in time $\tilde{O}(n + S \log(T) + S d)$ and the prover runs in time $2^{O(S)}$. For $d = O(\log(T))$, this matches the best known interactive proofs for deterministic algorithms, up to $\mathrm{polylog}(S)$ factors, and improves on the previous best verifier time for nondeterministic algorithms by a factor of $\log(T)$. We also improve the best prior verifier time for unbounded alternations by a factor of $S$.

Using known connections of bounded alternation algorithms to bounded depth circuits, we also obtain faster verifiers for bounded depth circuits with unbounded fan-in.

1. Added more discussion of interactive proofs for deterministic algorithms to the introduction.
2. Added references to older interactive proofs by Rudich for repeated matrix multiplication (Thanks to Edward Hirsch for showing them to us), although these proofs did not explicitly state they were for repeated matrix multiplication as Thaler had.

The celebrated $\mathbf{IP}=\mathbf{PSPACE}$ Theorem gives an efficient interactive proof for any bounded-space algorithm. In this work we study interactive proofs for non-deterministic bounded space computations. While Savitch's Theorem shows that nondeterministic bounded-space algorithms can be simulated by deterministic bounded-space algorithms, this simulation has a quadratic overhead. We give interactive protocols for nondeterministic algorithms directly to get faster verifiers.

More specifically, for any non-deterministic space $S$ algorithm, we construct an interactive proof in which the verifier runs in time $\tilde{O}(n+S^2)$. This improves on the best previous bound of $\tilde{O}(n+S^3)$ and matches the result for deterministic space bounded algorithms, up to $\mathrm{polylog}(S)$ factors.

We further generalize to alternating bounded space algorithms. For any language $L$ decided by a time $T$, space $S$ algorithm that uses $d$ alternations, we construct an interactive proof in which the verifier runs in time $\tilde{O}(n + S \log(T) + S d)$ and the prover runs in time $2^{O(S)}$. For $d = O(\log(T))$, this matches the best known interactive proofs for deterministic algorithms, up to $\mathrm{polylog}(S)$ factors, and improves on the previous best verifier time for nondeterministic algorithms by a factor of $\log(T)$. We also improve the best prior verifier time for unbounded alternations by a factor of $S$.

Using known connections of bounded alternation algorithms to bounded depth circuits, we also obtain faster verifiers for bounded depth circuits with unbounded fan-in.