Recurrent neural network properties and their verification with monte carlo techniques

As RNNs find its applications in medical and automotive fields, they became a part of critical systems, which traditionally require thorough verification processes. In this work we present how RNNs behaviors can be modeled as labeled transition systems and formally define a set of state and temporal safety properties for such models. To verify those properties we propose to use the Monte Carlo approach and evaluate its effectiveness for different type of properties.We perform empirical evaluation on two RNN models to determine to what extent they satisfy the properties and how many the samples of Monte Carlo required to provide accurate results. Our experiments show that our models satisfy better state properties than temporal properties. In addition, we show that Monte Carlo sampling is quite effective for state property verification, which commonly requires a small fraction of RNN's model to be explored. However, for verification of temporal properties Monte Carlo needs to analyze up to 20% of computations.