ReachNN*: A Tool for Reachability Analysis of Neural-Network Controlled Systems

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

*Corresponding author for this work

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

Abstract

We introduce ReachNN*, a tool for reachability analysis of neural-network controlled systems (NNCSs). The theoretical foundation of ReachNN* is the use of Bernstein polynomials to approximate any Lipschitz-continuous neural-network controller with different types of activation functions, with provable approximation error bounds. In addition, the sampling-based error bound estimation in ReachNN* is amenable to GPU-based parallel computing. For further improvement in runtime and error bound estimation, ReachNN* also features optional controller re-synthesis via a technique called verification-aware knowledge distillation (KD) to reduce the Lipschitz constant of the neural-network controller. Experiment results across a set of benchmarks show to efficiency improvement over the previous prototype. Moreover, KD enables proof of reachability of NNCSs whose verification results were previously unknown due to large overapproximation errors. An open-source implementation of ReachNN* is available at https://github.com/JmfanBU/ReachNNStar.git.

Original languageEnglish (US)
Title of host publicationAutomated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Proceedings
EditorsDang Van Hung, Oleg Sokolsky
PublisherSpringer Science and Business Media Deutschland GmbH
Pages537-542
Number of pages6
ISBN (Print)9783030591519
DOIs
StatePublished - 2020
Event18th International Symposium on Automated Technology for Verification and Analysis, ATVA 2020 - Hanoi, Viet Nam
Duration: Oct 19 2020Oct 23 2020

Publication series

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

Conference

Conference18th International Symposium on Automated Technology for Verification and Analysis, ATVA 2020
CountryViet Nam
CityHanoi
Period10/19/2010/23/20

Keywords

  • Bernstein polynomials
  • GPU acceleration
  • Knowledge distillation
  • Neural-network controlled systems
  • Reachability

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'ReachNN*: A Tool for Reachability Analysis of Neural-Network Controlled Systems'. Together they form a unique fingerprint.

Cite this