기술 요약: DNN의 글로벌 강건성 검증을 위한 차분 존토프 (Differential Zonotopes)

1. 문제 정의

심층 신경망(DNN)은 교통 및 의료와 같이 보안이 중요한 도메인에 점점 더 많이 배치되고 있으며, 여기서 입력 섭동(perturbation)에 대한 강건성은 필수적입니다. 국소적 강건성(특정 입력 주변의 작은 섭동에 대해 예측이 변하지 않음을 보장하는 것)은 잘 연구된 안전 속성이지만, 글로벌 강건성은 이보다 엄격한 요구 사항입니다. 글로벌 강건성은 특정 거리 내의 모든 입력 쌍에 대해 모델의 예측이 일관되게 유지되어야 함을 요구합니다.

형식적으로, 글로벌 강건성은 단일 실행 트레이스가 아닌 두 개의 유니버설 양화된(universally quantified) 실행 트레이스 간의 관계를 검증해야 하는 2-안전성(2-safety) 속성입니다. 이러한 복잡성으로 인해 글로벌 검증은 로컬 검증보다 훨씬 더 까다롭습니다. 신뢰도 기반 글로벌 강건성(결정 경계를 피하기 위해 높은 신뢰도의 예측에만 보증을 제한함)에 대한 기존 방법들은 특화된 만족도 해결사(satisfiability solvers)에 의존하지만, 현재 수십 개의 뉴런을 가진 네트워크로 제한될 만큼 확장성 측면에서 취약합니다.

2. 방법론

본 논문은 효율적인 글로벌 강건성 검증을 위해 **차분 헤일로 존토프(differential halo zonotopes)**에 기반한 새로운 정적 분석 프레임워크를 제안합니다.

2.1 차분 헤일로 존토프 (Differential Halo Zonotopes)

핵심적인 기술 혁신은 존토프(zonotope) 추상 도메인의 확장입니다. 표준 존토프는 중심(center)과 생성 행렬(generator matrix)을 통해 점들의 집합을 표현합니다. 글로벌 강건성을 검증하기 위해, 저자들은 서로 다른 입력을 가진 동일한 DNN의 두 실행을 동시에 추적해야 합니다.

• 과제: (입력이 동일한 경우의) DNN 동등성(equivalence) 검증에 사용되었던 차분 존토프의 나이브한 적용은 글로벌 강건성 검증에서 실패합니다. 입력을 동일하게 초기화하거나 완전히 독립적인 생성자를 사용하는 것은 부정확하거나 과도한 과대 근사(over-approximation, 정밀도 손실)를 초래합니다.
• 해결책: 저자들은 **차분 헤일로 아핀 형식(differential halo affine forms)**을 도입합니다. 이 인코딩은 섭동 범위 $\epsilon$을 두 개의 생성자에 분배합니다:
  1. 상관관계를 유지하기 위해 두 실행 간에 공유되는 기본 생성자(primary generator).
  2. 각 실행에 대해 독립적으로 작용하여 섭동을 모델링하는 보조 생성자(secondary generators).
• 메커니즘: 이 "헤일로(halo)" 구조를 통해 시스템은 두 입력 $x$와 $y$가 바운딩 박스 $[l, u]$ 내에 있고 $|x - y| \le \epsilon$을 만족한다는 조건을 정확하고 건전하게 인코딩할 수 있습니다. 차분 존토프 $\mathcal{Z}_\Delta$는 개별 존토프를 빼는 것보다 더 타이트한 실행 간의 발산(divergence) 경계 값을 추적합니다.

2.2 대칭적 신뢰도 기반 글로벌 강건성

본 논문은 기존의 신뢰도 기반 글로벌 강건성 정의(비대칭 버전)의 한계를 지적합니다. 비대칭 버전은 고신뢰도 입력 $x$가 $y$의 신뢰도와 관계없이 다른 클래스 $y$로 변하지 않아야 한다고 요구합니다. 저자들은 $y$의 낮은 신뢰도로 인한 다른 예측(예: 수동 검토를 트리거함)은 실질적으로 수용 가능하다는 점에서 이 방식이 지나치게 제한적이라고 주장합니다.

이에 따라 대칭적 변형을 제안합니다:

• 정의: 거리 $\epsilon$ 내의 임의의 두 입력 $x, y$에 대해, 만약 둘 다 임계값 $\tau$ 이상의 신뢰도로 분류된다면, 이들은 반드시 동일한 클래스에 속해야 합니다.
• 이점: 이러한 완화는 저신뢰도 출력이 폴백(fallback) 메커니즘을 통해 처리되는 실제 안전 필수 애플리케이션에 부합하면서도, 더 넓은 범위의 네트워크를 "강건함"의 범주에 포함시킬 수 있게 합니다.

2.3 검증 알고리즘

검증 과정(도구 TwoSafe로 구현됨)은 다음 단계를 따릅니다:

1. 초기화: 입력 공간과 섭동 제약을 나타내는 차분 헤일로 존토프를 구성합니다.
2. 전파(Propagation): DNN 레이어를 통해 존토프를 전파합니다. ReLU 활성화 함수의 경우, 비선형성을 과대 근사하기 위해 새로운 생성자를 도입하여 차분 구조를 유지합니다.
3. 속성 체크: 출력 단계에서, 두 출력이 모두 신뢰도 임계값 $\tau$를 만족하면서 클래스가 서로 다른 경우가 존재하는지 확인하기 위해 선형 계획법(LP) 문제를 구성합니다.
4. 정교화(Refinement): 과대 근사로 인해 결과가 불확명한 경우, 알고리즘은 **생성자 분할(generator splitting)**을 수행합니다. 이는 표준적인 입력 분할과 달리, 섭동 공간의 커버리지를 잃지 않으면서 차분 헤일로 존토프의 생성자를 분할하여 근사를 정교화합니다.

3. 주요 기여

1. 차분 헤일로 존토프: 두 개의 섭동된 입력을 결합하여 락스텝(lock-step)으로 전파하고 발산을 타이트하게 경계 짓는 새로운 추상 도메인입니다. 이를 통해 개별 분석보다 더 높은 정밀도로 글로벌 2-안전성 속성을 검증할 수 있습니다.
2. 대칭적 신뢰도 기반 글로벌 강건성: 고신뢰도 예측 사이에서만 일관성을 요구하는 새로운 글로벌 강건성 정의입니다. 이 정의는 비대칭 버전보다 엄격함이 낮으며, 제안된 프레임워크 내에서 효율적인 검증을 가능하게 합니다.
3. 건전성 증명: 차분 존토프 기반 정적 분석의 건전성에 대한 공식적인 증명을 제공하며, 핵심 결과는 Isabelle을 통해 정형화되었습니다.
4. TwoSafe 도구 및 평가: 제안된 방식을 TwoSafe라는 새로운 도구로 구현하였으며, 이는 정밀도와 확장성 모두에서 최신 기술(CGR 베이스라인)을 크게 능가합니다.

4. 실험 결과

저자들은 네 가지 벤치마크(Law(소규모), LHC(입자 분류), ACAS Xu(충돌 회피), HAR(인간 활동 인식))를 통해 TwoSafe를 평가했습니다.

• 확장성: TwoSafe는 500개의 ReLU 뉴런과 561개의 입력 차원(HAR 벤치마크)을 가진 네트워크에 대해서도 글로벌 강건성 검증에 성공했습니다. 반면, 베이스라인(CGR)은 이러한 대규모 네트워크에서 시간 초과가 발생하거나 메모리를 모두 소모했습니다.
• 정밀도: 베이스라인은 특히 출력 클래스가 많은 네트워크에서 거친 소프트맥스 근사로 인해 빈번하게 **허위 반례(spurious counterexamples)**를 보고했습니다. TwoSafe는 이러한 위양성(false positives)을 방지했습니다.
• 성능: TwoSafe는 상당한 속도 향상을 보여주었습니다. 예를 들어, LHC 벤치마크에서 베이스라인이 2시간 후 타임아웃된 반면, TwoSafe는 3초 미만에 강건성을 검증했습니다.
• 대칭 vs 비대칭: 대칭적 속성은 비대칭 속성이 불명확하거나 실패했던 파라미터 영역에서도 성공적인 검증을 가능하게 했습니다. 예를 들어, $\epsilon=0.01$인 HAR 벤치마크에서 대칭적 속성은 검증 가능했으나 비대칭 버전은 타임아웃되었습니다.

5. 의의 및 주장

본 논문은 강건성 보증의 강도와 검증 도구의 확장성 사이의 내재된 긴장을 해결한다고 주장합니다. 로컬에서 글로벌 강건성 검증으로 전환하고 차분 헤일로 존토프를 활용함으로써, 저자들은 이전보다 훨씬 더 넓고 깊은 네트워크를 검증하는 것이 가능하다는 것을 입증했습니다.

대칭적 신뢰도 기반 글로벌 강건성의 도입은 저신뢰도 예측이 실제 시스템에서 다르게 처리된다는 점을 인정함으로써, 더 넓은 클래스의 네트워크에 적용 가능한 "의미 있는 강건성 개념"을 제공하는 실질적인 진전으로 제시됩니다. 이 연구는 차분 검증이 2-안전성 속성을 위해 적응되었을 때 기존 기술이 다루던 것보다 한 차원 더 큰 규모의 네트워크로 확장될 수 있음을 보여주며, 글로벌 강건성 인증을 실제 배포된 모델에 대해서도 실현 가능한 영역으로 만들었습니다.