近年來隨著人工智能的快速發展，愈來愈多安全問題出現，對於其安全性驗證的演算法也相繼被提出。本篇論文專注於驗證神經網路的局部穩定性 (local robustness)，也就是在特定擾動與資料庫的神經網路，驗證其穩定性 (robustness)。在眾多安全驗證演算法中，我們發現 Reluval 與 Neurify 在分析時，不同區間相互獨立，且包含大量乘加運算，適合用硬體加速，且同時符合健全性與完整性。
在本篇論文中，全硬體設計且加上 Reluval 沒有的卷積與池化運算。同時，在梯度 (gradient) 上也支援卷積與池化運算，可以從輸出層反推得到最具影響力的輸入，並切割區間得到更嚴謹的結果或反例。最後，我們實驗不同存儲裝置、切割區間的方式與梯度運算的方式的效果。同時，我們可以得到比 DeepPoly 與 Refinepoly 更快的分析速度。

In recent years, with the rapid development of artificial intelligence, more and more security problems have appeared, and many algorithms for formal verification have also been proposed. We focus on verifying the local robustness of neural networks, that is, neural networks under specific perturbations and databases. Among many formal verification algorithms, we found that Reluval and Neurify are suitable for hardware implementation. Because different intervals were independent of each other and include a large number of multiplication and addition operations. They are sound and complete which can make our analysis more precise. In this paper, we implement the full hardware design which is combined with convolution and pooling operations that Reluval does not have. At the same time, convolution and pooling operations are also supported by the gradient calculation, which can be inferred from the output layer to get the most influential input and split the interval to get more rigorous results or potential counterexamples. Finally, we experiment with the effects of different storage policies, ways of cutting intervals, and different policies of gradient calculation. At the same time, we can receive more conclusive results than DeepPoly and RefinePoly, and much faster than them.

[1] ETH Robustness Analyzer for Neural Networks (ERAN). https://github.com/ethsri/eran, 2020.

[2] Timon Gehr, Matthew Mirman, Dana Drachsler-Cohen, Petar Tsankov, Swarat Chaudhuri, and Martin Vechev. Ai2: Safety and robustness certification of neural networks with abstract interpretation. In 2018 IEEE Symposium on Security and Privacy (SP), pages 3–18. IEEE, 2018.

[3] Ian J Goodfellow, Jonathon Shlens, and Christian Szegedy. Explaining and harnessing adversarial examples. arXiv preprint arXiv:1412.6572, 2014.

[4] Matthias Hein and Maksym Andriushchenko. Formal guarantees on the robustness of a classifier against adversarial manipulation. Advances in neural information processing systems, 30, 2017.

[5] Guy Katz, Clark Barrett, David L Dill, Kyle Julian, and Mykel J Kochenderfer. Reluplex: An efficient smt solver for verifying deep neural networks. In International conference on computer aided verification, pages 97–117. Springer, 2017.

[6] Mykel J Kochenderfer, Jessica E Holland, and James P Chryssanthacopoulos. Next generation airborne collision avoidance system. Technical report, Massachusetts Institute of Technology-Lincoln Laboratory Lexington United States, 2012.

[7] Alexey Kurakin, Ian J Goodfellow, and Samy Bengio. Adversarial examples in the physical world. In Artificial intelligence safety and security, pages 99–112. Chapman and Hall/CRC, 2018.

[8] Yann LeCun and Corinna Cortes. MNIST handwritten digit database. 2010.

[9] Nicolas Papernot, Patrick McDaniel, Ian Goodfellow, Somesh Jha, Z Berkay Celik, and Ananthram Swami. Practical black-box attacks against machine learning. In Proceedings of the 2017 ACM on Asia conference on computer and communications security, pages 506–519, 2017.

[10] Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev. Boosting robustness certification of neural networks. In International Conference on Learning Representations, 2018.

[11] Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev. An abstract domain for certifying neural networks. Proceedings of the ACM on Programming Languages, 3(POPL):1–30, 2019.

[12] Chi-Kai Wang. Local robustness analysis on neural network with symbolic interval analysis by hardware acceleration method. Master’s thesis, 2021.

[13] Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana. Efficient formal safety analysis of neural networks. In S. Bengio, H. Wallach, H. Larochelle, 54 K. Grauman, N. Cesa-Bianchi, and R. Garnett, editors, Advances in Neural Information Processing Systems, volume 31. Curran Associates, Inc., 2018.

[14] Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana. Formal security analysis of neural networks using symbolic intervals. In 27th USENIX Security Symposium (USENIX Security 18), pages 1599–1614, 2018.

[15] Tsui-Wei Weng, Huan Zhang, Pin-Yu Chen, Jinfeng Yi, Dong Su, Yupeng Gao, Cho Jui Hsieh, and Luca Daniel. Evaluating the robustness of neural networks: An extreme value theory approach. arXiv preprint arXiv:1801.10578, 2018.

[16] Kaidi Xu, Huan Zhang, Shiqi Wang, Yihan Wang, Suman Jana, Xue Lin, and Cho-Jui Hsieh. Fast and complete: Enabling complete neural network verification with rapid and massively parallel incomplete verifiers. arXiv preprint arXiv:2011.13824, 2020.