Neural Network Repair with Reachability Analysis

Abstract

Safety is a critical concern for the next generation of autonomy that is likely to rely heavily on deep neural networks for perception and control. Formally verifying the safety and robustness of well-trained DNNs and learning-enabled systems under attacks, model uncertainties, and sensing errors is essential for safe autonomy. This research proposes a framework to repair unsafe DNNs in safety-critical systems with reachability analysis. The repair process is inspired by adversarial training which has demonstrated high effectiveness in improving the safety and robustness of DNNs. Different from traditional adversarial training approaches where adversarial examples are utilized from random attacks and may not be representative of all unsafe behaviors, our repair process uses reachability analysis to compute the exact unsafe regions and identify sufficiently representative examples to enhance the efficacy and efficiency of the adversarial training. The performance of our framework is evaluated on two types of benchmarks without safe models as references. One is a DNN controller for aircraft collision avoidance with access to training data. The other is a rocket lander where our framework can be seamlessly integrated with the well-known deep deterministic policy gradient (DDPG) reinforcement learning algorithm. The experimental results show that our framework can successfully repair all instances on multiple safety specifications with negligible performance degradation. In addition, to increase the computational and memory efficiency of the reachability analysis algorithm, we propose a depth-first-search algorithm that combines an existing exact analysis method with an over-approximation approach based on a new set representation. Experimental results show that our method achieves a five-fold improvement in runtime and a two-fold improvement in memory usage compared to exact analysis.

References in corpus (21)

• Continuous control with deep reinforcement learning
• Obfuscated Gradients Give a False Sense of Security: Circumventing Defenses to Adversarial Examples
• Theoretically Principled Trade-off between Robustness and Accuracy
• Efficient Neural Network Robustness Certification with General Activation Functions
• Evaluating Robustness of Neural Networks with Mixed Integer Programming
• Formal Security Analysis of Neural Networks using Symbolic Intervals
• An approach to reachability analysis for feed-forward ReLU neural networks
• Towards Fast Computation of Certified Robustness for ReLU Networks
• A Unified View of Piecewise Linear Neural Network Verification
• Reachable Set Computation and Safety Verification for Neural Networks with ReLU Activations
• Guaranteeing Safety for Neural Network-Based Aircraft Collision Avoidance Systems
• End-to-End Safe Reinforcement Learning through Barrier Functions for Safety-Critical Continuous Control Tasks
• Reinforcement Learning with Probabilistic Guarantees for Autonomous Driving
• Neurosymbolic Reinforcement Learning with Formally Verified Exploration
• Reachability Analysis for Feed-Forward Neural Networks using Face Lattices
• Repairing Deep Neural Networks: Fix Patterns and Challenges
• Scalable Synthesis of Verified Controllers in Deep Reinforcement Learning
• Robustness to Adversarial Attacks in Learning-Enabled Controllers
• A Review of Formal Methods applied to Machine Learning
• Reachability Analysis of Convolutional Neural Networks
• Runtime-Safety-Guided Policy Repair