Challenges in Assuring AI
Abstract: 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 that will encounter situations the designers never considered? This talk will attempt to lay out the problem space with insights into the structure of AI, and offer some ideas for how the verification community might start tackling the problem of assuring AI.
BIO: Dr. John Launchbury is chief scientist at Galois Inc., where he is working to leverage formal mathematical techniques to fundamentally improve cybersecurity. Dr. Launchbury was the original founder of Galois in 1999.Prior to rejoining Galois in 2017, John was Director of the Information Innovation Office (I2O) at DARPA, where he led nation-scale investments in cybersecurity and artificial intelligence. John received First Class Honors in Mathematics from Oxford University in 1985. He holds a Ph.D. in Computing Science from University of Glasgow and won the British Computer Society’s distinguished dissertation prize. In 2000 he became a full professor in Computer Science and Engineering at the OGI School of Science and Engineering at OHSU. In 2010, John was inducted as a Fellow of the Association for Computing Machinery (ACM).