Antonina Kolokolova, Department of Computer Science
Memorial University of Newfoundland
A unifying theme in complexity theory in the past few years has been the duality between lower bounds and algorithms. Indeed, some of the main recent lower bounds have been proven by developing better algorithms.
In this talk, I would like to focus on the other direction of this duality: obtaining new algorithms from (constructive) proofs. I will talk about a general method for extracting learning algorithms from natural proofs of lower bounds, which gave us the first algorithm for learning bounded-depth Boolean circuits with parity gates. Moreover, we show that natural proofs based on random restrictions contain new algorithms for compression and for counting satisfying assignments.
But what makes a proof constructive? One way to formalize this is to show that the proof can be carried out in a reasoning system of a given complexity: for example, natural proofs discussed above can be formalized in the theory of polynomial-time reasoning. Pinpointing the complexity of reasoning needed to prove complexity-theoretic statements can lead to more constructive proofs, and in turn to new results: time permitting, I will discuss one such example, where a low-complexity proof of existence of expander graphs allowed us to show that in the proof complexity setting, monotone reasoning is as powerful as non-monotone, in stark contrast with circuit complexity.
More about Antonina Kolokolova
200 University Avenue West
Waterloo, ON N2L 3G1