Star-based reachability analysis of deep neural networks

Hoang Dung Tran, Diago Manzanas Lopez, Patrick Musau, Xiaodong Yang, Luan Viet Nguyen, Weiming Xiang, Taylor T. Johnson

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

This paper proposes novel reachability algorithms for both exact (sound and complete) and over-approximation (sound) analysis of deep neural networks (DNNs). The approach uses star sets as a symbolic representation of sets of states, which are known in short as stars and provide an effective representation of high-dimensional polytopes. Our star-based reachability algorithms can be applied to several problems in analyzing the robustness of machine learning methods, such as safety and robustness verification of DNNs. The star-based reachability algorithms are implemented in a software prototype called the neural network verification (NNV) tool that is publicly available for evaluation and comparison. Our experiments show that when verifying ACAS Xu neural networks on a multi-core platform, our exact reachability algorithm is on average about 19 times faster than Reluplex, a satisfiability modulo theory (SMT)-based approach. Furthermore, our approach can visualize the precise behavior of DNNs because the reachable states are computed in the method. Notably, in the case that a DNN violates a safety property, the exact reachability algorithm can construct a complete set of counterexamples. Our star-based over-approximate reachability algorithm is on average 118 times faster than Reluplex on the verification of properties for ACAS Xu networks, even without exploiting the parallelism that comes naturally in our method. Additionally, our over-approximate reachability is much less conservative than DeepZ and DeepPoly, recent approaches utilizing zonotopes and other abstract domains that fail to verify many properties of ACAS Xu networks due to their conservativeness. Moreover, our star-based over-approximate reachability algorithm obtains better robustness bounds in comparison with DeepZ and DeepPoly when verifying the robustness of image classification DNNs.

Original languageEnglish (US)
Title of host publicationFormal Methods – The Next 30 Years - 3rd World Congress, FM 2019, Proceedings
EditorsMaurice H. ter Beek, Annabelle McIver, José N. Oliveira
PublisherSpringer
Pages670-686
Number of pages17
ISBN (Print)9783030309411
DOIs
StatePublished - Jan 1 2019
Externally publishedYes
Event23rd Symposium on Formal Methods, FM 2019, in the form of the 3rd World Congress on Formal Methods, 2019 - Porto, Portugal
Duration: Oct 7 2019Oct 11 2019

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11800 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference23rd Symposium on Formal Methods, FM 2019, in the form of the 3rd World Congress on Formal Methods, 2019
CountryPortugal
CityPorto
Period10/7/1910/11/19

Fingerprint

Reachability Analysis
Reachability
Stars
Star
Neural Networks
Robustness
Acoustic waves
Neural networks
Safety
Image classification
Conservativeness
Deep neural networks
Image Classification
Time-average
Violate
Polytopes
Learning systems
Parallelism
Counterexample
Modulo

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Tran, H. D., Manzanas Lopez, D., Musau, P., Yang, X., Nguyen, L. V., Xiang, W., & Johnson, T. T. (2019). Star-based reachability analysis of deep neural networks. In M. H. ter Beek, A. McIver, & J. N. Oliveira (Eds.), Formal Methods – The Next 30 Years - 3rd World Congress, FM 2019, Proceedings (pp. 670-686). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11800 LNCS). Springer. https://doi.org/10.1007/978-3-030-30942-8_39

Star-based reachability analysis of deep neural networks. / Tran, Hoang Dung; Manzanas Lopez, Diago; Musau, Patrick; Yang, Xiaodong; Nguyen, Luan Viet; Xiang, Weiming; Johnson, Taylor T.

Formal Methods – The Next 30 Years - 3rd World Congress, FM 2019, Proceedings. ed. / Maurice H. ter Beek; Annabelle McIver; José N. Oliveira. Springer, 2019. p. 670-686 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11800 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Tran, HD, Manzanas Lopez, D, Musau, P, Yang, X, Nguyen, LV, Xiang, W & Johnson, TT 2019, Star-based reachability analysis of deep neural networks. in MH ter Beek, A McIver & JN Oliveira (eds), Formal Methods – The Next 30 Years - 3rd World Congress, FM 2019, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11800 LNCS, Springer, pp. 670-686, 23rd Symposium on Formal Methods, FM 2019, in the form of the 3rd World Congress on Formal Methods, 2019, Porto, Portugal, 10/7/19. https://doi.org/10.1007/978-3-030-30942-8_39
Tran HD, Manzanas Lopez D, Musau P, Yang X, Nguyen LV, Xiang W et al. Star-based reachability analysis of deep neural networks. In ter Beek MH, McIver A, Oliveira JN, editors, Formal Methods – The Next 30 Years - 3rd World Congress, FM 2019, Proceedings. Springer. 2019. p. 670-686. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-030-30942-8_39
Tran, Hoang Dung ; Manzanas Lopez, Diago ; Musau, Patrick ; Yang, Xiaodong ; Nguyen, Luan Viet ; Xiang, Weiming ; Johnson, Taylor T. / Star-based reachability analysis of deep neural networks. Formal Methods – The Next 30 Years - 3rd World Congress, FM 2019, Proceedings. editor / Maurice H. ter Beek ; Annabelle McIver ; José N. Oliveira. Springer, 2019. pp. 670-686 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{9386c860691c48c0aff9e0a5ba58a29e,
title = "Star-based reachability analysis of deep neural networks",
abstract = "This paper proposes novel reachability algorithms for both exact (sound and complete) and over-approximation (sound) analysis of deep neural networks (DNNs). The approach uses star sets as a symbolic representation of sets of states, which are known in short as stars and provide an effective representation of high-dimensional polytopes. Our star-based reachability algorithms can be applied to several problems in analyzing the robustness of machine learning methods, such as safety and robustness verification of DNNs. The star-based reachability algorithms are implemented in a software prototype called the neural network verification (NNV) tool that is publicly available for evaluation and comparison. Our experiments show that when verifying ACAS Xu neural networks on a multi-core platform, our exact reachability algorithm is on average about 19 times faster than Reluplex, a satisfiability modulo theory (SMT)-based approach. Furthermore, our approach can visualize the precise behavior of DNNs because the reachable states are computed in the method. Notably, in the case that a DNN violates a safety property, the exact reachability algorithm can construct a complete set of counterexamples. Our star-based over-approximate reachability algorithm is on average 118 times faster than Reluplex on the verification of properties for ACAS Xu networks, even without exploiting the parallelism that comes naturally in our method. Additionally, our over-approximate reachability is much less conservative than DeepZ and DeepPoly, recent approaches utilizing zonotopes and other abstract domains that fail to verify many properties of ACAS Xu networks due to their conservativeness. Moreover, our star-based over-approximate reachability algorithm obtains better robustness bounds in comparison with DeepZ and DeepPoly when verifying the robustness of image classification DNNs.",
author = "Tran, {Hoang Dung} and {Manzanas Lopez}, Diago and Patrick Musau and Xiaodong Yang and Nguyen, {Luan Viet} and Weiming Xiang and Johnson, {Taylor T.}",
year = "2019",
month = "1",
day = "1",
doi = "10.1007/978-3-030-30942-8_39",
language = "English (US)",
isbn = "9783030309411",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer",
pages = "670--686",
editor = "{ter Beek}, {Maurice H.} and Annabelle McIver and Oliveira, {Jos{\'e} N.}",
booktitle = "Formal Methods – The Next 30 Years - 3rd World Congress, FM 2019, Proceedings",

}

TY - GEN

T1 - Star-based reachability analysis of deep neural networks

AU - Tran, Hoang Dung

AU - Manzanas Lopez, Diago

AU - Musau, Patrick

AU - Yang, Xiaodong

AU - Nguyen, Luan Viet

AU - Xiang, Weiming

AU - Johnson, Taylor T.

PY - 2019/1/1

Y1 - 2019/1/1

N2 - This paper proposes novel reachability algorithms for both exact (sound and complete) and over-approximation (sound) analysis of deep neural networks (DNNs). The approach uses star sets as a symbolic representation of sets of states, which are known in short as stars and provide an effective representation of high-dimensional polytopes. Our star-based reachability algorithms can be applied to several problems in analyzing the robustness of machine learning methods, such as safety and robustness verification of DNNs. The star-based reachability algorithms are implemented in a software prototype called the neural network verification (NNV) tool that is publicly available for evaluation and comparison. Our experiments show that when verifying ACAS Xu neural networks on a multi-core platform, our exact reachability algorithm is on average about 19 times faster than Reluplex, a satisfiability modulo theory (SMT)-based approach. Furthermore, our approach can visualize the precise behavior of DNNs because the reachable states are computed in the method. Notably, in the case that a DNN violates a safety property, the exact reachability algorithm can construct a complete set of counterexamples. Our star-based over-approximate reachability algorithm is on average 118 times faster than Reluplex on the verification of properties for ACAS Xu networks, even without exploiting the parallelism that comes naturally in our method. Additionally, our over-approximate reachability is much less conservative than DeepZ and DeepPoly, recent approaches utilizing zonotopes and other abstract domains that fail to verify many properties of ACAS Xu networks due to their conservativeness. Moreover, our star-based over-approximate reachability algorithm obtains better robustness bounds in comparison with DeepZ and DeepPoly when verifying the robustness of image classification DNNs.

AB - This paper proposes novel reachability algorithms for both exact (sound and complete) and over-approximation (sound) analysis of deep neural networks (DNNs). The approach uses star sets as a symbolic representation of sets of states, which are known in short as stars and provide an effective representation of high-dimensional polytopes. Our star-based reachability algorithms can be applied to several problems in analyzing the robustness of machine learning methods, such as safety and robustness verification of DNNs. The star-based reachability algorithms are implemented in a software prototype called the neural network verification (NNV) tool that is publicly available for evaluation and comparison. Our experiments show that when verifying ACAS Xu neural networks on a multi-core platform, our exact reachability algorithm is on average about 19 times faster than Reluplex, a satisfiability modulo theory (SMT)-based approach. Furthermore, our approach can visualize the precise behavior of DNNs because the reachable states are computed in the method. Notably, in the case that a DNN violates a safety property, the exact reachability algorithm can construct a complete set of counterexamples. Our star-based over-approximate reachability algorithm is on average 118 times faster than Reluplex on the verification of properties for ACAS Xu networks, even without exploiting the parallelism that comes naturally in our method. Additionally, our over-approximate reachability is much less conservative than DeepZ and DeepPoly, recent approaches utilizing zonotopes and other abstract domains that fail to verify many properties of ACAS Xu networks due to their conservativeness. Moreover, our star-based over-approximate reachability algorithm obtains better robustness bounds in comparison with DeepZ and DeepPoly when verifying the robustness of image classification DNNs.

UR - http://www.scopus.com/inward/record.url?scp=85076114147&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85076114147&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-30942-8_39

DO - 10.1007/978-3-030-30942-8_39

M3 - Conference contribution

AN - SCOPUS:85076114147

SN - 9783030309411

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 670

EP - 686

BT - Formal Methods – The Next 30 Years - 3rd World Congress, FM 2019, Proceedings

A2 - ter Beek, Maurice H.

A2 - McIver, Annabelle

A2 - Oliveira, José N.

PB - Springer

ER -