| dc.description.abstract | Deep Neural Networks (DNNs) have been increasingly applied in safety-critical applications such as self-driving cars, unmanned underwater vehicles (UUV), and medical image diagnostics recently. The ability to learn sophisticated features and functions makes DNNs outstanding compared to other techniques in solving complicated tasks. At the same time, due to high nonlinearity, DNNs behaviors are generally unpredictable. Additionally, they are also vulnerable to adversarial attacks, where slightly changing in the input can cause a dramatic change in the output of a network.
Since the failure of DNNs-based components in safety-critical systems can cause the loss of human lives, there is an urgent need for methods and tools to verify/certificate the safety and robustness of such systems. In this thesis, I propose a formal framework for verifying the safety and robustness of DNNs and learning-enabled Cyber-Physical Systems (CPS) using reachability analysis. The crux of our approach is a collection of reachability algorithms performing on novel geometrical set data structures that represent the bounded uncertainty of the input of a DNN or the initial conditions of a learning-enabled CPS efficiently. The proposed reachability algorithms construct a reachable set containing all possible outputs corresponding to the bounded uncertainty of a system. The reachable set is then used to reason about the safety or robustness of the systems. Our framework has been implemented in NNV, a neural network verification tool written in Matlab and Python that is gaining much attention from the research community and industry. Our generic framework has been tacked the following challenging subjects successfully: 1) safety and robustness verification of deep feed-forward neural networks (FNNs), 2) safety verification of neural-network-based control systems, 3) robustness verification of deep image classification convolutional neural networks (CNNs), 4) robustness verification of deep semantic segmentation networks (SSNs). | |
