Qualitative and Quantitative Model Checking against Recurrent Neural Networks

Recurrent neural networks (RNNs) have been heavily used in applications relying on sequence data such as time series and natural languages. As a matter of fact, their behaviors are short of rigorous quality assurance due to the black-box nature of deep learning. It is an urgent and challenging task to formally reason about behaviors of RNNs. To this end, we first present an extension of linear-time temporal logic to reason about properties with respect to RNNs, such as local robustness, reachability and some temporal properties. Based on the proposed logic, we formalize the verification obligation as a Hoare-like triple, from both qualitative and quantitative perspectives: the former concerns whether all the outputs resulting from the inputs fulfilling the pre-condition satisfy the post-condition, whereas the latter is to compute the probability that the post-condition is satisfied on the premise that the inputs fulfill the pre-condition. To tackle these problems, we have developed a systematic verification framework, mainly based on polyhedron propagation, dimension-preserving abstraction, and the Monte Carlo sampling. We have also implemented our algorithm with a prototype tool and conducted experiments to demonstrate its feasibility and efficiency.