In this work, we establish separation theorems for several subsystems of the Ideal Proof System (IPS), an algebraic proof system introduced by Grochow and Pitassi (J. ACM, 2018). Separation theorems are well-studied in the context of classical complexity theory, Boolean circuit complexity, and algebraic complexity. In an important work of Forbes, Shpilka, Tzameret, and Wigderson (ToC, 2021), two proof techniques were introduced to prove lower bounds for subsystems of the IPS, namely the functional method and the multiples method. We use these techniques and obtain the following results. Hierarchy theorem for constant-depth IPS: Recently, Limaye, Srinivasan, and Tavenas (J. ACM 2025) proved a hierarchy theorem for constant-depth algebraic circuits. We adapt the result and prove a hierarchy theorem for constant-depth $\mathsf{IPS}$. We show that there is an unsatisfiable multilinear instance refutable by a depth-$Δ$ $\mathsf{IPS}$ such that any depth-($Δ/10)$ $\mathsf{IPS}$ refutation for it must have superpolynomial size. This result is proved by building on the multiples method. Separation theorems for multilinear IPS: In an influential work, Raz (ToC, 2006) unconditionally separated two algebraic complexity classes, namely multilinear $\mathsf{NC}^{1}$ from multilinear $\mathsf{NC}^{2}$. In this work, we prove a similar result for a well-studied fragment of multilinear-$\mathsf{IPS}$. Specifically, we present an unsatisfiable instance such that its functional refutation, i.e., the unique multilinear polynomial agreeing with the inverse of the polynomial over the Boolean cube, has a small multilinear-$\mathsf{NC}^{2}$ circuit. However, any multilinear-$\mathsf{NC}^{1}$ $\mathsf{IPS}$ refutation ($\mathsf{IPS}_{\mathsf{LIN}}$) for it must have superpolynomial size. This result is proved by building on the functional method.

翻译：本文针对Grochow与Pitassi（J. ACM, 2018）提出的代数证明系统——理想证明系统（IPS）的若干子系统建立了分离性定理。分离性定理在经典计算复杂性理论、布尔电路复杂性及代数复杂性领域已有深入研究。在Forbes、Shpilka、Tzameret与Wigderson（ToC, 2021）的重要工作中，提出了两种证明IPS子系统下界的技术：函数方法与倍数方法。我们运用这些技术取得了以下成果。 常数深度IPS的层次定理：近期Limaye、Srinivasan与Tavenas（J. ACM 2025）证明了常数深度代数电路的层次定理。我们调整该结果并证明了常数深度$\mathsf{IPS}$的层次定理：存在一个不可满足的多线性实例，其可由深度为$Δ$的$\mathsf{IPS}$反驳，但任何深度为$Δ/10$的$\mathsf{IPS}$反驳必须具有超多项式规模。该证明基于倍数方法构建。 多线性IPS的分离性定理：在Raz（ToC, 2006）具有影响力的工作中，无条件分离了两个代数复杂性类——多线性$\mathsf{NC}^{1}$与多线性$\mathsf{NC}^{2}$。本文针对被深入研究的多线性$\mathsf{IPS}$片段证明了类似结果：我们构造了一个不可满足的实例，其函数式反驳（即在布尔立方上与多项式逆一致的唯一多线性多项式）具有小型多线性$\mathsf{NC}^{2}$电路，但任何针对该实例的多线性$\mathsf{NC}^{1}$ $\mathsf{IPS}$反驳（$\mathsf{IPS}_{\mathsf{LIN}}$）必须具有超多项式规模。该证明基于函数方法构建。