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）。