UR4NNV: Neural Network Verification, Under-approximation Reachability Works!
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , , , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2024
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866914649119653888 |
|---|---|
| author | Liang, Zhen Wu, Taoran Zhao, Ran Xue, Bai Wang, Ji Yang, Wenjing Deng, Shaojun Liu, Wanwei |
| author_facet | Liang, Zhen Wu, Taoran Zhao, Ran Xue, Bai Wang, Ji Yang, Wenjing Deng, Shaojun Liu, Wanwei |
| contents | Recently, formal verification of deep neural networks (DNNs) has garnered considerable attention, and over-approximation based methods have become popular due to their effectiveness and efficiency. However, these strategies face challenges in addressing the "unknown dilemma" concerning whether the exact output region or the introduced approximation error violates the property in question. To address this, this paper introduces the UR4NNV verification framework, which utilizes under-approximation reachability analysis for DNN verification for the first time. UR4NNV focuses on DNNs with Rectified Linear Unit (ReLU) activations and employs a binary tree branch-based under-approximation algorithm. In each epoch, UR4NNV under-approximates a sub-polytope of the reachable set and verifies this polytope against the given property. Through a trial-and-error approach, UR4NNV effectively falsifies DNN properties while providing confidence levels when reaching verification epoch bounds and failing falsifying properties. Experimental comparisons with existing verification methods demonstrate the effectiveness and efficiency of UR4NNV, significantly reducing the impact of the "unknown dilemma". |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2401_12550 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | UR4NNV: Neural Network Verification, Under-approximation Reachability Works! Liang, Zhen Wu, Taoran Zhao, Ran Xue, Bai Wang, Ji Yang, Wenjing Deng, Shaojun Liu, Wanwei Artificial Intelligence Machine Learning 68Q60, 68T07 D.2.4; I.2.0 Recently, formal verification of deep neural networks (DNNs) has garnered considerable attention, and over-approximation based methods have become popular due to their effectiveness and efficiency. However, these strategies face challenges in addressing the "unknown dilemma" concerning whether the exact output region or the introduced approximation error violates the property in question. To address this, this paper introduces the UR4NNV verification framework, which utilizes under-approximation reachability analysis for DNN verification for the first time. UR4NNV focuses on DNNs with Rectified Linear Unit (ReLU) activations and employs a binary tree branch-based under-approximation algorithm. In each epoch, UR4NNV under-approximates a sub-polytope of the reachable set and verifies this polytope against the given property. Through a trial-and-error approach, UR4NNV effectively falsifies DNN properties while providing confidence levels when reaching verification epoch bounds and failing falsifying properties. Experimental comparisons with existing verification methods demonstrate the effectiveness and efficiency of UR4NNV, significantly reducing the impact of the "unknown dilemma". |
| title | UR4NNV: Neural Network Verification, Under-approximation Reachability Works! |
| topic | Artificial Intelligence Machine Learning 68Q60, 68T07 D.2.4; I.2.0 |
| url | https://arxiv.org/abs/2401.12550 |