@inproceedings{807bcffe8268466287debf21aa841496,
title = "ReachNN*: A Tool for Reachability Analysis of Neural-Network Controlled Systems",
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.",
keywords = "Bernstein polynomials, GPU acceleration, Knowledge distillation, Neural-network controlled systems, Reachability",
author = "Jiameng Fan and Chao Huang and Xin Chen and Wenchao Li and Qi Zhu",
note = "Funding Information: J. Fan and C. Huang contributed equally. We acknowledge the support from NSF grants 1646497, 1834701, 1834324, 1839511, 1724341, ONR grant N00014-19-1-2496, and the US Air Force Research Laboratory (AFRL) under contract number FA8650-16-C-2642. Publisher Copyright: {\textcopyright} 2020, Springer Nature Switzerland AG.; 18th International Symposium on Automated Technology for Verification and Analysis, ATVA 2020 ; Conference date: 19-10-2020 Through 23-10-2020",
year = "2020",
doi = "10.1007/978-3-030-59152-6_30",
language = "English (US)",
isbn = "9783030591519",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Science and Business Media Deutschland GmbH",
pages = "537--542",
editor = "Hung, {Dang Van} and Oleg Sokolsky",
booktitle = "Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Proceedings",
address = "Germany",
}