A Tale of Two Approximations: Tightening Over-Approximation for DNN Robustness Verification via Under-Approximation

要約

ディープ ニューラル ネットワーク (DNN) の堅牢性は、ホスティング システムの信頼性とセキュリティにとって非常に重要です。
正式な検証は、証明可能な堅牢性の保証を提供するのに効果的であることが実証されています。
スケーラビリティを向上させるために、DNN の非線形活性化関数を線形制約によって過剰近似することが広く採用されており、これにより検証問題が効率的に解ける線形計画問題に変換されます。
過大近似による過大評価を減らすために、いわゆる最密近似を定義することに多くの努力が払われてきました。
この論文では、既存のアプローチを研究し、厳密な近似を定義する際の主要な要素、つまり活性化関数の近似領域を特定します。
近似領域で定義された厳密な近似は、実際の領域での近似ほど厳密ではない可能性があるにもかかわらず、既存のアプローチはすべて近似領域のみに依存していることがわかりました。
この観察に基づいて、活性化関数の過小評価領域を利用して厳密な近似限界を定義し、過剰近似を厳密化する新しい双対近似アプローチを提案します。
私たちは、それぞれモンテカルロ シミュレーションと勾配降下法に基づいた 2 つの相補的なアルゴリズムを使用してアプローチを DualApp と呼ばれるツールに実装します。
さまざまなアーキテクチャの DNN の包括的なベンチマークで評価します。
私たちの実験結果は、DualApp が最先端のアプローチを大幅に上回り、検証済みの堅牢性比で 100% ～ 1000% の改善、認定された下限で平均 10.64% (最大 66.53%) の改善を示していることを示しています。

要約(オリジナル)

The robustness of deep neural networks (DNNs) is crucial to the hosting system’s reliability and security. Formal verification has been demonstrated to be effective in providing provable robustness guarantees. To improve its scalability, over-approximating the non-linear activation functions in DNNs by linear constraints has been widely adopted, which transforms the verification problem into an efficiently solvable linear programming problem. Many efforts have been dedicated to defining the so-called tightest approximations to reduce overestimation imposed by over-approximation. In this paper, we study existing approaches and identify a dominant factor in defining tight approximation, namely the approximation domain of the activation function. We find out that tight approximations defined on approximation domains may not be as tight as the ones on their actual domains, yet existing approaches all rely only on approximation domains. Based on this observation, we propose a novel dual-approximation approach to tighten over-approximations, leveraging an activation function’s underestimated domain to define tight approximation bounds. We implement our approach with two complementary algorithms based respectively on Monte Carlo simulation and gradient descent into a tool called DualApp. We assess it on a comprehensive benchmark of DNNs with different architectures. Our experimental results show that DualApp significantly outperforms the state-of-the-art approaches with 100% – 1000% improvement on the verified robustness ratio and 10.64% on average (up to 66.53%) on the certified lower bound.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google