Scalable Surrogate Verification of Image-based Neural Network Control Systems using Composition and Unrolling

• URL: http://arxiv.org/abs/2405.18554v1
• Date: Tue, 28 May 2024 19:56:53 GMT
• Title: Scalable Surrogate Verification of Image-based Neural Network Control Systems using Composition and Unrolling
• Authors: Feiyang Cai, Chuchu Fan, Stanley Bak,
• Abstract summary: We build on work that considers a surrogate verification approach, training a conditional generative adversarial network (cGAN) as an image generator in place of the real world. We overcome one-step error by composing the system's dynamics along with the cGAN and neural network controller. We reduce multi-step error by repeating the single-step composition, essentially unrolling multiple steps of the control loop into a large neural network.
• Score: 9.633494094538017
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Verifying safety of neural network control systems that use images as input is a difficult problem because, from a given system state, there is no known way to mathematically model what images are possible in the real-world. We build on recent work that considers a surrogate verification approach, training a conditional generative adversarial network (cGAN) as an image generator in place of the real world. This enables set-based formal analysis of the closed-loop system, providing analysis beyond simulation and testing. While existing work is effective on small examples, excessive overapproximation both within a single control period and across multiple control periods limits its scalability. We propose approaches to overcome these two sources of error. First, we overcome one-step error by composing the system's dynamics along with the cGAN and neural network controller, without losing the dependencies between input states and the control outputs as in the monotonic analysis of the system dynamics. Second, we reduce multi-step error by repeating the single-step composition, essentially unrolling multiple steps of the control loop into a large neural network. We then leverage existing network verification tools to compute accurate reachable sets for multiple steps, avoiding the accumulation of abstraction error at each step. We demonstrate the effectiveness of our approach in terms of both accuracy and scalability using two case studies: an autonomous aircraft taxiing system and an advanced emergency braking system. On the aircraft taxiing system, the converged reachable set is 175% larger using the prior baseline method compared with our proposed approach. On the emergency braking system, with 24x the number of image output variables from the cGAN, the baseline method fails to prove any states are safe, whereas our improvements enable set-based safety analysis.

Related papers

• Verification of Neural Network Control Systems in Continuous Time [1.5695847325697108]
  We develop the first verification method for continuously-actuated neural network control systems. We accomplish this by adding a level of abstraction to model the neural network controller. We demonstrate the approach's efficacy by applying it to a vision-based autonomous airplane taxiing system.
  arXiv  Detail & Related papers  (2024-05-31T19:39:48Z)
• Transfer learning-based physics-informed convolutional neural network for simulating flow in porous media with time-varying controls [0.0]
  A physics-informed convolutional neural network is proposed to simulate two phase flow in porous media. finite volume scheme is adopted to discretize flow equations. N Neumann boundary conditions are seamlessly incorporated into the semi-discretized equations.
  arXiv  Detail & Related papers  (2023-10-10T05:29:33Z)
• Interval Reachability of Nonlinear Dynamical Systems with Neural Network Controllers [5.543220407902113]
  This paper proposes a computationally efficient framework, based on interval analysis, for rigorous verification of nonlinear continuous-time dynamical systems with neural network controllers. Inspired by mixed monotone theory, we embed the closed-loop dynamics into a larger system using an inclusion function of the neural network and a decomposition function of the open-loop system. We show that one can efficiently compute hyper-rectangular over-approximations of the reachable sets using a single trajectory of the embedding system.
  arXiv  Detail & Related papers  (2023-01-19T06:46:36Z)
• Finite-time System Identification and Adaptive Control in Autoregressive Exogenous Systems [79.67879934935661]
  We study the problem of system identification and adaptive control of unknown ARX systems. We provide finite-time learning guarantees for the ARX systems under both open-loop and closed-loop data collection.
  arXiv  Detail & Related papers  (2021-08-26T18:00:00Z)
• Manifold Regularized Dynamic Network Pruning [102.24146031250034]
  This paper proposes a new paradigm that dynamically removes redundant filters by embedding the manifold information of all instances into the space of pruned networks. The effectiveness of the proposed method is verified on several benchmarks, which shows better performance in terms of both accuracy and computational cost.
  arXiv  Detail & Related papers  (2021-03-10T03:59:03Z)
• Control of Stochastic Quantum Dynamics with Differentiable Programming [0.0]
  We propose a framework for the automated design of control schemes based on differentiable programming. We apply this approach to state preparation and stabilization of a qubit subjected to homodyne detection. Despite the resulting poor signal-to-noise ratio, we can train our controller to prepare and stabilize the qubit to a target state with a mean fidelity around 85%.
  arXiv  Detail & Related papers  (2021-01-04T19:00:03Z)
• Optimizing Mixed Autonomy Traffic Flow With Decentralized Autonomous Vehicles and Multi-Agent RL [63.52264764099532]
  We study the ability of autonomous vehicles to improve the throughput of a bottleneck using a fully decentralized control scheme in a mixed autonomy setting. We apply multi-agent reinforcement algorithms to this problem and demonstrate that significant improvements in bottleneck throughput, from 20% at a 5% penetration rate to 33% at a 40% penetration rate, can be achieved.
  arXiv  Detail & Related papers  (2020-10-30T22:06:05Z)
• A Hamiltonian Monte Carlo Method for Probabilistic Adversarial Attack and Learning [122.49765136434353]
  We present an effective method, called Hamiltonian Monte Carlo with Accumulated Momentum (HMCAM), aiming to generate a sequence of adversarial examples. We also propose a new generative method called Contrastive Adversarial Training (CAT), which approaches equilibrium distribution of adversarial examples. Both quantitative and qualitative analysis on several natural image datasets and practical systems have confirmed the superiority of the proposed algorithm.
  arXiv  Detail & Related papers  (2020-10-15T16:07:26Z)
• Reach-SDP: Reachability Analysis of Closed-Loop Systems with Neural Network Controllers via Semidefinite Programming [19.51345816555571]
  We propose a novel forward reachability analysis method for the safety verification of linear time-varying systems with neural networks in feedback. We show that we can compute these approximate reachable sets using semidefinite programming. We illustrate our method in a quadrotor example, in which we first approximate a nonlinear model predictive controller via a deep neural network and then apply our analysis tool to certify finite-time reachability and constraint satisfaction of the closed-loop system.
  arXiv  Detail & Related papers  (2020-04-16T18:48:25Z)
• Logarithmic Regret Bound in Partially Observable Linear Dynamical Systems [91.43582419264763]
  We study the problem of system identification and adaptive control in partially observable linear dynamical systems. We present the first model estimation method with finite-time guarantees in both open and closed-loop system identification. We show that AdaptOn is the first algorithm that achieves $textpolylogleft(Tright)$ regret in adaptive control of unknown partially observable linear dynamical systems.
  arXiv  Detail & Related papers  (2020-03-25T06:00:33Z)
• Firearm Detection and Segmentation Using an Ensemble of Semantic Neural Networks [62.997667081978825]
  We present a weapon detection system based on an ensemble of semantic Convolutional Neural Networks. A set of simpler neural networks dedicated to specific tasks requires less computational resources and can be trained in parallel. The overall output of the system given by the aggregation of the outputs of individual networks can be tuned by a user to trade-off false positives and false negatives.
  arXiv  Detail & Related papers  (2020-02-11T13:58:16Z)

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.