Abstractions for Verifying DNN

Abstract

Deep learning has performed well in many areas, but it doesn’t know how the results were derived and is vulnerable to errors like adversarial examples. Therefore, much research is being conducted to ensure the safety and robustness of deep neural networks. Since deep neural networks are large in scale and the activation function is non-linear, a method of approximating the activation function linearly is generally proposed and widely used during verification. In this thesis, we propose layered abstraction, which is a new abstraction method for activation functions such as ReLU and Tanh, and a verification algorithm based on it. Layered abstraction is an abstraction method in which the abstraction of each activation function is divided into levels. The algorithm using layered abstraction applies abstraction sequentially from low accuracy to high accuracy until the verification result is obtained. We implement an algorithm by extending the existing SMT-based methods. In this thesis, we find that the implemented algorithm performed better than the existing tool. Furthermore, it is confirmed that SMT verification of DNN with Tanh and Sigmoid activation function, which were not possible in the past, are possible by layered abstraction

딥 러닝은 다양한 분야에서 좋은 성과를 내고 있지만 그 결과 값이 어떻게 도출되었는지 알 수 없어서 적대적 예제와 같은 오류에 취약하다. 따라서 심층 신경망(deep neural network)의 안전성과 강건성을 보장하기 위한 많은 연구가 이루어지고 있다. 심층 신경망은 규모가 크고 활성화 함수(activation function)들이 비선형이기 때문에 일반적으로 검증 시 활성화 함수를 선형으로 근사하는 방법이 제안되어 널리 사용되고 있다. 본 논문에서는 ReLU, Tanh, Sigmoid 활성화 함수에 대해 새로운 근사 방법인 계층별 요약(layered abstraction) 및 이에 기반한 검증 알고리즘을 제안한다. 계층별 요약은 각 활성화 함수의 요약을 단계별로 나눈 새로운 요약 기법이다. 계층별 요약을 활용한 알고리즘은 요약을 낮은 정확도부터 높은 정확도까지 검증 결과를 얻을 때까지 순차적으로 적용한다. 본 논문에서는 알고리즘의 구현을 위해 기존의 SMT 기반 방식을 확장했다. 또한 구현된 알고리즘이 기존 도구보다 성능이 향상되었음을 확인했다. 마지막으로 기존에는 불가능했던 Tanh와 Sigmoid 활성화 함수를 가진 심층 신경망의 SMT 검증이 계층별 요약을 통해 합리적인 시간 내에 가능함을 확인했다.