Safe and Effective Learning through Formal Simulation


At a glance

Introduction and Motivation
Neural networks are powerful models that have recently achieved impressive accuracy in various computer vision tasks, e.g. object detection, segmentation. For this reason, they are starting to be extensively used in autonomous vehicle (AV) technology. Since autonomous vehicles are safety-critical, accuracy as well as robustness of the neural networks are of utmost importance. However, training a robust neural network with high accuracy is expensive. Collecting a large and diverse training dataset and the annotation process normally requires a lot of manual effort. In addition, with larger datasets, the training process tends to cost more time and energy. A central question is: How can we generate a large and diverse dataset that increases accuracy of the network, maintains training efficiency, and improves safety of the overall closed-loop autonomous vehicle?
We plan to leverage simulation environments that are now getting more attention in the autonomous driving, computer vision (CV) and machine learning (ML) communities. However, most of the work on simulation environments is on creating a realistic environment that can produce large amounts of training data. Our focus is to use existing simulation environments more effectively for safe and accurate learning by using formal methods -- an approach we term formal simulation.

Research agenda and challenges
We plan to build upon the previous work in PI Seshia’s group on simulation-based falsification of systems with ML (deep learning) components [DDS17], which identifies corner-case scenarios that could lead to safety violations. This approach can synthesize inputs (including images) that cause a deep learning based system to enter an unsafe state. A key contribution is a framework for synthesizing images to do systematic testing of Convolutional Neural Networks for autonomous driving [DGSS17]. A prototype tool has been built on top of the Udacity Self-Driving Simulator, and preliminary results can be seen in this video: In order to get synthesized images of higher fidelity and get a higher-dimension modification space, we are building a simulation environment based on Grand Theft Auto V (GTA-V), a commercial video game. In our simulation environment, various aspects of the scene and each vehicle can be controlled (in theory), giving huge flexibility in generating a great variety of traffic scenarios. The following video illustrates our current capabilities in synthesizing scenes with various features: However, the scalability, usability and effectiveness of this approach needs to be greatly improved. In this project, we propose to create a robust formal simulation-based dataset synthesizer with the following three aspects:

Driving scenario description language: We plan to develop a driving scenario description language to let the user be able to declaratively specify desired traffic scenarios (e.g. "a line of cars viewed at roughly a 60 degree angle"). Then our simulation takes the description as input and instantiates them into concrete driving scenes. To our best knowledge, no similar description language has been presented before. This language/framework would help generate traffic scenarios that are hard to get in the real world, e.g. traffic accidents, and the collected labeled data can be valuable for the training process to get robust neural nets.
Diverse synthesized dataset and neural nets testing/retraining: The training data points in most current datasets for autonomous driving are not well organized in terms of driving scenarios. We plan to adapt and extend systematic constraint-based sampling methods developed in the formal verification community to generate a “diverse” synthesized dataset for autonomous driving. For each kind of driving scenario, such as bumper-to-bumper traffic,lane merges, or dangerous intersections, a large number of scenes will be generated. For each scene, various ground-truth data, such as pixel segmentation label, 3D bounding box of each vehicle, 3D Lidar point cloud, etc. will be also collected for training purposes. The whole dataset can then be used to systematically test the robustness and accuracy of different neural nets for autonomous driving purposes. We will focus (at least initially) on SqueezeDet [W+16] to test our methods.
Targeted data augmentation and domain adaptation: A simulation environment provides good control over the driving scene, which can be leveraged for targeted data augmentation and domain adaptation. The performance of the neural nets would be first evaluated on synthesized data. As our final goal is to get high performance on real-world data, domain adaptation methods will also be explored to make the neural nets perform well on real-world datasets. This task will be coordinated with a complementary effort on domain adaptation in Prof. Keutzer’s group.

principal investigatorsresearchersthemes
Sanjit SeshiaKurt KeutzerDeep Neural Networks, Simulation, Verification, Testing, Training Data Generation/Augmentation