# POLAR: A Polynomial Arithmetic Framework for Verifying Neural-Network Controlled Systems

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

## Key facts

- Cited by 39 papers in the map (data through 14 Oct 2026).
- Builds on 10 of its 45 references that are in the map.
- First posted on arXiv 25 Jun 2021.

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

- [Continuous control with deep reinforcement learning](https://mlsanity.com/paper/1509.02971/) (2015)
- [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)
- [Towards Fast Computation of Certified Robustness for ReLU Networks](https://mlsanity.com/paper/1804.09699/) (2018)
- [Formal Security Analysis of Neural Networks using Symbolic Intervals](https://mlsanity.com/paper/1804.10829/) (2018)
- [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)
- [ReachNN: Reachability Analysis of Neural-Network Controlled Systems](https://mlsanity.com/paper/1906.10654/) (2019)

## Built on by (most cited first, 30 of 39)

- [Enforcing Hard Constraints with Soft Barriers: Safe Reinforcement Learning in Unknown Stochastic Environments](https://mlsanity.com/paper/2209.15090/) (2022)
- [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)
- [Efficient Global Robustness Certification of Neural Networks via Interleaving Twin-Network Encoding](https://mlsanity.com/paper/2203.14141/) (2022)
- [Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs](https://mlsanity.com/paper/2401.06379/) (2024)
- [POLAR-Express: Efficient and Precise Formal Reachability Analysis of Neural-Network Controlled Systems](https://mlsanity.com/paper/2304.01218/) (2023)
- [Neural Network Verification is a Programming Language Challenge](https://mlsanity.com/paper/2501.05867/) (2025)
- [Joint Differentiable Optimization and Verification for Certified Reinforcement Learning](https://mlsanity.com/paper/2201.12243/) (2022)
- [Efficient Interaction-Aware Interval Analysis of Neural Network Feedback Loops](https://mlsanity.com/paper/2307.14938/) (2023)
- [Data-Driven Reachability Analysis of Stochastic Dynamical Systems with Conformal Inference](https://mlsanity.com/paper/2309.09187/) (2023)
- [Formal Verification of Graph Convolutional Networks with Uncertain Node Features and Uncertain Graph Structure](https://mlsanity.com/paper/2404.15065/) (2024)
- [Provably Safe Neural Network Controllers via Differential Dynamic Logic](https://mlsanity.com/paper/2402.10998/) (2024)
- [Risk Verification of Stochastic Systems with Neural Network Controllers](https://mlsanity.com/paper/2209.09881/) (2022)
- [Fully Automatic Neural Network Reduction for Formal Verification](https://mlsanity.com/paper/2305.01932/) (2023)
- [A Toolbox for Fast Interval Arithmetic in numpy with an Application to Formal Verification of Neural Network Controlled Systems](https://mlsanity.com/paper/2306.15340/) (2023)
- [Unifying Qualitative and Quantitative Safety Verification of DNN-Controlled Systems](https://mlsanity.com/paper/2404.01769/) (2024)
- [BERN-NN: Tight Bound Propagation For Neural Networks Using Bernstein Polynomial Interval Arithmetic](https://mlsanity.com/paper/2211.14438/) (2022)
- [Bridging Dimensions: Confident Reachability for High-Dimensional Controllers](https://mlsanity.com/paper/2311.04843/) (2023)
- [Real-Time Safe Control of Neural Network Dynamic Models with Sound Approximation](https://mlsanity.com/paper/2404.13456/) (2024)
- [Statistical Reachability Analysis of Stochastic Cyber-Physical Systems under Distribution Shift](https://mlsanity.com/paper/2407.11609/) (2024)
- [Reachability Verification Based Reliability Assessment for Deep Reinforcement Learning Controlled Robotics and Autonomous Systems](https://mlsanity.com/paper/2210.14991/) (2022)
- [A Neurosymbolic Approach to the Verification of Temporal Logic Properties of Learning enabled Control Systems](https://mlsanity.com/paper/2303.05394/) (2023)
- [Contraction-Guided Adaptive Partitioning for Reachability Analysis of Neural Network Controlled Systems](https://mlsanity.com/paper/2304.03671/) (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)
- [Neural Abstraction-Based Controller Synthesis and Deployment](https://mlsanity.com/paper/2307.03783/) (2023)
- [Parallel Differentiable Reachability for Learning and Planning with Certified Neural Dynamics and Controllers](https://mlsanity.com/paper/2605.25346/) (2026)
- [Certified Neural Approximations of Nonlinear Dynamics](https://mlsanity.com/paper/2505.15497/) (2025)
- [The FABRIC Strategy for Verifying Neural Feedback Systems](https://mlsanity.com/paper/2603.08964/) (2026)

## Abstract (arXiv)

We present POLAR, a polynomial arithmetic-based framework for efficient bounded-time reachability analysis of neural-network controlled systems (NNCSs). Existing approaches that leverage the standard Taylor Model (TM) arithmetic for approximating the neural-network controller cannot deal with non-differentiable activation functions and suffer from rapid explosion of the remainder when propagating the TMs. POLAR overcomes these shortcomings by integrating TM arithmetic with textbfBernstein B'ezier Form and symbolic remainder. The former enables TM propagation across non-differentiable activation functions and local refinement of TMs, and the latter reduces error accumulation in the TM remainder for linear mappings in the network. Experimental results show that POLAR significantly outperforms the current state-of-the-art tools in terms of both efficiency and tightness of the reachable set overapproximation. The source code can be found in https://github.com/ChaoHuang2018/POLARTool