从拓扑视角验证神经网络安全性

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