🤖 machine learning

Branch and Bound for Relational Verification of Neural Networks

이 논문은 이중 정식화 선택 전략을 기반으로 관계형 뉴런을 분할함으로써 효율성과 확장성을 개선하여 여러 벤치마크에서 기존 베이스라인들을 능가하는 관계형 신경망 검증을 위한 분기 한정 프레임워크인 SaBRe를 소개한다.

원저자: Kota Fukuda, Zhenya Zhang, Guanqin Zhang, Jianjun Zhao

게시일 2026-08-14

📖 3 분 읽기☕ 가벼운 읽기

CC BY 4.0

원저자: Kota Fukuda, Zhenya Zhang, Guanqin Zhang, Jianjun Zhao

원본 논문은 CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) 라이선스로 제공됩니다. ✨ 이것은 아래 논문에 대한 AI 생성 설명입니다. 저자가 작성하거나 승인한 것이 아닙니다. 기술적 정확성을 위해서는 원본 논문을 참조하세요. 전체 면책 조항 읽기

당신이 자율주행 자동차 함대의 안전 검사관이라고 상상해 보십시오. 이 자동차들은 "신경망"이라고 불리는, 일종의 초지능형 컴퓨터 뇌에 의해 구동됩니다. 이 뇌는 수백만 개의 사례를 관찰함으로써 정지 표지판이나 보행자 같은 것들을 인식하는 법을 배웁니다. 하지만 여기에는 함정이 있습니다. 이 뇌들은 지나치게 민감할 수 있다는 점입니다. 만약 정지 표지판에 아주 작은 스티커가 붙어 있거나 조명이 아주 조금만 변해도, 자동차는 갑자기 이를 속도 제한 표지판이라고 착각하여 그대로 질주해 버릴 수도 있습니다. 모두의 안전을 지키기 위해, 우리는 자동차의 뇌가 작은 변화에도 혼란을 느끼지 않을 것이라는 점을 증명해야 합니다. 이것을 "검증(verification)"이라고 부릅니다.

오랫동안 안전 검사관들은 자동차가 한 번에 하나의 특정 변화만을 감당할 수 있는지, 예를 들어 "내가 이미지에 아주 작은 점 하나를 추가해도 자동차가 여전히 정지 표지판을 볼 수 있을까?"와 같은 것들만을 확인해 왔습니다. 하지만 현실 세계에서 우리는 훨씬 더 큰 문제를 다뤄야 합니다: "날씨가 어떤 상황이든, 혹은 도로가 약간 젖어 있든 간에 자동차가 일관되게 행동할 것인가?" 이것이 바로 "관계적 검증(relational verification)"입니다. 즉, "두 개의 약간 다른 시나리오에서 운전했을 때, 자동차가 두 경우 모두 동일하게 안전한 결정을 내릴 것인가?"라고 묻는 것입니다. 문제는 두 개의 시나리오를 동시에 확인하는 것이 한 번에 하나를 확인하는 것보다 수학적으로 훨씬 더 어렵다는 점입니다. 이는 마치 하나의 접시를 돌리는 대신 두 개의 회전하는 접시를 동시에 균형 잡으려는 것과 같습니다. 기존의 도구들은 실제로는 위험이 없는데도 "위험!"이라고 비명을 지르며 혼란스러워하거나, 혹은 실제 위험을 놓치기도 합니다.

이 논문은 이 까다로운 균형 잡기 문제를 해결하기 위한 새로운 도구인 SABRE(Splitting Approximated Bounds for RElational verification)를 소개합니다. 기존의 방식이 방을 정리할 때 양말을 한 번에 한 짝씩 줍는 것이라면, SABRE는 전략을 바꿉니다. 만약 방이 아주 크고 양말이 사방에 널려 있다면, 우리는 영원히 양말을 줍기만 하다가 구석에 있는 커다란 빨래 더미를 놓칠 수도 있습니다. 저자들은 "관계적" 문제(두 가지 시나리오를 동시에 확인하는 문제)의 세계에서는, 실제 지저 혹은 엉망인 부분은 개별적인 데이터 포인트(양말 한 짝)가 아니라 두 더미 사이의 차이라는 점을 깨달았습니다.

그래서 SABRE는 전략을 변경합니다. 두 더미 사이의 차이를 포착하여 그것을 나누는 방식입니다. 여러분에게 거의 동일한 두 개의 도시 지도가 있다고 상상해 보십시오. 기존의 방법은 두 지도상의 모든 거리 하나하나를 따로 확인하려 할 것입니다. 하지만 SABRE는 두 지도 사이의 미세한 차이점에 주목하고, 그 차이점을 바탕으로 문제를 분할합니다. 만약 두 지도가 특정 회전 구간에 대해 서로 다르게 나타난다면, SAB서 즉시 그 불일치 지점에 집중합니다.

연구진은 ACAS Xu(항공 교통 제어), MNIST, CIFAR, GTSRB(이미지 인식)와 같은 표준 데이터셋을 사용하여 817개의 다양한 안전 문제를 대상으로 이 새로운 방법을 테스트했습니다. 그 결과, SABRE가 이전의 최고 방법들보다 이 문제들을 훨씬 더 잘 해결한다는 것을 발견했습니다. 실제로 SABRE는 훨씬 더 많은 문제를 해결했으며, 더 빠르게 수행했습니다. 예를 들어, ACAS Xu 데이터셋에서 기존 방법이 42개의 문제를 해결할 때 SABRE는 67개의 문제를 해결했습니다. GTSRB 데이터셋에서는 기존 방법이 9개를 해결한 것에 비해 SABRE는 33개를 해결했습니다.

결정적으로, 이 논문은 문제를 나누는 기존의 방식—신경망의 개별 부분에 집중하는 방식—이 이러한 "두 가지를 동시에" 체크하는 작업에서는 종종 잘못된 선택이라는 점을 주장합니다. 두 시나리오 사이의 관계에 집중함으로써, SABRE는 훨씬 더 효율적으로 혼란을 뚫고 나갑니다. 또한 저자들은 SABRE가 다음에 어떤 차이점을 분할할지 결정할 수 있도록 돕는 스마트한 "선택기(selector)"를 설계했습니다. 이는 마치 미스터리를 가장 빠르게 풀기 위해 정확히 어떤 단서를 따라가야 할지 아는 탐정과 같습니다. 이 스마트한 선택기를 무작위로 추측하는 모델과 비교 테스트했을 때, 스마트한 선택기가 훨씬 더 많은 문제를 해결했다는 점은 '무엇을' 분할할지 아는 것이 '어떻게' 분할하는지만큼 중요하다는 것을 입증했습니다.

요약하자면, 이 논문은 문제를 쪼개는 방식—시나리오 자체보다는 두 시나리오 사이의 관계에 집중하는 방식—을 바꿈으로써, 자율주행 자동차와 같은 AI 시스템을 훨씬 더 안전하고 검증하기 쉽게 만들 수 있음을 시사합니다. 이 방법이 세상의 모든 문제를 아직 다 해결한 것은 아니지만, 기존보다 훨씬 더 나은 명확한 길을 보여주고 있습니다.

기술 요약: 신경망의 관계적 검증을 위한 분기 한정법 (SABRE)

문제 정의
본 논문은 관계적 사양(relational specifications), 특히 **전역적 강건성(global robustness)**에 대한 신경망 검증 문제를 다룹니다. 단일 입력에 대한 작은 섭동(perturbation) 하에서 네트워크 출력이 안정적으로 유지되는지를 보장하는 국소적 강건성과 달리, 전역적 강건성은 여러 네트워크 추론 사이의 관계를 추론할 것을 요구합니다. 형식적으로, 네트워크가 전역적으로 강건하다는 것은 유계된 거리 $\epsilon$ 내에 있는 임의의 두 입력에 대해, 그 출력값의 차이가 $\delta$ 이내로 제한됨을 의미합니다.

기존의 관계적 검증 방식은 주로 출력 간의 차이를 제한하기 위해 볼록 영역(convex domains)을 사용하는 사운드한 과대 근사(sound over-approximation) 기술(예: RaVeN)에 의존합니다. 이러한 방식은 효율적이지만, 근사의 느슨함으로 인해 본질적으로 불완전하며 허위 알람(false alarms)(가짜 반례)이 발생하기 쉽습니다. 분기 한정법(Branch and Bound, BaB)은 개별 뉴런을 분할하여 국소적 강건성 검증에서 근사를 정교화하는 데 사용되는 표준적인 기법이지만, 관계적 검증에 적용하는 사례는 제한적이었습니다. 이전의 시도들(예: RABBit)은 개별 뉴런을 분할하여 관계적 문제에 BaB를 적용했으나, 저자들은 이러한 방식이 관계적 제약의 특정 구조를 활용하지 못하고 최적화되지 않은 정교화를 초-래할 수 있다고 주장합니다.

방법론: SABRE 프레임워크
저자들은 관계적 검증을 위해 특별히 설계된 BaB 프레임워크인 SABRE(Splitting Approximated Bounds for RElational verification)를 제안합니다. 핵심 혁신은 분할 전략을 개별 뉴런에서 **관계적 뉴런(relational neurons)**으로 전환하는 데 있습니다.

관계적 뉴런 및 문제 분할:
- 이 프레임워크는 두 개의 병렬 네트워크 복사본 간의 추론 차이를 나타내는 관계적 뉴런( $\Delta y^{(i)}_j = y^{(i)}_j - \hat{y}^{(i)}_j$ )을 사용하여 네트워크 추론 간의 차이를 모델링합니다.
- 개별 뉴런의 활성화 상태(예: $x > 0$ 대 $x < 0$ )를 기준으로 분할하는 대신, SABRE는 관계적 뉴런의 입력 부호( $\Delta x^{(i)}_j \geq 0$ 대 $\Delta x^{(i)}_j \leq 0$ )를 기준으로 분할합니다.
- 이 접근 방식은 개별 구성 요소를 분할하는 것보다 출력 차이의 경계를 더 효과적으로 조여, 관계적 차이의 불확실성을 직접적으로 겨냥합니다.
Dual 기반 뉴런 선택 전략:
- BaB의 효율성을 결정하는 중요한 요소는 각 단계에서 어떤 뉴런을 분할할지 선택하는 것입니다. 하위 문제의 영향을 추정하기 위해 문제를 푸는 계산 비용을 피하기 위해, SABRE는 검증 문제의 라그랑주 쌍대(Lagrangian dual) 정식화를 채택합니다.
- 저자들은 목적 함수가 뉴런별 항들의 합으로 구성된 쌍대 문제를 도출합니다. 이 항들은 선형 완화(linear relaxation) 하에서 특정 뉴런이 최종 출력 경계에 기여하는 정도를 포착합니다.
- 특정 관계적 뉴런을 분할하는 것이 쌍대 목적 함수의 계수에 어떻게 영향을 미치는지 분석함으로써, SABRE는 하위 문제를 실제로 풀지 않고도 잠재적인 정교화(경계 조임) 정도를 효율적으로 추정할 수 있습니다. 알고리즘은 추정된 개선 효과를 최대화하는 관계적 뉴런을 선택합니다.
워크플로:
- 프로세스는 전역 강건성 속성을 확인하기 위해 근사 검증기(예: RaVeN)로부터 시작됩니다.
- 허위 알람이 감지되면, 알고리즘은 쌍대 기반 전략을 사용하여 관계적 뉴런을 선택합니다.
- 선택된 관계적 뉴런에 대한 제약 조건을 추가하여 문제를 두 개의 하위 문제로 분할합니다.
- 이 재귀적 과정은 모든 하위 문제가 검증되거나 실제 반례가 발견될 때까지 계속됩니다.

주요 기여

새로운 분할 전략: 본 논문은 개별 뉴런이 아닌 관계적 뉴런을 분할하는 것을 우선시하는 BaB 프레임워크를 도입하며, 이것이 관계적 사양의 근사 오차를 직접적으로 해결한다고 주장합니다.
Dual 기반 선택 휴리스틱: 저자들은 (국소적 강건성에서 사용되었던) 쌍대 정식화 접근 방식을 관계적 설정으로 확장하여, 가장 영향력 있는 관계적 뉴런을 선택하여 분할할 수 있도록 효율적이고 데이터 중심적인 가이드를 제공합니다.
SABRE 구현: 다양한 네트워크 아키텍처에 걸쳐 전역 강건성 속성을 처리할 수 있는 전략이 통합된 완전한 검증 프레임워크를 구현했습니다.

실험 결과
저자들은 ACAS Xu, MNIST-F, MNIST-C, CIFAR, GTSRB의 5개 데이터셋에 걸친 817개의 검증 인스턴스에 대해 SABRE를 평가했습니다. SABRE를 다음 모델들과 비교했습니다:

RaVeN: 정교화 과정이 없는 최첨단 근사 검증기.
ClasIS & DualIS: 개별 뉴런을 분할하는 BaB 변형 모델 (ClasIS는 표준 선택을 사용하며, DualIS는 제안된 쌍대 정식화를 사용하지만 개별 뉴런에 적용함).
RandRS: 무작위 뉴런 선택을 사용하는 SABRE의 변형.

주요 결과:

RaVeN 대비 성능: SABRE는 RaVeN이 검증할 수 없었던 근사치를 효과적으로 정교화함으로써 훨씬 더 많은 인스턴스를 해결하여 RaVeN보다 성능이 크게 향상되었습니다.
관계적 vs. 개별 분할: 대부분의 벤치마크(ACAS Xu, MNIST-F, MNIST-C, GTSRB)에서 SABRE(관계적 분할)는 개별 분할 방식(ClasIS, DualIS)보다 더 많은 인스턴스를 해결했고, 더 적은 하위 문제를 탐색했으며, 더 적은 시간이 소요되었습니다.
- 참고 (CIFAR): 작은 섭동 반경( $\epsilon$ )을 가진 CIFAR 데이터셋의 경우, 개별 분할 방식이 처음에 SABRE보다 우세했습니다. 저자들은 이를 CIFAR 모델 내의 불안정한 ReLU 수가 많아 관계적 분할의 국소적 영향력이 희석되었기 때문이라고 설명합니다. 그러나 $\epsilon$ 이 증가함에 따라 관계적 분할이 더 효과적이 되었습니다.
선택 전략: 쌍대 기반 선택 전략(SABRE)은 모든 데이터셋에서 무작위 선택(RandRS)보다 성능이 뛰어났으며, 많은 경우에서 하위 문제 수와 검증 시간을 약 50% 감소시켰습니다.
최대 검증 가능 섭동: SABRE는 다른 방법들이 아무것도 인증하지 못한 경우에도 비자명한 경계를 찾아내는 데 성공하며, 특히 ACAS Xu와 MNIST-F에서 베이스라인 방법들보다 일관되게 더 큰 섭동 영역( $\epsilon^*$ )을 인증했습니다.

의의 및 주장
본 논문은 관계적 뉴런을 분할하는 것이 개별 뉴런을 분할하는 것보다 전역 강건성 검증의 근사를 정교화하는 데 더 효과적인 전략임을 입증함으로써, SABRE가 관계적 검증의 중요한 진전임을 주장합니다. 저자들은 제안된 쌍대 기반 선택 전략이 분할 우선순위에 대한 신뢰할 수 있는 가이드를 제공하여 검증 효율성과 확장성을 개선한다고 강조합니다.

이 연구는 접근 방식이 (근사의 특성상) 여전히 불완전함을 보여주지만, 제안된 기술들이 분할당 정교화 정도를 극대화하여 안전 필수 사이버 물리 시스템(CPS)을 위한 형식 검증을 더욱 실용적으로 만든다는 점을 강조합니다. 저자들은 향 \후 연구에서 개별 분할과 관계적 분할 사이를 동적으로 전환하는 하이브리드 전략을 탐구할 수 있음을 언급하면서도, 현재의 독점적인 관계적 뉴런 집중 방식만으로도 테스트된 대부분의 벤치마크에서 우수한 성능을 낸다고 주장합니다.

유사한 논문