해결책 인식형 vs 전역 ReLU 선택: 부분 MILP가 DNN 검증을 위해 다시 등장하다

복잡한 사례를 처리하기 위해, 우리는 복잡성을 분해하는 전략을 재검토하여, 적은 수의 복잡한 BaB 호출 대신 많은 수의 작은 {\em 부분적} MILP 호출에 의존한다. 핵심 과제는 비용이 큰 이진 변수를 사용해 처리해야 할 매우 적지만 매우 중요한 ReLU들을 선정하는 것이다. 이전의 접근 방식은 이 측면에서 최적화되지 못했다. 이러한 중요한 ReLU 변수를 선정하기 위해, 우리는 새로운 {\em 해 인식형} ReLU 점수화 기법({\sf SAS})을 제안하며, 동시에 BaB-SR 및 BaB-FSB 분기 함수를 {\em 전역적} ReLU 점수화({\sf GS}) 함수로 적응시킨다. 이들 방법을 이론적으로도 실험적으로도 비교한 결과, {\sf SAS}가 이진 변수를 사용해 열어야 할 변수 집합을 보다 효율적으로 선정함을 확인할 수 있었다. 기존 방법 대비 {\sf SAS}는 동일한 정확도를 유지하면서도 이진 변수의 수를 약 6배 감소시켰다. {\em Hybrid MILP}에 구현된 이 기법은 먼저 짧은 타임아웃으로 α,β-CROWN을 실행하여 비교적 간단한 사례를 해결한 후, 부분적 MILP를 호출함으로써 매우 정확하면서도 효율적인 검증기로 구현된다. 이로 인해 결정되지 않은 사례의 수가 최대 40%까지 감소하며, 낮은 수준(8–15%)으로 유지되며, 200만 개의 가중치를 가진 비교적 큰 CNN에 대해서도 합리적인 실행 시간(평균 46초~417초)을 유지할 수 있다.