Simple Hard Instances for Low-Depth Algebraic Proofs

TL;DR

This paper establishes super-polynomial lower bounds for constant-depth algebraic proof systems on a specific subset-sum variant, demonstrating that certain polynomial identities cannot be efficiently refuted within these systems.

Contribution

It introduces a new hard instance for low-depth algebraic proof systems that is itself computable with small circuits, extending recent lower bounds to a broader functional framework.

Findings

Super-polynomial lower bounds for constant-depth algebraic proof systems.

Construction of a small-depth circuit computable polynomial that is hard for these systems.

Extension of recent algebraic circuit lower bounds to functional lower bounds.

Abstract

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 - \beta=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.