神经网络验证的潜在空间：探索不确定性的阴影

神经网络无处不在。然而它们对小输入变化极其敏感。因此，为了防止在安全关键应用中出现意外行为，必须对其进行形式化验证——这是一个极其困难的问题。许多领先的验证算法使用可达性分析或抽象解释来封闭神经网络可能的输出集合。由于封闭的保守性，往往导致验证得不到结论。为此，我们提出了一种新颖的、以规范为导向的输入细化程序，即迭代地封闭神经网络所有不安全输出的原像，以缩小可能的输入集合以仅包含不安全输入。为此，我们利用潜在空间传递投影基集合表示通过神经网络，将输出规范传输到输入空间。投影基集合表示（例如 zonotope）是更高维集合的“阴影”——潜在空间——在神经网络通过过程中保持不变。因此，输入集合和输出封闭是同一潜在空间的“阴影”，我们可以利用它来传递约束。我们提出了一种高效的神经网络验证工具，使用迭代细化显著减少分支-界限程序中的子问题数量。使用 zonotope 作为集合表示，与许多其他领先方法不同，我们的方法仅需使用矩阵运算即可实现，通过高效的 GPU 加速实现显著提速。我们展示了该工具在与国际神经网络验证比赛中顶尖工具相当的性能。