Formal Reasoning About Confidence and Automated Verification of Neural Networks

이 논문은 신경망의 강건성과 신뢰도를 함께 고려하는 포괄적인 프레임워크를 제안하며, 간단한 문법과 추가 레이어를 도입해 기존 검증 도구를 활용하여 8,870 개의 벤치마크에서 기존 방법보다 뛰어난 성능을 입증했습니다.

핵심

이 논문은 인공지능 (AI), 특히 **'신경망 (Neural Network)'**이라는 기술이 얼마나 안전한지, 그리고 그 판단이 얼마나 **'확신 (Confidence)'**에 기반하는지를 검증하는 새로운 방법을 소개합니다.

쉽게 말해, **"AI 가 실수를 했을 때, 그 실수가 얼마나 무서운 실수인지, 아니면 그냥 '아, 헷갈렸네' 정도의 실수인지 구분하는 방법"**을 개발한 것입니다.

이 내용을 일상적인 비유로 설명해 드리겠습니다.

---

1. 기존 문제: "틀렸으면 무조건 나쁜 거야?" (Robustness 의 한계)

지금까지 AI 를 검증할 때는 **"입력이 조금만 바뀌어도 (예: 사진에 노이즈가 살짝 섞여도) AI 가 같은 답을 내는지"**만 확인했습니다. 이를 '강인성 (Robustness)'이라고 합니다.

• 비유: 비가 오는 날, 우산을 살짝 흔들었을 때 우산이 넘어지면 "이 우산은 나쁘다!"라고 판단하는 것과 같습니다.
• 문제점: 하지만 AI 가 우산을 흔들었을 때 넘어지더라도, **"아, 비가 너무 많이 와서 내가 헷갈린 거야 (확신도 낮음)"**라고 스스로 인정한다면, 그 우산은 사실 쓸만할 수도 있습니다.
• 기존 방식의 맹점: 기존의 검증 도구들은 AI 가 확신이 낮아서 (예: 20% 만 확신) 틀린 경우에도 "틀렸다! 위험하다!"라고만 외쳐서, 실제로는 안전한 AI 를 불필요하게 폐기하거나 과도하게 경계하게 만들었습니다.

2. 이 논문의 핵심 아이디어: "AI 의 '확신도'를 측정하자"

이 연구팀은 AI 가 답을 낼 때 가지는 **'확신도 (Confidence)'**를 검증에 포함시켰습니다.

• 새로운 기준:
  1. 이완된 강인성 (Relaxed Robustness): AI 가 틀렸지만, 확신이 매우 낮다면 (예: "아, 이거 말인지 사슴인지 모르겠는데...") 그건 '안전한 실수'로 간주합니다.
  2. 강한 강인성 (Strong Robustness): AI 가 답은 맞췄지만, 확신이 급격히 떨어졌다면 (예: 원래 99% 확신이었다가 30% 로 뚝 떨어짐) 그건 '위험한 신호'로 간주합니다.
  3. Top-k 강인성: 1 등만 중요한 게 아니라, 1 등, 2 등, 3 등 후보군 자체가 흔들리지 않는지 확인합니다.

3. 기술적 난제: "복잡한 규칙을 AI 에게 직접 가르치기엔 너무 어려워"

이런 '확신도'를 포함한 복잡한 규칙을 검증하려면, AI 가 수학적으로 매우 복잡한 계산 (소프트맥스 함수 등) 을 해야 합니다. 하지만 기존 검증 도구들은 이런 복잡한 수학식을 직접 처리하기가 매우 어렵거나, 도구를 뜯어고쳐야만 했습니다.

• 비유: AI 는 '수학 천재'지만, '복잡한 문장'을 직접 해석하는 능력은 부족합니다. 검증 도구들은 '단순한 산수'만 잘 봅니다. 우리가 "AI 가 확신이 낮으면 괜찮아"라는 복잡한 문장을 주면, 검증 도구는 "이게 뭐야? 못 해!"라고 외칩니다.

4. 이 논문의 해결책: "AI 에게 '보조 기계'를 달아주자"

저자들은 아주 창의적인 해결책을 제시했습니다. 검증 도구를 뜯어고칠 필요 없이, AI 모델 자체에 '보조 레이어 (추가된 층)'를 몇 개 덧붙이는 것입니다.

• 비유:
  • 기존 방식: 복잡한 문장을 해석할 수 있도록 AI(수학 천재) 의 머리를 수술해서 고치려 했습니다. (매우 위험하고 어렵습니다.)
  • 이 논문의 방식: AI 옆에 **'번역가 (보조 레이어)'**를 앉힙니다.
    • 검증 도구가 원하는 복잡한 규칙 (확신도 포함) 을 먼저 이 '번역가'가 해석합니다.
    • 번역가는 그 규칙을 AI 가 이해할 수 있는 아주 단순한 신호 (예: "0 보다 크면 OK") 로 바꿔서 AI 에게 전달합니다.
    • AI 는 그 단순한 신호만 보고 판단하면 되므로, 기존 검증 도구들도 아무 문제없이 작동합니다.

이 '번역가'는 **ReLU(활성화 함수)**라는 간단한 도구를 이용해 논리 연산 (AND, OR 등) 을 수행합니다. 마치 레고 블록을 조립하듯 복잡한 규칙을 AI 의 구조 안에 자연스럽게 녹여낸 것입니다.

5. 실험 결과: "기존 방식보다 훨씬 빠르고 정확해"

저자들은 8,870 개의 다양한 테스트 (MNIST, CIFAR-10, 교통 표지판 인식 등) 에서 이 방법을 검증했습니다.

• 결과:
  • 기존에 복잡한 규칙을 직접 코딩해서 검증하던 방식보다 훨씬 빠르고 효율적이었습니다.
  • 특히, 가장 강력한 검증 도구인 'αβ-CROWN'과 이 방법을 결합했을 때, 거대한 AI 모델 (파라미터 1 억 3 천만 개!) 도 빠르게 검증할 수 있었습니다.
  • 실제 사례: 어떤 AI 는 이미지를 잘못 분류했지만 확신이 20% 밖에 안 됐습니다. 기존 방식은 "위험하다!"고 했지만, 이 방식은 "확신이 낮으니 괜찮다"고 판단하여 불필요한 경보를 줄였습니다.

요약

이 논문은 **"AI 가 틀렸을 때, 그 실수가 얼마나 심각한지 '확신도'라는 기준으로 판단하는 새로운 언어 (문법)"**를 만들었습니다. 그리고 그 복잡한 언어를 AI 가 이해할 수 있도록 AI 옆에 '번역가 (추가 레이어)'를 붙여주는 지혜로운 방법을 제시했습니다.

이 덕분에 우리는 AI 가 안전할 때를 더 정확하게 알 수 있게 되었고, 불필요하게 AI 를 의심하거나 폐기하는 일을 줄일 수 있게 되었습니다. 마치 운전자가 "이 길은 비가 와서 시야가 안 좋으니 천천히 가자"라고 판단할 때, 그냥 "이 차는 위험하다"고 차를 버리는 대신, 상황에 맞는 적절한 조치를 취할 수 있게 된 것과 같습니다.

기술 요약

이 논문은 신경망의 강건성 (Robustness) 검증에 있어 기존 연구들이 간과해 온 신뢰도 (Confidence) 요소를 통합적으로 다루기 위한 포괄적인 프레임워크를 제안합니다. 입력 데이터의 미세한 교란 (perturbation) 에 대한 출력의 불변성을 확인하는 기존 강건성 검증과 달리, 본 논문은 분류 결과에 대한 신경망의 신뢰도 (Softmax 확률) 를 명시적으로 고려한 다양한 강건성 변형들을 정의하고, 이를 효율적으로 검증할 수 있는 새로운 방법을 제시합니다.

다음은 논문의 주요 내용을 기술적으로 요약한 것입니다.

---

1. 문제 정의 (Problem Statement)

• 기존 강건성 검증의 한계: 기존의 신경망 강건성 검증 연구는 주로 입력의 작은 변화가 분류 레이블 (Class Label) 을 변경하는지 여부 (이진 분류) 에만 초점을 맞추었습니다. 그러나 분류 레이블이 변경되지 않더라도, 신뢰도가 급격히 떨어지는 경우나 낮은 신뢰도로 잘못된 분류가 발생하는 경우를 무시하는 문제가 있었습니다.
• 다양한 강건성 요구사항: 실제 안전 임계 (Safety-critical) 응용 분야에서는 다양한 강건성 정의가 필요합니다.
  • 완화된 강건성 (Relaxed Robustness): 낮은 신뢰도를 가진 오분류는 허용할 수 있는가?
  • 강한 강건성 (Strong Robustness): 레이블은 유지되더라도 신뢰도가 임계값 이하로 떨어지면 취약한 것으로 간주해야 하는가?
  • Top-k 강건성: Top-k 예측 집합이 교란 하에서 유지되어야 하는가?
  • 부드러움 (Smoothness): 입력 교란에 따른 신뢰도 변화의 폭을 제한해야 하는가?
• 검증 도구의 제약: 이러한 복잡한 신뢰도 기반 속성 (Confidence-based properties) 은 비선형 함수 (Softmax) 와 복잡한 논리 조합 (Boolean combinations) 을 포함합니다. 기존 검증 도구 (VNN-COMP 표준인 vnnlib 등) 는 주로 단순한 선형 제약이나 간단한 논리 연산에 최적화되어 있어, 복잡한 속성을 직접 검증하거나 커스텀 코드를 수정하는 데 큰 어려움이 있었습니다.

2. 방법론 (Methodology)

저자들은 신뢰도 기반 명세를 포착하는 문법 (Grammar) 을 정의하고, 이를 신경망 검증 도구와 호환되도록 변환하는 층 추가 (Layer Addition) 기법을 제안합니다.

2.1 신뢰도 기반 문법 및 Softmax 근사

• 문법 정의: 선형 표현식 (Linear Expressions) 과 신뢰도 제약 (Confidence Constraints, $Conf(\bar{y}, t) \bowtie b$) 의 부울 조합으로 구성된 포스트 컨디션 (Post-condition) 문법을 정의했습니다.
• Softmax 근사: 신뢰도 계산에 사용되는 Softmax 함수는 지수 함수를 포함하여 비선형성이 강합니다. 이를 검증 도구에서 처리 가능한 선형 유리수 산술 (LRA, Linear Real Arithmetic) 제약으로 근사화했습니다.
  • $Conf(\bar{y}, t) < b$와 같은 조건을, 주어진 클래스 $t$의 로짓 (logit) 값 $y_t$와 두 번째로 큰 로짓 값 $y_{t'}$ 사이의 차이 ($\delta$) 를 이용한 선형 부등식 ($y_t < y_{t'} + \delta$) 으로 변환했습니다.
  • 이 근사는 오차에 대한 형식적 보장 (Formal guarantees) 을 제공하며, 사용자가 설정한 신뢰도 임계값에 따라 오차 범위를 조절할 수 있습니다.

2.2 추가 층을 통한 인코딩 (Encoding via Additional Layers)

• 핵심 아이디어: 복잡한 부울 논리 (AND, OR, NOT 등) 와 선형 제약이 섞인 포스트 컨디션을 검증 도구가 처리할 수 있는 단순한 형태 ($y \ge 0$ 또는 $y > 0$) 로 변환하기 위해, 기존 신경망의 출력 뒤에 몇 개의 추가 층 (Layers) 을 연결하는 기법을 개발했습니다.
• 작동 원리:
  • ReLU 활용: ReLU 활성화 함수를 사용하여 논리 연산을 모델링합니다. (예: 입력이 모두 음수일 때 출력 0, 하나라도 양수일 때 양수 출력 등을 통해 AND/OR 논리 구현).
  • Flip 연산: AND 와 OR 연산의 입력 신호 해석 방식이 반대이므로, 신호의 부호를 반전시키는 flip 연산을 도입하여 논리 연산들을 계층적으로 조합합니다.
  • 결과: 복잡한 속성 $Q$를 만족하는지 여부는, 변환된 신경망 $N'$의 최종 출력 $y$가 특정 임계값 ($\eta$) 보다 작은지/큰지 확인하는 단순한 검증 쿼리로 바뀝니다.
• 장점: 이 방식은 검증 도구 (Verifier) 의 소스 코드를 수정할 필요 없이, 검증 도구를 블랙박스 (Black-box) 로 사용할 수 있게 합니다. 따라서 $\alpha\beta$-CROWN, PyRAT 등 최신 검증 도구들을 즉시 활용할 수 있습니다.

3. 주요 기여 (Key Contributions)

1. 일반화된 신뢰도 문법: 기존 문헌의 다양한 강건성 정의 (완화된, 강한, Top-k, 부드러움 등) 를 포괄하는 통일된 문법을 제시했습니다.
2. 새로운 강건성 개념 정의: 신뢰도 임계값을 기반으로 낮은 신뢰도의 오분류를 허용하는 '완화된 강건성'과 신뢰도 급감을 감지하는 '강한 강건성' 등을 공식적으로 정의하고 검증 가능한 형태로 만들었습니다.
3. Softmax 근사 및 형식적 보장: Softmax 함수를 선형 제약으로 근사화하는 알고리즘을 제안하고, 이 과정에서 발생하는 오차에 대한 하한/상한을 수학적으로 증명했습니다.
4. 범용 검증 기술 (Layer-based Encoding): 복잡한 속성을 신경망의 추가 층으로 변환하는 기술을 개발하여, 기존 검증 도구 (특히 $\alpha\beta$-CROWN) 를 활용한 효율적인 검증을 가능하게 했습니다.
5. 광범위한 실험 평가: MNIST, CIFAR-10, GTSRB, ImageNet 등 다양한 데이터셋과 8,870 개의 벤치마크 (최대 138M 파라미터, 13.16M 활성화 단위) 를 대상으로 실험을 수행했습니다.

4. 실험 결과 (Results)

• 성능 비교: 제안된 '층 기반 인코딩 (Layer-based encoding)' 방식은 기존에 속성을 직접 제약으로 인코딩하는 'Ad-hoc' 방식 (Marabou 솔버 사용) 보다 압도적으로 우수한 성능을 보였습니다.
• 검증 도구 활용: 제안된 기법을 통해 VNN-COMP 에서 1 위를 차지한 $\alpha\beta$-CROWN 을 복잡한 신뢰도 기반 속성 검증에 적용할 수 있었습니다. $\alpha\beta$-CROWN 은 PGD 공격 및 CROWN 기법을 활용하여 Marabou 보다 훨씬 빠르고 정확하게 검증했습니다.
• 확장성: 138M 파라미터 규모의 대규모 네트워크 (VGGNet-16) 에서도 성공적으로 검증이 이루어졌으며, 다양한 신뢰도 임계값 ($\tau$) 에 따라 검증 결과 (Safe/Unsafe/Timeout) 가 논리적으로 일관되게 변화하는 것을 확인했습니다.
• 특이 발견: GTSRB(교통 표지판) 데이터셋의 경우, 시드 이미지와 교란 이미지의 신뢰도가 모두 100% 에 가까워 신뢰도 기반 검증이 취약점을 드러내는 중요한 사례를 보여주었습니다.

5. 의의 및 결론 (Significance)

이 논문은 신경망 검증 분야에서 신뢰도 (Confidence) 를 핵심 요소로 통합하여, 단순한 분류 오류를 넘어 신뢰할 수 없는 결정까지 포착할 수 있는 새로운 패러다임을 제시했습니다.

• 실용성: 검증 도구의 코드를 수정하지 않고도 복잡한 속성을 검증할 수 있게 함으로써, 연구자와 실무자가 다양한 안전 기준을 쉽게 적용할 수 있습니다.
• 이론적 엄밀성: Softmax 근사에 대한 오차 분석과 층 추가 변환의 정확성을 수학적으로 증명하여, 형식적 검증의 신뢰도를 높였습니다.
• 미래 방향: 자율 주행, 의료 진단 등 안전이 최우선인 분야에서 신경망의 결정을 단순히 '맞다/틀리다'가 아닌 '얼마나 확신하는가'의 관점에서 검증할 수 있는 토대를 마련했습니다.

결론적으로, 이 연구는 신경망의 강건성을 다차원적으로 평가할 수 있는 강력한 프레임워크를 제공하며, 기존 검증 도구들의 한계를 극복하고 더 정교한 안전 보장을 가능하게 합니다.