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

Wang, Yixuan, Zhou, Weichao, Fan, Jiameng, Wang, Zhilu, Li, Jiajun ORCID: 0000-0001-8989-7739, Chen, Xin, Huang, Chao ORCID: 0000-0002-9300-1787, Li, Wenchao and Zhu, Qi (2023) POLAR-Express: Efficient and Precise Formal Reachability Analysis of Neural-Network Controlled Systems. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 43 (3). p. 1.

Text
TCAD___POLAR.pdf - Author Accepted Manuscript
Download (3MB) | Preview

Official URL: http://dx.doi.org/10.1109/tcad.2023.3331215

Abstract

Neural networks (NNs) playing the role of controllers have demonstrated impressive empirical performance on challenging control problems. However, the potential adoption of NN controllers in real-life applications has been significantly impeded by the growing concerns over the safety of these NN-controlled systems (NNCSs). 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 (TM) arithmetic to propagate TMs layer-by-layer across an NN to compute an overapproximation of the NN. It can be applied to analyze any feedforward NNs with continuous activation functions, such as ReLU, Sigmoid, and Tanh activation functions that cover the common benchmarks for NNCS reachability analysis. Compared with its earlier prototype POLAR, we develop a novel approach in POLAR-Express to propagate TMs more efficiently and precisely across ReLU activation functions, and provide parallel computation support for TM propagation, thus significantly improving the efficiency and scalability. Across the comparison with six other state-of-the-art tools on a diverse set of common benchmarks, POLAR-Express achieves the best verification efficiency and tightness in the reachable set analysis. POLAR-Express is publicly available at https://github.com/ChaoHuang2018/POLAR_Tool.

Item Type:	Article
Divisions:	Faculty of Science and Engineering > School of Electrical Engineering, Electronics and Computer Science
Depositing User:	Symplectic Admin
Date Deposited:	28 Nov 2023 08:17
Last Modified:	17 Mar 2024 23:59
DOI:	10.1109/tcad.2023.3331215
Related URLs:	Publisher
URI:	https://livrepository.liverpool.ac.uk/id/eprint/3177034