Verification of Recurrent Neural Networks with Star Reachability
Verification of Recurrent Neural Networks with Star Reachability
复制标题
DOI：
10.1145/3575870.3587128
复制
发表时间：
2023-05
期刊：
影响因子：
--
通讯作者：
Hoang-Dung Tran;Sung-Woo Choi;Xiaodong Yang;Tomoya Yamaguchi;Bardh Hoxha;D. Prokhorov
中科院分区：
文献类型：
--
作者：
Hoang-Dung Tran;Sung-Woo Choi;Xiaodong Yang;Tomoya Yamaguchi;Bardh Hoxha;D. Prokhorov
该论文扩展了最近的星可达性方法，以验证循环神经网络（RNN）在安全关键应用中的鲁棒性。 RNN 是一种适用于各种应用的流行机器学习方法，但它们很容易受到对抗性攻击，其中轻微扰动输入序列可能会导致意外结果。最近用于验证 RNN 的值得注意的技术包括展开和不变推理方法。第一种方法存在缩放问题，因为展开 RNN 会创建一个大型前馈神经网络。第二种方法使用不变集，具有更好的可扩展性，但由于过度逼近误差随时间的积累，可能会产生未知的结果。本文介绍了一种健全且完整的 RNN 补充验证方法。松弛参数可用于将该方法转换为仍然提供稳健性保证的快速过逼近方法。该方法旨在与 NNV 一起使用，NNV 是一种用于验证深度神经网络和支持学习的网络物理系统的工具。与最先进的方法相比，扩展精确可达性方法快 10 倍，过近似方法快 100 倍到 5000 倍。
The paper extends the recent star reachability method to verify the robustness of recurrent neural networks (RNNs) for use in safety-critical applications. RNNs are a popular machine learning method for various applications, but they are vulnerable to adversarial attacks, where slightly perturbing the input sequence can lead to an unexpected result. Recent notable techniques for verifying RNNs include unrolling, and invariant inference approaches. The first method has scaling issues since unrolling an RNN creates a large feedforward neural network. The second method, using invariant sets, has better scalability but can produce unknown results due to the accumulation of overapproximation errors over time. This paper introduces a complementary verification method for RNNs that is both sound and complete. A relaxation parameter can be used to convert the method into a fast overapproximation method that still provides soundness guarantees. The method is designed to be used with NNV, a tool for verifying deep neural networks and learning-enabled cyber-physical systems. Compared to state-of-the-art methods, the extended exact reachability method is 10 × faster, and the overapproximation method is 100 × to 5000 × faster.