Neural networks (NNs) are increasingly applied in safety-critical systems such as autonomous vehicles. However, they are fragile and are often ill-behaved. Consequently, their behaviors should undergo rigorous guarantees before deployment in practice. In this paper, we propose a set-boundary reachability method to investigate the safety verification problem of NNs from a topological perspective. Given an NN with an input set and a safe set, the safety verification problem is to determine whether all outputs of the NN resulting from the input set fall within the safe set. In our method, the homeomorphism property and the open map property of NNs are mainly exploited, which establish rigorous guarantees between the boundaries of the input set and the boundaries of the output set. The exploitation of these two properties facilitates reachability computations via extracting subsets of the input set rather than the entire input set, thus controlling the wrapping effect in reachability analysis and facilitating the reduction of computation burdens for safety verification. The homeomorphism property exists in some widely used NNs such as invertible residual networks (i-ResNets) and Neural ordinary differential equations (Neural ODEs), and the open map is a less strict property and easier to satisfy compared with the homeomorphism property. For NNs establishing either of these properties, our set-boundary reachability method only needs to perform reachability analysis on the boundary of the input set. Moreover, for NNs that do not feature these properties with respect to the input set, we explore subsets of the input set for establishing the local homeomorphism property and then abandon these subsets for reachability computations. Finally, some examples demonstrate the performance of the proposed method.

翻译：摘要：神经网络（NNs）日益应用于安全关键系统（如自动驾驶车辆）。然而，它们具有脆弱性且往往表现不佳。因此，在实际部署前需对其行为进行严格保证。本文从拓扑视角提出一种集合边界可达性方法，用于研究神经网络的安全验证问题。给定一个具备输入集合与安全集合的神经网络，安全验证问题在于确定该网络由输入集合产生的所有输出是否均落在安全集合内。该方法主要利用神经网络的同胚性与开映射性质，从而在输入集合边界与输出集合边界之间建立严格保证。通过提取输入集合的子集而非整个集合进行计算，这两种性质的应用有助于控制可达性分析中的包裹效应，并降低安全验证的计算负担。同胚性存在于部分广泛使用的神经网络中，例如可逆残差网络（i-ResNets）和神经常微分方程（Neural ODEs），而开映射是较同胚性更宽松、更易满足的性质。对于具备其中任一性质的神经网络，本集合边界可达性方法仅需对输入集合边界进行可达性分析。此外，针对不具备这些性质（相对于输入集合）的网络，我们通过探索输入集合的子集建立局部同胚性，进而舍弃这些子集进行可达性计算。最后，通过若干示例验证了所提出方法的性能。