DiffRNN: Differential Verification of Recurrent Neural Networks
DiffRNN: Differential Verification of Recurrent Neural Networks
复制标题
DOI：
10.1007/978-3-030-85037-1_8
复制
发表时间：
2020-07
期刊：
影响因子：
--
通讯作者：
Sara Mohammadinejad;Brandon Paulsen;Chao Wang;Jyotirmoy V. Deshmukh
中科院分区：
文献类型：
--
作者：
Sara Mohammadinejad;Brandon Paulsen;Chao Wang;Jyotirmoy V. Deshmukh
递归神经网络（RNN），如长短期记忆（LSTM）网络，在各种应用中已经变得流行，如图像处理，数据分类，语音识别，以及作为自治系统中的控制器。在实际环境中，通常需要在资源受限的平台上部署此类RNN，例如移动的电话或嵌入式设备。由于这些组件的内存占用和能耗成为瓶颈，因此有兴趣使用一系列启发式技术来压缩和优化这些网络。然而，这些技术不能保证优化网络的安全性，例如，对抗对抗性输入，或者优化网络和原始网络的等价性。为了解决这个问题，我们提出了DiffRNN，这是RNN的第一种差分验证方法，可以证明两个结构相似的神经网络的等价性。基于ReLU的前馈神经网络差分验证的现有工作不适用于RNN，其中无法避免非线性激活函数，如Sigmoid和Tanh。RNN还带来了独特的挑战，例如处理顺序输入，复杂的反馈结构以及门和状态之间的相互作用。在DiffRNN中，我们通过用线性约束非线性激活函数，然后解决约束优化问题来计算高维空间中非线性表面上的紧密边界框来克服这些挑战。然后使用dRealSMT求解器证明这些边界框的合理性。我们证明了我们的技术在各种基准测试中的实际效果，并表明DiffRNN优于最先进的RNN验证工具，如Popqorn。
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 proposeDiffRNN, the first differential verification method for RNNs to certify the equivalence of two structurally similar neural networks. Existing work on differential verification forReLU-based feed-forward neural networks does not apply to RNNs where nonlinear activation functions such asSigmoidandTanhcannot be avoided. RNNs also pose unique challenges such as handling sequential inputs, complex feedback structures, and interactions between the gates and states. InDiffRNN, we overcome these challenges by bounding nonlinear activation functions with linear constraints and then solving constrained optimization problems to compute tight bounding boxes on non-linear surfaces in a high-dimensional space. The soundness of these bounding boxes is then proved using thedRealSMT solver. We demonstrate the practical efficacy of our technique on a variety of benchmarks and show thatDiffRNNoutperforms state-of-the-art RNN verification tools such asPopqorn.