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
N1 - Publisher Copyright:
© 2023, The Author(s), under exclusive license to Springer Nature Switzerland AG.
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
AN - SCOPUS:85163990011
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 -