Compositional Inductive Invariant Based Verification of Neural Network Controlled Systems

• URL: http://arxiv.org/abs/2312.10842v2
• Date: Tue, 26 Mar 2024 19:45:15 GMT
• Title: Compositional Inductive Invariant Based Verification of Neural Network Controlled Systems
• Authors: Yuhao Zhou, Stavros Tripakis,
• Abstract summary: This paper introduces a novel approach to NNCS safety verification, leveraging the inductive invariant method. We present an algorithm capable of automatically verifying the inductiveness of given candidates by automatically inferring the necessary decomposition predicates.
• Score: 11.811233105411976
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: The integration of neural networks into safety-critical systems has shown great potential in recent years. However, the challenge of effectively verifying the safety of Neural Network Controlled Systems (NNCS) persists. This paper introduces a novel approach to NNCS safety verification, leveraging the inductive invariant method. Verifying the inductiveness of a candidate inductive invariant in the context of NNCS is hard because of the scale and nonlinearity of neural networks. Our compositional method makes this verification process manageable by decomposing the inductiveness proof obligation into smaller, more tractable subproblems. Alongside the high-level method, we present an algorithm capable of automatically verifying the inductiveness of given candidates by automatically inferring the necessary decomposition predicates. The algorithm significantly outperforms the baseline method and shows remarkable reductions in execution time in our case studies, shortening the verification time from hours (or timeout) to seconds.

Related papers

• Automated Design of Linear Bounding Functions for Sigmoidal Nonlinearities in Neural Networks [23.01933325606068]
  Existing complete verification techniques offer provable guarantees for all robustness queries but struggle to scale beyond small neural networks. We propose a novel parameter search method to improve the quality of these linear approximations. Specifically, we show that using a simple search method, carefully adapted to the given verification problem through state-of-the-art algorithm configuration techniques, improves the average global lower bound by 25% on average over the current state of the art.
  arXiv  Detail & Related papers  (2024-06-14T16:16:26Z)
• Learning-Based Verification of Stochastic Dynamical Systems with Neural Network Policies [7.9898826915621965]
  We use a verification procedure that trains another neural network, which acts as a certificate proving that the policy satisfies the task. For reach-avoid tasks, it suffices to show that this certificate network is a reach-avoid supermartingale (RASM)
  arXiv  Detail & Related papers  (2024-06-02T18:19:19Z)
• Lyapunov-stable Neural Control for State and Output Feedback: A Novel Formulation [67.63756749551924]
  Learning-based neural network (NN) control policies have shown impressive empirical performance in a wide range of tasks in robotics and control. Lyapunov stability guarantees over the region-of-attraction (ROA) for NN controllers with nonlinear dynamical systems are challenging to obtain. We demonstrate a new framework for learning NN controllers together with Lyapunov certificates using fast empirical falsification and strategic regularizations.
  arXiv  Detail & Related papers  (2024-04-11T17:49:15Z)
• Unifying Qualitative and Quantitative Safety Verification of DNN-Controlled Systems [18.049286149364075]
  The rapid advance of deep reinforcement learning techniques enables the oversight of safety-critical systems through the utilization of Deep Neural Networks (DNNs) Most of the existing verification approaches rely on qualitative approaches, predominantly employing reachability analysis. We propose a novel framework for unifying both qualitative and quantitative safety verification problems.
  arXiv  Detail & Related papers  (2024-04-02T09:31:51Z)
• The #DNN-Verification Problem: Counting Unsafe Inputs for Deep Neural Networks [94.63547069706459]
  #DNN-Verification problem involves counting the number of input configurations of a DNN that result in a violation of a safety property. We propose a novel approach that returns the exact count of violations. We present experimental results on a set of safety-critical benchmarks.
  arXiv  Detail & Related papers  (2023-01-17T18:32:01Z)
• Quantization-aware Interval Bound Propagation for Training Certifiably Robust Quantized Neural Networks [58.195261590442406]
  We study the problem of training and certifying adversarially robust quantized neural networks (QNNs) Recent work has shown that floating-point neural networks that have been verified to be robust can become vulnerable to adversarial attacks after quantization. We present quantization-aware interval bound propagation (QA-IBP), a novel method for training robust QNNs.
  arXiv  Detail & Related papers  (2022-11-29T13:32:38Z)
• Backward Reachability Analysis of Neural Feedback Loops: Techniques for Linear and Nonlinear Systems [59.57462129637796]
  This paper presents a backward reachability approach for safety verification of closed-loop systems with neural networks (NNs) The presence of NNs in the feedback loop presents a unique set of problems due to the nonlinearities in their activation functions and because NN models are generally not invertible. We present frameworks for calculating BP over-approximations for both linear and nonlinear systems with control policies represented by feedforward NNs.
  arXiv  Detail & Related papers  (2022-09-28T13:17:28Z)
• Comparative Analysis of Interval Reachability for Robust Implicit and Feedforward Neural Networks [64.23331120621118]
  We use interval reachability analysis to obtain robustness guarantees for implicit neural networks (INNs) INNs are a class of implicit learning models that use implicit equations as layers. We show that our approach performs at least as well as, and generally better than, applying state-of-the-art interval bound propagation methods to INNs.
  arXiv  Detail & Related papers  (2022-04-01T03:31:27Z)
• Neural Network Verification in Control [3.3123634393237706]
  This tutorial first introduces and unifies recent techniques for verifying robustness properties of NNs. The techniques are then extended to provide formal guarantees of neural feedback loops. The provided tools are shown to enable closed-loop reachability analysis and robust deep reinforcement learning.
  arXiv  Detail & Related papers  (2021-09-30T22:28:44Z)
• Fast Falsification of Neural Networks using Property Directed Testing [0.1529342790344802]
  We propose a falsification algorithm for neural networks that directs the search for a counterexample. Our algorithm uses a derivative-free sampling-based optimization method. We show that our falsification procedure detects all the unsafe instances that other verification tools also report as unsafe.
  arXiv  Detail & Related papers  (2021-04-26T09:16:27Z)
• GraN: An Efficient Gradient-Norm Based Detector for Adversarial and Misclassified Examples [77.99182201815763]
  Deep neural networks (DNNs) are vulnerable to adversarial examples and other data perturbations. GraN is a time- and parameter-efficient method that is easily adaptable to any DNN. GraN achieves state-of-the-art performance on numerous problem set-ups.
  arXiv  Detail & Related papers  (2020-04-20T10:09:27Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.