Algebraic circuit lower bounds need strong proof systems
Meta-Mathematics of Algebraic Complexity
Computational ComplexityLogic in Computer Science
Summary
Understanding why some computer problems are hard to solve often involves proving certain limits, called lower bounds, for algebraic circuits. This paper finds that these proofs require relatively strong logical systems to work efficiently. The authors show that weaker reasoning systems are not enough to prove many known algebraic circuit lower bounds. Their work suggests that proving bigger lower bounds will need even more powerful reasoning methods than currently used.
What this means in practice
- •For complexity theory tool developers: Design proof systems for automating algebraic lower bound proofs requiring reasoning at or above NC^2 complexity.
- •For formal verification engineers: Avoid relying on weaker algebraic constant-depth reasoning when verifying algebraic circuit complexity properties.
A theory result. No direct application yet.
Authors
Michal Garlik, Svyatoslav Gryaznov, Jiaqi Lu, Rahul Santhanam, Iddo Tzameret
Abstract
We initiate the study of the meta-mathematics of algebraic circuit lower bounds, aiming both to gain insight into the methods sufficient and necessary to prove algebraic circuit lower bounds, and to contribute to the study of bounded arithmetic as a logical foundation for complexity lower bounds. We demonstrate that while algebraic circuit lower bounds are hard for somewhat weak proof systems such as Polynomial Calculus Resolution ($\mathsf{PCR}$), contemporary lower bounds are efficiently provable in proof systems and bounded arithmetic theories corresponding to $\mathsf{NC}^2$, such as $\mathsf{VNC}^2$ and the corresponding class of propositional Frege proofs of quasipolynomial-size. Moreover, going below $\mathsf{VNC}^2$ into algebraic constant-depth reasoning is likely insufficient to efficiently prove already constant-depth algebraic circuit lower bounds. Under an algebraic analogue of the Krajicek--Razborov conjecture, our results suggest that proving superpolynomial lower bounds for general algebraic circuits will require stronger reasoning than that used in the rank-based proofs studied here. Specifically, we show the following.