CUDA 中人工神经网络的增量有界模型检测
计算机科学中的逻辑
2019-07-31 v1 机器学习
神经与进化计算
摘要
人工神经网络（ANN）因其泛化能力和对意外输入/模式的响应能力而被用于各类应用中的强大计算系统。然而，用于安全关键系统的 ANN 实现可能导致故障，这些故障在设计阶段难以预测，因为 ANN 高度并行且其参数难以解释。在此我们开发并评估了一种基于增量有界模型检测（BMC）的新型符号软件验证框架，用于检查多层感知机（MLP）中的对抗样本与覆盖方法。特别地，我们进一步开发了高效的基于 SMT 的图形处理器上下文有界模型检测器（ESBMC-GPU），以确保某些安全关键系统可能失效并作出错误决策、从而导致不必要物质损害甚至危及生命的安全属性的可靠性。本文标志着首个对 CUDA 中实现的人工神经网络进行推理的符号验证框架。我们的实验结果表明，在 ESBMC-GPU 中实现的方法能够成功验证 ANN 中的安全属性和覆盖方法，并正确生成 28 个 MLP 中的对抗样本。
引用
@article{arxiv.1907.12933,
title = {Incremental Bounded Model Checking of Artificial Neural Networks in CUDA},
author = {Luiz H. Sena and Iury V. Bessa and Mikhail R. Gadelha and Lucas C. Cordeiro and Edjard Mota},
journal= {arXiv preprint arXiv:1907.12933},
year = {2019}
}
备注
8 pages