Topic: Sure, Your Algorithm Is Really Fast, But Is It Really Correct?

When: 15 April 12.00 to 13.00

Where: Online

Speaker: Jakob Nordström, University of Copenhagen and Lund University

Moderator: Jacek Malec, Computer Science, Lund University 

Spoken language: English

Abstract

Ensuring correctness of computer software, safety of air traffic control, and validity of smart crypto contracts are examples of extremely challenging problems for which modern research has delivered inexplicably efficient algorithms. There is only one catch: These amazing algorithms are sometimes wrong. And we currently have no way of knowing for sure when this is the case. As these tools are increasingly being used autonomously, sometimes even in life-critical applications, it is urgent to ensure that what they compute is valid.

This talk is about the most promising way of solving this problem: to use proof logging to make the algorithms output not only an answer, but a machine-verifiable proof that this answer has been computed correctly. Crucially, such proofs should require low overhead to generate and be easy to check, but should still supply 100% correctness guarantees.

Proof logging has witnessed a revolution of its own in the last decade, which promises to open up also new possibilities for algorithm development and analysis, software debugging, and even research into AI explainability. We will give an introduction to what proof logging is, describe how it works, and discuss what it can be used for.