Analysis of Recurrent Neural Networks via Property-Directed Verification of Surrogate Models

Autor: Igor Khmelnitsky, Daniel Neider, Rajarshi Roy, Xuan Xie, Benoît Barbot, Benedikt Bollig, Alain Finkel, Serge Haddad, Martin Leucker, Lina Ye
Přispěvatelé: Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Modeling and Exploitation of Interaction and Concurrency (MEXICO), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Carl Von Ossietzky Universität Oldenburg, Max Planck Institute for Software Systems (MPI-SWS), Université Paris-Est Créteil Val-de-Marne - Paris 12 (UPEC UP12), Universität zu Lübeck = University of Lübeck [Lübeck], Carl Von Ossietzky Universität Oldenburg = Carl von Ossietzky University of Oldenburg (OFFIS), Bollig, Benedikt
Jazyk: angličtina
Rok vydání: 2022
Předmět:
Zdroj: International Journal on Software Tools for Technology Transfer
International Journal on Software Tools for Technology Transfer, Springer Verlag, In press
International Journal on Software Tools for Technology Transfer, inPress
ISSN: 1433-2779
1433-2787
Popis: This paper presents a property-directed approach to verifying recurrent neural networks (RNNs). To this end, we learn a deterministic finite automaton as a surrogate model from a given RNN using active automata learning. This model may then be analyzed using model checking as a verification technique. The term property-directed reflects the idea that our procedure is guided and controlled by the given property rather than performing the two steps separately. We show that this not only allows us to discover small counterexamples fast, but also to generalize them by pumping toward faulty flows hinting at the underlying error in the RNN. We also show that our method can be efficiently used for adversarial robustness certification of RNNs.
Databáze: OpenAIRE
Externí odkaz: