Date and time: 7 April 2025, 10:00-11:00 followed by 30 min for questions
Speaker: Sanjit A. Seshia, University of California, Berkeley
Title: Towards a Design Flow for Verified AI-Based Autonomy
Where: Digital Futures hub, Osquars Backe 5, floor 2 at KTH main campus OR Zoom
Directions: https://www.digitalfutures.kth.se/contact/how-to-get-here/
OR
Zoom: https://kth-se.zoom.us/j/69560887455
This is joint TECoSA and Digital Futures seminar.
Host: Martin Törngren
Bio: Sanjit A. Seshia is a Professor in the Department of Electrical Engineering and Computer Sciences at the University of California, Berkeley.
He received an MS and PhD in Computer Science from Carnegie Mellon University, and a BTech in Computer Science and Engineering from the Indian Institute of Technology, Bombay.
His research interests are in dependable computing and computational logic, with a current focus on applying automated formal methods to problems in cyber-physical systems, computer security, electronic design automation, and synthetic biology. His PhD thesis work on the UCLID verifier and decision procedure helped pioneer the area of satisfiability modulo theories (SMT) and SMT-based verification.
He is co-author of a widely-used textbook on embedded cyber-physical systems, and has led the development of technologies for cyber-physical systems education based on formal methods. His awards and honors include a Presidential Early Career Award for Scientists and Engineers (PECASE), an Alfred P. Sloan Research Fellowship, the Frederick Emmons Terman Award for contributions to electrical engineering and computer science education, and the School of Computer Science Distinguished Dissertation Award at Carnegie Mellon University.
Abstract: Verified artificial intelligence (AI) is the goal of designing AI systems that have strong, ideally provable, assurances of correctness with respect to formally-specified requirements. This talk will review the main challenges to achieving Verified AI, and the progress the research community has made towards this goal.
A particular focus will be on AI-based autonomous and semi-autonomous cyber-physical systems (CPS), and on the role of environment/world modelling throughout the design cycle. We argue for developing a new generation of design automation techniques, rooted in formal methods, to enable and support the routine development of high assurance AI-based autonomy.
I will describe our work on formal methods for Verified AI-based autonomy, implemented in the open-source Scenic and VerifAI toolkits. The use of these tools will be demonstrated in industrial case studies involving deep learning-based autonomy in ground and air vehicles. We conclude with an outlook to the future of the Verified AI agenda.
