Assuring AI

John Launchbury, Chief Scientist of Galois Inc, gives the second keynote of the ICFP conference. Somewhat ironically, just as traditional systems software finally comes within reach of detailed mathematical verification, the demand for verification technology is rapidly expanding into domains that pose very different kinds of challenges. How could a face recognition technology be verified, for example, when it is not clear even how to state a correctness property? Or how should we attempt to verify an autonomous system like a self-driving car? This talk will attempt to lay out the problem space, and offer some ideas for how the verification community might start tackling the problem of assuring AI.