リラクゼーションのコスト：凸型ニューラルネットワーク検証における誤差の評価

要旨: 多くのニューラルネットワーク（NN）検証システムでは、ネットワークの入出力関係を制約プログラムとして表現する。健全性かつ完全性のある表現では、活性化をシミュレートするために整数制約が用いられる。近年の研究では、整数制約を凸（convex）に緩和することで、健全性を犠牲にしつつ性能が向上することが示されている。凸緩和は、元のネットワークによって到達不能な出力を考慮してしまう。本研究では、元のネットワークとその凸緩和の間における最悪の場合の発散（divergence）を、定性的および定量的に調べる。緩和の空間は格子（lattice）を形成し、その上端の要素は、すべてのニューロンを線形化した完全な緩和に対応する。下端の要素は元のネットワークに対応する。完全に緩和された出力と元の出力の間の l_infty-距離について、解析的な上界および下界を与える。この距離は、ネットワークの深さに関して指数的に増大し、入力の半径に関して線形に増大する。誤分類確率は、入力半径に関して段階的（step-like）な振る舞いを示す。我々の結果は、MNIST、Fashion MNIST、ならびにランダムネットワークに対する実験によって裏づけられる。