Proof Complexity Lower Bounds from Algebraic Circuit Complexity

Proof complexity studies the complexity of mathematical proofs, with the aim of exhibiting (true) statements whose proofs are always necessarily long. One well-known proof system is Hilbert's Nullstellensatz, which shows that if the family $F=\{f_1,\ldots ,f_m\}$ of $n$-variate polynomials have no common solution to the system $f_1=\cdots=f_m=0$, then there is a proof of this fact of the following form: there are polynomials $G=\{g_1,\ldots ,g_m\}$ such that $f_1\cdot g_1+\cdots +f_m\cdot g_m=1$ is an identity. From the perspective of computer science, it is most natural to assume that the "boolean axioms" $x_i^2-x_i$ are among the polynomials $F$, and to ask how succinctly one can express the proof $G$. Assuming $NP\ne coNP$, there must be systems $F$ such that any proof $G$ requires super-polynomial size to write down, and the goal is to furnish such systems $F$ unconditionally. Substantial work on the Nullstellensatz system has measured the complexity of $G$ in terms of their degree or sparsity, and obtained the desired lower bounds for these measures. Grochow and Pitassi have recently argued that it is natural to measure the complexity of $G$ by the size needed to express them as algebraic circuits, as this can be exponentially more succinct than counting monomials. They called the resulting system the Ideal Proof System (IPS), and showed that it captures the power of well-known strong proof systems such as the Frege proof system, as well as showing that certain natural lower bounds for the size of IPS proofs would imply $VP\ne VNP$, an algebraic analogue of $P\ne NP$. This is in contrast to other proof systems, where direct ties to computational lower bounds are often lacking. Motivated by their work, we study the IPS proof system further. We first show that weak subsystems of IPS can be quite powerful. We consider the subset-sum axiom, that $x_1+\cdots +x_n+1$ is unsatisfiable over the boolean cube. In prior work, Impagliazzo, Pudlak, and Sgall showed that any proof of unsatisfiability requires exponentially many monomials to write down. Here, we give an efficient proof even in restricted subclasses of the IPS proof system, showing that the proof can be expressed as a polynomial-size read-once oblivious algebraic branching program (roABP) or depth-3 multilinear formula. We then consider lower bounds for subclasses of IPS. We obtain certain extensions to existing lower bound techniques, obtaining "functional lower bounds" as well as "lower bounds for multiples". Using these extensions, we show that variants of the subset-sum axiom require super-polynomially large proofs to prove their unsatisfiability when the size of the algebraic circuits are measured as roABPs, sums of powers of low-degree polynomials, or multilinear formulas. No specific knowledge of proof complexity or algebraic circuit complexity will be assumed. Joint work with Amir Shpilka, Iddo Tzameret, and Avi Wigderson.