Property-Directed Verification of Recurrent Neural Networks

TL;DR

This paper introduces a property-guided verification method for RNNs that learns a finite automaton model to efficiently find and analyze counterexamples, improving the verification process.

Contribution

It proposes a novel property-directed approach combining automata learning and model checking for RNN verification, enabling faster error detection and analysis.

Findings

Fast discovery of small counterexamples

Generalization of counterexamples through pumping

Effective identification of underlying errors in RNNs

Abstract

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 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 towards faulty flows hinting at the underlying error in the RNN.