神经网络的区间通用逼近

为了验证神经网络的安全性与鲁棒性，研究人员已成功应用了抽象解释，主要使用区间抽象域。在本文中，我们研究了区间域在神经网络验证中的理论能力与局限。首先，我们引入了区间通用逼近（IUA）定理。IUA 表明，正如我们几十年来所知，神经网络不仅能逼近任何连续函数 $f$（通用逼近），而且我们可以使用任何性质良好的激活函数找到一个神经网络，其区间界能任意逼近 $f$ 的集合语义（将 $f$ 应用于一组输入的结果）。我们将这种逼近概念称为区间逼近。我们的定理将 Baader 等人 (2020) 的近期结果从 ReLU 推广到了我们称之为可压缩函数的一大类激活函数。此外，IUA 定理意味着，使用几乎任何实用的激活函数，我们总能在 $\ell_\infty$-范数下构造出可证明鲁棒的神经网络。其次，我们研究了构造适用于精确区间分析的神经网络的计算复杂度。这是一个关键问题，因为我们对 IUA 的构造性证明在逼近域的大小上是指数级的。我们将这个问题归结为逼近具有可压缩激活函数的神经网络输出范围的问题。我们证明了范围逼近问题（RA）是一个 $\Delta_2$-中间问题，在假设 $\mathsf{coNP}\not\subset \mathsf{NP}$ 的情况下，它严格难于 $\mathsf{NP}$-完全问题。因此，IUA 是一个固有的难题：无论我们考虑使用何种抽象域或计算工具来实现区间逼近，都不存在对此类通用逼近器的高效构造。