作为一种新的编程范式,基于神经网络的机器学习已将其应用扩展到许多现实世界中的问题。由于神经网络的黑盒性质,验证和解释其行为变得越来越重要,尤其是当它们部署在安全至关重要的应用中时。现有的验证工作主要集中于定性验证,该验证询问是否存在针对神经网络的输入(指定区域),以便违反财产(例如,局部鲁棒性)。但是,在许多实际应用中,几乎可以肯定存在这样的(对抗性)输入,这使得定性答案降低了有意义。在这项工作中,我们研究了一个更有趣,更具挑战性的问题,即对神经网络的定量验证,该验证询问财产经常得到满足或侵犯财产的频率。我们针对二进制神经网络(BNNS),一般神经网络的1位量化。BNN最近在深度学习中引起了越来越多的关注,因为它们可以大幅度地减少记忆存储和执行时间,而智力操作在求助方案中至关重要,例如,嵌入式设备用于物联网的嵌入式设备。朝着对BNNS的定量验证,我们提出了一种新型算法方法,用于将BNN作为二进制决策图(BDDS),这是一种在形式验证和知识表示中广泛研究的模型。通过利用BNN的内部结构,我们的编码将BNN中块的输入输出关系转化为基数约束,然后由BDD编码。基于新的BDD编码,我们为BNN开发了一个定量验证框架,可以在其中对BNN进行精确和全面的分析。为了提高BDD编码的可扩展性,我们还研究了各个级别的并行化策略。我们通过为BNN提供定量鲁棒性验证和解释性来证明我们的框架的应用。广泛的实验评估证实了我们方法的有效性和效率。
主要关键词