DIKU Bits: Sure, your algorithm is really fast, but is it really correct?

Speaker

Jakob Nordström, Professor in the Algorithms and Complexity (AC) section

Title

Sure, your algorithm is really fast, but is it really correct?

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 when this is the case. This talk is about a way of solving this problem: to use proof logging to make the algorithm output not only an answer, but a machine-verifiable proof that this answer has been computed correctly.

Which courses do you teach?

I am teaching Advanced Algorithms and Data Structures (MSc level), Computability and Complexity (MSc level) and Introduction to Discrete Mathematics and Algorithms (BSc level)

Which technology/research/projects/startup are you excited to see the evolution of?

Automated reasoning has undergone a silent revolution since the turn of the millennium --- arguably every bit as impressive as machine learning, and with applications all over science and industry, but with less of a marketing splash. I believe that the most promising direction to make ML models robust, reliable, and explainable is to combine them with symbolic automated reasoning, and there should be huge potential for proof logging techniques to play an important role here.