NoShortProof · Nonexistence of Short Proofs

Efficient algorithms are vital for dealing with the ever growing amounts of data in our modern world. A particularly tricky task is posed by so-called combinatorial problems, where objects need to be combined together to form a solution satisfying some specified constraints. Increasing data size quickly causes an exponential growth in the search space for such problems, and despite decades of effort no algorithms have been designed that are guaranteed to tame this combinatorial explosion. In practice, however, it is often possible to find algorithmic shortcuts that work reasonably well, although there is very limited scientific understanding of when and why this is the case. This points to a fundamental challenge: We need a better understanding of the power and limitations of modern algorithm design.An important tool for algorithm analysis is to describe its method of reasoning in a formal proof system. When the algorithm terminates, the execution trace can be viewed as a proof of correctness of the result computed. If we can prove mathematically that no short proofs exist for certain types of statements, then this shows that the algorithm cannot possibly solve the corresponding problems efficiently.The goal of this project is to shed light on proof systems corresponding to some of the most powerful algorithmic paradigms in wide use and to delineate their potential. One concrete objective is to study combinatorial and algebraic methods for solving well-known graph problems such as Clique. Another goal is to compare semidefinite programming to traditional algorithms for solving non-Gaussian component analysis (NGCA), a fundamental problem in statistical learning. I will do so by strengthening existing techniques for analyzing these proof systems and combining them in novel ways. In particular, one important challenge will be to study the setting where the power of a proof system needs to be understood for a distribution of problems from which the input is drawn.