Using Z3 for Formal Modeling and Verification of FNN Global Robustness

要約

タイトル：Z3を使用したFNNグローバル頑健性の形式的モデリングと検証

要約：

・FNNはさまざまなタスクで注目すべき成功を収めているが、アドバーサルな例に対して脆弱であることがある。
・FNNのアドバーサル耐性を検証するためにいくつかの技術が開発されているが、ほとんどは単一のデータポイントの局所摂動近傍に対する頑健性検証に焦点を当てている。
・グローバル頑健性分析にはまだ大きな研究のギャップがある。
・DeepGlobalというグローバル頑健性検証可能なフレームワークが提案された。
・DeepGlobalはFNNのすべての可能なアドバーサル危険領域(ADR)を特定するために設計されており、テストセットのデータサンプルに限定されていない。
・本論文では、より明示的な定義のためにSMTソルバーZ3を利用したDeepGlobalの完全な仕様と実装を提案し、より効率的な検証のためにDeepGlobalのいくつかの改善を提案する。
・我々の実装と改善の効果を評価するために、ベンチマークデータセットの一連の実験を実施した。
・実験結果の可視化により、このアプローチの有効性が示された。

要約(オリジナル)

While Feedforward Neural Networks (FNNs) have achieved remarkable success in various tasks, they are vulnerable to adversarial examples. Several techniques have been developed to verify the adversarial robustness of FNNs, but most of them focus on robustness verification against the local perturbation neighborhood of a single data point. There is still a large research gap in global robustness analysis. The global-robustness verifiable framework DeepGlobal has been proposed to identify \textit{all} possible Adversarial Dangerous Regions (ADRs) of FNNs, not limited to data samples in a test set. In this paper, we propose a complete specification and implementation of DeepGlobal utilizing the SMT solver Z3 for more explicit definition, and propose several improvements to DeepGlobal for more efficient verification. To evaluate the effectiveness of our implementation and improvements, we conduct extensive experiments on a set of benchmark datasets. Visualization of our experiment results shows the validity and effectiveness of the approach.

arxiv情報

提供元, 利用サービス

arxiv.jp, OpenAI