境界伝播法は、分岐限定法と組み合わせると、正確性、ロバスト性、安全性などの深層ニューラル ネットワークのプロパティを形式的に検証する最も効果的な方法の 1 つです。ただし、既存の作業では、従来のソルバーで広く受け入れられている切断面制約の一般的な形式を処理できません。これは、強化された凸緩和で検証器を強化するために重要です。この論文では、既存の境界伝播の定式化には現れない緩和された整数変数を含むものを含む、任意の切断面の制約を追加できるように境界伝播手順を一般化します。私たちの一般化された境界伝播法である GCP-CROWN は、境界伝播法の効率と GPU アクセラレーションの恩恵を受けながら、ニューラル ネットワークの検証に一般的な切断面法を適用する機会を開きます。ケーススタディとして、市販の混合整数計画法 (MIP) ソルバーによって生成された切断面の使用を調査します。 MIP ソルバーは、新しい定式化を使用して、境界伝搬ベースの検証器を強化するための高品質の切断面を生成できることがわかりました。分岐に焦点を当てた境界伝播手順と切断面に焦点を当てた MIP ソルバーは、さまざまな種類のハードウェア (GPU と CPU) を使用して並行して実行できるため、それらを組み合わせることで、強力な切断面を持つ多数の分岐をすばやく探索でき、強力な検証性能。実験は、私たちの方法が oval20 ベンチマークを完全に解決し、VNN-COMP 2021 の最高のツールと比較して oval21 ベンチマークで 2 倍のインスタンスを検証できる最初の検証者であることを示しています。幅広いベンチマーク。 GCP-CROWN は、VNN-COMP 2022 の勝者である α,\!β-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 α,\!β-CROWN verifier, the VNN-COMP 2022 winner. Code is available at http://PaperCode.cc/GCP-CROWN