Learning Lookahead Lemmas for Neural Network Verification

기술 요약: 신경망 검증을 위한 룩어헤드 레마(Lookahead Lemmas) 학습

문제 정의
최첨단 신경망 검증기들은 비선형 활성화 함수(특히 ReLU)를 분할하여 하위 문제를 분석하는 분기 한정(branch-and-bound, BaB) 절차에 의존한다. 최근의 발전은 브랜칭 휴리스틱을 개선하고, 실행 불가능한 하위 문제로부터 불리언 컷(boolean cuts)을 도출하는 방식을 개선해 왔으나, 이러한 접근 방식들은 대체로 *반응적(reactive)*이다. 즉, 이미 탐색 과정에서 비용을 지불하여 얻은 정보를 활용할 뿐이다. 현대적인 SAT 솔버가 주기적으로 탐색을 일시 중단하여 선제적으로 새로운 정보를 도출하는 인프로세싱(inprocessing) 기법을 사용하는 것과 달리, 신경망 검증에는 이와 유사한 메커니즘이 결여되어 있다. 본 논문은 이러한 인프로세싱 기반의 선제적 정보 도출 메커니즘을 BaB 해결 루프에 통합하는 문제를 다룬다.

방법론
저자들은 **룩어헤드 절차(lookahead procedure)**의 변형에 의해 구동되는 인프로세싱 프레임워크를 제안한다. 이 프레근은 룩어헤드를 단순히 다음 브랜칭 변수를 선택하는 용도로만 사용하는 대신, 불안정한 ReLU의 단계(활성 또는 비활성)에 관한 새로운 논리적 레마(lemma)를 도출하는 데 사용한다.

핵심 방법론은 세 가지 구성 요소로 이루어진다:

1. 함축 그래프(Implication Graph) 구축:
   프레임워크는 노드가 불안정한 ReLU의 단계 고정($r_i$는 활성, $\neg r_i$는 비활성)을 나타내는 유향 함축 그래프 $G = (V, E)$를 구축한다.

   • 룩어헤드 프로브(Lookahead Probe): 각 불안정한 ReLU에 대해, 해당 ReLU를 활성 및 비활성 단계로 각각 고정하는 상황을 시뮬레이션한다. 제한된 예산 내의 경계 전파(DeepPoly를 사용한 Marabou 또는 $\alpha$-$\beta$-CROWN을 위한 단일 $\alpha$-CROWN 패스)가 수행된다.
   • 레마 도출(Lemma Derivation): 만약 특정 단계 고정이 실행 불가능(infeasibility)로 이어진다면, 그 보수(complement)를 **단위 레마(unit lemma)**로 기록한다. 만약 특정 단계 고정이 다른 불안정한 ReLU를 특정 단계로 강제한다면, 이진 함축(binary implication)($r_i \to r_j$)을 기록한다.
   • 헐 경계(Hull Bounds): 또한 두 단계 시뮬레이션으로부터 도출된 경계들의 헐(hull)을 취함으로써 더 타이트한 경계를 계산한다.

2. SAT 폐쇄(SAT Closure)를 통한 탐색 공간 프루닝:
   함축 그래프는 명제 공식 $\Sigma$로 취급된다. 임의의 BaB 노드에서 솔버는 $\Sigma \cup R$의 만족 가능성을 확인하며, 여기서 $R$은 현재 탐색 경로를 따라 확정된 단계 고정들을 나타낸다. 만약 이 합집합이 불만족(unsatisfiable)하다면, 추가적인 경계 전파나 분할 없이 해당 하위 문제를 즉시 프루닝한다.

3. 동적 업데이트 및 컷 비비피케이션(Cut Vivification):

   • 리프로빙(Reprobing): 탐색이 진행됨에 따라 더 많은 ReLU가 고정되고 탐색 공간이 좁아진다. 프레임워크는 특정 간격(새로운 브랜칭 결정이 강제되지 않고 확립된 단계의 집합이 증가했을 때)마다 제한된 쿼리에 대해 룩어헤드 절차를 다시 실행하도록 리프로빙을 트리거한다. 이를 통해 루트 노드에서는 증명할 수 없었던 새로운 사실들로 함축 그래프를 업데이트한다.
   • 컷 비비피케이션(Cut Vivification): 하위 문제가 UNSAT으로 판명되면, 표준 검증기들은 불리언 컷(예: BICCOS 또는 PICID)을 채굴한다. 프레임워크는 함축 그래프를 사용하여 이러한 컷을 **비비피케이션(vivify)**한다. 이는 함축 관계를 추적함으로써 컷에서 중복된 단계 고정을 식별하고 제거한다. 만약 어떤 컷이 그래프의 폐쇄에 대해 불만족스러운 것으로 밝혀지면, 프레임워크는 **불만족 핵심(unsatisfiable core)**을 추출한다(종종 컷을 크기 2 또는 단일 단위 레마로 축소함). 이렇게 단축된 컷은 다시 글로벌 문제와 함축 그래프에 추가되어 미래의 프루닝 성능을 강화한다.

주요 기여

• 인프로세싱 프레임워크: 본 논문은 신경망 검증을 위한 최초의 완전한 인프로세싱 프레임워크를 제안하며, 반응적인 정보 활용에서 선제적인 정보 도출로 패러다임을 전환한다.
• 룩어헤드 유도 레마: 룩어헤드 절차를 단순한 브랜칭 휴리스틱이 아닌, ReLU 단계 관계에 대한 동적 함축 그래프를 생성하는 용도로 적응시킨다.
• 기존 검증기와의 통합: 이 프레임워크는 두 가지 서로 다른 최첨단 검증기인 Marabou(SMT 기반, CPU)와 $\alpha$-$\beta$-CROWN(경계 전파 기반, GPU)에 구현되었다.
• 컷 강화: 함축 그래프를 사용하여 불리언 컷을 비비피케이션함으로써, 컷을 필수적인 불만족 핵심으로 효과적으로 단축하는 메커니즘을 도입한다.

실험 결과
프레임워크는 표준 벤치마크(Marabou의 경우 ACASXu, MNIST, SafeNLP; $\alpha$-$\beta$-CROWN의 경우 CIFAR 및 TinyImageNet)를 통해 평가되었다.

• 성능 향상: 프레임워크는 두 검증기 모두에서 성능을 향상시켰다. 구체적으로, 베이스라인 검증기 대비 최대 34% 더 많은 인스턴스를 UNSAT으로 증명했다.
• 효율성: 룩어헤드 프로빙 및 리프로빙 단계의 오버헤드는 미미했다. 예를 들어, SafeNLP에서 프로빙은 실제 실행 시간의 0.1% 미만을 차지했으며, MNIST에서도 피크 시 19.2%를 기록했으나, 순 이득인 추가적인 UNSAT 인스턴스 해결 수(35개 추가)가 그 비용을 상회했다.
• 강건성: 이 접근 방식은 모든 테스트 벤치마크에서 타임아웃 횟수와 평균 탐색 상태를 감소시켰다.

의의 및 주장
본 논문은 SAT 솔버의 인프로세싱과 유사한 선제적 정보 도출 메커니즘을 도입함으로써 신경망 검증의 중요한 공백을 메운다고 주장한다. 저자들은 자신의 접근 방식이 정보의 도출을 브랜칭 휴리스틱의 부산물이 아니라, 솔브 절차의 필수적인 부분으로 취급한다는 점을 강조한다.

결과는 룩어헤드를 활용하여 함축 그래프를 구축하는 것이 검증기가 탐색 공간을 더 효과적으로 프루닝하고 불리언 컷을 강화할 수 있음을 입증한다. 저자들은 현재 구현이 이진 함축과 단위 레마에 집중하고 있지만, 향후 연구에서는 전파 중복 클로즈(propagation-redundant clauses)를 도출하거나 선형 제약 조건으로 추론을 격상하는 방안을 탐구할 수 있다고 언급한다. 또한, 쿼리 간에 그래프를 유지하는 것이 점진적 검증(incremental verification)을 개선할 수 있다고 제안하지만, 이는 향후 연구 과제로 남겨두었다.