Ensuring the safety and reliability of AI-based autonomous systems like self-driving cars remains a difficult problem, due to the overwhelming complexity of such systems and the environments they must operate in. In this talk, I will describe tools which enable the rigorous design of such systems through formal models and analysis: Scenic and VerifAI. Scenic is a probabilistic environment modeling language that allows encoding complex scenarios in a concise and readable yet fully-precise way: for example, the scenario “a badly-parked car, which suddenly pulls into the road as the AV approaches” could be encoded by a Scenic program in just a few lines. Scenic scenarios can be used not only to drive testing in simulation, but also to generate synthetic data, which can be used for example to eliminate bugs in ML-based perception systems through targeted retraining. Our VerifAI tool builds on Scenic to provide a unified framework for retraining and many other tasks in the design of AI-based systems, including modeling, falsification, debugging, and synthesis. I will give a general overview of our work with these tools, including case studies finding bugs in industrial cyber-physical systems from several domains, both in simulation and in the real world.

 

 

Daniel Fremont is an Assistant Professor in the Computer Science and Engineering department at the University of California, Santa Cruz. He works in the area of formal methods, using automated reasoning to improve the reliability of software, hardware, and cyber-physical systems. He develops practical algorithms for system design, verification, and testing, as well as theory for the core computational problems underlying them. He received the ACM SIGBED Paul Caspi Memorial Dissertation Award for his work on algorithmic improvisation, a mathematical framework enabling the correct-by-construction synthesis of systems which use randomness to enhance robustness, variety, or unpredictability. Among other applications, he has used his tools to synthesize robotic controllers, verify quantitative security properties of programs, and systematically test and train machine learning models for autonomous vehicles.