加速神经网络可验证解释

可验证解释是对神经网络决策进行解释的原则方法，而神经网络本质上是黑箱模型。然而，这些技术面临显著的可扩展性挑战，因为它们需要对神经网络验证器进行多次调用，而每个验证器的最坏情况复杂度为指数级。我们提出了 FaVeX—a 一种新型算法用于计算可验证解释。FaVeX 通过动态组合输入特征的批处理和顺序处理，并在证明特定输入特征不变性以及搜索改变预测的特征赋值时复用来自先前查询的信息，从而加速计算。此外，我们提出了一种新颖且分层的可验证解释定义，称为“验证器最优鲁棒解释”，该定义明确地考虑了网络验证器不完整性。我们的全面实验评估表明，FaVeX 以及验证器最优鲁棒解释在可扩展性方面具有优势，两者共同能够在数十万个非线性激活函数的网络上生成有意义的形式化解释。