General Cutting Planes for Bound-Propagation-Based Neural Network Verification

要約

境界伝播法は、branch and boundと組み合わせた場合、正しさ、ロバスト性、安全性といったディープニューラルネットワークの特性を形式的に検証する最も有効な方法の1つである。しかし、既存の作品は、従来のソルバーで広く受け入れられている切断面制約の一般的な形式を扱うことができず、凸の緩和を厳しくして検証器を強化するために重要である。本論文では、既存の境界伝播の定式化に現れない緩和された整数変数を含む任意の切断面制約を追加できるように、境界伝播の手順を一般化する。一般化された境界伝播法であるGCP-CROWNは、境界伝播法の効率性とGPUによる高速化の恩恵を受けながら、ニューラルネットワーク検証のための一般的な切断面法}を適用する機会を開くものである。ケーススタディとして、市販の混合整数計画法（MIP）ソルバーで生成された切断面の利用を調査しました。その結果、MIPソルバは、我々の新しい定式化を用いて、境界伝播に基づく検証器を強化するための高品質な切断面を生成できることがわかりました。分岐に着目した境界伝播法と切断面に着目したMIPソルバーは、異なる種類のハードウェア（GPUとCPU）を用いて並列に実行できるため、これらを組み合わせることで強力な切断面を持つ多数の分岐を迅速に探索し、高い検証性能を実現することができます。本手法は、VNN-COMP 2021のベストツールと比較して、oval20ベンチマークを完全に解き、oval21ベンチマークで2倍のインスタンスを検証できる最初の検証器であり、また幅広いベンチマークで最先端の検証器を顕著に上回ることを実験的に実証しています。GCP-CROWNは、VNN-COMP 2022の優勝者である$alpha$,$eta$-CROWN検証器の一部です。コードは http://PaperCode.cc/GCP-CROWN で入手できます。

要約(オリジナル)

Bound propagation methods, when combined with branch and bound, are among the most effective methods to formally verify properties of deep neural networks such as correctness, robustness, and safety. However, existing works cannot handle the general form of cutting plane constraints widely accepted in traditional solvers, which are crucial for strengthening verifiers with tightened convex relaxations. In this paper, we generalize the bound propagation procedure to allow the addition of arbitrary cutting plane constraints, including those involving relaxed integer variables that do not appear in existing bound propagation formulations. Our generalized bound propagation method, GCP-CROWN, opens up the opportunity to apply general cutting plane methods} for neural network verification while benefiting from the efficiency and GPU acceleration of bound propagation methods. As a case study, we investigate the use of cutting planes generated by off-the-shelf mixed integer programming (MIP) solver. We find that MIP solvers can generate high-quality cutting planes for strengthening bound-propagation-based verifiers using our new formulation. Since the branching-focused bound propagation procedure and the cutting-plane-focused MIP solver can run in parallel utilizing different types of hardware (GPUs and CPUs), their combination can quickly explore a large number of branches with strong cutting planes, leading to strong verification performance. Experiments demonstrate that our method is the first verifier that can completely solve the oval20 benchmark and verify twice as many instances on the oval21 benchmark compared to the best tool in VNN-COMP 2021, and also noticeably outperforms state-of-the-art verifiers on a wide range of benchmarks. GCP-CROWN is part of the $\alpha$,$\beta$-CROWN verifier, the VNN-COMP 2022 winner. Code is available at http://PaperCode.cc/GCP-CROWN

arxiv情報

提供元, 利用サービス

arxiv.jp, DeepL