The Taub Faculty of Computer Science Events and Talks

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} of n-variate polynomials have no common solution to the system f1=…=fm=0, then there is a proof of this fact of the following form: there are polynomials G={g1,…,gm} such that f1.g1+…+fm.gm=1 is an identity. From the perspective of computer science, it is most natural to ask how succinctly one can express the proof G.

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 Pitassqi have recently argued that it is natural to measure the complexity of G by the size needed to express them as algebraic circuits. 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≠VNP, an algebraic analogue of P≠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 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 read-once algebraic branching programs, 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 Michael Forbes, Iddo Tzameret, and Avi Wigderson.