Functional Lower Bounds in Algebraic Proofs: Symmetry, Lifting, and Barriers

Strong algebraic proof systems such as IPS (Ideal Proof System;) offer a general model for deriving polynomials in an ideal and refuting unsatisfiable propositional formulas, subsuming most standard propositional proof systems. A major approach for lower bounding the size of IPS refutations is the Functional Lower Bound Method (Forbes, Shpilka, Tzameret and Wigderson [FSTW21]), which reduces the hardness of refuting a polynomial equation f (x) = 0 with no Boolean solutions to the hardness of computing the function 1 /f(x) over the Boolean cube with an algebraic circuit. Using symmetry, we provide a general way to obtain many new hard instances against fragments of IPS via the functional lower bound method. This includes hardness over finite fields and hard instances different from Subset Sum variants, both of which were unknown before, and stronger constant-depth lower bounds. Conversely, we expose the limitation of this method by showing it cannot lead to proof complexity lower bounds for any hard Boolean instance (e.g., CNFs) for any sufficiently strong proof systems. Specifically, we show the following: Nullstellensatz degree lower bounds using symmetry: Extending [FSTW21] we show that every unsatisfiable symmetric polynomial with n variables requires degree > n refutations (over sufficiently large characteristic). Using symmetry again, by characterising the n /2-homogeneous slice appearing in refutations, we give examples of unsatisfiable invariant polynomials of degree n /2 that require degree ≥ n refutations.

Lifting to size lower bounds: Lifting our Nullstellensatz degree bounds to IPS-size lower bounds, we obtain exponential lower bounds for any poly-logarithmic degree symmetric instance against IPS refutations written as oblivious read-once algebraic programs (roABP-IPS). For invariant polynomials, we show lower bounds against roABP-IPS and refutations written as multilinear formulas in the placeholder IPS regime (studied by Andrews-Forbes [AF22]), where the hard instances do not necessarily have small roABPs themselves, including over positive characteristic fields. This provides the first explicit example of a hard instance against IPS fragments over finite fields. By an adaptation of the work of Amireddy, Garg, Kayal, Saha and Thankey [AGK + 23], we extend and strengthen the constant-depth IPS lower bounds obtained recently in Govindasamy, Hakoniemi and Tzameret [GHT22] which held only for multilinear proofs, to poly(log log n) individual degree proofs. This is a natural and stronger constant depth proof system than in [GHT22], which we show admits small refutations for standard hard instances like the pigeonhole principle and Tseitin formulas. Barriers for Boolean instances: While lower bounds against strong propositional proof systems were the original motivation for studying algebraic proof systems in the 1990s (Beame et al. [BIK + 96a] and Buss et al. [BIK + 96b]), we show that the functional lower bound method alone cannot establish any size lower bound for Boolean instances for any sufficiently strong proof systems, and in particular, cannot lead to lower bounds against AC 0 [p]-Frege and TC 0 -Frege. * A preliminary abbreviated version of this work appears in STOC 2024. The preliminary version included a quantitative strengthening of the lower bound against multilinear constant-depth IPS refutations from [GHT22]. The current version extends and strengthens the lower bound in [GHT22] to work against O(log log n) individual degree constant-depth IPS refutations.