| Integrated Static and Dynamic Approaches to High-Assurance for Learning-Enabled Cyber-Physical Systems |
Overview
The project aims to develop techniques to provide safety assurance for autonomous vehicles that rely on learning-enabled components (LECs) for perception and control.
Machine learning promises a potentially revolutionary way for extracting semantic meaning suitable for higher-level autonomy. Unfortunately, our current lack of understanding of when and how machine learning works, makes it challenging to provide guarantees for safety critical systems. Despite this, given the impressive experimental results of machine learning, researchers have quickly incorporated learning in perception-action loops even in driverless cars, where the safety requirements are very high. This has resulted in unreliable behavior and public failures (including several fatal accidents involving autonomous vehicles) that may undermine trust in autonomy.
Our approach relies of several inter-related design-time and run-time techniques to provide assurance. At a very high level, design-time analysis provides safety guarantees for the vehicle under certain assumptions about the vehicle's environment and operating scenarios, while run-time monitoring helps ensure that these assumptions are satisfied. The high-level architecture for an autonomous vehicle that relies on technologies developed in out project is shown below. It elaborates on the vision put forth by the DARPA Assured Autonomy program.
Research Thrusts
Verification of deep neural network controllers
We have developed Verisig, a scalable tool for verifying safety properties of closed-loop systems with deep neural network (DNN) controllers. Verisig transforms the DNN into an equivalent hybrid system and composes it with the hybrid system model of the plant. Then, Verisig uses the reachability analysis tool Flow* to check whether the correctness specification for the whole system can be violated.Safety Verification and Robustness Analysis of Neural Networks via Quadratic Constraints and Semidefinite Programming
Analyzing the robustness of neural networks against norm-bounded uncertainties and adversarial attacks in their input has found many applications ranging from safety verification to robust training. In this paper, we propose a semidefinite programming (SDP) framework for safety verification and robustness analysis of neural networks with general activation functions. Our main idea is to abstract various properties of activation functions (e.g., monotonicity, bounded slope, bounded values, and repetition across layers) with the formalism of quadratic constraints. We then analyze the safety properties of the abstracted network via the S-procedure and semidefinite programming. Compared to other semidefinite relaxations proposed in the literature, our method is less conservative, especially for deep networks, with an order of magnitude reduction in computational complexity. Furthermore, our approach is applicable to any activation functions.Manifold-based classifier confidence evaluation
A classifier is an important building block for autonomous systems, but confidence on classification can be very “wrong” on miss-classified prediction. To this end, we propose a confidence auditor based on manifolds. This estimates the confidence of a classifier under dataset shift by exploiting manifolds generated by label-invariant transformations.Online reachability analysis
We apply predictive monitoring techniques to calculate an approximation of the reachable set of states that can be used in dynamic replanning of the mission. To reduce resource requirements of the monitor, we are also developing techniques to approximate the monitor with a deep neural network.Data shift monitoring
Most machine learning techniques rely on statistical assumptions about training data and their relation to the data encountered during operation. Violations of these assumptions are known as data shifts, covariate shifts, prior probability shifts. Many of these problems can be detected using well-known statistical techniques. However, choosing the right technique is tricky and requires considerable expertise. We are developing tools to identify these assumptions and generating appropriate statistical monitors for them.Composable Specifications for Reinforcement Learning
Reinforcement learning has recently emerged as an effective technique for designing controllers for autonomous systems. Its performance, in terms of how well the learned control policy meets the desired goals, crucially depends on user-specified reward functions. The goal of this paper is to allow the user to specify desired tasks only at a high-level without having to worry about low-level reward functions. Our language is rooted in temporal logic (over finite horizon), and allows composable specifications of tasks such as avoiding obstacles, reaching targets, and limiting the usage of resources. The compiler translates the logical specification into a quantitative and nondeterministic monitor that is composed with the controlled system. We then use reinforcement learning to learn a policy that depends on both the state of the system and the state of the monitor. Our framework resolves the nondeterminism in the monitor, and furthermore automatically performs reward shaping to assign partial credit for satisfying subtasks. We have implemented the proposed approach in a tool called SPECTRL. Our experimental evaluation shows that SPECTRL successfully solves a number of control tasks with probability at least 94%, and furthermore outperforms two baselines.Correct-by-construction complex mission planning in unknown environments
Existing works on mission planning assume the existence of a known environmental map. We provide scalable and computationally efficient tools for verified autonomy in the presence of joint semantic-metric map uncertainty. Our tool designs optimal controllers with provable guarantees that accomplish complex tasks expressed using formal languages. This is the first approach that bridges the gap between complex mission planning, simultaneous localization and mapping (SLAM), and active sensing.Assurance cases with dynamic evidence
With increasingly high use of learning enabled components (LECs) in safety-critical cyber physical systems, such as autonomous vehicles, providing guarantees about the safety properties of these systems becomes ever more important. This is challenging because LECs, in particular perception LECs, are often less predictable than conventional components and suffer from very high-dimensional input spaces (e.g., images). New techniques for reasoning about safety of LEC-based systems are just now starting to emerge. These new techniques have to be combined with traditional means of assuring safety of the whole system. We are developing new argument patterns that can be applied to LEC-based system. Some of the evidence that can be used to reason about safety is not available until the system is deployed; in particular evidence to support assumptions about the operatonal environment. We are focusing on techniques to evaluate this evidence at run-time and incorporate them into the overall assurance argument.Personnel
The project team includes members from Penn and University of Virginia.University of Pennsylvania Participants:
|
Faculty: Rajeev Alur Insup Lee (PI) Manfred Morari George Pappas Oleg Sokolsky James Weimer Postdoc Fellows: Mahyar Fazlyab Radoslav Ivanov Yiannis Kantaros |
Graduate Students: Taylor Carpenter Matthew Cleaveland Sooyong Jang Ramneet Kaur Kishor Jothimurugan Sangdon Park |
University of Virginia Participants:
|
Faculty: Nicola Bezzo |
Graduate Students: Esen Yel |
Publications
Downloads
Meetings
Acknowledgement
This project is supported by the Air Force Research Laboratory and the Defense Advanced Research Projects Agency under Contract No. FA8750-18-C-0090. Any opinions, findings and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the Air Force Research Laboratory (AFRL), the Defense Advanced Research Projects Agency (DARPA), the Department of Defense, or the United States Government.