Proof Complexity Lower Bounds from Algebraic Circuit Complexity - Forbes

Computer Science/Discrete Mathematics Seminar
Topic: Proof Complexity Lower Bounds from Algebraic Circuit Complexity
Speaker: Michael Forbes
Date: Tuesday, January 19

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={f1,…,fm}F={f1,…,fm} of nn-variate polynomials have no common solution to the system f1=⋯=fm=0f1=⋯=fm=0, then there is a proof of this fact of the following form: there are polynomials G={g1,…,gm}G={g1,…,gm} such that f1⋅g1+⋯+fm⋅gm=1f1⋅g1+⋯+fm⋅gm=1 is an identity. From the perspective of computer science, it is most natural to assume that the "boolean axioms" x2i−xixi2−xi are among the polynomials FF, and to ask how succinctly one can express the proof GG. Assuming NP≠coNPNP≠coNP, there must be systems FF such that any proof GG requires super-polynomial size to write down, and the goal is to furnish such systems FF unconditionally. Substantial work on the Nullstellensatz system has measured the complexity of GG 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 GG 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≠VNPVP≠VNP, an algebraic analogue of P≠NPP≠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 x1+⋯+xn+1x1+⋯+xn+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.