Open- and Closed-Loop Neural Network Verification Using Polynomial Zonotopes

Niklas Kochdumper; Christian Schilling; Matthias Althoff; Stanley Bak

doi:10.1007/978-3-031-33170-1_2

Open- and Closed-Loop Neural Network Verification Using Polynomial Zonotopes

Niklas Kochdumper
, Christian Schilling
, Matthias Althoff
, Stanley Bak

Computer Science

Stony Brook University

Stony Brook University
Aalborg University
Technical University of Munich

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

35 Scopus citations

Abstract

We present a novel approach to efficiently compute tight non-convex enclosures of the image through neural networks with ReLU, sigmoid, or hyperbolic tangent activation functions. In particular, we abstract the input-output relation of each neuron by a polynomial approximation, which is evaluated in a set-based manner using polynomial zonotopes. While our approach can also can be beneficial for open-loop neural network verification, our main application is reachability analysis of neural network controlled systems, where polynomial zonotopes are able to capture the non-convexity caused by the neural network as well as the system dynamics. This results in a superior performance compared to other methods, as we demonstrate on various benchmarks.

Original language	English
Title of host publication	NASA Formal Methods - 15th International Symposium, NFM 2023, Proceedings
Editors	Kristin Yvonne Rozier, Swarat Chaudhuri
Publisher	Springer Science and Business Media Deutschland GmbH
Pages	16-36
Number of pages	21
ISBN (Print)	9783031331695
DOIs	https://doi.org/10.1007/978-3-031-33170-1_2
State	Published - 2023
Event	15th International Symposium on NASA Formal Methods, NFM 2023 - Houston, United States Duration: May 16 2023 → May 18 2023

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	13903 LNCS

Conference

Conference	15th International Symposium on NASA Formal Methods, NFM 2023
Country/Territory	United States
City	Houston
Period	05/16/23 → 05/18/23

Keywords

Formal verification
Neural network controlled systems
Neural network verification
Polynomial zonotopes
Reachability analysis

Access to Document

10.1007/978-3-031-33170-1_2

Cite this

Kochdumper, N., Schilling, C., Althoff, M., & Bak, S. (2023). Open- and Closed-Loop Neural Network Verification Using Polynomial Zonotopes. In K. Y. Rozier, & S. Chaudhuri (Eds.), NASA Formal Methods - 15th International Symposium, NFM 2023, Proceedings (pp. 16-36). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 13903 LNCS). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-031-33170-1_2

Kochdumper, Niklas ; Schilling, Christian ; Althoff, Matthias et al. / Open- and Closed-Loop Neural Network Verification Using Polynomial Zonotopes. NASA Formal Methods - 15th International Symposium, NFM 2023, Proceedings. editor / Kristin Yvonne Rozier ; Swarat Chaudhuri. Springer Science and Business Media Deutschland GmbH, 2023. pp. 16-36 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{573f3fb9f4204d55a4a237e95db67aff,

title = "Open- and Closed-Loop Neural Network Verification Using Polynomial Zonotopes",

abstract = "We present a novel approach to efficiently compute tight non-convex enclosures of the image through neural networks with ReLU, sigmoid, or hyperbolic tangent activation functions. In particular, we abstract the input-output relation of each neuron by a polynomial approximation, which is evaluated in a set-based manner using polynomial zonotopes. While our approach can also can be beneficial for open-loop neural network verification, our main application is reachability analysis of neural network controlled systems, where polynomial zonotopes are able to capture the non-convexity caused by the neural network as well as the system dynamics. This results in a superior performance compared to other methods, as we demonstrate on various benchmarks.",

keywords = "Formal verification, Neural network controlled systems, Neural network verification, Polynomial zonotopes, Reachability analysis",

author = "Niklas Kochdumper and Christian Schilling and Matthias Althoff and Stanley Bak",

note = "Publisher Copyright: {\textcopyright} 2023, The Author(s), under exclusive license to Springer Nature Switzerland AG.; 15th International Symposium on NASA Formal Methods, NFM 2023 ; Conference date: 16-05-2023 Through 18-05-2023",

year = "2023",

doi = "10.1007/978-3-031-33170-1\_2",

language = "English",

isbn = "9783031331695",

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 = "16--36",

editor = "Rozier, \{Kristin Yvonne\} and Swarat Chaudhuri",

booktitle = "NASA Formal Methods - 15th International Symposium, NFM 2023, Proceedings",

}

Kochdumper, N, Schilling, C, Althoff, M & Bak, S 2023, Open- and Closed-Loop Neural Network Verification Using Polynomial Zonotopes. in KY Rozier & S Chaudhuri (eds), NASA Formal Methods - 15th International Symposium, NFM 2023, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 13903 LNCS, Springer Science and Business Media Deutschland GmbH, pp. 16-36, 15th International Symposium on NASA Formal Methods, NFM 2023, Houston, United States, 05/16/23. https://doi.org/10.1007/978-3-031-33170-1_2

Open- and Closed-Loop Neural Network Verification Using Polynomial Zonotopes. / Kochdumper, Niklas; Schilling, Christian; Althoff, Matthias et al.
NASA Formal Methods - 15th International Symposium, NFM 2023, Proceedings. ed. / Kristin Yvonne Rozier; Swarat Chaudhuri. Springer Science and Business Media Deutschland GmbH, 2023. p. 16-36 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 13903 LNCS).

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

TY - GEN

T1 - Open- and Closed-Loop Neural Network Verification Using Polynomial Zonotopes

AU - Kochdumper, Niklas

AU - Schilling, Christian

AU - Althoff, Matthias

AU - Bak, Stanley

PY - 2023

Y1 - 2023

N2 - We present a novel approach to efficiently compute tight non-convex enclosures of the image through neural networks with ReLU, sigmoid, or hyperbolic tangent activation functions. In particular, we abstract the input-output relation of each neuron by a polynomial approximation, which is evaluated in a set-based manner using polynomial zonotopes. While our approach can also can be beneficial for open-loop neural network verification, our main application is reachability analysis of neural network controlled systems, where polynomial zonotopes are able to capture the non-convexity caused by the neural network as well as the system dynamics. This results in a superior performance compared to other methods, as we demonstrate on various benchmarks.

AB - We present a novel approach to efficiently compute tight non-convex enclosures of the image through neural networks with ReLU, sigmoid, or hyperbolic tangent activation functions. In particular, we abstract the input-output relation of each neuron by a polynomial approximation, which is evaluated in a set-based manner using polynomial zonotopes. While our approach can also can be beneficial for open-loop neural network verification, our main application is reachability analysis of neural network controlled systems, where polynomial zonotopes are able to capture the non-convexity caused by the neural network as well as the system dynamics. This results in a superior performance compared to other methods, as we demonstrate on various benchmarks.

KW - Formal verification

KW - Neural network controlled systems

KW - Neural network verification

KW - Polynomial zonotopes

KW - Reachability analysis

UR - https://www.scopus.com/pages/publications/85163990011

U2 - 10.1007/978-3-031-33170-1_2

DO - 10.1007/978-3-031-33170-1_2

M3 - Conference contribution

SN - 9783031331695

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

SP - 16

EP - 36

BT - NASA Formal Methods - 15th International Symposium, NFM 2023, Proceedings

A2 - Rozier, Kristin Yvonne

A2 - Chaudhuri, Swarat

PB - Springer Science and Business Media Deutschland GmbH

T2 - 15th International Symposium on NASA Formal Methods, NFM 2023

Y2 - 16 May 2023 through 18 May 2023

ER -

Kochdumper N, Schilling C, Althoff M, Bak S. Open- and Closed-Loop Neural Network Verification Using Polynomial Zonotopes. In Rozier KY, Chaudhuri S, editors, NASA Formal Methods - 15th International Symposium, NFM 2023, Proceedings. Springer Science and Business Media Deutschland GmbH. 2023. p. 16-36. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-031-33170-1_2

Open- and Closed-Loop Neural Network Verification Using Polynomial Zonotopes

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this