Bound Tightening using Rolling-Horizon Decomposition for Neural Network Verification
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2024
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866916185451266048 |
|---|---|
| author | Zhao, Haoruo Hijazi, Hassan Jones, Haydn Moore, Juston Tanneau, Mathieu Van Hentenryck, Pascal |
| author_facet | Zhao, Haoruo Hijazi, Hassan Jones, Haydn Moore, Juston Tanneau, Mathieu Van Hentenryck, Pascal |
| contents | Neural network verification aims at providing formal guarantees on the output of trained neural networks, to ensure their robustness against adversarial examples and enable their deployment in safety-critical applications. This paper introduces a new approach to neural network verification using a novel mixed-integer programming rolling-horizon decomposition method. The algorithm leverages the layered structure of neural networks, by employing optimization-based bound-tightening on smaller sub-graphs of the original network in a rolling-horizon fashion. This strategy strikes a balance between achieving tighter bounds and ensuring the tractability of the underlying mixed-integer programs. Extensive numerical experiments, conducted on instances from the VNN-COMP benchmark library, demonstrate that the proposed approach yields significantly improved bounds compared to existing effective bound propagation methods. Notably, the parallelizable nature of the proposed method proves effective in solving open verification problems. Our code is built and released as part of the open-source mathematical modeling tool Gravity (https://github.com/coin-or/Gravity), which is extended to support generic neural network models. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2401_05280 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Bound Tightening using Rolling-Horizon Decomposition for Neural Network Verification Zhao, Haoruo Hijazi, Hassan Jones, Haydn Moore, Juston Tanneau, Mathieu Van Hentenryck, Pascal Optimization and Control Neural network verification aims at providing formal guarantees on the output of trained neural networks, to ensure their robustness against adversarial examples and enable their deployment in safety-critical applications. This paper introduces a new approach to neural network verification using a novel mixed-integer programming rolling-horizon decomposition method. The algorithm leverages the layered structure of neural networks, by employing optimization-based bound-tightening on smaller sub-graphs of the original network in a rolling-horizon fashion. This strategy strikes a balance between achieving tighter bounds and ensuring the tractability of the underlying mixed-integer programs. Extensive numerical experiments, conducted on instances from the VNN-COMP benchmark library, demonstrate that the proposed approach yields significantly improved bounds compared to existing effective bound propagation methods. Notably, the parallelizable nature of the proposed method proves effective in solving open verification problems. Our code is built and released as part of the open-source mathematical modeling tool Gravity (https://github.com/coin-or/Gravity), which is extended to support generic neural network models. |
| title | Bound Tightening using Rolling-Horizon Decomposition for Neural Network Verification |
| topic | Optimization and Control |
| url | https://arxiv.org/abs/2401.05280 |