Scalable Polyhedral Verification of Recurrent Neural Networks
| Main Authors: | Ryou, Wonryong, Chen, Jiyau, Mislav, Balunovic, Singh, Gagandeep, Dan, Andrei-Marian, Vechev, Martin |
|---|---|
| Format: | info software Journal |
| Bahasa: | eng |
| Terbitan: |
, 2021
|
| Subjects: | |
| Online Access: |
https://zenodo.org/record/4742650 |
Daftar Isi:
- We present a scalable and precise verifier for recurrent neural networks, called Prover. Prover relies 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 and speech classification beyond the reach of prior work. Please follow the `readme.md` located in the home directory. The system requires: Gurobi optimizer licence - please refer to https://www.gurobi.com/academia/academic-program-and-licenses/ GPU available environment (not necessary but highly recommended) Preliminary information for the VM: 1. List of essential files and directory * /home/cav2021-paper187/readme.md: includes detailed instructions about how to prepare and run the artifact. * /home/cav2021-paper187/CAV2021_paper_187.pdf: the accepted paper pdf. * /home/cav2021-paper187/artifact/: the artifact codes and necessaries. 2. Recommended resource allocaiton * Memory: 4GB * Disk: 20GB because of the dataset * GPU available environment 3. Credentials * ID: cav2021-paper187 * PW: 2021-187-prover