Recurrent neural networks (RNNs) such as Long Short Term Memory (LSTM) networks have become popular in a variety of applications such as image processing, data classification, speech recognition, and as controllers in autonomous systems. In practical settings, there is often a need to deploy such RNNs on resource-constrained platforms such as mobile phones or embedded devices. As the memory footprint and energy consumption of such components become a bottleneck, there is interest in compressing and optimizing such networks using a range of heuristic techniques. However, these techniques do not guarantee the safety of the optimized network, e.g., against adversarial inputs, or equivalence of the optimized and original networks. To address this problem, we propose DIFFRNN, the first differential verification method for RNNs to certify the equivalence of two structurally similar neural networks. Existing work on differential verification for ReLUbased feed-forward neural networks does not apply to RNNs where nonlinear activation functions such as Sigmoid and Tanh cannot be avoided. RNNs also pose unique challenges such as handling sequential inputs, complex feedback structures, and interactions between the gates and states. In DIFFRNN, we overcome these challenges by bounding nonlinear activation functions with linear constraints and then solving constrained optimization problems to compute tight bounding boxes on nonlinear surfaces in a high-dimensional space. The soundness of these bounding boxes is then proved using the dReal SMT solver. We demonstrate the practical efficacy of our technique on a variety of benchmarks and show that DIFFRNN outperforms state-of-the-art RNN verification tools such as POPQORN.
Property-Directed Verification of Recurrent Neural Networks
LSV, CNRS, ENS Paris-Saclay, Université Paris-Saclay（巴黎萨克雷高等师范学院、巴黎萨克雷大学、法国国家科学研究中心、验证与安全实验室）；Inria（法国国家信息与自动化研究所）；Max Planck Institute for Software Systems（马克斯·普朗克软件系统研究所）；Université Paris-Est Créteil（巴黎东大克雷泰伊校区）；Universität zu Lübeck（吕贝克大学）；CentraleSupélec（中央理工-高等电力学院）；Institut Universitaire de France（法国大学研究院）
Counterexample-Guided Strategy Improvement for POMDPs Using Recurrent Neural Networks
The University of Texas at Austin（得克萨斯大学奥斯汀分校）；Radboud University（拉德堡德大学）；Albert-Ludwigs-Universität Freiburg（阿尔伯特-路德维希大学弗莱堡分校）；Concept Engineering GmbH（康赛普特工程有限公司）
