Verification of Neural Network Control Systems using Symbolic Zonotopes and Polynotopes
Not on the map. Why?
Abstract (arXiv)
Verification and safety assessment of neural network controlled systems (NNCSs) is an emerging challenge. To provide guarantees, verification tools must efficiently capture the interplay between the neural network and the physical system within the control loop. In this paper, a compositional approach focused on inclusion preserving long term symbolic dependency modeling is proposed for the analysis of NNCSs. First of all, the matrix structure of symbolic zonotopes is exploited to efficiently abstract the input/output mapping of the loop elements through (inclusion preserving) affine symbolic expressions, thus maintaining linear dependencies between interacting blocks. Then, two further extensions are studied. Firstly, symbolic polynotopes are used to abstract the loop elements behaviour by means of polynomial symbolic expressions and dependencies. Secondly, an original input partitioning algorithm takes advantage of symbol preservation to assess the sensitivity of the computed approximation to some input directions. The approach is evaluated via different numerical examples and benchmarks. A good trade-off between low conservatism and computational efficiency is obtained.
Key facts. Cited by 3 papers in the map (data through 13 Oct 2026). Builds on 20 of its 39 references that are in the map. First posted on arXiv 26 Jun 2023.
Builds on
20 of 39 references.
References · 20
- 2013Intriguing properties of neural networkscited by 5,137
- 2016Adversarial examples in the physical worldcited by 1,767
- 2017Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networkscited by 742
- 2018Efficient Neural Network Robustness Certification with General Activation Functionscited by 442
- 2018On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Modelscited by 326
- 2019Algorithms for Verifying Deep Neural Networkscited by 221
- 2018Formal Security Analysis of Neural Networks using Symbolic Intervalscited by 185
- 2020NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systemscited by 128
- 2019Safety Verification and Robustness Analysis of Neural Networks via Quadratic Constraints and Semidefinite Programmingcited by 100
- 2017Output Reachable Set Estimation and Verification for Multi-Layer Neural Networkscited by 80
- 2020Verification of Deep Convolutional Neural Networks Using ImageStarscited by 75
- 2020Reach-SDP: Reachability Analysis of Closed-Loop Systems with Neural Network Controllers via Semidefinite Programmingcited by 43
8 more
- 2021OVERT: An Algorithm for Safety Verification of Neural Network Control Policies for Nonlinear Systemscited by 38
- 2020Reachable Set Estimation for Neural Network Control Systems: A Simulation-Guided Approachcited by 36
- 2017Output Range Analysis for Deep Neural Networkscited by 30
- 2019ReachNN: Reachability Analysis of Neural-Network Controlled Systemscited by 26
- 2021Verification of Neural-Network Control Systems by Integrating Taylor Models and Zonotopescited by 26
- 2021Efficient Reachability Analysis of Closed-Loop Systems with Neural Network Controllerscited by 10
- 2020Safety Verification of Neural Network Controlled Systemscited by 9
- 2020Functional sets with typed symbols : Mixed zonotopes and Polynotopes for hybrid nonlinear reachability and filteringcited by 2
Built on by
Citing papers per year: 2024: 2; 2025: 1.
3 papers.