Scalable Polyhedral Verification of Recurrent Neural Networks
| Autor: | Gagandeep Singh, Mislav Balunovic, Wonryong Ryou, Martin Vechev, Andrei Marian Dan, Jiayu Chen |
|---|---|
| Přispěvatelé: | Silva, Alexandra, Leino, K. Rustan M. |
| Jazyk: | angličtina |
| Rok vydání: | 2021 |
| Předmět: |
FOS: Computer and information sciences
Computer Science - Machine Learning Sound (cs.SD) Theoretical computer science Abstraction refinement Computer science Data classification Machine Learning (stat.ML) 02 engineering and technology Gas meter prover Polyhedral abstraction Computer Science - Sound Machine Learning (cs.LG) Set (abstract data type) Statistics - Machine Learning Audio and Speech Processing (eess.AS) Long short-term memory 0202 electrical engineering electronic engineering information engineering FOS: Electrical engineering electronic engineering information engineering Preprocessor Speech classifier verification 020207 software engineering Pipeline (software) Robustness verification Recurrent neural networks Recurrent neural network Scalability 020201 artificial intelligence & image processing Gradient descent Electrical Engineering and Systems Science - Audio and Speech Processing |
| Zdroj: | Lecture Notes in Computer Science, 12759 Computer Aided Verification Computer Aided Verification ISBN: 9783030816841 CAV (1) |
| ISSN: | 0302-9743 1611-3349 |
| Popis: | 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 nonlinear 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. Lecture Notes in Computer Science, 12759 ISSN:0302-9743 ISSN:1611-3349 Computer Aided Verification ISBN:978-3-030-81685-8 ISBN:978-3-030-81684-1 |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|