POLAR-Express: Efficient and Precise Formal Reachability Analysis of Neural-Network Controlled Systems
Not on the map. Why?
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.
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
27 of 81 references.
References · 27
- 2015Continuous control with deep reinforcement learningcited by 3,407
- 2016End to End Learning for Self-Driving Carscited by 1,009
- 2015End-to-End Training of Deep Visuomotor Policiescited by 875
- 2017Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networkscited by 744
- 2018Efficient Neural Network Robustness Certification with General Activation Functionscited by 445
- 2016Safety Verification of Deep Neural Networkscited by 263
- 2021Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verificationcited by 228
- 2019Machine Learning Testing: Survey, Landscapes and Horizonscited by 218
- 2018Formal Security Analysis of Neural Networks using Symbolic Intervalscited by 185
- 2018Evaluating the Robustness of Neural Networks: An Extreme Value Theory Approachcited by 182
- 2020NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systemscited by 128
- 2017An approach to reachability analysis for feed-forward ReLU neural networkscited by 127
15 more
- 2019Safety Verification and Robustness Analysis of Neural Networks via Quadratic Constraints and Semidefinite Programmingcited by 101
- 2017Maximum Resilience of Artificial Neural Networkscited by 97
- 2018Reachability Analysis of Deep Neural Networks with Provable Guaranteescited by 93
- 2018Verisig: verifying safety properties of hybrid systems with neural network controllerscited by 84
- 2022Enforcing Hard Constraints with Soft Barriers: Safe Reinforcement Learning in Unknown Stochastic Environmentscited by 60
- 2021POLAR: A Polynomial Arithmetic Framework for Verifying Neural-Network Controlled Systemscited by 39
- 2021Verification of Neural-Network Control Systems by Integrating Taylor Models and Zonotopescited by 26
- 2022Provably Safe Reinforcement Learning via Action Projection using Reachability Analysis and Polynomial Zonotopescited by 26
- 2020One for Many: Transfer Learning for Building HVAC Controlcited by 16
- 2022Efficient Global Robustness Certification of Neural Networks via Interleaving Twin-Network Encodingcited by 15
- 2022Physics-Aware Safety-Assured Design of Hierarchical Neural Network based Plannercited by 9
- 2020Energy-Efficient Control Adaptation with Safety Guarantees for Learning-Enabled Cyber-Physical Systemscited by 7
- 2022Safety-driven Interactive Planning for Neural Network-based Lane Changingcited by 6
- 2020Opportunistic Intermittent Control with Safety Guarantees for Autonomous Systemscited by 5
- 2021Learning-based Framework for Sensor Fault-Tolerant Building HVAC Control with Model-assisted Learningcited by 4
Built on by
Citing papers per year: 2023: 4; 2024: 3; 2025: 4; 2026: 1.
12 papers.
- 2023Empowering Autonomous Driving with Large Language Models: A Safety Perspectivecited by 34
- 2023State-Wise Safe Reinforcement Learning With Pixel Observationscited by 9
- 2024Verified Safe Reinforcement Learning for Neural Network Dynamic Modelscited by 7
- 2023DeepBern-Nets: Taming the Complexity of Certifying Neural Networks using Bernstein Polynomial Activations and Precise Bound Propagationcited by 5
- 2023Bridging Dimensions: Confident Reachability for High-Dimensional Controllerscited by 5
- 2024textttimmrax: A Parallelizable and Differentiable Toolbox for Interval Analysis and Mixed Monotone Reachability in JAXcited by 4
- 2024Certified Training with Branch-and-Bound for Lyapunov-stable Neural Controlcited by 3
- 2026Parallel Differentiable Reachability for Learning and Planning with Certified Neural Dynamics and Controllerscited by 2
- 2025Learning Verifiable Control Policies Using Relaxed Verificationcited by 1
- 2025Neural Network Verification for Gliding Drone Control: A Case Studycited by 0
- 2025Language Models That Walk the Talk: A Framework for Formal Fairness Certificatescited by 0
- 2025Verification of Visual Controllers via Compositional Geometric Transformationscited by 0
- 2026Parallel Differentiable Reachability for Learning and Planning with Certified Neural Dynamics and Controllers25 May 2026
- 2025Verification of Visual Controllers via Compositional Geometric Transformations6 Jul 2025
- 2025Language Models That Walk the Talk: A Framework for Formal Fairness Certificates19 May 2025
- 2025Neural Network Verification for Gliding Drone Control: A Case Study1 May 2025
- 2025Learning Verifiable Control Policies Using Relaxed Verification23 Apr 2025
- 2024Certified Training with Branch-and-Bound for Lyapunov-stable Neural Control27 Nov 2024
- 2024Verified Safe Reinforcement Learning for Neural Network Dynamic Models25 May 2024
- 2024textttimmrax: A Parallelizable and Differentiable Toolbox for Interval Analysis and Mixed Monotone Reachability in JAX21 Jan 2024
- 2023Empowering Autonomous Driving with Large Language Models: A Safety Perspective28 Nov 2023
- 2023Bridging Dimensions: Confident Reachability for High-Dimensional Controllers8 Nov 2023
- 2023State-Wise Safe Reinforcement Learning With Pixel Observations3 Nov 2023
- 2023DeepBern-Nets: Taming the Complexity of Certifying Neural Networks using Bernstein Polynomial Activations and Precise Bound Propagation22 May 2023