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 …

Recurrent neural networks (RNNs) are a state-of-the-art tool to represent and learn
sequence-based models. They have applications in time-series prediction, sentiment
analysis, and many more. In particular, they are increasingly used in safety-critical
applications and act, for example, as controllers in cyber-physical systems. Thus, there is a
growing need for formal verification. However, research in this domain is only at the
beginning. While formal-methods based techniques, such as model checking, have been …