Portfolio solver for verifying Binarized Neural Networks

Kovásznai, Gergely, Gajdár, Krisztián, Narodytska, Nina (2021) Portfolio solver for verifying Binarized Neural Networks Annales Mathematicae et Informaticae (53.): Selected papers of the 1st Conference on Information Technology and Data Science. pp. 183-200. ISSN 1787-6117 (Online)

[thumbnail of AMI_53_from183to200.pdf] pdf
AMI_53_from183to200.pdf

Download (1MB) [error in script]
Hivatalos webcím (URL): https://doi.org/10.33039/ami.2021.03.007

Absztrakt (kivonat)

Although deep learning is a very successful AI technology, many concerns have been raised about to what extent the decisions making process of deep neural networks can be trusted. Verifying of properties of neural networks such as adversarial robustness and network equivalence sheds light on the trustiness of such systems. We focus on an important family of deep neural networks, the Binarized Neural Networks (BNNs) that are useful in resourceconstrained environments, like embedded devices. We introduce our portfolio solver that is able to encode BNN properties for SAT, SMT, and MIP solvers and run them in parallel, in a portfolio setting. In the paper we propose all the corresponding encodings of different types of BNN layers as well as BNN properties into SAT, SMT, cardinality constrains, and pseudo-Boolean constraints. Our experimental results demonstrate that our solver is capable of verifying adversarial robustness of medium-sized BNNs in reasonable time and seems to scale for larger BNNs. We also report on experiments on network equivalence with promising results.

Mű típusa: Folyóiratcikk - Journal article
Szerző:
Szerző neve
Email
MTMT azonosító
ORCID azonosító
Közreműködés
Kovásznai, Gergely
NEM RÉSZLETEZETT
NEM RÉSZLETEZETT
NEM RÉSZLETEZETT
Szerző
Gajdár, Krisztián
NEM RÉSZLETEZETT
NEM RÉSZLETEZETT
NEM RÉSZLETEZETT
Szerző
Narodytska, Nina
NEM RÉSZLETEZETT
NEM RÉSZLETEZETT
NEM RÉSZLETEZETT
Szerző
Kapcsolódó URL-ek:
Kulcsszavak: Artificial intelligence, neural network, adversarial robustness, formal method, verification, SAT, SMT, MIP
Nyelv: angol
DOI azonosító: 10.33039/ami.2021.03.007
ISSN: 1787-6117 (Online)
Felhasználó: Tibor Gál
Dátum: 18 Máj 2021 16:21
Utolsó módosítás: 18 Máj 2021 16:21
URI: http://publikacio.uni-eszterhazy.hu/id/eprint/7004
Műveletek (bejelentkezés szükséges)
Tétel nézet Tétel nézet