# POLAR-Express: Efficient and Precise Formal Reachability Analysis of Neural-Network Controlled Systems

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

## Key facts

- Cited by 12 papers in the map (data through 14 Oct 2026).
- Builds on 27 of its 81 references that are in the map.
- First posted on arXiv 31 Mar 2023.

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

- [Continuous control with deep reinforcement learning](https://mlsanity.com/paper/1509.02971/) (2015)
- [End to End Learning for Self-Driving Cars](https://mlsanity.com/paper/1604.07316/) (2016)
- [End-to-End Training of Deep Visuomotor Policies](https://mlsanity.com/paper/1504.00702/) (2015)
- [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)
- [Safety Verification of Deep Neural Networks](https://mlsanity.com/paper/1610.06940/) (2016)
- [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)
- [Machine Learning Testing: Survey, Landscapes and Horizons](https://mlsanity.com/paper/1906.10742/) (2019)
- [Formal Security Analysis of Neural Networks using Symbolic Intervals](https://mlsanity.com/paper/1804.10829/) (2018)
- [Evaluating the Robustness of Neural Networks: An Extreme Value Theory Approach](https://mlsanity.com/paper/1801.10578/) (2018)
- [NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems](https://mlsanity.com/paper/2004.05519/) (2020)
- [An approach to reachability analysis for feed-forward ReLU neural networks](https://mlsanity.com/paper/1706.07351/) (2017)
- [Safety Verification and Robustness Analysis of Neural Networks via Quadratic Constraints and Semidefinite Programming](https://mlsanity.com/paper/1903.01287/) (2019)
- [Maximum Resilience of Artificial Neural Networks](https://mlsanity.com/paper/1705.01040/) (2017)
- [Reachability Analysis of Deep Neural Networks with Provable Guarantees](https://mlsanity.com/paper/1805.02242/) (2018)
- [Verisig: verifying safety properties of hybrid systems with neural network controllers](https://mlsanity.com/paper/1811.01828/) (2018)
- [Enforcing Hard Constraints with Soft Barriers: Safe Reinforcement Learning in Unknown Stochastic Environments](https://mlsanity.com/paper/2209.15090/) (2022)
- [POLAR: A Polynomial Arithmetic Framework for Verifying Neural-Network Controlled Systems](https://mlsanity.com/paper/2106.13867/) (2021)
- [Verification of Neural-Network Control Systems by Integrating Taylor Models and Zonotopes](https://mlsanity.com/paper/2112.09197/) (2021)
- [Provably Safe Reinforcement Learning via Action Projection using Reachability Analysis and Polynomial Zonotopes](https://mlsanity.com/paper/2210.10691/) (2022)
- [One for Many: Transfer Learning for Building HVAC Control](https://mlsanity.com/paper/2008.03625/) (2020)
- [Efficient Global Robustness Certification of Neural Networks via Interleaving Twin-Network Encoding](https://mlsanity.com/paper/2203.14141/) (2022)
- [Physics-Aware Safety-Assured Design of Hierarchical Neural Network based Planner](https://mlsanity.com/paper/2201.09140/) (2022)
- [Energy-Efficient Control Adaptation with Safety Guarantees for Learning-Enabled Cyber-Physical Systems](https://mlsanity.com/paper/2008.06162/) (2020)
- [Safety-driven Interactive Planning for Neural Network-based Lane Changing](https://mlsanity.com/paper/2201.09112/) (2022)
- [Opportunistic Intermittent Control with Safety Guarantees for Autonomous Systems](https://mlsanity.com/paper/2005.03726/) (2020)
- [Learning-based Framework for Sensor Fault-Tolerant Building HVAC Control with Model-assisted Learning](https://mlsanity.com/paper/2106.14144/) (2021)

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

- [Empowering Autonomous Driving with Large Language Models: A Safety Perspective](https://mlsanity.com/paper/2312.00812/) (2023)
- [State-Wise Safe Reinforcement Learning With Pixel Observations](https://mlsanity.com/paper/2311.02227/) (2023)
- [Verified Safe Reinforcement Learning for Neural Network Dynamic Models](https://mlsanity.com/paper/2405.15994/) (2024)
- [DeepBern-Nets: Taming the Complexity of Certifying Neural Networks using Bernstein Polynomial Activations and Precise Bound Propagation](https://mlsanity.com/paper/2305.13508/) (2023)
- [Bridging Dimensions: Confident Reachability for High-Dimensional Controllers](https://mlsanity.com/paper/2311.04843/) (2023)
- [textttimmrax: A Parallelizable and Differentiable Toolbox for Interval Analysis and Mixed Monotone Reachability in JAX](https://mlsanity.com/paper/2401.11608/) (2024)
- [Certified Training with Branch-and-Bound for Lyapunov-stable Neural Control](https://mlsanity.com/paper/2411.18235/) (2024)
- [Parallel Differentiable Reachability for Learning and Planning with Certified Neural Dynamics and Controllers](https://mlsanity.com/paper/2605.25346/) (2026)
- [Learning Verifiable Control Policies Using Relaxed Verification](https://mlsanity.com/paper/2504.16879/) (2025)
- [Neural Network Verification for Gliding Drone Control: A Case Study](https://mlsanity.com/paper/2505.00622/) (2025)
- [Language Models That Walk the Talk: A Framework for Formal Fairness Certificates](https://mlsanity.com/paper/2505.12767/) (2025)
- [Verification of Visual Controllers via Compositional Geometric Transformations](https://mlsanity.com/paper/2507.04523/) (2025)

## Abstract (arXiv)

Neural networks (NNs) playing the role of controllers have demonstrated impressive empirical performances on challenging control problems. However, the potential adoption of NN controllers in real-life applications also gives rise to a growing concern over the safety of these neural-network controlled systems (NNCSs), especially when used in safety-critical applications. In this work, we present POLAR-Express, an efficient and precise formal reachability analysis tool for verifying the safety of NNCSs. POLAR-Express uses Taylor model arithmetic to propagate Taylor models (TMs) across a neural network layer-by-layer to compute an overapproximation of the neural-network function. It can be applied to analyze any feed-forward neural network with continuous activation functions. We also present a novel approach to propagate TMs more efficiently and precisely across ReLU activation functions. In addition, POLAR-Express provides parallel computation support for the layer-by-layer propagation of TMs, thus significantly improving the efficiency and scalability over its earlier prototype POLAR. Across the comparison with six other state-of-the-art tools on a diverse set of benchmarks, POLAR-Express achieves the best verification efficiency and tightness in the reachable set analysis.