ソリューション認識型とグローバルなReLU選択：部分MILPがDNN検証において再び力を発揮する

複雑なケースを処理するため、複雑さを分解するための分割統治アプローチを再検討し、少数の複雑なBaB呼び出しに頼るのではなく、多数の小さな「部分的」MILP呼び出しに依存する。このアプローチの鍵となるのは、（高コストな）バイナリ変数を用いて処理すべき非常に少数ながら極めて重要なReLUノードを選択することである。従来のアプローチは、この点において最適でなかった。本研究では、これらの重要なReLU変数を効果的に選定するため、新たな「解に依存する」ReLUスコアリング手法（{\sf SAS}）を提案するとともに、BaB-SRおよびBaB-FSBのブランチング関数を「グローバル」なReLUスコアリング関数（{\sf GS}）として再定義する。これらを理論的・実験的に比較した結果、{\sf SAS}はバイナリ変数を用いて開くべき変数集合をより効率的に選定できることを示した。従来の手法と比較して、{\sf SAS}は同程度の精度を維持しつつ、バイナリ変数の数を約6倍削減した。この手法を「Hybrid MILP」に実装し、まず短時間のタイムアウトでα,β-CROWNを実行して容易なケースを解いた後、部分的MILPを適用することで、非常に高精度かつ効率的な検証器が得られた。これにより、未決定のケース数は最大で40％削減され、低水準（8〜15％）まで低下した一方で、200万パラメータを持つ比較的大規模なCNNに対しても、平均1インスタンスあたり46〜417秒という合理的な実行時間を維持した。