FAME: Formal Abstract Minimal Explanation for Neural Networks

이 논문은 추상 해석과 LiRPA 기반 바운딩을 활용하여 대규모 신경망에서도 설명 크기를 줄이면서 확장 가능한 새로운 형태의 귀납적 설명인 FAME(Formal Abstract Minimal Explanation) 을 제안하고, 이를 통해 기존 방법 대비 설명 크기와 실행 시간 측면에서 일관된 개선을 달성했음을 보여줍니다.

핵심

이 논문은 **"FAME(Formal Abstract Minimal Explanation)"**이라는 새로운 기술을 소개합니다. 이 기술은 인공지능 (AI) 이 왜 특정 결정을 내렸는지, 그 이유를 가장 짧고 확실하게 설명해 주는 도구입니다.

기존의 AI 설명 기술은 너무 느리거나, 복잡한 AI 모델에는 적용하기 어려웠습니다. FAME 은 이 문제를 해결하여 대규모 AI 모델에서도 빠르고 정확하게 이유를 찾아낼 수 있게 해줍니다.

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

---

🕵️‍♂️ 비유: "수백 명의 합창단 중 진짜 목소리를 찾아내는 사건"

AI 가 이미지를 보고 "이건 고양이야!"라고 판단했다고 가정해 봅시다. 우리는 AI 가 정확히 어떤 부분 (고양이의 귀, 눈, 수염 등) 을 보고 그렇게 판단했는지 알고 싶습니다. 하지만 AI 는 수천 개의 픽셀 (화소) 을 동시에 보고 결정하기 때문에, 모든 픽셀을 하나씩 확인하는 건 마치 수백 명의 합창단에서 진짜 노래를 부른 사람만 찾아내는 것처럼 어렵고 시간이 오래 걸립니다.

1. 기존 기술의 문제점: "한 명씩 확인하는 고된 작업"

기존의 방법 (VERIX+ 등) 은 합창단원들을 한 명씩 불러내서 "너가 노래에 필수적이니?"라고 물어보는 방식이었습니다.

• 문제: 합창단원이 1,000 명이라면 1,000 번을 물어봐야 합니다.
• 결과: 시간이 너무 오래 걸리고, AI 모델이 크면 (이미지가 복잡하면) 아예 작업을 포기해야 할 정도로 느려집니다.

2. FAME 의 혁신: "한 번에 대거 추방하는 '집단 해고' 전략"

FAME 은 이 문제를 해결하기 위해 두 가지 똑똑한 전략을 사용합니다.

전략 A: "한 번에 여러 명을 의심하는 '집단 해고' (Abstract Batch Certificate)"
FAME 은 "너희 100 명은 노래에 전혀 영향을 안 줬을 거야. 너희는 다 나가!"라고 한 번에 여러 명을 의심합니다.

• 비유: 마치 경찰이 "이 구역의 100 명은 범인일 확률이 0% 라서 다 나가도 돼"라고 집단적으로 확인하는 것과 같습니다.
• 핵심: 기존에는 한 명씩 확인해야 했지만, FAME 은 수학적 증명 (리니어 Relaxation) 을 통해 한 번에 수십, 수백 명을 동시에 "무관하다"고 증명해냅니다. 이렇게 하면 불필요한 픽셀들을 순식간에 제거할 수 있습니다.

전략 B: "조금씩 좁혀가는 '수색 범위 축소' (Recursive Refinement)"
처음에 한 번에 너무 많은 사람을 쫓아내면, 실수로 진짜 범인 (필수적인 픽셀) 을 놓칠 수 있습니다. 그래서 FAME 은 다음과 같이 합니다.

1. 일단 의심스러운 100 명을 쫓아냅니다.
2. 남은 사람들로 범위를 좁힙니다.
3. 좁혀진 범위에서 다시 "이제 50 명은 나가도 돼"라고 확인합니다.
4. 이 과정을 반복하며 범위를 점점 좁혀가면서 진짜 필요한 사람 (픽셀) 만 남깁니다.

이 과정은 마치 수색대를 보내어 범위를 좁혀가는 탐정과 같습니다. 처음엔 넓은 지역을 빠르게 훑고, 점점 좁은 구역으로 들어가서 정밀 수색을 하는 방식입니다.

3. 최종 결과: "최소한의 증거로 확실한 결론"

FAME 은 이렇게 불필요한 것들을 대거 제거한 후, 남은 것들이 정말 필요한지 마지막에 한 번 더 꼼꼼히 확인합니다.

• 결과: AI 가 "고양이"라고 판단한 이유를 설명할 때, 수천 개의 픽셀 중 정말 중요한 10~20 개만 골라냅니다.
• 장점: 기존 방법보다 수십 배 빠르면서도, 설명의 길이는 훨씬 짧고 명확합니다.

---

💡 왜 이것이 중요한가요?

1. 신뢰성 (Trust): AI 가 왜 그런 결정을 내렸는지 수학적으로 확실하게 증명해 줍니다. "그냥 느낌"이 아니라 "이 픽셀들이 없으면 고양이라고 판단할 수 없다"는 것을 보여줍니다.
2. 확장성 (Scalability): 예전에는 복잡한 AI (예: 의료 영상 분석, 자율주행) 에는 설명을 해줄 수 없었습니다. 하지만 FAME 은 거대한 AI 모델에서도 빠르게 작동합니다.
3. 효율성: 불필요한 계산을 줄여서 에너지를 아끼고, 빠른 시간 안에 결과를 얻을 수 있습니다.

📝 한 줄 요약

FAME 은 AI 의 복잡한 두뇌 속에서, "정말 중요한 이유"만 골라내는 초고속 탐정입니다. 한 명씩 확인하는 대신, 한 번에 대거 불필요한 것을 제거하는 똑똑한 전략으로, 거대한 AI 모델에서도 빠르고 확실한 설명을 가능하게 합니다.

이 기술은 앞으로 AI 가 우리 삶에 더 깊게 들어올 때, 그 결정 과정을 투명하게 보여주고 신뢰를 얻는 데 큰 역할을 할 것입니다.

기술 요약

FAME: 신경망을 위한 공식적 추상 최소 설명 (Formal Abstract Minimal Explanation) 기술 요약

이 논문은 ICLR 2026 에 게재된 **"FAME (Formal Abstract Minimal Explanations)"**이라는 새로운 프레임워크를 제안합니다. FAME 은 추상 해석 (Abstract Interpretation) 을 기반으로 한 귀납적 설명 (Abductive Explanations) 의 새로운 클래스로, 대규모 신경망 (NN) 에도 확장 가능하면서도 설명의 크기를 줄이는 데 중점을 둡니다.

1. 문제 정의 (Problem)

신경망 기반 시스템의 의사결정 과정을 이해하는 것은 신뢰할 수 있는 AI 를 구축하는 데 필수적입니다. 기존에 제안된 공식적 XAI (Formal XAI) 방법론은 논리적 추론을 기반으로 수학적으로 증명 가능한 설명 (Abductive Explanations, AXp) 을 제공하지만, 다음과 같은 치명적인 한계가 있었습니다:

• 확장성 부족: 신경망의 크기가 커질수록 설명을 계산하는 데 필요한 계산 비용이 기하급수적으로 증가하여 대규모 모델에 적용하기 어렵습니다.
• 순차적 병목 현상 (Sequential Bottleneck): 기존 방법들 (예: VERIX+) 은 입력 특징 (feature) 을 하나씩 제거하거나 추가하는 순차적 탐색 (traversal order) 에 의존합니다. 이는 특징의 중요도를 미리 알 수 없는 상황에서 순서를 정해야 하는 순환적 의존성 문제를 일으키며, 병렬 처리가 어려워 실행 시간이 매우 길어집니다.
• 정확한 해의 계산 비용: 완전한 최소 설명 (True Minimal Explanation) 을 찾기 위한 정확한 검증기 (Exact Solvers, 예: Marabou) 는 GPU 가속을 활용하기 어렵고 대규모 모델에서는 계산이 불가능 (intractable) 해집니다.

2. 방법론 (Methodology)

FAME 은 순차적 병목 현상을 제거하고 GPU 기반의 병렬 처리를 활용하여 대규모 신경망에 적용 가능한 하이브리드 접근법을 제시합니다. 핵심 구성 요소는 다음과 같습니다.

2.1. 추상 배치 인증서 (Abstract Batch Certificate, $\Phi$)

기존의 이진 검증 (SAT/UNSAT) 은 여러 특징을 동시에 제거할 때 특징 간의 상호작용을 고려하지 못해 비안전 (unsound) 할 수 있습니다. FAME 은 **선형 완화 기반 섭동 분석 (LiRPA)**을 사용하여 추상 배치 인증서를 정의합니다.

• 이 인증서는 특정 특징 집합 $A$를 동시에 제거 (freeing) 했을 때, 모델의 출력이 여전히 속성 $P$를 만족하는지 수학적으로 보장합니다.
• 이를 통해 순차적 탐색 없이도 여러 특징을 동시에 제거할 수 있게 되어 병렬 처리가 가능해집니다.

2.2. 탐욕적 배치 제거 및 0/1 다차원 배낭 문제 (Greedy Batch Freeing & MKP)

최대 규모의 불필요한 특징 집합을 찾아내는 문제는 0/1 다차원 배낭 문제 (MKP) 로 모델링됩니다.

• 정확한 MILP 솔버를 사용하면 계산 비용이 너무 높으므로, FAME 은 탐욕적 휴리스틱 (Greedy Heuristic) 알고리즘을 사용합니다.
• 이 알고리즘은 모든 클래스에 대한 제약 조건을 위반할 가능성이 가장 낮은 특징을 순차적으로 선택하여 배치로 제거합니다. 이 과정은 GPU 에서 병렬로 계산 가능하여 매우 효율적입니다.

2.3. 순환적 추상 도메인 정제 (Recursive Abstract Domain Refinement)

단순한 배치 제거만으로는 충분하지 않을 수 있으므로, FAME 은 **카디널리티 제약 (Cardinality-constrained)**을 가진 새로운 섭동 도메인 ($\Omega_m$) 을 도입합니다.

• 동작 원리: 한 번에 $m$개의 특징만 변할 수 있도록 도메인을 제한합니다. 이 제한된 도메인에서 LiRPA 경계를 재계산하면 오버-추정 (over-approximation) 오차가 줄어들어 더 많은 특징을 제거할 수 있게 됩니다.
• 재귀적 과정: 이 과정을 반복하여 도메인을 점진적으로 축소하고, 제거된 특징 집합을 확장합니다. 이는 고정된 순서 (traversal order) 없이 동적으로 특징을 선택하는 적응형 추상화 메커니즘입니다.

2.4. 하이브리드 파이프라인 (Hybrid Pipeline)

FAME 은 두 단계로 구성된 파이프라인을 사용합니다:

1. 추상 가지치기 (Abstract Pruning): LiRPA 와 탐욕적 알고리즘을 사용하여 대규모의 불필요한 특징을 빠르게 제거하고 **추상 최소 설명 ($wAXp^A$)**을 생성합니다.
2. 정확한 정제 (Exact Refinement): 생성된 설명을 기반으로 VERIX+ 와 같은 정확한 검증기를 사용하여 최종적으로 **최소 설명 (Minimal Explanation)**을 보장합니다. 이 단계에서는 VERIX+ 를 가속화하기 위해 FAME 의 초기 결과를 시드 (seed) 로 사용합니다.

3. 주요 기여 (Key Contributions)

1. 공식적 추상 설명의 도입: 추상 해석에서 유래한 최초의 귀납적 설명 클래스를 제안하여 고차원 신경망 처리를 가능하게 했습니다.
2. 순차적 병목 현상 제거: 특징의 순차적 순서 (traversal order) 가 필요 없는 재귀적 정제 절차와 LiRPA 기반 인증서를 설계하여 병렬 처리를 가능하게 했습니다.
3. 증명 가능한 품질 보장: 추상 최소 설명과 실제 최소 설명 사이의 최악의 경우 거리 (worst-case gap) 를 측정하는 절차를 제안했습니다. 이는 적대적 공격 (Adversarial Attacks) 과 선택적 VERIX+ 정제 단계를 결합합니다.
4. 확장성 입증: 중간 규모부터 대규모 신경망 (ResNet-2B 등) 에서 기존 SOTA 인 VERIX+ 대비 설명 크기와 실행 시간 모두에서 일관된 개선을 보여주었습니다. 특히 CIFAR-10 의 ResNet 아키텍처에서 최초의 공식적 추상 귀납적 설명을 생성했습니다.

4. 실험 결과 (Results)

MNIST, GTSRB, CIFAR-10 (ResNet-2B) 데이터셋 및 모델에 대한 벤치마크 결과는 다음과 같습니다:

• 실행 시간 (Runtime): FAME 은 VERIX+ 대비 수 배에서 25 배까지 빠른 속도를 기록했습니다. 예를 들어, GTSRB-CNN 모델에서 VERIX+ 는 약 185 초가 걸린 반면, FAME 은 약 7.4 초 만에 설명을 생성했습니다.
• 설명 크기 (Explanation Size): FAME 은 VERIX+ 가 생성한 설명보다 더 작거나 동등한 크기의 설명을 생성했습니다. 특히 반복적 정제 (Iterative Refinement) 를 적용하면 설명 크기가 크게 감소했습니다 (예: MNIST-CNN 에서 36% 감소).
• 탐욕적 알고리즘 vs MILP: 단일 배치 제거 단계에서 탐욕적 휴리스틱은 최적의 MILP 솔버와 거의 동일한 설명 크기 (평균 9 개 미만의 특징 차이) 를 유지하면서 9 배에서 12 배 빠른 속도를 보여주었습니다.
• 대규모 모델 확장성: ResNet-2B (CIFAR-10) 와 같은 깊은 네트워크에서는 정확한 검증기가 메모리 부족이나 시간 초과로 실패했지만, FAME 은 성공적으로 실행되어 약 32 분 내에 설명을 생성했습니다.

5. 의의 및 결론 (Significance & Conclusion)

FAME 은 공식적 XAI 의 가장 큰 장벽인 확장성 문제를 해결하는 중요한 전환점이 됩니다.

• 실용성: GPU 가속과 병렬 처리를 활용하여 대규모 신경망에 대한 공식적 설명을 실용적으로 가능하게 했습니다.
• 하이브리드 전략의 효과: 빠르지만 불완전한 추상 해석 (LiRPA) 과 정확하지만 느린 검증기를 결합한 하이브리드 접근법이 최적의 성능 (속도 vs 정확도) 을 제공함을 입증했습니다.
• 미래 지향성: 이 프레임워크는 분류 작업뿐만 아니라 회귀, 이산 특징, 지역 안정성 등 다양한 머신러닝 응용 분야로 확장 가능하며, 추상 해석 기술의 발전과 함께 더 정밀한 설명을 제공할 수 있는 기반을 마련했습니다.

결론적으로, FAME 은 "형식적 보장 (Formal Guarantees)"과 "실제적 확장성 (Practical Scalability)" 사이의 간극을 메우는 핵심 기술로, 복잡한 신경망 모델의 신뢰성과 해석 가능성을 높이는 데 기여합니다.