| Title | Robustness Contracts for Scalable Verification of Neural Network-Enabled Cyber-Physical Systems |
| Publication Type | Conference Paper |
| Year of Publication | 2020 |
| Authors | Naik, Nikhil, Nuzzo, Pierluigi |
| Conference Name | 2020 18th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE) |
| Date Published | dec |
| Keywords | Artificial neural networks, Complexity theory, compositionality, contract-based design, contracts, Cyber-physical systems, deep reinforcement learning, Neural networks, Predictive Metrics, Programming, pubcrawl, Resiliency, Robustness, Safety, Scalability, scalable verification, verification |
| Abstract | The proliferation of artificial intelligence based systems in all walks of life raises concerns about their safety and robustness, especially for cyber-physical systems including multiple machine learning components. In this paper, we introduce robustness contracts as a framework for compositional specification and reasoning about the robustness of cyber-physical systems based on neural network (NN) components. Robustness contracts can encompass and generalize a variety of notions of robustness which were previously proposed in the literature. They can seamlessly apply to NN-based perception as well as deep reinforcement learning (RL)-enabled control applications. We present a sound and complete algorithm that can efficiently verify the satisfaction of a class of robustness contracts on NNs by leveraging notions from Lagrangian duality to identify system configurations that violate the contracts. We illustrate the effectiveness of our approach on the verification of NN-based perception systems and deep RL-based control systems. |
| DOI | 10.1109/MEMOCODE51338.2020.9315118 |
| Citation Key | naik_robustness_2020 |
Robustness Contracts for Scalable Verification of Neural Network-Enabled Cyber-Physical Systems