论文标题
低深度代数证明的简单硬实例
Simple Hard Instances for Low-Depth Algebraic Proofs
论文作者
论文摘要
我们证明，在零特性的磁场上具有恒定深度代数电路的命题证明系统的大小上，我们证明了超多项式下限。 Specifically, we show that the subset-sum variant $\sum_{i,j,k,\ell\in[n]} z_{ijk\ell}x_ix_j x_k x_\ell - β=0$, for Boolean variables, does not have polynomial-size IPS refutations where the refutations are multilinear and written as constant-depth circuits. Andrews和Forbes（Stoc'22）最近建立了一个恒定的IPS下限，但是它们的硬实例本身并没有恒定的深度电路，而我们的实例已经可以计算出具有小的Depth-2电路。 我们的论点依靠将Limaye，Srinivasan和Tavenas（focs'21）（focs'21）的恒定深度代数回路的最新突破范围扩展到福布斯，Shpilka，Shpilka，Tzameret和Wigderson（TOC'21）的功能下限框架，并可能具有独立的利益。具体而言，我们构建了一个可计算的多项式$ f $，具有小尺寸的恒定深度电路，以便在布尔值及其适当的set-multilinear投影上，多连线多项式计算$ 1/f $对于恒定的深度电路很难。
We prove super-polynomial lower bounds on the size of propositional proof systems operating with constant-depth algebraic circuits over fields of zero characteristic. Specifically, we show that the subset-sum variant $\sum_{i,j,k,\ell\in[n]} z_{ijk\ell}x_ix_j x_k x_\ell - β=0$, for Boolean variables, does not have polynomial-size IPS refutations where the refutations are multilinear and written as constant-depth circuits. Andrews and Forbes (STOC'22) established recently a constant-depth IPS lower bound, but their hard instance does not have itself small constant-depth circuits, while our instance is computable already with small depth-2 circuits. Our argument relies on extending the recent breakthrough lower bounds against constant-depth algebraic circuits by Limaye, Srinivasan and Tavenas (FOCS'21) to the functional lower bound framework of Forbes, Shpilka, Tzameret and Wigderson (ToC'21), and may be of independent interest. Specifically, we construct a polynomial $f$ computable with small-size constant-depth circuits, such that the multilinear polynomial computing $1/f$ over Boolean values and its appropriate set-multilinear projection are hard for constant-depth circuits.
