Although neural networks are widely used, it remains challenging to formally verify the safety and robustness of neural networks in real-world applications. Existing methods are designed to verify the network before deployment, which are limited to relatively simple specifications and fixed networks. These methods are not ready to be applied to real-world problems with complex and/or dynamically changing specifications and networks. To effectively handle such problems, verification needs to be performed online when these changes take place. However, it is still challenging to run existing verification algorithms online. Our key insight is that we can leverage the temporal dependencies of these changes to accelerate the verification process. This paper establishes a novel framework for scalable online verification to solve real-world verification problems with dynamically changing specifications and/or networks. We propose three types of acceleration algorithms: Branch Management to reduce repetitive computation, Perturbation Tolerance to tolerate changes, and Incremental Computation to reuse previous results. Experiment results show that our algorithms achieve up to $100\times$ acceleration, and thus show a promising way to extend neural network verification to real-world applications.

翻译：尽管神经网络已被广泛应用，但在实际场景中正式验证其安全性与鲁棒性仍具挑战性。现有方法旨在部署前验证网络，仅适用于相对简单的规范及固定网络，难以应对规范与网络复杂动态变化的实际问题。为有效处理此类问题，需在变化发生时进行在线验证。然而，现有验证算法仍难以在线运行。我们的核心洞察在于：可利用这些变化的时间依赖性来加速验证过程。本文建立了一套可扩展在线验证的新框架，用于解决规范与网络动态变化的实际验证问题。我们提出三类加速算法：分支管理（减少重复计算）、扰动容忍（适应变化）与增量计算（复用历史结果）。实验表明，我们的算法可实现高达$100\times$的加速，为将神经网络验证拓展至实际应用提供了可行路径。