Huang, Chao 
ORCID: 0000-0002-9300-1787, Fan, Jiameng, Wang, Zhilu, Wang, Yixuan, Zhou, Weichao, Li, Jiajun ORCID: 0000-0001-8989-7739, Chen, Xin, Li, Wenchao and Zhu, Qi
(2021)
POLAR: A Polynomial Arithmetic Framework for Verifying Neural-Network
Controlled Systems.
[Preprint]
|
Text
2106.13867v3.pdf - Submitted version Download (15MB) | Preview |
Abstract
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 \textbf{Bernstein B{\'e}zier Form} and \textbf{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/POLAR_Tool
| Item Type: | Preprint |
|---|---|
| Additional Information: | Accepted by ATVA 2022 |
| Uncontrolled Keywords: | eess.SY, eess.SY, cs.LG, cs.SY |
| Divisions: | Faculty of Science and Engineering > School of Electrical Engineering, Electronics and Computer Science |
| Depositing User: | Symplectic Admin |
| Date Deposited: | 22 Sep 2021 11:02 |
| Last Modified: | 15 Mar 2024 18:00 |
| DOI: | 10.48550/arxiv.2106.13867 |
| Related URLs: | |
| URI: | https://livrepository.liverpool.ac.uk/id/eprint/3137907 |
Dimensions
Dimensions
