Scalable Polyhedral Verification of Recurrent Neural Networks

Wonryong Ryou; Jiayu Chen; Mislav Balunovic; Gagandeep Singh; Andrei Dan; Martin Vechev

doi:10.1007/978-3-030-81685-8_10

Scalable Polyhedral Verification of Recurrent Neural Networks

Wonryong Ryou, Jiayu Chen, Mislav Balunovic, Gagandeep Singh, Andrei Dan, Martin Vechev

Siebel School of Computing and Data Science

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

Abstract

We present a scalable and precise verifier for recurrent neural networks, called Prover based on two novel ideas: (i) a method to compute a set of polyhedral abstractions for the non-convex and non-linear recurrent update functions by combining sampling, optimization, and Fermat’s theorem, and (ii) a gradient descent based algorithm for abstraction refinement guided by the certification problem that combines multiple abstractions for each neuron. Using Prover, we present the first study of certifying a non-trivial use case of recurrent neural networks, namely speech classification. To achieve this, we additionally develop custom abstractions for the non-linear speech preprocessing pipeline. Our evaluation shows that Prover successfully verifies several challenging recurrent models in computer vision, speech, and motion sensor data classification beyond the reach of prior work.

Original language	English (US)
Title of host publication	Computer Aided Verification - 33rd International Conference, CAV 2021, Proceedings
Subtitle of host publication	33rd International Conference, CAV 2021, Virtual Event, July 20–23, 2021, Proceedings, Part I
Editors	Alexandra Silva, K. Rustan Leino
Publisher	Springer
Pages	225-248
Number of pages	24
ISBN (Electronic)	978-3-030-81685-8
ISBN (Print)	978-3-030-81684-1
DOIs	https://doi.org/10.1007/978-3-030-81685-8_10
State	Published - Jul 15 2021

Publication series

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

Keywords

Abstraction refinement
Long short-term memory
Polyhedral abstraction
Recurrent neural networks
Robustness verification
Speech classifier verification

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Online availability

10.1007/978-3-030-81685-8_10

Library availability

Discover UIUC Full Text

Cite this

Ryou, W., Chen, J., Balunovic, M., Singh, G., Dan, A., & Vechev, M. (2021). Scalable Polyhedral Verification of Recurrent Neural Networks. In A. Silva, & K. R. Leino (Eds.), Computer Aided Verification - 33rd International Conference, CAV 2021, Proceedings: 33rd International Conference, CAV 2021, Virtual Event, July 20–23, 2021, Proceedings, Part I (pp. 225-248). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12759 LNCS). Springer. https://doi.org/10.1007/978-3-030-81685-8_10

Scalable Polyhedral Verification of Recurrent Neural Networks. / Ryou, Wonryong; Chen, Jiayu; Balunovic, Mislav et al.
Computer Aided Verification - 33rd International Conference, CAV 2021, Proceedings: 33rd International Conference, CAV 2021, Virtual Event, July 20–23, 2021, Proceedings, Part I. ed. / Alexandra Silva; K. Rustan Leino. Springer, 2021. p. 225-248 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12759 LNCS).

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

Ryou, W, Chen, J, Balunovic, M, Singh, G, Dan, A & Vechev, M 2021, Scalable Polyhedral Verification of Recurrent Neural Networks. in A Silva & KR Leino (eds), Computer Aided Verification - 33rd International Conference, CAV 2021, Proceedings: 33rd International Conference, CAV 2021, Virtual Event, July 20–23, 2021, Proceedings, Part I. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 12759 LNCS, Springer, pp. 225-248. https://doi.org/10.1007/978-3-030-81685-8_10

Ryou W, Chen J, Balunovic M, Singh G, Dan A, Vechev M. Scalable Polyhedral Verification of Recurrent Neural Networks. In Silva A, Leino KR, editors, Computer Aided Verification - 33rd International Conference, CAV 2021, Proceedings: 33rd International Conference, CAV 2021, Virtual Event, July 20–23, 2021, Proceedings, Part I. Springer. 2021. p. 225-248. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-81685-8_10

Ryou, Wonryong ; Chen, Jiayu ; Balunovic, Mislav et al. / Scalable Polyhedral Verification of Recurrent Neural Networks. Computer Aided Verification - 33rd International Conference, CAV 2021, Proceedings: 33rd International Conference, CAV 2021, Virtual Event, July 20–23, 2021, Proceedings, Part I. editor / Alexandra Silva ; K. Rustan Leino. Springer, 2021. pp. 225-248 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{0bfcf517a7ad4f47b3115fe3d65eaa1f,

title = "Scalable Polyhedral Verification of Recurrent Neural Networks",

abstract = "We present a scalable and precise verifier for recurrent neural networks, called Prover based on two novel ideas: (i) a method to compute a set of polyhedral abstractions for the non-convex and non-linear recurrent update functions by combining sampling, optimization, and Fermat{\textquoteright}s theorem, and (ii) a gradient descent based algorithm for abstraction refinement guided by the certification problem that combines multiple abstractions for each neuron. Using Prover, we present the first study of certifying a non-trivial use case of recurrent neural networks, namely speech classification. To achieve this, we additionally develop custom abstractions for the non-linear speech preprocessing pipeline. Our evaluation shows that Prover successfully verifies several challenging recurrent models in computer vision, speech, and motion sensor data classification beyond the reach of prior work.",

keywords = "Abstraction refinement, Long short-term memory, Polyhedral abstraction, Recurrent neural networks, Robustness verification, Speech classifier verification",

author = "Wonryong Ryou and Jiayu Chen and Mislav Balunovic and Gagandeep Singh and Andrei Dan and Martin Vechev",

year = "2021",

month = jul,

day = "15",

doi = "10.1007/978-3-030-81685-8_10",

language = "English (US)",

isbn = "978-3-030-81684-1",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "225--248",

editor = "Alexandra Silva and Leino, {K. Rustan}",

booktitle = "Computer Aided Verification - 33rd International Conference, CAV 2021, Proceedings",

address = "Germany",

}

TY - GEN

T1 - Scalable Polyhedral Verification of Recurrent Neural Networks

AU - Ryou, Wonryong

AU - Chen, Jiayu

AU - Balunovic, Mislav

AU - Singh, Gagandeep

AU - Dan, Andrei

AU - Vechev, Martin

PY - 2021/7/15

Y1 - 2021/7/15

N2 - We present a scalable and precise verifier for recurrent neural networks, called Prover based on two novel ideas: (i) a method to compute a set of polyhedral abstractions for the non-convex and non-linear recurrent update functions by combining sampling, optimization, and Fermat’s theorem, and (ii) a gradient descent based algorithm for abstraction refinement guided by the certification problem that combines multiple abstractions for each neuron. Using Prover, we present the first study of certifying a non-trivial use case of recurrent neural networks, namely speech classification. To achieve this, we additionally develop custom abstractions for the non-linear speech preprocessing pipeline. Our evaluation shows that Prover successfully verifies several challenging recurrent models in computer vision, speech, and motion sensor data classification beyond the reach of prior work.

AB - We present a scalable and precise verifier for recurrent neural networks, called Prover based on two novel ideas: (i) a method to compute a set of polyhedral abstractions for the non-convex and non-linear recurrent update functions by combining sampling, optimization, and Fermat’s theorem, and (ii) a gradient descent based algorithm for abstraction refinement guided by the certification problem that combines multiple abstractions for each neuron. Using Prover, we present the first study of certifying a non-trivial use case of recurrent neural networks, namely speech classification. To achieve this, we additionally develop custom abstractions for the non-linear speech preprocessing pipeline. Our evaluation shows that Prover successfully verifies several challenging recurrent models in computer vision, speech, and motion sensor data classification beyond the reach of prior work.

KW - Abstraction refinement

KW - Long short-term memory

KW - Polyhedral abstraction

KW - Recurrent neural networks

KW - Robustness verification

KW - Speech classifier verification

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

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

U2 - 10.1007/978-3-030-81685-8_10

DO - 10.1007/978-3-030-81685-8_10

M3 - Conference contribution

SN - 978-3-030-81684-1

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

SP - 225

EP - 248

BT - Computer Aided Verification - 33rd International Conference, CAV 2021, Proceedings

A2 - Silva, Alexandra

A2 - Leino, K. Rustan

PB - Springer

ER -

Scalable Polyhedral Verification of Recurrent Neural Networks

Abstract

Publication series

Keywords

ASJC Scopus subject areas

Online availability

Library availability

Related links

Fingerprint

Cite this