
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.
Complexity of proofs, FOS: Computer and information sciences, Technology, HARDNESS, Computer Science - Logic in Computer Science, Theory & Methods, 1702 Cognitive Sciences, IPS, Computational Complexity (cs.CC), hardness versus randomness, Nullstellensatz, POLYNOMIAL CALCULUS, lower bounds, Computer Science, Theory & Methods, NULLSTELLENSATZ, proof complexity, FOS: Mathematics, Complexity classes (hierarchies, relations among complexity classes, etc.), Algebraic Complexity, algebraic circuit complexity, 0802 Computation Theory and Mathematics, Science & Technology, Networks and circuits as models of computation; circuit complexity, SUM, Proof Complexity, Subset-Sum, Mathematics - Logic, functional lower bounds, 004, Logic in Computer Science (cs.LO), Computer Science - Computational Complexity, RESOLUTION, HITTING-SETS, Computer Science, Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.), Proof complexity, polynomial calculus, Logic (math.LO), ABPs, ARITHMETIC CIRCUITS, algebraic proof systems, ddc: ddc:004
Complexity of proofs, FOS: Computer and information sciences, Technology, HARDNESS, Computer Science - Logic in Computer Science, Theory & Methods, 1702 Cognitive Sciences, IPS, Computational Complexity (cs.CC), hardness versus randomness, Nullstellensatz, POLYNOMIAL CALCULUS, lower bounds, Computer Science, Theory & Methods, NULLSTELLENSATZ, proof complexity, FOS: Mathematics, Complexity classes (hierarchies, relations among complexity classes, etc.), Algebraic Complexity, algebraic circuit complexity, 0802 Computation Theory and Mathematics, Science & Technology, Networks and circuits as models of computation; circuit complexity, SUM, Proof Complexity, Subset-Sum, Mathematics - Logic, functional lower bounds, 004, Logic in Computer Science (cs.LO), Computer Science - Computational Complexity, RESOLUTION, HITTING-SETS, Computer Science, Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.), Proof complexity, polynomial calculus, Logic (math.LO), ABPs, ARITHMETIC CIRCUITS, algebraic proof systems, ddc: ddc:004
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 0 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
