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

Jiameng Fan; Chao Huang; Xin Chen; Wenchao Li; Qi Zhu

doi:10.1007/978-3-030-59152-6_30

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

Electrical and Computer Engineering

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

36 Scopus citations

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 language	English (US)
Title of host publication	Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Proceedings
Editors	Dang Van Hung, Oleg Sokolsky
Publisher	Springer Science and Business Media Deutschland GmbH
Pages	537-542
Number of pages	6
ISBN (Print)	9783030591519
DOIs	https://doi.org/10.1007/978-3-030-59152-6_30
State	Published - 2020
Event	18th International Symposium on Automated Technology for Verification and Analysis, ATVA 2020 - Hanoi, Viet Nam Duration: Oct 19 2020 → Oct 23 2020

Publication series

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

Conference

Conference	18th International Symposium on Automated Technology for Verification and Analysis, ATVA 2020
Country/Territory	Viet Nam
City	Hanoi
Period	10/19/20 → 10/23/20

Funding

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.

Keywords

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

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/978-3-030-59152-6_30

Cite this

Fan, J., Huang, C., Chen, X., Li, W., & Zhu, Q. (2020). ReachNN*: A Tool for Reachability Analysis of Neural-Network Controlled Systems. In D. V. Hung, & O. Sokolsky (Eds.), Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Proceedings (pp. 537-542). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12302 LNCS). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-030-59152-6_30

Fan, Jiameng ; Huang, Chao ; Chen, Xin et al. / ReachNN* : A Tool for Reachability Analysis of Neural-Network Controlled Systems. Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Proceedings. editor / Dang Van Hung ; Oleg Sokolsky. Springer Science and Business Media Deutschland GmbH, 2020. pp. 537-542 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@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 = "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",

}

Fan, J, Huang, C, Chen, X, Li, W & Zhu, Q 2020, ReachNN*: A Tool for Reachability Analysis of Neural-Network Controlled Systems. in DV Hung & O Sokolsky (eds), Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 12302 LNCS, Springer Science and Business Media Deutschland GmbH, pp. 537-542, 18th International Symposium on Automated Technology for Verification and Analysis, ATVA 2020, Hanoi, Viet Nam, 10/19/20. https://doi.org/10.1007/978-3-030-59152-6_30

ReachNN*: A Tool for Reachability Analysis of Neural-Network Controlled Systems. / Fan, Jiameng; Huang, Chao; Chen, Xin et al.
Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Proceedings. ed. / Dang Van Hung; Oleg Sokolsky. Springer Science and Business Media Deutschland GmbH, 2020. p. 537-542 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12302 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - ReachNN*

T2 - 18th International Symposium on Automated Technology for Verification and Analysis, ATVA 2020

AU - Fan, Jiameng

AU - Huang, Chao

AU - Chen, Xin

AU - Li, Wenchao

AU - Zhu, Qi

PY - 2020

Y1 - 2020

N2 - 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.

AB - 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.

KW - Bernstein polynomials

KW - GPU acceleration

KW - Knowledge distillation

KW - Neural-network controlled systems

KW - Reachability

UR - http://www.scopus.com/inward/record.url?scp=85093825421&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85093825421&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-59152-6_30

DO - 10.1007/978-3-030-59152-6_30

M3 - Conference contribution

AN - SCOPUS:85093825421

SN - 9783030591519

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 537

EP - 542

BT - Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Proceedings

A2 - Hung, Dang Van

A2 - Sokolsky, Oleg

PB - Springer Science and Business Media Deutschland GmbH

Y2 - 19 October 2020 through 23 October 2020

ER -

Fan J, Huang C, Chen X, Li W, Zhu Q. ReachNN*: A Tool for Reachability Analysis of Neural-Network Controlled Systems. In Hung DV, Sokolsky O, editors, Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Proceedings. Springer Science and Business Media Deutschland GmbH. 2020. p. 537-542. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-59152-6_30

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

Abstract

Publication series

Conference

Funding

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this