# Open- and Closed-Loop Neural Network Verification using Polynomial Zonotopes

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

## Key facts

- Cited by 24 papers in the map (data through 14 Oct 2026).
- Builds on 21 of its 49 references that are in the map.
- First posted on arXiv 6 Jul 2022.

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

- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Towards Fast Computation of Certified Robustness for ReLU Networks](https://mlsanity.com/paper/1804.09699/) (2018)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification](https://mlsanity.com/paper/2103.06624/) (2021)
- [Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers](https://mlsanity.com/paper/2011.13824/) (2020)
- [Formal Security Analysis of Neural Networks using Symbolic Intervals](https://mlsanity.com/paper/1804.10829/) (2018)
- [Semidefinite relaxations for certifying robustness to adversarial examples](https://mlsanity.com/paper/1811.01057/) (2018)
- [Branch and Bound for Piecewise Linear Neural Network Verification](https://mlsanity.com/paper/1909.06588/) (2019)
- [NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems](https://mlsanity.com/paper/2004.05519/) (2020)
- [Maximum Resilience of Artificial Neural Networks](https://mlsanity.com/paper/1705.01040/) (2017)
- [Verisig: verifying safety properties of hybrid systems with neural network controllers](https://mlsanity.com/paper/1811.01828/) (2018)
- [The Second International Verification of Neural Networks Competition (VNN-COMP 2021): Summary and Results](https://mlsanity.com/paper/2109.00498/) (2021)
- [POLAR: A Polynomial Arithmetic Framework for Verifying Neural-Network Controlled Systems](https://mlsanity.com/paper/2106.13867/) (2021)
- [Reachable Polyhedral Marching (RPM): A Safety Verification Algorithm for Robotic Systems with Deep Neural Network Components](https://mlsanity.com/paper/2011.11609/) (2020)
- [JuliaReach: a Toolbox for Set-Based Reachability](https://mlsanity.com/paper/1901.10736/) (2019)
- [Verification of Neural-Network Control Systems by Integrating Taylor Models and Zonotopes](https://mlsanity.com/paper/2112.09197/) (2021)
- [Reachable Set Estimation and Safety Verification for Piecewise Linear Systems with Neural Network Controllers](https://mlsanity.com/paper/1802.06981/) (2018)
- [DeepChess: End-to-End Deep Neural Network for Automatic Learning in Chess](https://mlsanity.com/paper/1711.09667/) (2017)
- [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)

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

- [Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs](https://mlsanity.com/paper/2401.06379/) (2024)
- [Neural Network Verification is a Programming Language Challenge](https://mlsanity.com/paper/2501.05867/) (2025)
- [Formal Verification of Graph Convolutional Networks with Uncertain Node Features and Uncertain Graph Structure](https://mlsanity.com/paper/2404.15065/) (2024)
- [Reachable Polyhedral Marching (RPM): An Exact Analysis Tool for Deep-Learned Control Systems](https://mlsanity.com/paper/2210.08339/) (2022)
- [Fully Automatic Neural Network Reduction for Formal Verification](https://mlsanity.com/paper/2305.01932/) (2023)
- [Set-Based Training for Neural Network Verification](https://mlsanity.com/paper/2401.14961/) (2024)
- [Out of the Shadows: Exploring a Latent Space for Neural Network Verification](https://mlsanity.com/paper/2505.17854/) (2025)
- [Abstraction-Based Proof Production in Formal Verification of Neural Networks](https://mlsanity.com/paper/2506.09455/) (2025)
- [Contraction-Guided Adaptive Partitioning for Reachability Analysis of Neural Network Controlled Systems](https://mlsanity.com/paper/2304.03671/) (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)
- [Automated Reachability Analysis of Neural Network-Controlled Systems via Adaptive Polytopes](https://mlsanity.com/paper/2212.07553/) (2022)
- [Verifying Safety of Neural Networks from Topological Perspectives](https://mlsanity.com/paper/2306.15403/) (2023)
- [The FABRIC Strategy for Verifying Neural Feedback Systems](https://mlsanity.com/paper/2603.08964/) (2026)
- [The inverse problem for neural networks](https://mlsanity.com/paper/2308.14093/) (2023)
- [UR4NNV: Neural Network Verification, Under-approximation Reachability Works!](https://mlsanity.com/paper/2401.12550/) (2024)
- [Efficient model predictive control for nonlinear systems modelled by deep neural networks](https://mlsanity.com/paper/2405.10372/) (2024)
- [Safe and High-Performance Learning of Model Predicitve Control using Kernel-Based Interpolation](https://mlsanity.com/paper/2410.06771/) (2024)
- [Language Models That Walk the Talk: A Framework for Formal Fairness Certificates](https://mlsanity.com/paper/2505.12767/) (2025)
- [Perception with Guarantees: Certified Pose Estimation via Reachability Analysis](https://mlsanity.com/paper/2602.10032/) (2026)
- [Lipschitz-Based Robustness Certification Under Floating-Point Execution](https://mlsanity.com/paper/2603.13334/) (2026)
- [Safety Screening for Voltage Control in Active Distribution Grids via Distributionally Robust Conformal Screening](https://mlsanity.com/paper/2608.30889/) (2026)
- [Certified Mechanistic Interpretability: Lifting Single-Input Findings to Bounded Neighbourhoods](https://mlsanity.com/paper/2609.26112/) (2026)
- [Stochastic World Models for Verifying Vision-Based Neural Feedback Systems](https://mlsanity.com/paper/2609.38120/) (2026)

## Abstract (arXiv)

We present a novel approach to efficiently compute tight non-convex enclosures of the image through neural networks with ReLU, sigmoid, or hyperbolic tangent activation functions. In particular, we abstract the input-output relation of each neuron by a polynomial approximation, which is evaluated in a set-based manner using polynomial zonotopes. While our approach can also can be beneficial for open-loop neural network verification, our main application is reachability analysis of neural network controlled systems, where polynomial zonotopes are able to capture the non-convexity caused by the neural network as well as the system dynamics. This results in a superior performance compared to other methods, as we demonstrate on various benchmarks.