Towards Safe, Intelligent, and Interactive Autonomous Systems

Speaker: Sanjit A. Seshia
Affiliation: UC Berkeley

Abstract: Society is rapidly advancing towards autonomous cyber-physical systems (CPS) that are intelligent and interactive — that is, they must learn from experience and collaborate with humans. Examples include semi-autonomous vehicles interacting with drivers and pedestrians, medical robots interacting with doctors and nurses, and many more. The safety-critical nature of these systems requires us to provide strong correctness guarantees on their performance in interaction with humans. However, the combination of intelligence and autonomy in these systems, and their interactions with humans, make them particularly challenging for verification and control.

In this talk, I will discuss our recent work on the topics of safe and interactive autonomy and verified intelligent systems. First, I will describe a learning-based game-theoretic approach to design autonomous systems that are mindful of their effects on humans, and further leverage these effects for better efficiency, coordination, and estimation. I will also discuss techniques to systematically verify robustness and safety of such systems. Next, I will discuss the use of machine learning, including deep learning, in perception components of CPS, and present our approach to verifying such systems. Finally, I will discuss the broader challenges for verified artificial intelligence, and corresponding promising directions to tackle these challenges.

Biography: Sanjit A. Seshia is a Professor in the Department of Electrical Engineering and Computer Sciences at the University of California, Berkeley. He received an M.S. and Ph.D. in Computer Science from Carnegie Mellon University, and a B.Tech. in Computer Science and Engineering from the Indian Institute of Technology, Bombay. His current research interests center on formal methods and their application to cyber-physical systems, computer security, and artificial intelligence. His Ph.D. 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, the Donald O. Pederson Best Paper Award for the IEEE Transactions on CAD, and the School of Computer Science Distinguished Dissertation Award at Carnegie Mellon University.

For more information, contact Prof. Paulo Tabuada (Tabuada@ucla.edu)

Date/Time:
Date(s) - Oct 02, 2017
12:30 pm - 1:30 pm

Location:
EE-IV Shannon Room #54-134
420 Westwood Plaza - 5th Flr., Los Angeles CA 90095