Formal Mechanistic Interpretability: Automated Circuit Discovery with Provable Guarantees

이 논문은 ICLR 2026에 발표된 "Formal Mechanistic Interpretability: Automated Circuit Discovery with Provable Guarantees"로, 신경망의 기계적 해석 가능성 (Mechanistic Interpretability, MI) 분야에서 공식적 검증 (Formal Verification) 기술을 활용하여 증명 가능한 보장을 가진 회로 (Circuit) 자동 발견을 제안합니다.

기존의 회로 발견 방법론이 휴리스틱이나 근사치에 의존하여 연속적인 입력 도메인에서 회로의 충실도 (Faithfulness) 를 보장하지 못한다는 한계를 극복하고, 신경망 검증 (Neural Network Verification) 의 최신 발전을 기반으로 한 새로운 프레임워크를 제시합니다.

아래는 논문의 상세 기술 요약입니다.

---

1. 문제 정의 (Problem)

기계적 해석 가능성의 핵심 과제 중 하나는 특정 행동을 유발하는 신경망 내의 하위 그래프인 '회로 (Circuit)'를 식별하는 것입니다. 그러나 기존 방법론들은 다음과 같은 심각한 한계를 가집니다:

• 휴리스틱 의존성: 대부분의 알고리즘은 샘플링 기반의 근사적 접근을 사용합니다.
• 보장 부재: 발견된 회로가 이산적인 데이터 포인트에서는 모델과 일치하더라도, 연속적인 입력 도메인 (Continuous Input Domain) 내의 미세한 교란 (Perturbation) 이 발생하면 회로의 충실도가 깨질 수 있습니다.
• 패칭 (Patching) 의 불안정성: 회로 외부의 활성화를 고정하는 패칭 과정에서 사용되는 값 (예: 0, 평균) 이 분포 밖 (Out-of-Distribution) 일 수 있으며, 연속적인 패칭 변화에 대해 회로의 안정성이 보장되지 않습니다.

이러한 한계는 안전성 (Safety) 과 관련된 응용 분야에서 치명적일 수 있으므로, 수학적 증명이 가능한 (Provable) 보장을 갖춘 회로 발견이 시급합니다.

2. 방법론 (Methodology)

저자들은 신경망 검증 도구 (특히 $\alpha$-$\beta$-CROWN) 를 활용하여 세 가지 핵심 보장을 제공하는 자동화 알고리즘을 제안합니다.

A. 증명 가능한 보장 (Provable Guarantees)

1. 입력 도메인 강건성 (Input Domain Robustness):
   • 회로가 특정 입력 점뿐만 아니라, 연속적인 입력 영역 (예: $\ell_p$-볼) 전체에서 원본 모델과 일치함을 보장합니다.
   • 시메스 (Siamese) 인코딩: 원본 모델 $G$와 회로 $C$를 공유 입력을 가진 하나의 결합 모델로 구성하여, 검증 도구를 통해 입력 변화에 따른 출력 차이를 공식적으로 증명합니다.
2. 패칭 도메인 강건성 (Patching Domain Robustness):
   • 회로 외부의 활성화 값을 고정된 상수가 아닌, 연속적인 입력 도메인에서 유도된 가능한 모든 활성화 값으로 대체했을 때도 회로가 충실함을 보장합니다.
   • 이중 시메스 인코딩: 원본 모델과 회로가 서로 다른 입력을 받되, 회로의 비회로 구성 요소 활성화가 원본 모델의 활성화 범위 내에서 임의의 값을 가질 수 있도록 설계하여 검증합니다.
3. 최소성 (Minimality):
   • 회로의 크기를 최소화하는 다양한 개념 (준-최소, 국소 최소, 부분집합 최소, 카디널 최소) 을 정의하고, 이를 달성하는 알고리즘을 제공합니다.

B. 알고리즘 및 이론적 연결

• 회로 단조성 (Circuit Monotonicity): 충실도 예측자 (Predicate) $\Phi$가 단조적일 때 (회로에 구성 요소를 추가해도 충실도가 깨지지 않음), 탐욕적 (Greedy) 알고리즘이 부분집합 최소 (Subset-Minimal) 회로로 수렴함을 증명합니다.
• 회로와 차단 집합 (Blocking-sets) 의 이중성:
  • 충실도를 깨뜨리는 최소한의 구성 요소 집합인 '차단 집합 (Blocking-set)'과 '회로' 사이의 이중성 (Duality) 을 규명했습니다.
  • 최소 히팅 집합 (Minimum Hitting Set, MHS) 문제를 활용하여, NP-완전 문제임에도 불구하고 현대 솔버 (MILP, MaxSAT) 를 통해 카디널 최소 (Cardinally-Minimal, 전역 최적) 회로를 효율적으로 근사하거나 정확히 찾을 수 있는 알고리즘 (Algorithm 2) 을 제안했습니다.

3. 주요 기여 (Key Contributions)

1. 이론적 기여:
   • 연속 도메인 전체에서 유효한 새로운 증명 가능한 보장 (입력/패칭 강건성, 다양한 최소성) 을 공식화했습니다.
   • 입력 강건성, 패칭 강건성, 최소성 보장 사이의 깊은 이론적 연결 (단조성, 이중성) 을 규명하여 알고리즘의 수렴 조건을 명확히 했습니다.
2. 알고리즘적 기여:
   • 신경망 검증을 기반으로 한 자동화 알고리즘을 개발하여, 샘플링 기반 방법론보다 훨씬 강력한 강건성을 가진 회로를 생성합니다.
   • 계산 비용과 달성되는 최소성 수준 사이의 트레이드오프를 조절할 수 있는 알고리즘 군 (Greedy, Binary Search, MHS 기반) 을 제시했습니다.
3. 실험적 기여:
   • MNIST, CIFAR-10, GTSRB, TaxiNet 등 다양한 비전 모델에서 상태-of-the-art(SOTA) 검증 도구인 $\alpha$-$\beta$-CROWN 을 사용하여 실험을 수행했습니다.

4. 실험 결과 (Results)

• 강건성 (Robustness):
  • 입력 강건성: 샘플링 기반 방법은 10~50% 정도의 강건성만 보인 반면, 제안된 증명 가능한 방법은 100% 의 강건성을 달성했습니다. (회로 크기는 유사하거나 약간 더 큼)
  • 패칭 강건성: 0 패칭 (Zero-patching) 이나 평균 패칭 (Mean-patching) 은 작은 교란에도 회로가 무너지는 반면, 증명 가능한 패칭 방법은 모든 연속적인 패칭 변화에 대해 100% 의 강건성을 보장했습니다.
• 최소성 (Minimality):
  • MHS 기반 알고리즘 (Algorithm 2) 은 이론적 하한선 (Lower Bound) 에 근접하거나 전역 최적의 최소 회로를 발견했습니다.
  • 단순한 탐욕적 알고리즘 (Algorithm 1) 은 국소 최소에 머무르는 경우가 많았으나, MHS 접근법은 더 작은 크기의 회로를 찾거나 그 한계를 명확히 보여주었습니다.
• 성능:
  • 증명 가능한 검증 과정으로 인해 샘플링 기반 방법보다 계산 시간이 길어졌으나 (예: CIFAR-10 에서 약 2900 초 vs 0.2 초), 얻어지는 신뢰성 (Reliability) 과 안전성 보장이 그 비용을 정당화함을 보여주었습니다.

5. 의의 및 결론 (Significance)

이 논문은 기계적 해석 가능성 분야에서 휴리스틱을 넘어선 엄밀한 수학적 기반을 마련했다는 점에서 의의가 큽니다.

• 안전성 보장: 자율 주행, 의료 진단 등 고위험 분야에서 신경망의 내부 작동 원리를 설명할 때, 작은 입력 변화에도 설명이 무너지지 않음을 수학적으로 증명할 수 있게 되었습니다.
• 이론과 실증의 통합: 신경망 검증 (Formal Verification) 과 기계적 해석 (Mechanistic Interpretability) 을 결합하여, 두 분야의 방법론적 발전을 상호 시너지 있게 이끌었습니다.
• 미래 연구 방향: 확장 가능한 검증 기술의 발전과 함께, 더 복잡한 모델 (Transformer 등) 에 대한 증명 가능한 회로 발견 연구의 토대를 제공했습니다.

요약하자면, 이 연구는 "신경망이 왜 특정 결정을 내리는가"에 대한 설명을 단순한 관찰이 아닌, 연속적인 환경 변화 하에서도 변하지 않는 '증명된 사실'로 만드는 획기적인 접근법을 제시합니다.