부분적 다중 뉴런 완화 (Partial Multi-Neuron Relaxation)를 이용한 신경망 검증

심층 신경망 (Deep Neural Networks)이 핵심 시스템에 통합되는 사례가 증가함에 따라, 그 동작에 대한 안전성 속성 (Safety Properties)을 공식적으로 보장하려는 이론적 및 실무적 관심이 높아지고 있습니다. 이를 달성하기 위해, 현대의 검증 알고리즘은 네트워크의 비선형 활성화 함수 (Non-linear Activation Functions)에 대한 선형 완화 (Linear Relaxations)를 계산하는 것에 의존합니다. 선형 완화에 대한 기존 접근 방식은 일반적으로 두 가지 범주 중 하나에 속합니다: 각 활성화 뉴런 (Activation Neuron)이 그 소스(Sources)의 관점에서 경계가 지정되는 단일 뉴런 완화 (Single-neuron Relaxation), 그리고 여러 활성화 뉴런과 그 소스를 포함하는 선형 경계 (Linear Bounds)를 계산하는 다중 뉴런 완화 (Multi-neuron Relaxation)입니다. 그러나 기존 방법들은 엄밀함 (Tightness)과 확장성 (Scalability) 사이의 균형을 맞추는 데 실패할 수 있습니다. 단일 뉴런 경계는 검증을 완료하는 데 필요한 충분히 엄밀한 경계를 도출하지 못할 수 있는 반면, 모든 활성화 뉴런에 대해 다중 뉴런 완화를 생성하는 것은 계산 비용이 많이 들기 때문입니다. 본 논문에서는 휴리스틱 (Heuristically)하게 선택된 소수의 뉴런 부분 집합에 대해서만 다중 뉴런 경계를 생성하는 부분적 다중 뉴런 완화 (Partial Multi-neuron Relaxation)를 특징으로 하는 절충안을 제시합니다. 이를 달성하기 위해, 우리는 뉴런 선택을 위한 기존의 분기 휴리스틱 (Branching Heuristics)과 다중 뉴런 경계를 위한 경계 초평면 (Bounding Hyper-planes) 최적화 방식을 기반으로 구축하였습니다. 우리는 제안된 방법을 Marabou 검증기 (Verifier) 내에 통합하였으며, 기존의 경계 강화 (Bound Tightening) 방법들과 비교하여 유리한 결과를 얻었습니다. 우리의 실험은 신경망 검증을 위한 우리 기술의 잠재력을 보여줍니다.