Using Z3 for Formal Modeling and Verification of FNN Global Robustness

要約

タイトル：Z3を用いたFNNグローバルロバスト性の形式的モデリングと検証
要約：
– フィードフォワードニューラルネットワーク（FNN）は様々なタスクにおいて驚くべき成功を収めているが、敵対的例に対して脆弱である。
– FNNの敵対的な頑健性を確認するための様々な技術が開発されてきたが、ほとんどが単一のデータポイントの近傍の頑強性検証に焦点を当てている。
– グローバル頑健性分析にはまだ大きな研究の隙間がある。DeepGlobalというグローバル頑健性検証可能なフレームワークが提案されているが、テストセット内のデータサンプルに限定されず、FNNのすべての可能な敵対的危険領域（ADR）を特定することを目的としている。
– 本稿では、より明示的な定義のためにSMTソルバーZ3を利用した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