Most work on the formal verification of neural networks has focused on bounding the set of outputs 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, or over-approximating the set of inputs that lead to certain outputs. We present the INVPROP algorithm for verifying properties over the preimage of a linearly constrained output set, which can be combined with branch-and-bound to increase precision. Contrary to other approaches, our efficient algorithm is GPU-accelerated and does not require a linear programming solver. We demonstrate our algorithm for identifying safe control regions for a dynamical system via backward reachability analysis, verifying adversarial robustness, and detecting out-of-distribution inputs to a neural network. Our results show that in certain settings, we find over-approximations over 2500x tighter than prior work while being 2.5x faster. By strengthening robustness verification with output constraints, we consistently verify more properties than the previous state-of-the-art on multiple benchmarks, including a large model with 167k neurons in VNN-COMP 2023. Our algorithm has been incorporated into the $\alpha,\!\beta$-CROWN verifier, available at https://abcrown.org.

翻译：大多数关于神经网络形式化验证的工作都集中于给定输入集（例如，标称输入的有界扰动）所对应的输出集的边界界定。然而，神经网络验证的许多应用场景需要解决逆问题，即过度逼近导致特定输出的输入集。我们提出了INVPROP算法，用于验证线性约束输出集的原像上的性质，该算法可与分支定界法结合以提高精度。与其他方法相反，我们高效的算法采用GPU加速且无需线性规划求解器。我们展示了该算法在通过反向可达性分析识别动力系统的安全控制区域、验证对抗鲁棒性以及检测神经网络中的分布外输入方面的应用。结果表明，在某些场景下，我们找到的过度逼近比先前工作紧致超过2500倍，同时速度快2.5倍。通过用输出约束增强鲁棒性验证，我们在多个基准测试中持续验证了比先前最先进方法更多的性质，包括VNN-COMP 2023中一个具有16.7万个神经元的大模型。我们的算法已整合到 $\alpha,\!\beta$-CROWN 验证器中，可通过 https://abcrown.org 获取。