IP = PSPACE

形式陈述 ​

采用多项式轮数、每轮多项式消息长度的交互证明理路交互式证明系统Interactive proof system · IP由计算受限的概率验证者与计算无界证明者多轮交互定义的证明模型。：验证者为概率多项式时间，prover 计算能力不受限；完备性至少 $2/3$，可靠性至多 $1/3$。Shamir 定理断言

常数误差可由顺序重复和多数表决放大，等式不依赖这里选取的具体 $2/3,1/3$。证明包含两个方向，所用资源和量词不同。

方向 PSPACE理路复杂度类 PSPACEComplexity class PSPACE可由确定性图灵机在多项式空间内判定的语言类。 $\subseteq \mathbf{IP}$ 的可核验骨架以 TQBF理路TQBF 的 PSPACE 完全性PSPACE-completeness of TQBF · QBF is PSPACE-complete判定全量化布尔公式真值的问题在多项式时间归约下是 PSPACE 完全的。 为完全问题。先对量词自由矩阵作算术化理路算术化Arithmetization把布尔关系嵌入有限域低次多项式，使离散正确性声明可由随机代数恒等式检查。，再借用Sum-check理路Sum-check 协议Sum-check protocol · Sumcheck protocol以逐变量低次多项式承诺和随机挑战验证 Boolean cube 上指数项多项式求和的交互协议。的低次承诺与随机挑战思路逐变量检查：布尔 AND/OR 由域多项式表示，$\mathrm{\forall }x$ 对应两个布尔取值结果的 AND，$\mathrm{\exists }x$ 对应 OR。在量词步骤中，prover 提交前一多项式的单变量限制；验证者检查其在 $0,1$ 的 AND/OR 组合是否等于当前声明，再在收到多项式后随机选 $r\in \mathbb{F}$，转而检查前一多项式在这个随机点的值。

直接消去量词会让次数快速增长，因此插入降次算子

它在 $X_i=0,1$ 时与 $p$ 一致，而关于 $X_i$ 的次数至多为一。要验证声明 $(R_{i}p)(a_i,a_{-i})=v$，prover 先发送受次数界约束的 $q(T)$，声称它等于 $p(T,a_{-i})$。验证者先检查 $(1-a_i)q(0)+a_{i}q(1)=v$，再抽取新鲜随机挑战 $r$，把下一项声明改成 $p(r,a_{-i})=q(r)$。若原声明错误却通过了端点检查，$q$ 必与真实限制不同，根数界因而仍约束此次漏检概率。Shen，§2，Case R。

对长度为 $L$ 的量化公式，先对初始矩阵逐变量降次，再在每次消去量词后对剩余变量逐一降次，共需 $O(L^2)$ 个操作。初始算术化次数为 $O(L)$；多线性多项式经一次 AND/OR 量词组合后，每个剩余变量的次数至多为二，后续降次又将其恢复为一，因此所有阶段的次数界保持 $O(L)$。验证者逐步反向检查这些操作，最后直接求值已知矩阵公式，无需展开中间多项式。诚实递归给 perfect completeness。设总操作数为 $s$、最大次数界为 $d$，取多项式规模的 $|\mathbb{F}|=2^{\ell }>3sd$；其二元不可约多项式表示可在多项式时间内枚举构造，每次挑战用恰好 $\ell$ 个公平随机 bit 均匀采样。对各步根数错误事件应用并合界理路并集界Union bound · Boole 不等式多个坏事件中至少一个发生的概率，不超过各事件概率之和。，总 soundness 至多 $sd/|\mathbb{F}|<1/3$，且抽样不损失完备性。

$\mathbf{IP}\subseteq \mathbf{PSPACE}$ 可以直接模拟原协议，不需要先做 public-coin 转换。固定输入后，验证者的多项式长度随机带、双方的多项式长度消息和多项式轮数形成一棵有限博弈树。对每份 prover 可见的 transcript，模拟器枚举其下一条可能消息并取最优值；对验证者的随机选择则按概率加权求和，验证者的确定性计算由模拟器直接执行。

若验证者使用私有随机币，递归不能把隐藏随机带透露给 prover：产生同一可见 transcript 的随机分支必须归入同一个信息集，并共用同一条 prover 回复。多项式空间机器可按 transcript 反复枚举与之相容的随机带，深度优先重算各分支，而不同时保存整层状态。随机位总数为多项式，所以接受概率可写成分母 $2^{q(n)}$ 的有理数；累计计数与和完备性、可靠性阈值的比较只需多项式位。模拟可能耗费指数时间，但任一时刻只保存当前 transcript、递归栈、候选消息和计数器，因此使用多项式空间。public-coin 转换可以作为另一种呈现方式，却不是这个包含方向的证明前置。