Dissertação

Automated verification and refutation of quantized neural networks

Artificial Neural Networks (ANNs) are being deployed for an increasing number of safety- critical applications, including autonomous cars and medical diagnosis. However, con- cerns about their reliability have been raised due to their black-box nature and apparent fragility to adversarial attacks...

ver descrição completa

Autor principal: Sena, Luiz Henrique Coelho
Outros Autores: http://lattes.cnpq.br/1493664223350422
Grau: Dissertação
Idioma: eng
Publicado em: Universidade Federal do Amazonas 2022
Assuntos:
CIENCIAS EXATAS E DA TERRA
Model Checking
Neural Networks
Quantized Neural Networks
Acesso em linha: https://tede.ufam.edu.br/handle/tede/8845
id oai:https:--tede.ufam.edu.br-handle-:tede-8845
recordtype dspace
spelling oai:https:--tede.ufam.edu.br-handle-:tede-88452022-05-02T05:03:48Z Automated verification and refutation of quantized neural networks Sena, Luiz Henrique Coelho Cordeiro, Lucas Carvalho http://lattes.cnpq.br/1493664223350422 http://lattes.cnpq.br/5005832876603012 Lima Filho, Eddie Batista de Santos, Eulanda Miranda dos CIENCIAS EXATAS E DA TERRA Model Checking Neural Networks Quantized Neural Networks Artificial Neural Networks (ANNs) are being deployed for an increasing number of safety- critical applications, including autonomous cars and medical diagnosis. However, con- cerns about their reliability have been raised due to their black-box nature and apparent fragility to adversarial attacks. These concerns are amplified when ANNs are deployed on restricted system, which limit the precision of mathematical operations and thus in- troduce additional quantization errors. Here, we develop and evaluate a novel symbolic verification framework using software model checking (SMC) and satisfiability modulo theories (SMT) to check for vulnerabilities in ANNs and mainly in Multilayer Perceptron (MLP). More specifically, here is proposed several ANN-related optimizations for SMC, including invariant inference via interval analysis, slicing, expression simplifications, and discretization of non-linear activation functions. With this verification framework, we can provide formal guarantees on the safe behavior of ANNs implemented both in floating- and fixed-point arithmetic. In this regard, the current verification approach was able to verify and produce adversarial examples for 52 test cases spanning image classifica- tion and general machine learning applications. Furthermore, for small- to medium-sized ANN, this approach completes most of its verification runs in minutes. Moreover, in con- trast to most state-of-the-art methods, the presented approach is not restricted to specific choices regarding activation functions and non-quantized representations. Experiments show that this approach can analyze larger ANN implementations and substantially re- duce the verification time compared to state-of-the-art techniques that use SMT solving. Artificial Neural Networks (ANNs) are being deployed for an increasing number of safety- critical applications, including autonomous cars and medical diagnosis. However, con- cerns about their reliability have been raised due to their black-box nature and apparent fragility to adversarial attacks. These concerns are amplified when ANNs are deployed on restricted system, which limit the precision of mathematical operations and thus in- troduce additional quantization errors. Here, we develop and evaluate a novel symbolic verification framework using software model checking (SMC) and satisfiability modulo theories (SMT) to check for vulnerabilities in ANNs and mainly in Multilayer Perceptron (MLP). More specifically, here is proposed several ANN-related optimizations for SMC, including invariant inference via interval analysis, slicing, expression simplifications, and discretization of non-linear activation functions. With this verification framework, we can provide formal guarantees on the safe behavior of ANNs implemented both in floating- and fixed-point arithmetic. In this regard, the current verification approach was able to verify and produce adversarial examples for 52 test cases spanning image classifica- tion and general machine learning applications. Furthermore, for small- to medium-sized ANN, this approach completes most of its verification runs in minutes. Moreover, in con- trast to most state-of-the-art methods, the presented approach is not restricted to specific choices regarding activation functions and non-quantized representations. Experiments show that this approach can analyze larger ANN implementations and substantially re- duce the verification time compared to state-of-the-art techniques that use SMT solving 2022-05-02T04:25:57Z 2022-03-04 Dissertação SENA, Luiz Henrique Coelho. Automated Verification and Refutation of Quantized Neural Networks. 2022. 55 f. Dissertação (Mestrado em Engenharia Elétrica) - Universidade Federal do Amazonas, Manaus (AM), 2022. https://tede.ufam.edu.br/handle/tede/8845 eng Acesso Aberto application/pdf Universidade Federal do Amazonas Faculdade de Tecnologia Brasil UFAM Programa de Pós-graduação em Engenharia Elétrica
institution TEDE - Universidade Federal do Amazonas
collection TEDE-UFAM
language eng
topic CIENCIAS EXATAS E DA TERRA
Model Checking
Neural Networks
Quantized Neural Networks
spellingShingle CIENCIAS EXATAS E DA TERRA
Model Checking
Neural Networks
Quantized Neural Networks
Sena, Luiz Henrique Coelho
Automated verification and refutation of quantized neural networks
topic_facet CIENCIAS EXATAS E DA TERRA
Model Checking
Neural Networks
Quantized Neural Networks
description Artificial Neural Networks (ANNs) are being deployed for an increasing number of safety- critical applications, including autonomous cars and medical diagnosis. However, con- cerns about their reliability have been raised due to their black-box nature and apparent fragility to adversarial attacks. These concerns are amplified when ANNs are deployed on restricted system, which limit the precision of mathematical operations and thus in- troduce additional quantization errors. Here, we develop and evaluate a novel symbolic verification framework using software model checking (SMC) and satisfiability modulo theories (SMT) to check for vulnerabilities in ANNs and mainly in Multilayer Perceptron (MLP). More specifically, here is proposed several ANN-related optimizations for SMC, including invariant inference via interval analysis, slicing, expression simplifications, and discretization of non-linear activation functions. With this verification framework, we can provide formal guarantees on the safe behavior of ANNs implemented both in floating- and fixed-point arithmetic. In this regard, the current verification approach was able to verify and produce adversarial examples for 52 test cases spanning image classifica- tion and general machine learning applications. Furthermore, for small- to medium-sized ANN, this approach completes most of its verification runs in minutes. Moreover, in con- trast to most state-of-the-art methods, the presented approach is not restricted to specific choices regarding activation functions and non-quantized representations. Experiments show that this approach can analyze larger ANN implementations and substantially re- duce the verification time compared to state-of-the-art techniques that use SMT solving.
author_additional Cordeiro, Lucas Carvalho
author_additionalStr Cordeiro, Lucas Carvalho
format Dissertação
author Sena, Luiz Henrique Coelho
author2 http://lattes.cnpq.br/1493664223350422
author2Str http://lattes.cnpq.br/1493664223350422
title Automated verification and refutation of quantized neural networks
title_short Automated verification and refutation of quantized neural networks
title_full Automated verification and refutation of quantized neural networks
title_fullStr Automated verification and refutation of quantized neural networks
title_full_unstemmed Automated verification and refutation of quantized neural networks
title_sort automated verification and refutation of quantized neural networks
publisher Universidade Federal do Amazonas
publishDate 2022
url https://tede.ufam.edu.br/handle/tede/8845
_version_ 1831970067556859904
score 11.753735

Registros relacionados