Technical Summary: Towards a Doubly Efficient IP = PSPACE

1. Problem Statement

The paper addresses the construction of doubly efficient interactive proof (IP) systems for languages in PSPACE. In such systems, a prover (who possesses the computational power to solve the problem) and a verifier (who has limited computational resources) interact to convince the verifier of the correctness of a computation.

The specific challenge is to achieve this for computations running in time $T(n)$ and space $S(n)$ such that:

• The prover's runtime is polynomial in the computation time, i.e., $\text{poly}(T(n))$.
• The verifier's runtime is significantly sublinear in $T(n)$, ideally polynomial in the input size $n$ (or polynomial in the space bound $S$ and a sublinear function of $T$).

Prior to this work, the best known regime for doubly efficient IPs covered time complexities of $T(n) = n^{O(\sqrt{\log n / \log \log n})}$ (established by Berger, Goyal, Hong, and Kalai, 2025). The goal is to extend this regime to $T(n) = n^{O(\log n)}$, which covers a broader class of PSPACE computations.

2. Methodology

The authors propose a direct construction of a doubly efficient IP, diverging from the indirect "black-box" approach used in previous works (RRR16, BGHK25). Previous methods first constructed batch interactive proofs for unambiguous interactive proofs and then used these as a subroutine. The authors argue that this indirect route faces barriers (specifically the need for a "rate-1" batch IP) and is conceptually complex.

Instead, this paper constructs a protocol that directly batches deterministic time-space bounded (TISP) computations. The core methodology involves a recursive protocol, denoted as Batch($t, k$), which verifies $k$ statements of time-$t$ computations.

Key Technical Ingredients

1. Midpoint Expansion and Matrix Representation:
   To reduce the verification time $t$, the prover sends $\lambda$ intermediate configurations (midpoints) for each of the $k$ computation paths. These are arranged into a $k \times \lambda$ matrix $M$, where each row represents the sequence of configurations for one computation. This transforms $k$ statements of time $t$ into $k \cdot \lambda$ statements of time $t/\lambda$.

2. Unique-Decoding Checksums:
   To prevent the prover from sending inconsistent or malicious intermediate configurations without being detected, the prover sends checksums ($\chi$) of the columns of matrix $M$. These checksums are derived from linear error-correcting codes (specifically Reed-Solomon codes) with a unique-decoding radius $d$. This ensures that if the prover deviates from the "true" witness by more than $d$ rows, the checksums will not match.

3. Interactive Proof of Proximity with Row Reduction (Row-IPP):
   The protocol utilizes a generalized Interactive Proof of Proximity (IPP) that operates on matrices. Instead of verifying the entire matrix $M$, the verifier uses the Row-IPP to check if $M$ is "close" (in row-distance) to satisfying a specific low-depth predicate $\Phi_{reduce}$.

   • The predicate $\Phi_{reduce}$ checks three conditions:
     1. The matrix $M$ is consistent with the checksums $\chi$.
     2. The expanded batch of statements (derived from $M$) satisfies the recursive claim $\Psi_{\uparrow}$ (from a sub-protocol).
     3. The matrix satisfies an auxiliary predicate $\Phi$.
   • If the matrix is far from satisfying these conditions, the Row-IPP allows the verifier to sample a small subset of rows $Q$ (size $\approx k/d$) and a low-depth predicate $\Psi_{IPP}$ such that the verifier only needs to check the sub-matrix $M[Q, :]$.

4. Recursive Reduction (The "Win-Win" Argument):
   The protocol recursively reduces the problem size in two dimensions:

   • Reducing Time ($t$): By expanding midpoints, the time per statement drops from $t$ to $t/\lambda$, but the number of statements increases to $k \cdot \lambda$.
   • Reducing Batch Size ($k$): By applying the Row-IPP, the number of statements is reduced from $k$ to $k/d$ (where $d$ is the distance parameter), while the time $t$ remains the same.

   The recursion continues until either the time $t$ becomes small enough for the GKR protocol (Goldwasser, Kalai, Rothblum, 2015) to verify directly, or the batch size $k$ is small enough to be handled explicitly.

Protocol Flow (Batch($t, k$))

1. Checksums: Prover sends column checksums of the midpoint matrix $M$.
2. Time Reduction (Recursive Call 1): The parties run Batch($t/\lambda, k \cdot \lambda$) on the expanded batch of statements derived from $M$. This yields a predicate $\Psi_{\uparrow}$ that must hold for the expanded statements.
3. Row-IPP: The parties run a Row-IPP to verify that $M$ is close to satisfying the conjunction of: (a) consistency with checksums, (b) satisfaction of $\Psi_{\uparrow}$, and (c) the current auxiliary predicate $\Phi$. This outputs a subset of rows $Q$ and a predicate $\Psi_{IPP}$.
4. Batch Reduction (Recursive Call 2): The parties run Batch($t, k/d$) on the reduced set of statements corresponding to rows $Q$, verifying that they satisfy $\Psi_{IPP}$.

3. Key Contributions

1. Extended Regime for Doubly Efficient IPs:
   The paper constructs a doubly efficient IP for any language computable in polynomial space and time $T(n) = n^{O(\log n)}$.

   • Prover Runtime: $\text{poly}(T)$.
   • Verifier Runtime: $\text{poly}(S, 2^{\sqrt{\log T}})$.
   • Specifically, for $T = n^{O(\log n)}$, the verifier runs in $\text{poly}(n)$.

2. Direct Construction:
   The authors provide a direct construction for batching TISP computations, avoiding the intermediate step of batching unambiguous interactive proofs. This simplifies the proof structure and removes the reliance on "black-box" batch unambiguous IPs, which the authors argue are subject to theoretical barriers (specifically the difficulty of achieving rate-1 batch IPs).

3. Simplified Analysis:
   The protocol's recursive structure is analyzed using a recurrence tree based on Catalan numbers. The authors demonstrate that by setting the splitting parameter $\lambda = 2^{\sqrt{\log T}}$, the verifier's complexity is optimized to $2^{O(\sqrt{\log T})} \cdot \text{poly}(S)$.

4. Results

The main formal result is stated in Theorem 2 (and Corollary 1 for the specific case of $T = n^{O(\log n)}$):

• Theorem: There exists an interactive proof for every language in $\text{TISP}(T, S)$ where:

  • The prover runs in time $\text{poly}(T, S)$.
  • The verifier runs in time $2^{O(\sqrt{\log T})} \cdot S^2 \cdot \text{poly}(\sigma, \log S)$, where $\sigma$ is the soundness parameter.
  • The communication complexity is $2^{O(\sqrt{\log T})} \cdot S \cdot \text{poly}(\sigma, \log S)$.

• Implication: For languages decidable in time $T(n) = n^{O(\log n)}$ (which includes a significant portion of PSPACE), the verifier runs in time $\text{poly}(n)$.

5. Significance and Claims

The paper claims that this work represents a substantial improvement over the state-of-the-art:

• Range Improvement: It extends the time complexity regime from $T(n) = n^{O(\sqrt{\log n / \log \log n})}$ to $T(n) = n^{O(\log n)}$.
• Conceptual Simplicity: The direct construction is described as "substantially simpler" than previous indirect approaches. The authors argue that previous methods, which relied on black-box batch unambiguous IPs, hit a barrier requiring a "rate-1" batch IP (where communication for $k$ statements is $(1+o(1))$ times the cost of one). Constructing such a rate-1 IP is considered challenging.
• Future Potential: The authors posit that their direct approach points to a "more promising route for future improvements," suggesting that further optimizations might be possible by refining the direct batching of TISP computations rather than trying to overcome the barriers inherent in the black-box unambiguous IP approach.

The work relies on standard cryptographic and complexity-theoretic primitives (finite fields, Reed-Solomon codes, GKR protocol, Row-IPP) but synthesizes them in a novel recursive framework to achieve the stated efficiency gains.