Most work on the formal verification of neural networks has focused on bounding forward images of neural networks, i.e., the set of outputs of a neural network that correspond to a given set of inputs (for example, bounded perturbations of a nominal input). However, many use cases of neural network verification require solving the inverse problem, i.e, over-approximating the set of inputs that lead to certain outputs. In this work, we present the first efficient bound propagation algorithm, INVPROP, for verifying properties over the preimage of a linearly constrained output set of a neural network, which can be combined with branch-and-bound to achieve completeness. Our efficient algorithm allows multiple passes of intermediate bound refinements, which are crucial for tight inverse verification because the bounds of an intermediate layer depend on relaxations both before and after this layer. We demonstrate our algorithm on applications related to quantifying safe control regions for a dynamical system and detecting out-of-distribution inputs to a neural network. Our results show that in certain settings, we can find over-approximations that are over 2500 times tighter than prior work while being 2.5 times faster on the same hardware.

本文介绍了第一个有效的边界传播算法 INVPROP，用于在神经网络的线性约束输出集的原像上验证属性，并可以与分支和限制相结合以实现完整性。我们的算法在安全控制区域量化和神经网络中检测超出分配的输入方面具有应用价值，并且在相同硬件上比先前的工作快2.5倍，可以找到超过2500倍的最紧近似。

可证明边界的神经网络原像