Repair Instead of Retraining: A Constraint-Guided Framework for Neural Network Repair

기술 요약: 재학습 대신 수리: 신경망 수리를 위한 제약 조건 가이드 프레임워크

문제 정의
안전 필수 애플리케이션에 배포된 심층 신경망(DNN)은 적대적 섭동(adversarial perturbations)과 백도어 공격에 여전히 취약하다. 재학습이나 미세 조정(fine-tuning)이 이러한 문제를 완화할 수 있지만, 이러한 접근 방식은 계산 비용이 많이 들고, 이미 배포된 모델에 선택적으로 적용하기 어려우며, 관찰된 특정 결함 너머의 통제 불가능한 행동 드리프트(behavioral drift)를 유발할 위험이 있다. 기존의 수리 방법들은 제한된 해석 가능성을 가진 휴리스틱 탐색(그레이 박스)에 의존하거나, 확장성이 떨어지는 정형 건축적 변환 및 수동으로 지정된 폴리토프(polytope) 제약을 요구하는 (증명 가능한 방법들) 경우가 많다. 따라서 전체 재학습 없이 해석 가능성, 행동 충실도, 계산 비용 사이의 균형을 맞추는 사후(post-hoc) 수리 접근법이 필요하다.

방법론
저자들은 신경망 수리를 희소한 국소 파라미터 집합에 대한 논리 인지 최적화 문제로 다루는 구성 가능한 제약 가이드 프레임워크를 제안한다. 이 프레임워크는 네 가지 결합된 단계로 작동한다:

1. 결함 국소화 (Fault Localization): 시스템은 DeepSHAP을 사용하여 정상 입력과 적대적 입력 모두에 대한 뉴런 수준의 기여도 마스크(attribution masks)를 계산한다. 이는 "공격 전용(attack-only)" 뉴런—정상 입력 시에는 기여도가 낮지만 적대적 입력 시에는 높은 기여도를 보이는 뉴런—을 식별한다. 이 대조적 기여도는 희소한 결함 관련 가중치 집합을 국소화하는 신호 역할을 한다.
2. 수리 대상 선택 (Repair-Target Selection): 국소화된 뉴런을 기반으로 네트워크 파라미터 상에 희소한 이진 마스크($\Theta_S$)를 생성한다. 프레임워크는 다음의 설계 공간을 탐색한다:
   • 가중치 방향 (Weight Direction): 핵심 뉴런의 유입 가중치(incoming weights), 유출 가중치(outgoing weights), 또는 편향(biases)을 수정함.
   • 선택 정책 (Selection Policy): 백분위 임계값(예: 상위 5% 크기) 또는 무작위 고정 예산($k$)을 통해 가중치를 선택함.
3. 경로 제약 명세 (Path-Constraint Specification): 수리 의도는 concolic execution(PyCT를 통해)을 사용한 경로 수준 제약으로 인코딩된다.
   • 강한 제약 (Hard Constraints): 올바른 내부 분기 로직을 보존하기 위해 정상 트레이스(benign traces)로부터 도출됨.
   • 약한 제약 (Soft Constraints): 관찰된 결함 경로로부터 실행을 우회하도록 강제하기 위해 적대적 트레이스(adversarial traces)로부터 도출됨.
   • 대리 네트워크 (Surrogate Networks): 전체 규모의 네트워크를 Max-SMT 솔버로 인코딩하는 데 따르는 난해함을 해결하기 위해, 프레임워크는 두 가지 분석 대리 모델을 도입한다:
     • $N^\Delta_w$ (삼진 대리 모델): 비수리 가중치를 크기에 따라 $\{-1, 0, +1\}$로 매핑하여 공식 복잡도를 줄임.
     • $N^\Delta_i$ (활성화 게이트 대리 모델): 입력 활성화 크기에 따라 비수리 에지를 제거(pruning)함.
   • 결정적으로, 수리 가중치($\Theta_S$)는 모든 공식에서 정확한 심볼릭 미지수(exact symbolic unknowns)로 남는 반면, 비수리 구성 요소들은 단순화되거나 게이팅된다.
4. 제약 가이드 수리 및 검증 (Constraint-Guided Repair & Validation): 시스템은 후보 가중치 업데이트를 합성하기 위해 Z3를 사용하는 Top-K Max-SMT 문제를 해결한다. 후보들은 원래의 배포 네트워크 $N$에 대한 충실한 검증(faithful validation)(정확한 아핀 연산을 사용)을 통해 균형 잡힌 점수로 순위가 매겨지며, 이를 통해 보고된 지표가 대리 모델의 아티팩트가 아닌 실제 런타임 동작을 반영하도록 보장한다.

주요 기여

• 구성 가능한 논리 인지 프레임워크: DeepSHAP 국소화, concolic 경로 제약 추출, 삼진/활성화 게이트 대리 모델, 그리고 Max-SMT 최적화를 결합한 통합 파이프라인.
• 정형화된 수리 설계 공간: 저자들은 뉴런 소스(공격 전용 vs 교집합), 가중치 방향(유입, 유출, 편향), 그리고 열 단위 선택 정책 간의 상호작용을 명시적으로 규명하여, 단일한 "레시피"가 보편적으로 최적은 아님을 입증했다.
• 인코딩 시점의 엄격한 단순화: 공통 부분식 제거(common subexpression elimination), 부정 정규화(negation normalization), 표현 프루닝(expression pruning)과 같은 기법들이 수리 세만틱을 변경하지 않으면서도 concolic 제약을 Max-SMT에 적합하게 유지하도록 도입되었다.
• 대리 모델 공식화: $N^\Delta_w$와 $N^\Delta_i$의 도입을 통해, 수리 변수에 대해서는 정확한 심볼릭 표현을 유지하면서도 단순화된 모델 위에서 경로 제약을 수집할 수 있게 하였다.
• 충실한 검증 프로토콜: 제약 수집과 최종 성능 평가를 분리하여, 모든 정확도 및 공격 성공률(ASR)이 원래 네트워크 $N$에서 측정되도록 하는 엄격한 평가 방법을 제공한다.

실험 결과
프레임워크는 6개의 벤치마크(Fashion-MNIST, MNIST-BD, CIFAR-10, GTSRB, MNIST-6, ResNet18)에 대해 4,737회의 실행을 통해 평가되었다. 주요 결과는 다음과 같다:

• 백도어 벤치마크: Fashion-MNIST와 MNIST-BD에서 프레임워크는 거의 완전한 백도어 제거를 달성했다. 구체적으로, ASR이 98% 이상에서 8% 미만으로 급감했다(예: Fashion-MNIST에서 99.77% $\to$ 6.66%). 가장 효과적인 구성은 유출 가중치(outgoing weight) 수정과 **활성화 게이트 대리 모델($N^\Delta_i$)**을 사용한 것이었다.
• 적대적 벤치마크: 핵심적인 발견은 **편향 전용 수리(bias-only repair)**의 효능이었다. MNIST-6에서 편향 방향 수리는 ASR을 100%에서 5.81%로 낮추면서 클린 정확도를 100% 유지했다. ResNet18에서는 ASR을 85.51%에서 40.42%로 낮췄다. 이 방향은 이전에 탐구되지 않았던 영역이며, 유입 또는 유출 가중치에만 집중하는 방법론에서는 놓칠 수 있었던 부분이다.
• 확장성 한계: CIFAR-10과 GTSRB는 단일 레이어 수리 하에서 까다로운 것으로 나타났다. 부분적인 개선은 보였으나, GTSRB는 ASR 감소가 미미했는데, 이는 단일 레이어 제약이 복잡하고 분산된 결함에는 불충분하다는 '확장성-충실도(tractability-fidelity)' 트레이드오프를 보여준다.
• CARE와의 비교: 그레이 박스 방식인 CARE(인과 관계 기반 국소화 + PSO)와 비교했을 때, 제안된 프레임워크는 일반적으로 Fashion-MNIST와 MNIST-BD에서 더 낮은 ASR과 더 나은 클린 정확도 보존을 달성했으며, 실행 시간(wall-clock time)도 훨씬 짧았다(예: MNIST-BD에서 74.4초 vs 8,745초). 그러나 CARE는 GTSRB에서 완전한 백도어 제거를 달 수 있었는데, 이는 제안된 방법의 단일 레이어 범위가 특정 아키텍처에서는 한계가 될 수 있음을 시사한다.

의의 및 주장
본 논문은 효과적인 구성을 발견하기 위해서는 수리 설계 공간에 대한 체계적인 탐색이 필수적이며, 단일 휴리스틱이 모든 시나리오를 지배하지 않는다는 점을 주장한다. 저자들은 편향 방향 수리가 적대적 교정을 위한 중요한, 이전에 탐구되지 않은 옵션이며, 이러한 체계적 접근을 통해서만 발견될 수 있음을 강조한다.

본 연구는 휴리스틱 탐색과 정형 검증 사이의 중간 지점을 제시한다. 즉, 그레이 박스 방법보다 더 많은 해석 가능성과 논리적 제어를 제공하면서도, 건축적 변환이나 수동으로 지정된 폴리토프를 요구하지 않는다. 저자들은 자신의 프레임워크가 **제약 가이드 방식이지만 정형적으로 인증된 것은 아님(not formally certified)**을 겸허히 인정한다. 즉, Max-SMT를 사용하여 합성을 수행하지만, 최종 보장은 전체 입력 공간에 대한 정형 증명이 아닌, 실제 네트워크에 대한 충실한 검증에 의존하는 경험적 결과이다. 결과적으로 이 연구는 강력한 단순화(대리 모델에서의 큰 $\Delta$)가 솔버 시간을 줄여주지만, 적절히 조정되지 않으면 수리 가이드를 왜곡할 수 있다는 확장성-충실도 트레이드오프를 부각시킨다.