Precise Verification of Transformers through ReLU-Catalyzed Abstraction Refinement

기술 요약: ReLU 촉매 추상화 정제를 통한 트랜스포머의 정밀 검증

문제 제기
트랜스포머 모델이 자율 주행 및 의료와 같은 안전-중요 응용 분야에 배포됨에 따라, 트랜스포머 모델의 형식적 검증이 중요해졌습니다. 그러나 트랜스포머를 검증하는 것은 추론 계산의 높은 복잡성, 특히 자기-주의 (self-attention) 계층 내의 내적 (dot products) 으로 인해 기존 순방향 피드포워드 신경망 (FFNN) 을 검증하는 것보다 훨씬 더 어렵습니다. 기존 검증 방법은 출력 범위의 볼록한 과대근사 (convex over-approximations) 를 구성하기 위해 추상 해석에 의존합니다. 이러한 접근법은 효율적이지만, 종종 "완전성 문제"로 고통받습니다. 즉, 과대근사가 상당한 오차를 유발하여 실제 출력은 강건성 속성을 위반하지 않음에도 불구하고 근사된 출력이 이를 위반하는 것으로 나타나는 빈번한 오경보 (false alarms) 를 초래합니다. 구체적으로, 현재 최첨단 방법들 (예: Shi et al. [23]) 은 내적에 대해 엄격하게 타당한 하지만 종종 최적이지 않은 경직된 평면 경계 (rigid planar bounds) 를 사용하며, 이는 두 변수의 곱으로 형성된 쌍곡 포물면 (hyperbolic paraboloid) 을 엄격하게 경계 짓는 데 실패합니다.

방법론
저자들은 내적에 대한 여러 평면 경계를 융합하고 이를 ReLU 함수로 표현함으로써 정밀도를 향상시키는 새로운 검증 프레임워크인 BuFFeT(BoUnd Fusing-based reFinEment for Transformers) 를 제안합니다.

1. 이중 경계 구성: 이 논문은 이전 연구에서 사용된 표준 평면 경계 (식 4) 가 내적 ($z=xy$) 을 나타내는 쌍곡 포물면의 한쪽 면만을 커버한다는 점을 규명합니다. 저자들은 반대쪽 면을 커버하는 "이중" 평면 경계 (식 5) 를 유도합니다.
2. ReLU 기반 표현: 단순히 두 평면 경계의 최솟값을 취하는 것에서 비롯될 비선형 min/max 함수를 전파할 때 발생하는 지수적 복잡성을 피하기 위해, 저자들은 융합된 경계를 ReLU 함수를 사용하여 표현합니다. 구체적으로, 더 엄격한 상한선은 원래 경계에서 ReLU 항을 뺀 것으로, 더 엄격한 하한선은 원래 경계에 ReLU 항을 더한 것으로 구성됩니다 (식 8 및 9).
3. 추상화 정제 전략: 핵심 혁신은 이러한 ReLU 항의 선형 완화 (linear relaxation) 를 최적화하는 데 있습니다. ReLU 의 선형 하한은 기울기 $\alpha \in [0, 1]$로 매개변수화됩니다. 저자들은 최적의 $\alpha$를 결정하기 위해 고전적인 FFNN 검증에서 두 가지 전략을 확장합니다.
   • r-BuFFeT (규칙 기반): ReLU 의 입력 범위에 따라 $\alpha$(0 또는 1) 를 선택하여 과대근사의 면적을 최소화하는 [24] 의 휴리스틱을 적용합니다. 이는 본질적으로 특정 인스턴스에 대해 두 평면 경계 중 더 나은 것을 선택합니다.
   • o-BuFFeT (최적화 기반): $\alpha$를 최적화 문제의 결정 변수로 취급합니다. 검증 작업을 ReLU 경계에서 유도된 선형 제약 조건을 따르는 손실 함수 (음수 마진의 softplus) 를 최소화하는 문제로 공식화합니다. 현대의 경사 기반 솔버 (예: Adam) 를 사용하여 $\alpha$를 반복적으로 정제하여 강건성을 인증하는 해를 찾음으로써, 가능한 경계의 공간을 효과적으로 탐색합니다.

주요 기여

• 새로운 ReLU 활용: 이 논문은 ReLU 함수를 사용하여 내적에 대한 정밀한 비선형 경계를 표현하는 방법을 도입함으로써, 트랜스포머 검증과 고전적 신경망에서의 광범위한 ReLU 완화 문헌 간의 간극을 메웁니다.
• 이론적 통합: 저자들은 최첨단 접근법 [23] 에서 사용된 평면 경계와 그 이중 경계가 각각 $\alpha=0$과 $\alpha=1$에 해당하는 ReLU 기반 표현의 특정 사례임을 증명하여, 이러한 고정된 전략들이 종종 최적이지 않은 이유를 설명합니다.
• 두 가지 새로운 프레임워크: r-BuFFeT 와 o-BuFFeT 의 제안은 효율적이고 정밀한 검증을 위한 두 가지 명확한 경로를 제공하며, 최적화 기반 접근법은 강건성이 인증될 때까지 근사를 반복적으로 정제하는 메커니즘을 제공합니다.

실험 결과
저자들은 감정 분석 데이터셋 (SST 및 Yelp) 으로 훈련된 10 개의 트랜스포머 모델 (1 층에서 6 층까지의 표준 아키텍처 및 TinyBERT 포함) 에 대해 BuFFeT 를 평가했습니다. 평가는 최첨단 기준 [23] 에 대비하여 1,400 개의 검증 작업을 포함했습니다.

• 정밀도: 두 BuFFeT 접근법 모두 정밀도에서 상당한 개선을 보여주었습니다. 더 깊은 모델 (예: $N=6$) 의 경우, r-BuFFeT 는 최대 검증된 교란 ($\epsilon$) 을 기준 대비 최대 1.8 배 향상시켰으며, o-BuFFeT 는 최대 3.6 배의 개선을 달성했습니다. o-BuFFeT 는 특히 복잡한 모델에서 r-BuFFeT 를 일관되게 능가했습니다.
• 효율성: ReLU 입력 범위 계산으로 인해 r-BuFFeT 는 기준 대비 1.1 배에서 1.7 배의 modest 한 시간 오버헤드를 발생시켰습니다. o-BuFFeT 는 반복적 최적화 과정으로 인해 기준 대비 33 배에서 96 배의 더 높은 오버헤드를 도입했습니다. 그러나 저자들은 6 층 모델과 TinyBERT 에 대한 검증은 여전히 몇 분 내에 완료될 수 있으며, 오버헤드 비율은 모델 깊이에 관계없이 안정적으로 유지되었다고 지적합니다.
• 강건성: 기준이 강건성 검증에 실패한 경우 (음수 마진), o-BuFFeT 는 속성을 인증하기 위해 근사를 성공적으로 정제하여 오경보를 제거하는 능력을 입증했습니다.

의의 및 주장
이 논문은 BuFFeT 가 오경보로 이어지는 근사 오차를 줄여 트랜스포머 검증의 신뢰성을 크게 향상시킨다고 주장합니다. 주요 의의는 방법론적 가교에 있습니다. ReLU 표현을 활용함으로써 이 접근법은 고전적 신경망 검증에서 확립된 분석 기법을 트랜스포머의 고유한 도전 과제 (특히 자기-주의 내적) 에 적용할 수 있게 합니다. 저자들은 이 작업을 트랜스포머 검증에 대한 미래 연구의 길을 여는 것으로 위치시키며, ReLU 기반 정제의 사용이 다른 영역으로 확장되고 의미 있는 NLP 검증을 위해 기존 기법과 결합될 수 있음을 시사합니다. 이 작업은 모든 검증 과제를 해결한다고 주장하지는 않지만, 정밀도와 효율성 사이의 실용적인 균형을 제공하여 최첨단 수준을 크게 향상시킵니다.