Visible to the public Robustness Contracts for Scalable Verification of Neural Network-Enabled Cyber-Physical Systems

TitleRobustness Contracts for Scalable Verification of Neural Network-Enabled Cyber-Physical Systems
Publication TypeConference Paper
Year of Publication2020
AuthorsNaik, Nikhil, Nuzzo, Pierluigi
Conference Name2020 18th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE)
Date Publisheddec
KeywordsArtificial 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
AbstractThe 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.
Citation Keynaik_robustness_2020