Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Tuomas Hakoniemi, Nutan Limaye, Iddo Tzameret

TL;DR

The paper advances proof complexity by extending the Functional Lower Bound Method to a broader family of algebraic hard instances, including symmetric and vector-invariant polynomials, and by lifting degree lower bounds to size lower bounds for IPS fragments (roABP-IPS and multilinear-IPS) across fixed and arbitrary variable orders. It introduces new hard instances over finite fields and achieves constant-depth IPS lower bounds via APP-based analyses, while also proving a fundamental barrier showing that this approach cannot suffice for Boolean CNF lower bounds against sufficiently strong proof systems. The results significantly widen the repertoire of explicit hard instances for IPS and related models, connect invariant theory with algebraic circuit lower bounds, and demonstrate compatibility with modern constant-depth lower-bound techniques. Collectively, the work clarifies both the reach and the limits of the functional-lower-bound paradigm in driving long-standing open questions in propositional proof complexity.

Abstract

Strong algebraic proof systems such as IPS (Ideal Proof System; Grochow-Pitassi [GP18]) 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.

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

TL;DR

The paper advances proof complexity by extending the Functional Lower Bound Method to a broader family of algebraic hard instances, including symmetric and vector-invariant polynomials, and by lifting degree lower bounds to size lower bounds for IPS fragments (roABP-IPS and multilinear-IPS) across fixed and arbitrary variable orders. It introduces new hard instances over finite fields and achieves constant-depth IPS lower bounds via APP-based analyses, while also proving a fundamental barrier showing that this approach cannot suffice for Boolean CNF lower bounds against sufficiently strong proof systems. The results significantly widen the repertoire of explicit hard instances for IPS and related models, connect invariant theory with algebraic circuit lower bounds, and demonstrate compatibility with modern constant-depth lower-bound techniques. Collectively, the work clarifies both the reach and the limits of the functional-lower-bound paradigm in driving long-standing open questions in propositional proof complexity.

Abstract

Strong algebraic proof systems such as IPS (Ideal Proof System; Grochow-Pitassi [GP18]) 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.
Paper Structure (59 sections, 46 theorems, 166 equations)

This paper contains 59 sections, 46 theorems, 166 equations.

Table of Contents

  1. Introduction
  2. Proof Complexity and Strong Algebraic Proof Systems
  3. Different IPS Lower Bound Methods.
  4. The Functional Lower Bound Method
  5. Our Results and Techniques
  6. Summary and Organisation
  7. Notation.
  8. Nullstellensatz Degree Lower Bounds
  9. Symmetric Instances.
  10. Vector Invariant Polynomials.
  11. Lifting Degree to Size Lower Bounds
  12. Using Lifting against IPS.
  13. Symmetric Instances under Lifting.
  14. Invariant Instances under Lifting.
  15. Proof Overview.
  16. ...and 44 more sections

Key Result

Theorem 1

Let $\mathcal{C}\subseteq\mathbb{F}[\overline x]$ be a circuit class closed under (partial) field-element assignments (which stands for the class of "polynomials with small circuits"). Let $f(\overline x)\in \mathcal{C}$ be a polynomial, where the collection of polynomials $f(\overline x)$ and $\ove Then, $f(\overline x)$ and $\overline x^2-\overline x$ do not have $\mathcal{C}$-$\textnormal{IPS}_

Theorems & Definitions (91)

  • Theorem 1: Functional Lower Bound Method; Lemma 5.2 in FSTW21
  • Corollary : see Cor. \ref{['cor:NS-full-symmetric-deg-lower bound']}; Single unsatisfiable symmetric polynomials require high degree refutations
  • Claim : see Claim \ref{['cla:action-of-Sn-x-e-d']}; Multilinearizing the product of elementary symmetric polynomials yields high degree
  • Theorem : see Thm. \ref{['thm:ns-degreeLB-Q']}; Nullstellensatz degree lower bounds for invariant instances
  • Corollary : Symmetric instances are hard for roABP-$\textnormal{IPS}_{\textnormal{LIN}'}$; see Cor. \ref{['res:lbs-fn:lbs-ips:vary-order']}
  • Theorem : see Thm. \ref{['thm:any-order']}
  • Corollary 2: New functional formula lower bound
  • Theorem : Constant-depth IPS lower bounds; See Thm. \ref{['thm:constant-depth-lower-bounds']}
  • Theorem : Main barrier; see Thm. \ref{['thm:barrier']}
  • Definition 3: Symmetric polynomial
  • ...and 81 more