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

Niklas Kochdumper; Christian Schilling; Matthias Althoff; Stanley Bak

doi:10.48550/arXiv.2207.02715

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

Niklas Kochdumper, Christian Schilling, Matthias Althoff, Stanley Bak

Research output: Contribution to book/anthology/report/conference proceeding › Article in proceeding › Research › peer-review

5 Citations (Scopus)

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
Number of pages	20
Publisher	Springer Nature Switzerland AG
Publication date	2023
Pages	272-291
ISBN (Print)	978-3-031-33169-5
ISBN (Electronic)	978-3-031-33170-1
DOIs	https://doi.org/10.48550/arXiv.2207.02715 https://doi.org/10.1007/978-3-031-33170-1
Publication status	Published - 2023
Event	NASA Formal Methods: 15th International Symposium - University of Houston, Houston, United States Duration: 16 May 2023 → 18 May 2023 Conference number: 15 https://conf.researchr.org/home/nfm-2023

Conference

Conference	NASA Formal Methods: 15th International Symposium
Number	15
Location	University of Houston
Country/Territory	United States
City	Houston
Period	16/05/2023 → 18/05/2023
Internet address	https://conf.researchr.org/home/nfm-2023

Series	Lecture Notes in Computer Science
Volume	13903
ISSN	0302-9743

Keywords

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

Access to Document

https://arxiv.org/pdf/2207.02715Licence: CC BY 4.0

AUB Link

Search for the material in Aalborg University Library's search engine

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. 272-291). Springer Nature Switzerland AG. https://doi.org/10.48550/arXiv.2207.02715, https://doi.org/10.1007/978-3-031-33170-1

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 Nature Switzerland AG, 2023. pp. 272-291 (Lecture Notes in Computer Science, Vol. 13903).

@inproceedings{42b376e13ea942e3a22ac0e8a9b16aef,

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 = "Neural network verification, Neural network controlled systems, Reachability analysis, Polynomial zonotopes, Formal verification",

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

year = "2023",

doi = "10.48550/arXiv.2207.02715",

language = "English",

isbn = "978-3-031-33169-5",

series = "Lecture Notes in Computer Science",

publisher = "Springer Nature Switzerland AG",

pages = "272--291",

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

booktitle = "NASA Formal Methods",

address = "Switzerland",

note = "NASA Formal Methods: 15th International Symposium, NFM 2023 ; Conference date: 16-05-2023 Through 18-05-2023",

url = "https://conf.researchr.org/home/nfm-2023",

}

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. Springer Nature Switzerland AG, Lecture Notes in Computer Science, vol. 13903, pp. 272-291, NASA Formal Methods: 15th International Symposium, Houston, Texas, United States, 16/05/2023. https://doi.org/10.48550/arXiv.2207.02715, https://doi.org/10.1007/978-3-031-33170-1

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 Nature Switzerland AG, 2023. p. 272-291 (Lecture Notes in Computer Science, Vol. 13903).

Research output: Contribution to book/anthology/report/conference proceeding › Article in proceeding › Research › 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

N1 - Conference code: 15

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 - Neural network verification

KW - Neural network controlled systems

KW - Reachability analysis

KW - Polynomial zonotopes

KW - Formal verification

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

U2 - 10.48550/arXiv.2207.02715

DO - 10.48550/arXiv.2207.02715

M3 - Article in proceeding

SN - 978-3-031-33169-5

T3 - Lecture Notes in Computer Science

SP - 272

EP - 291

BT - NASA Formal Methods

A2 - Rozier, Kristin Yvonne

A2 - Chaudhuri, Swarat

PB - Springer Nature Switzerland AG

T2 - NASA Formal Methods: 15th International Symposium

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 Nature Switzerland AG. 2023. p. 272-291. (Lecture Notes in Computer Science, Vol. 13903). doi: 10.48550/arXiv.2207.02715, 10.1007/978-3-031-33170-1

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

Abstract

Conference

Keywords

Access to Document

AUB Link

Other files and links

Fingerprint

Cite this