Proof complexity lower bounds from algebraic circuit complexity
From MaRDI portal
Abstract: We give upper and lower bounds on the power of subsystems of the Ideal Proof System (IPS), the algebraic proof system recently proposed by Grochow and Pitassi, where the circuits comprising the proof come from various restricted algebraic circuit classes. This mimics an established research direction in the boolean setting for subsystems of Extended Frege proofs, where proof-lines are circuits from restricted boolean circuit classes. Except one, all of the subsystems considered in this paper can simulate the well-studied Nullstellensatz proof system, and prior to this work there were no known lower bounds when measuring proof size by the algebraic complexity of the polynomials (except with respect to degree, or to sparsity). We give two general methods of converting certain algebraic lower bounds into proof complexity ones. Our methods require stronger notions of lower bounds, which lower bound a polynomial as well as an entire family of polynomials it defines. Our techniques are reminiscent of existing methods for converting boolean circuit lower bounds into related proof complexity results, such as feasible interpolation. We obtain the relevant types of lower bounds for a variety of classes (sparse polynomials, depth-3 powering formulas, read-once oblivious algebraic branching programs, and multilinear formulas), and infer the relevant proof complexity results. We complement our lower bounds by giving short refutations of the previously-studied subset-sum axiom using IPS subsystems, allowing us to conclude strict separations between some of these subsystems.
Recommendations
- Circuit complexity, proof complexity, and polynomial identity testing. The ideal proof system
- The strength of multilinear proofs
- The surprising power of constant depth algebraic proofs
- Characterizing propositional proofs as noncommutative formulas
- Another look at degree lower bounds for polynomial calculus
Cited in
(16)- Feasibly constructive proofs of succinct weak circuit lower bounds
- Resolution with counting: dag-like lower bounds and different moduli
- Factorization of polynomials given by arithmetic branching programs
- Lower bounds: from circuits to QBF proof systems
- Proof Complexity Modulo the Polynomial Hierarchy: Understanding Alternation as a Source of Hardness
- scientific article; zbMATH DE number 7009617 (Why is no real title available?)
- Circuit complexity, proof complexity, and polynomial identity testing. The ideal proof system
- scientific article; zbMATH DE number 6866317 (Why is no real title available?)
- On Proving Circuit Lower Bounds against the Polynomial-Time Hierarchy
- scientific article; zbMATH DE number 7471587 (Why is no real title available?)
- Factorization of polynomials given by arithmetic branching programs
- Semi-algebraic proofs, IPS lower bounds, and the τ-conjecture: can a natural number be negative?
- Proving Circuit Lower Bounds in High Uniform Classes
- Discovering the Roots: Uniform Closure Results for Algebraic Classes Under Factoring
- Iterated lower bound formulas: a diagonalization-based approach to proof complexity
- Symmetric proofs in the ideal proof system
This page was built for publication: Proof complexity lower bounds from algebraic circuit complexity
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5368766)
