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

Chao Huang*, Jiameng Fan, Xin Chen, Wenchao Li, Qi Zhu

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution

27 Scopus citations

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.

Original languageEnglish (US)
Title of host publicationAutomated Technology for Verification and Analysis - 20th International Symposium, ATVA 2022, Proceedings
EditorsAhmed Bouajjani, Lukáš Holík, Zhilin Wu
PublisherSpringer Science and Business Media Deutschland GmbH
Pages414-430
Number of pages17
ISBN (Print)9783031199912
DOIs
StatePublished - 2022
Event20th International Symposium on Automated Technology for Verification and Analysis, ATVA 2022 - Virtual, Online
Duration: Oct 25 2022Oct 28 2022

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume13505 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference20th International Symposium on Automated Technology for Verification and Analysis, ATVA 2022
CityVirtual, Online
Period10/25/2210/28/22

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'POLAR: A Polynomial Arithmetic Framework for Verifying Neural-Network Controlled Systems'. Together they form a unique fingerprint.

Cite this