形式陈述
采用多项式轮数、每轮多项式消息长度的交互证明 公理库 交互式证明系统 Interactive proof system · IP 由计算受限的概率验证者与计算无界证明者多轮交互定义的证明模型。 :验证者为概率多项式时间,prover 计算能力不受限;完备性至少 2 / 3 ,可靠性至多 1 / 3 。Shamir 定理断言
IP = PSPACE . 常数误差可由顺序重复和多数表决放大,等式不依赖这里选取的具体 2 / 3 , 1 / 3 。证明包含两个方向,所用资源和量词不同。
PSPACE ⊆ IP 的可核验骨架以 TQBF 公理库 TQBF 的 PSPACE 完全性 PSPACE-completeness of TQBF · QBF is PSPACE-complete 判定全量化布尔公式真值的问题在多项式时间归约下是 PSPACE 完全的。 为完全问题。先把量词自由矩阵算术化并逐变量检查 公理库 Sum-check 协议 Sum-check protocol · Sumcheck protocol 以逐变量低次多项式承诺和随机挑战验证 Boolean cube 上指数项多项式求和的交互协议。 :布尔 AND/OR 由域多项式表示,∀ x 对应两个布尔取值结果的 AND,∃ x 对应 OR。Prover 每轮提交某个量词后缀的低次单变量多项式;验证者检查其在 0 , 1 的组合是否等于上一轮承诺,再在收到承诺后随机选 r ∈ F 把问题降一维。直接消去量词会让 degree 快速增长,协议在每层加入重新多线性化/低次数化检查。诚实递归给 perfect completeness;一旦承诺错误,非零低次差多项式只在至多其次数个随机点继续伪装。取 | F | 大于总轮数与 degree 的足够多项式并放大,可把总 soundness 压到 1 / 3 。
IP ⊆ PSPACE 可以直接模拟原协议,不需要先做 public-coin 转换。固定输入后,验证者的多项式长度随机带、双方的多项式长度消息和多项式轮数形成一棵有限博弈树。对每份 prover 可见的 transcript,模拟器枚举其下一条可能消息并取最优值;对验证者的随机选择则按概率加权求和,验证者的确定性计算由模拟器直接执行。
若验证者使用私有随机币,递归不能把隐藏随机带透露给 prover:产生同一可见 transcript 的随机分支必须归入同一个信息集,并共用同一条 prover 回复。多项式空间机器可按 transcript 反复枚举与之相容的随机带,深度优先重算各分支,而不同时保存整层状态。随机位总数为多项式,所以接受概率可写成分母 2 q ( n ) 的有理数;累计计数与和完备性、可靠性阈值的比较只需多项式位。模拟可能耗费指数时间,但任一时刻只保存当前 transcript、递归栈、候选消息和计数器,因此使用多项式空间。public-coin 转换可以作为另一种呈现方式,却不是这个包含方向的证明前置。
直觉
PSPACE 计算可以隐含一棵指数大的递归树。交互让 prover 每次声称这棵树某一层的代数摘要,验证者用随机点把下一轮承诺绑到上一轮;它无需展开全部分支,只需让任何前后不一致以高概率暴露。
反方向则利用“空间可复用”:PSPACE 模拟器确实遍历指数博弈树,但结束一个分支后丢弃它,只保留当前路径。等式比较的是可判定语言能力,不是说交互协议能在多项式时间独自完成 PSPACE 计算。
例子与边界
量化公式
∃ x ∀ y ( x ∨ y ) 为真,因为可选 x = 1 。矩阵算术化为 p ( x , y ) = x + y − x y ;对固定 x ,全称量词的布尔值可写成 p ( x , 0 ) p ( x , 1 ) ,再对 x = 0 , 1 取 OR 多项式。这个小例子展示端点组合,但大型 TQBF 不能把递归多项式完整展开,否则次数和表示长度会爆炸;随机低次承诺正是省略展开的机制。
原始 sum-check 只验证 Boolean cube 上的多项式求和,不能未经改造直接处理交替的 ∃ / ∀ 。TQBF 协议还需处理 OR/AND 量词和逐层 degree reduction;把“算术化后调用 sum-check”写成一句会漏掉证明核心。
在 I P ⊆ P S P A C E 中,深度优先枚举不要求多项式时间。若错误地同时保存整层所有 transcript,空间会指数增长;若只取某个 prover 消息而不做最大化,又无法覆盖 soundness 中的任意欺骗策略。对私有币协议,还不能先按隐藏随机带分别最大化再取平均:那等于允许 prover 看见私有币,改变了原协议的信息结构。
推论与应用
I P = P S P A C E 表明随机交互显著强于静态 NP 证书,同时仍受多项式空间精确刻画。它开辟了用代数承诺、随机挑战和逐层降维验证巨大计算的路线。
结论不限制 prover 属于 PSPACE,也不表示 PSPACE 问题拥有无交互的多项式证书。把多轮交互压缩成参数更强的协议需要额外结果,不能从类相等本身推出。
参考资料
Adi Shamir, “IP = PSPACE,” Journal of the ACM 39(4), 1992, pp. 869–877.
Carsten Lund, Lance Fortnow, Howard Karloff, and Noam Nisan, “Algebraic Methods for Interactive Proof Systems,” Journal of the ACM 39(4), 1992, pp. 859–868.