Title: New Connections between Lower Bounds on Algorithms, Circuits, and Proofs
Speaker: Joshua Grochow, Univ. of Toronto
Date: Wednesday, February 19, 2014 11:00-12:00pm
Location: CoRE Bldg, Room 301A, Rutgers University, Busch Campus, Piscataway, NJ
NP versus coNP is the very natural question of whether, for every graph that doesn't have a Hamiltonian path, there is a short proof of this fact. One of the arguments for the utility of proof complexity is that by proving lower bounds against stronger and stronger proof systems, we "make progress" towards proving NP is different from coNP. However, until now this argument has been more the expression of a philosophy or hope, as there is no known proof system for which lower bounds imply computational complexity lower bounds.
We remedy this situation by introducing a very natural algebraic proof system*, which has very tight connections to (algebraic) circuit complexity. We show that any lower bound on any boolean tautology in our proof system implies that the permanent does not have polynomial-size algebraic constant-free circuits over any ring (VNP^0 \neq VP^0). Note that, prior to our work, essentially all implications went the opposite direction - a circuit complexity lower bound implying a proof complexity lower bound.
This allows us to give a very simple and completely self-contained proof that NP not in coMA implies ParityP/poly differs from NC^1/poly, by applying the preceding result over F_2. Our proof system also has the advantage that it begins to make clear and precise how much harder it is to prove lower bounds in algebraic proof complexity than in algebraic circuit complexity. It thus helps explain why it has been so difficult to prove true size lower bounds on algebraic proof systems, and thereby also lower bounds on AC^0[p]-Frege systems (a > 30-year barrier). Finally, we flip this difference in hardness on its head, to suggest a new way to transfer techniques from algebraic proof complexity, such as the method of partial derivatives, to prove lower bounds in algebraic proof complexity. Joint work in progress with Toniann Pitassi.
* - As with many algebraic proof systems, a proof is checkable in probabilistic polynomial time.