# Verification of Neural-Network Control Systems by Integrating Taylor Models and Zonotopes

arXiv: https://arxiv.org/abs/2112.09197 · HTML: https://mlsanity.com/paper/2112.09197/

## Key facts

- Cited by 26 papers in the map (data through 14 Oct 2026).
- Builds on 11 of its 39 references that are in the map.
- First posted on arXiv 16 Dec 2021.

## Builds on (most cited first, 11 of 11)

- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems](https://mlsanity.com/paper/2004.05519/) (2020)
- [Verisig: verifying safety properties of hybrid systems with neural network controllers](https://mlsanity.com/paper/1811.01828/) (2018)
- [Verification of Deep Convolutional Neural Networks Using ImageStars](https://mlsanity.com/paper/2004.05511/) (2020)
- [OVERT: An Algorithm for Safety Verification of Neural Network Control Policies for Nonlinear Systems](https://mlsanity.com/paper/2108.01220/) (2021)
- [JuliaReach: a Toolbox for Set-Based Reachability](https://mlsanity.com/paper/1901.10736/) (2019)
- [ReachNN: Reachability Analysis of Neural-Network Controlled Systems](https://mlsanity.com/paper/1906.10654/) (2019)
- [Reachable Set Estimation and Safety Verification for Piecewise Linear Systems with Neural Network Controllers](https://mlsanity.com/paper/1802.06981/) (2018)
- [Sparse Polynomial Zonotopes: A Novel Set Representation for Reachability Analysis](https://mlsanity.com/paper/1901.01780/) (2019)
- [Safety Verification of Neural Network Controlled Systems](https://mlsanity.com/paper/2011.05174/) (2020)
- [LazySets.jl: Scalable Symbolic-Numeric Set Computations](https://mlsanity.com/paper/2110.01711/) (2021)

## Built on by (most cited first, 26 of 26)

- [Empowering Autonomous Driving with Large Language Models: A Safety Perspective](https://mlsanity.com/paper/2312.00812/) (2023)
- [Open- and Closed-Loop Neural Network Verification using Polynomial Zonotopes](https://mlsanity.com/paper/2207.02715/) (2022)
- [POLAR-Express: Efficient and Precise Formal Reachability Analysis of Neural-Network Controlled Systems](https://mlsanity.com/paper/2304.01218/) (2023)
- [Neural Abstractions](https://mlsanity.com/paper/2301.11683/) (2023)
- [Interval Reachability of Nonlinear Dynamical Systems with Neural Network Controllers](https://mlsanity.com/paper/2301.07912/) (2023)
- [Efficient Interaction-Aware Interval Analysis of Neural Network Feedback Loops](https://mlsanity.com/paper/2307.14938/) (2023)
- [Scalable Surrogate Verification of Image-based Neural Network Control Systems using Composition and Unrolling](https://mlsanity.com/paper/2405.18554/) (2024)
- [Provably Safe Neural Network Controllers via Differential Dynamic Logic](https://mlsanity.com/paper/2402.10998/) (2024)
- [ModelVerification.jl: a Comprehensive Toolbox for Formally Verifying Deep Neural Networks](https://mlsanity.com/paper/2407.01639/) (2024)
- [Contraction-Guided Adaptive Partitioning for Reachability Analysis of Neural Network Controlled Systems](https://mlsanity.com/paper/2304.03671/) (2023)
- [Verification of Neural Network Control Systems using Symbolic Zonotopes and Polynotopes](https://mlsanity.com/paper/2306.14619/) (2023)
- [Forward Invariance in Neural Network Controlled Systems](https://mlsanity.com/paper/2309.09043/) (2023)
- [Certified Robust Invariant Polytope Training in Neural Controlled ODEs](https://mlsanity.com/paper/2408.01273/) (2024)
- [Certified Training with Branch-and-Bound for Lyapunov-stable Neural Control](https://mlsanity.com/paper/2411.18235/) (2024)
- [PICID: Proof-Driven Clause Learning in Neural Network Verification](https://mlsanity.com/paper/2503.12083/) (2025)
- [Automated Reachability Analysis of Neural Network-Controlled Systems via Adaptive Polytopes](https://mlsanity.com/paper/2212.07553/) (2022)
- [Taming Reachability Analysis of DNN-Controlled Systems via Abstraction-Based Training](https://mlsanity.com/paper/2211.11127/) (2022)
- [On the Trade-off Between Efficiency and Precision of Neural Abstraction](https://mlsanity.com/paper/2307.15546/) (2023)
- [The inverse problem for neural networks](https://mlsanity.com/paper/2308.14093/) (2023)
- [Compositional Inductive Invariant Based Verification of Neural Network Controlled Systems](https://mlsanity.com/paper/2312.10842/) (2023)
- [Learning from Uncertain Data: From Possible Worlds to Possible Models](https://mlsanity.com/paper/2405.18549/) (2024)
- [The Reachability Problem for Neural-Network Control Systems](https://mlsanity.com/paper/2407.04988/) (2024)
- [Neural Network-assisted Interval Reachability for Systems with Control Barrier Function-Based Safe Controllers](https://mlsanity.com/paper/2504.08249/) (2025)
- [Of Good Demons and Bad Angels: Guaranteeing Safe Control under Finite Precision](https://mlsanity.com/paper/2507.22760/) (2025)
- [Robust Verification of Controllers under State Uncertainty via Hamilton-Jacobi Reachability Analysis](https://mlsanity.com/paper/2511.14755/) (2025)
- [NNV3: Expanding Neural Network Verification to New Architectures and Domains](https://mlsanity.com/paper/2609.30050/) (2026)

## Abstract (arXiv)

We study the verification problem for closed-loop dynamical systems with neural-network controllers (NNCS). This problem is commonly reduced to computing the set of reachable states. When considering dynamical systems and neural networks in isolation, there exist precise approaches for that task based on set representations respectively called Taylor models and zonotopes. However, the combination of these approaches to NNCS is non-trivial because, when converting between the set representations, dependency information gets lost in each control cycle and the accumulated approximation error quickly renders the result useless. We present an algorithm to chain approaches based on Taylor models and zonotopes, yielding a precise reachability algorithm for NNCS. Because the algorithm only acts at the interface of the isolated approaches, it is applicable to general dynamical systems and neural networks and can benefit from future advances in these areas. Our implementation delivers state-of-the-art performance and is the first to successfully analyze all benchmark problems of an annual reachability competition for NNCS.