具有不确定参数的神经网络可达性分析

当前关于神经网络可达性分析方法的文献仅关注网络输入上的不确定性。本文中，我们提出两种新方法，用于对内部参数（各层的权重矩阵与偏置向量）存在额外不确定性的神经网络进行可达性分析，这或将形式化方法在神经网络领域的应用拓展至安全训练或网络修复等新课题。我们提出的第一种也是主要的方法依赖于基于混合单调性的现有可达性分析方法（最初为动力系统引入）。第二种提出的方法扩展了ESIP（基于误差的符号区间传播）方法，该方法最初在验证工具Neurify中实现，并首次提及于验证工具VeriNet的出版物中。尽管ESIP方法在仅输入存在不确定性的经典情形下常被证明优于混合单调性可达性分析，我们在本文中通过数值模拟表明，在处理权重与偏置的不确定性时，情况发生了极大逆转（在精度、计算时间、内存占用及更广适用性方面）。