Artificial Neural Networks (ANNs) are being deployed for an increasing number of safety-critical applications, including autonomous cars and medical diagnosis. However, concerns 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 introduce 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. More specifically, we propose 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, our verification approach was able to verify and produce adversarial examples for $52$ test cases spanning image classification and general machine learning applications. Furthermore, for small- to medium-sized ANN, our approach completes most of its verification runs in minutes. Moreover, in contrast to most state-of-the-art methods, our approach is not restricted to specific choices regarding activation functions and non-quantized representations. Our experiments show that our approach can analyze larger ANN implementations and substantially reduce the verification time compared to state-of-the-art techniques that use SMT solving.
翻译:人工神经网络(ANNs)正在被部署用于越来越多的安全关键应用程序,包括自主汽车和医疗诊断,但是,由于这些应用程序的黑箱性质和对对抗性攻击的明显脆弱性,人们对其可靠性提出了关切;当将非本国网络部署在限制的系统上,限制数学操作的精确度,从而引入额外的量化错误时,这些关切就更加突出;在这里,我们利用软件模型检查和可视性模调理论,开发并评价一个新型的象征性核查框架,以检查非本国网络的弱点。更具体地说,我们建议对SMC采用一些与非本国网络有关的优化,包括通过间隔分析、剪裁、简化表达简化和非线性激活功能的变异性推断。根据这一核查框架,我们可以对非本国网络在浮动和固定点算术中实施的安全行为提供正式保证。在这方面,我们的核查方法能够核实和生成520美元测试案例的对抗性范例,跨越图像分类和一般机器学习应用程序。此外,对于最小规模和最小规模的不定期的核查方法,我们最小规模的对非定期的核查,在最小规模的ANNM的试验方法中,可以显示我们最小规模和最小规模的演示方法。