TECoSA Seminar – Towards a Design Flow for Verified AI-Based Autonomy

We aim to bring you a TECoSA Seminar each month during term-time.  All are welcome to attend and we look forward to some lively discussions. Members can accept the Outlook invitations, non-members can email tecosa-admin@kth.se to register.

Our April seminar is with Sanjit Seshia, Cadence Founders Chair Professor in the Department of Electrical Engineering and Computer Sciences (EECS) at the University of California, Berkeley. The seminar will take place at Digital Futures hub, floor 2 at KTH main Campus. It will also be possible to attend the seminar via Zoom. For more information on Digital Futures, click here.

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.

Bio: Sanjit A. Seshia is the Cadence Founders Chair Professor in the Department of Electrical Engineering and Computer Sciences (EECS) at the University of California, Berkeley. His research interests are in formal methods for dependable and secure computing, spanning the areas of cyber-physical systems (CPS), computer security, distributed systems, artificial intelligence (AI), machine learning, and robotics. 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 EECS education, the IEEE TCCPS Mid-Career Award, a Distinguished Alumnus Award from IIT Bombay, and the Computer-Aided Verification (CAV) Award for contributions to the foundations of SMT solving. He is a Fellow of the ACM and the IEEE.