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

Huang, Chao ORCID: 0000-0002-9300-1787, Fan, Jiameng, Chen, Xin, Li, Wenchao and Zhu, Qi (2022) POLAR: A Polynomial Arithmetic Framework for Verifying Neural-Network Controlled Systems. .

Text
ATVA2022 (2).pdf - Author Accepted Manuscript
Download (18MB) | Preview

Official URL: http://dx.doi.org/10.1007/978-3-031-19992-9_27

Abstract

We present POLAR (The source code can be found at https://github.com/ChaoHuang2018/POLAR_Tool. The full version of this paper can be found at https://arxiv.org/abs/2106.13867. ), a POLynomial ARithmetic-based framework for efficient time-bounded reachability analysis of neural-network controlled systems. Existing approaches leveraging 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 TMs. POLAR overcomes these shortcomings by integrating TM arithmetic with Bernstein polynomial interpolation and symbolic remainders. 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 neural network. Experimental results show POLAR significantly outperforms the state-of-the-art tools on both efficiency and tightness of the reachable set overapproximation.

Item Type:	Conference or Workshop Item (Unspecified)
Depositing User:	Symplectic Admin
Date Deposited:	05 Dec 2022 16:42
Last Modified:	21 Oct 2023 01:30
DOI:	10.1007/978-3-031-19992-9_27
Related URLs:	Publisher
URI:	https://livrepository.liverpool.ac.uk/id/eprint/3166497