マルチニューロンリラクゼーションガイドによる完全検証と枝分かれ境界法

最先端のニューラルネットワーク検証器は、基本的に2つのパラダイムのうちの1つに基づいています: すべての検証問題を緊密なマルチニューロン凸リラクゼーションを介してエンコードするか、または多くの簡単なサブプロブレム上で不正確であるが高速な境界手法を利用する枝分かれ境界法（BaB）手続きを適用するかです。前者は複雑なマルチニューロン依存関係を捉えることができますが、凸リラクゼーションの固有の制限により完全性を犠牲にします。後者は完全な検証を可能にしますが、より大きく、より難しいネットワークでは次第に効果が薄れます。本研究では、両方のパラダイムの強みを組み合わせた新しい完全検証器を提示します: それはマルチニューロンリラクゼーションを活用して、BaBプロセス中に生成されるサブプロブレムの数を劇的に減少させ、残りの問題を解決するために効率的なGPUベースの二重最適化手法を使用します。広範な評価により、我々の検証器が確立されたベンチマークだけでなく、以前に考慮されたよりもかなり高い精度のネットワークで新しい最先端を達成することが示されています。この後者の結果（最大28%の認証向上）は、実際に関連するネットワークを扱える検証器の作成に向けた有意義な進展を示しています。