구조적 성질을 활용한 심층신경망의 정형검증 기법

Abstract

심층 신경망(DNN)은 음성 인식, 이미지 분류 등의 다양한 분야에서 소프트웨어를 위하여 널리 활용되고 있다. 그 중 자율주행 차량과 같은 안전필수 시스템에 사용되는 DNN은 오류가 큰 인적, 물적 피해를 발생시키므로 DNN의 검증에 대한 필요성은 크게 증가하고 있다. DNN의 일반적인 안전성 평가는 주어진 테스트 입력에 대하여 실행 결과를 확인하는데, 이는 테스트되지 않은 입력에 대해 여전히 오류 가능성이 존재한다는 문제를 가지고 있다. 그러한 대표적인 예시가 적대적 예시로, 이는 기존 입력에 미세한 변화를 주었을 때 전혀 다른 결과가 나타나는 예제를 뜻한다. 적대적 예시와 같은 잘 알려진 DNN의 오류들이 없는지 검증하기 위해서 적대적 예시 방어, 테스트 입력 생성, 정형 검증 등 다양한 방법들이 연구되고 있다. 이 중 정형 검증은 DNN의 모든 입력에 대해 요구사항을 만족하는지를 검증할 수 있다. DNN의 정형 검증 방법은 학습이 끝난 DNN을 수학적인 함수로 표현하고, 검증하고자 하는 성질을 입력과 출력에 관한 수학적인 관계로 표현하여 이를 증명하는 방법이다. 그러나 DNN의 정형 검증은 활성함수로 선형함수를 가지는 DNN의 요구사항을 검증하는 문제가 NP-complete의 복잡도를 가질 정도로 어려운 문제이다. 기존 방법들은 DNN의 구조와 관계없이 사용 가능한 방법들을 연구해왔으며, 본 연구에서는 주로 사용되는 DNN의 특정한 구조를 분석하고 활용하여 DNN의 정형 검증 성능을 향상하는 방법에 대해 제시한다. 이 연구는 DNN의 정형 검증에 활용될 수 있는 DNN의 구조적 성질에 관한 연구이다. 먼저 DNN의 구조적 성질을 각 노드들이 가질 수 있는 상태의 집합으로 수학적으로 정의하고, ReLU를 활성함수로 가지는 DNN의 두 가지 구조적 성질을 제안하였으며 이들이 올바른 구조적 성질인지 증명하였다. 첫 번째로 제안한 구조적 성질은 노드의 가중치, 편향치를 활용하여 노드들의 상태를 분석하였으며, 두 번째로 제안한 구조적 성질은 노드의 범위를 활용하여 노드들의 상태를 분석하였다. 제안된 두 구조적 성질들은 SMT를 사용하는 기존의 DNN 정형 검증 기법에 적용되었다. 기존의 방법은 DNN과 그 요구사항을 SMT 식으로 변환하여 SMT 해석기에 입력하는 방법으로 검증하였다. 따라서 구조적 성질들은 SMT 식으로 변환되어 SMT 해석기에 추가로 입력했으며, 그 효과는 검증 속도의 비교를 통해 확인되었다. 실험은 3개 DNN 벤치마크에서 진행되었으며, 두 가지 구조적 성질을 모두 사용하는 경우 최대 99%의 검증 속도 향상을 얻을 수 있음을 확인하였다.

This thesis proposes a method that exploits the structural properties of deep neural networks (DNNs) to increase the efficiency of DNN verification. DNNs have achieved enormous popularity and used for safety-critical systems such as unmanned aircraft and autonomous driving. However, DNNs have suffered from its errors such as adversarial examples. To overcome these errors, many formal DNN-verification techniques have been proposed. We introduce a new formal verification technique that uses structural properties. DNNs have structural information such as node-connection structures, activation functions, and weights and bias of nodes. This thesis defines the structural property of DNNs using structural information. This thesis suggests two structural properties of a DNN that uses a rectified linear unit (ReLU) as an activation function: one using weights of nodes and one using bounds of nodes. We encode two structural properties of DNNs to satisfiability modulo theories (SMT) formula, then apply them to an SMT solver for formal verification of DNN. We demonstrate the usefulness of the structural properties by showing that the performance of DNN verification is increased by exploiting the structural properties.