Incremental Bounded Model Checking of Artificial Neural Networks in CUDA
Resumo
Artificial Neural networks (ANNs) are powerful computing systems employed for various applications due to their versatility to generalize and to respond to unexpected inputs/patterns. However, implementations of ANNs for safety-critical systems might lead to failures, which are hardly predicted in the design phase since ANNs are highly parallel and their parameters are hardly interpretable. Here we develop and evaluate a novel symbolic software verification framework based on incremental bounded model checking (BMC) to check for adversarial cases and coverage methods in multi-layer perceptron (MLP). In particular, we further develop the efficient SMT-based Context-Bounded Model Checker for Graphical Processing Units (ESBMC-GPU) in order to ensure the reliability of certain safety properties in which safety-critical systems can fail and make incorrect decisions, thereby leading to unwanted material damage or even put lives in danger. This paper marks the first symbolic verification framework to reason over ANNs implemented in CUDA. Our experimental results show that our approach implemented in ESBMC-GPU can successfully verify safety properties and covering methods in ANNs and correctly generate 28 adversarial cases in MLPs.
Referências
M. Bojarski D. Del Testa D. Dworakowski B. Firner B. Flepp P. Goyal L. D. Jackel M. Monfort U. Muller J. Zhang et al. "End to end learning for self-driving cars" 2016.
D. Gopinath K. Wang M. Zhang C. S. Pasareanu S. Khurshid "Symbolic execution for deep neural networks" CoRR vol. abs/1807.10439 2018 [online] Available: http://arxiv.org/abs/1807.10439.
Y. Sun X. Huang D. Kroening "Testing deep neural networks" 2018.
S. Zheng Y. Song T. Leung I. Goodfellow "Improving the robustness of deep neural networks via stability training" Proceedings of the ieee conference on computer vision and pattern recognition pp. 4480-4488 2016.
A. Krogh J. Vedelsby "Neural network ensembles cross validation and active learning" Advances in neural information processing systems pp. 231-238 1995.
X. Huang M. Kwiatkowska S. Wang M. Wu "Safety verification of deep neural networks" International Conference on Computer Aided Verification pp. 3-29 2017.
G. Katz C. Barrett D. L. Dill K. Julian M. J. Kochenderfer "Reluplex: An efficient smt solver for verifying deep neural networks" International Conference on Computer Aided Verification pp. 97-117 2017.
P. A. Pereira H. F. Albuquerque I. da Silva H. Marques F. R. Monteiro R. Ferreira L. C. Cordeiro "Smt-based context-bounded model checking for CUDA programs" Concurrency and Computation: Practice and Experience vol. 29 no. 22 2017.
F. R. Monteiro E. H. d. S. Alves I. S. Silva H. I. Ismail L. C. Cordeiro E. B. de Lima Filho "ESBMC-GPU a context-bounded model checking tool to verify cuda programs" Science of Computer Programming vol. 152 pp. 63-69 2018.
S. Chetlur C. Woolley P. Vandermersch J. Cohen J. Tran B. Catanzaro E. Shelhamer "cudnn: Efficient primitives for deep learning" 2014.
C. Nvidia Cublas library Santa Clara California:NVIDIA Corporation vol. 15 no. 27 pp. 31 2008.
C. M. Bishop Pattern Recognition and Machine Learning Springer 2006.
M. T. Hagan H. B. Demuth M. H. Beale O. De Jesús Neural network design Boston:Pws Pub vol. 20 1996.
