Verification of Neural Networks (Lecture Notes)

베네딕트 볼리그의 강의 노트를 바탕으로 한 "신경망 검증 (Verification of Neural Networks)" 논문에 대한 상세한 기술적 요약은 다음과 같습니다.

1. 문제 제기

이 논문은 자율 주행 차량, 의료 진단 등 안전이 중요한 시스템에 점점 더 많이 배포되고 있는 신경망 (NN) 에 대한 형식적 보장 (formal guarantees) 제공의 과제를 다룹니다. 전통적인 소프트웨어와 달리, NN 은 데이터로 학습된 "블랙박스" 모델이므로 그 동작이 불투명하며 표준적인 테스트를 통해 검증하기 어렵습니다.

핵심 문제는 **검증 (verification)**입니다. 즉, 정의된 도메인 내의 모든 가능한 입력에 대해 신경망이 특정 수명 명세 (예: 강건성, 공정성, 기능적 정확성) 를 만족하는지 여부를 결정하는 것입니다. 이 논문은 이 검증의 이론적 한계를 탐구하며, 특히 다음 사항에 초점을 맞춥니다:

• 결정 가능성 (Decidability): 명제가 성립하는지 알고리즘적으로 결정할 수 있는가?
• 복잡도 (Complexity): 검증의 계산 비용은 얼마인가?
• 표현력 (Expressiveness): 다양한 아키텍처 (순방향, 순환, 트랜스포머) 와 활성화 함수가 이러한 속성에 어떻게 영향을 미치는가?

2. 방법론

저자는 이론적 컴퓨터 과학 접근법을 활용하여 다음을 결합합니다:

• 형식 논리: **선형 실수 산술 (LRA)**을 사용하여 명세를 정의하고, 이를 **신경망 논리 (NNL)**로 확장합니다.
• 오토마타 이론: 실수를 모델링하고 산술 이론을 결정하기 위해 무한 단어 위에서 작동하는 **뷔히 오토마타 (Büchi automata)**를 활용합니다.
• 환원 (Reductions): 확률적 유한 오토마타의 공집합성 문제나 수정된 포스트 대응 문제 (Modified Post Correspondence Problem) 와 같은 알려진 결정 불가능 문제를 신경망 검증 문제로 환원시켜 결정 불가능성이나 난이도를 증명합니다.
• 아키텍처 분석: 순방향 신경망 (FFNN), 순환 신경망 (RNN), 그리고 트랜스포머 (어텐션 메커니즘) 를 체계적으로 분석합니다.

3. 주요 기여 및 결과

A. 순방향 신경망 (FFNNs)

• 명세 언어 (NNL): 저자는 네트워크의 입력 - 출력 관계를 나타내는 술어 $N(x) = y$를 포함하는 LRA 의 확장인 **신경망 논리 (NNL)**를 정의합니다.
• ReLU 에 대한 결정 가능성:
  • 정리: ReLU 활성화 함수를 사용하는 NNL 의 만족 가능성 문제 ($\text{SAT}(\text{NNL}[\text{ReLU}])$) 은 결정 가능합니다.
  • 방법: 증명 과정은 신경망을 동등한 LRA 수식으로 변환합니다. LRA 가 결정 가능하므로 (오토마타 이론적 기법을 통해), ReLU 네트워크에 대한 NN 검증 또한 결정 가능합니다.
• 복잡도:
  • ReLU 를 사용하는 NNL 의 **존재적 단편 (existential fragment)**은 NP-완전입니다.
  • **보편적 단편 (universal fragment)**은 coNP-완전입니다.
  • 난이도: 특정 입력에서 특정 상태에 도달할 수 있는지 확인하는 제한된 "도달 가능성 (reachability)" 문제조차 3SAT 로부터의 환원을 통해 NP-난해 (NP-hard) 임이 증명되었습니다.
• ReLU 를 넘어선 경우:
  • 시그모이드 ($\sigma$), tanh, 또는 NLReLU와 같은 활성화 함수를 사용하는 네트워크의 경우, 검증 문제는 **실수 지수체의 일차 논리 (First-Order Theory of the Real Exponential Field, REF)**와 동등해집니다.
  • 현황: REF 의 결정 가능성 (타르스키의 지수 함수 문제) 은 현재 알려지지 않았으므로, 이러한 일반적 네트워크에 대한 검증은 열린 문제입니다.

B. 순환 신경망 (RNNs)

• 결정 불가능성:
  • 정리: RNN 의 공집합성 문제 (emptiness problem) (네트워크가 양수로 분류하는 입력 시퀀스가 존재하는지 결정하는 문제) 는 결정 불가능합니다.
  • 증명 전략:
    1. (ReLU, 시그모이드)-RNN 이 **확률적 유한 오토마타 (PFAs)**를 시뮬레이션할 수 있음을 보입니다.
    2. PFA 의 공집합성 문제 (특히, 수용 확률이 임계값과 같거나 초과하는지 확인하는 문제) 가 결정 불가능하다는 알려진 결과 (수정된 포스트 대응 문제로부터 환원됨) 에 의존합니다.
  • 함의: 기본 공집합성 문제가 결정 불가능하므로, RNN 에 대한 대부분의 비자명한 검증 작업 또한 결정 불가능합니다.

C. 어텐션 및 트랜스포머

• 아키텍처: 이 논문은 어텐션 헤드, 멀티헤드 레이어, 인코더, 디코더를 포함한 트랜스포머 아키텍처를 형식화합니다.
• 표현력:
  • Encoder-Only 아키텍처를 사용하여 트랜스포머가 시퀀스 내 최대값 찾기, 정렬된 시퀀스 인식, 잘 형성된 괄호 문자열 인식과 같은 복잡한 함수를 계산할 수 있음이 보입니다.
  • 논문은 어텐션 메커니즘 (예: avg-argmax 어텐션) 과 순방향 레이어를 사용하여 이러한 작업을 수행하는 특정 트랜스포머를 구성하는 방법을 보여줍니다.
• 검증 현황:
  • 일반 트랜스포머 아키텍처의 튜링 완전성 (Turing completeness) (튜링 머신을 시뮬레이션할 수 있음) 으로 인해, 일반적인 검증은 결정 불가능할 가능성이 높습니다.
  • 논문은 특정 제한된 단편은 결정 가능할 수 있으나, 트랜스포머에 대한 일반적인 긍정적 결정 가능성 결과는 여전히 열린 연구 영역임을 강조합니다.

4. 중요성 및 함의

1. 이론적 경계: 이 연구는 이론적으로 검증 가능한 것과 불가능한 것 사이의 경계를 명확히 구분합니다. 단순한 ReLU 네트워크는 결정 가능하더라도 NP-난해한 반면, 순환성 (RNN) 이나 복잡한 비선형성 (지수/초월 함수) 을 추가하면 문제가 결정 불가능 영역이나 결정 가능성 미지의 영역으로 밀려난다는 것을 확립합니다.
2. 형식 명세: 강건성 (작은 입력 변화가 출력을 바꾸지 않음), 공정성 (민감한 특징을 무시함), 기능적 동등성과 같은 속성을 표현하기 위한 엄격한 논리 프레임워크 (NNL) 를 제공하여, 임시적인 테스트를 넘어설 수 있게 합니다.
3. 실무자 지침:
   • FFNN의 경우 검증은 가능하지만 계산 비용이 많이 듭니다. 실무자는 존재적 단편에 집중하거나 SMT 솔버를 사용해야 합니다.
   • RNN 과 트랜스포머의 경우, 일반적인 경우 정확한 검증은 이론적으로 불가능합니다. 이는 이러한 모델에 대한 검증이 추상화, 근사, 또는 아키텍처의 제한된 하위 클래스에 의존해야 함을 시사합니다.
4. 미래 연구 방향: 이 논문은 트랜스포머의 검증과 실수 지수체의 결정 가능성을 중요한 열린 문제로 식별합니다. 향후 연구는 유용성을 유지하면서 결정 가능성을 회복시키는 특정 아키텍처 제약을 규명하는 데 초점을 맞춰야 함을 제안합니다.

요약 결론

볼리그의 강의 노트는 신경망 검증에 대한 기초적인 이론적 분석을 제공합니다. 핵심 결론은 ReLU 활성화 함수를 가진 순방향 네트워크에 대한 검증은 결정 가능합니다 (선형 실수 산술로 환원 가능) 하지만, 순환 네트워크에 대해서는 결정 불가능해지며, 초월 활성화 함수를 가진 네트워크나 일반 트랜스포머에 대해서는 여전히 열린 문제로 남아있다는 점입니다. 이는 범용 정확한 검증에 의존하기보다 현대 딥러닝 아키텍처에 맞는 특수화된 근사 검증 도구 개발의 필요성을 강조합니다.