Cutting-edge Combinatorial Optimization with Certified Correctness

Modern combinatorial optimization has transformed entire sectors of industry, and has been applied to an ever expanding list of problems in, e.g., computer science, economics, chemistry, and medicine.

But such problems are computationally very challenging, requiring increasingly sophisticated algorithm design, and there is a poor scientific understanding of how these complex algorithms, called combinatorial solvers, work. More importantly, even mature commercial solvers are known to sometimes produce wrong results.

As these algorithms are being given control of our economy, our livelihoods, and sometimes even our lives, an urgent task is to ensure that the results they compute are correct and verifiable.This project aims to lay the foundation for a new generation of combinatorial solvers with proof logging, meaning that solvers output not only a result but also a machine-verifiable proof that this result has been computed correctly.

One can then feed the problem, solution, and proof to a dedicated proof checker to verify that there are no errors.

Crucially, such proofs should require low overhead to generate and be easy to check, but should supply 100% guarantees of correctness.My ultimate goal is to change the field of combinatorial optimization in such a way that solvers are not only made ever more efficient, but also produce verifiably correct results as a standard feature, so that the results produced by solvers always come with a proof that they are in fact valid.