[论文] Distribution and Clusters Approximations as Abstract Domains in Probab...

当神经网络遇见概率抽象解释：用分布与聚类丈量不可丈量之物

一座你想保护的城市

想象你是一座城市的防空指挥官。城里有几百万栋建筑，每栋建筑都可能受到不同强度的冲击。你不可能逐栋建筑去模拟——那太慢了；你也不能只看一栋就下结论——那太冒险了。你需要的是一张"概率地图"：哪些区域在哪些冲击强度下会怎样变形，整个城市的脆弱性分布是什么样的。

神经网络验证面临的就是这个问题。一个训练好的神经网络接受输入、产出输出，但输入空间是连续的、无限的——所有可能的图像、所有可能的文本、所有可能的扰动。你想知道的不是"这张熊猫图片会被分类成什么"，而是"所有看起来像熊猫的图片，被这个网络分类后，输出分布是什么样"。

Zhuofan Zhang 和 Herbert Wiklicky 在 2026 年 3 月的这篇论文做的事情，就是给这张概率地图发明了两种新的画法。

概率抽象解释：从逐点到逐流

先说清楚他们站在什么基础上。2024 年，同两位作者提出了"网格近似"（grids approximation）方法。核心思路是：把连续的输入空间切成一个个网格，每个网格代表一小片区域，用网格中心点代表这片区域的概率密度。然后追踪这些网格通过网络后，输出端的概率分布怎样变化——这就是"密度分布流"（density distribution flow）。

这属于一个更大的框架叫概率抽象解释（probabilistic abstract interpretation）。抽象解释是程序验证领域的经典技术：你没法精确追踪程序所有可能的行为，就用一个"抽象域"来近似。经典例子是用区间 \([a,b]\) 代替精确值 \(x\)——你不知道 \(x\) 具体是多少，但你知道它在 \([a,b]\) 里，于是你可以追踪"所有 \(x \in [a,b]\) 经过这个函数后，输出在什么范围"。

概率版本更进一步：输入不是确定的值，而是一个概率分布。你想知道的是，输入分布经过网络后，输出分布长什么样。这比确定性验证强得多——它不只告诉你"存在一个对抗样本会让网络出错"，而是告诉你"网络在多大比例的输入上会出错"。

但网格近似有局限。想象你用方格网格去覆盖一张地图：如果数据点分布是圆形的，方格要么浪费空间（格子大部分是空的），要么丢失精度（一个格子里混了不同类别的点）。当输入维度变高时，网格数量指数爆炸——这就是维度灾难。

分布近似：用函数代替格子

论文的第一种新方法叫分布近似（distribution approximation）。思路很直接：与其用离散的格子，不如用一个连续函数来拟合输入空间上的概率分布。

具体来说，给定一组数据点 \(\{x_1, x_2, \ldots, x_n\}\) 和它们的概率 \(\{p_1, p_2, \ldots, p_n\}\)，你找一个函数 \(y(x)\) 来近似这个分布。论文给了三种选择：

多项式。最简单的选择。找一个多项式 \(y = a_0 + a_1 x + a_2 x^2 + \ldots + a_n x^n\) 拟合数据点。优点是简单、可微；缺点是高次多项式会震荡，低次的又不够灵活。

径向基函数（Radial Basis Functions, RBF）。这是论文重点讨论的。每个"中心" \(c_i\) 贡献一个钟形函数 \(\phi(\|x - c_i\|)\)，整体拟合是这些钟形函数的加权和：

其中 \(\phi\) 通常是高斯函数 \(e^{-\|x-c\|^2}\)。直觉上，就像在数据点上放一个个"小山丘"，每个山丘的高度由系数 \(a_i\) 控制，所有山丘叠加起来就是分布的近似形状。

关键问题是：选哪些点作为中心？论文用穷举搜索——在所有数据点中选 \(N\) 个作为中心，使得均方误差 \(R_{MS}\) 最小。对于小规模问题这够用，但大规模数据需要更聪明的选点策略。

傅里叶变换。把分布看作周期函数（周期无限长），用三角函数展开。论文指出这更适合周期性分布，也可以作为"二步抽象"——先用 RBF 拟合成连续函数，再用傅里叶进一步分析频率成分。

有了连续函数近似后，抽象变换器 \(f^\#\) 就定义为：给定输入分布 \(y(x)\)，输出分布是 \(y(f^{-1}(x))\)——把网络函数 \(f\) 的逆作用在分布上。这比网格版本的"逐格映射"精确得多，因为连续函数保留了分布的形状信息。

聚类近似：用代表点代替格子

第二种新方法叫聚类近似（clusters approximation）。思路又不一样：不拟合连续函数，而是把数据点分成若干组，每组用一个代表点（质心）来代替。

这其实是对网格近似的推广。网格可以看作一种特殊的聚类——把空间切成超立方体，每个立方体里的点算一组，中心就是格子代表。但聚类更灵活：组的形状可以是任意的，由数据本身决定。

论文讨论了两种聚类方法：

K-means。最经典的聚类算法。给定数据集 \(\{x^{(1)}, \ldots, x^{(m)}\}\) 和预设的簇数 \(K\)：

1. 随机初始化 \(K\) 个质心 \(\mu_1, \mu_2, \ldots, \mu_K\) 2. 重复直到收敛：

• 每个点分配到最近的质心：\(c^{(i)} := \arg\min_k \|x^{(i)} - \mu_k\|^2\)
• 每个质心更新为簇内均值：\(\mu_k := \frac{\sum_{i: c^{(i)}=k} x^{(i)}}{\sum_{i: c^{(i)}=k} 1}\)

高斯混合模型（Gaussian Mixture Model, GMM）。比 K-means 更进一步：每个簇不是用一个点代表，而是用一个高斯分布代表。整个数据分布被建模为 \(K\) 个高斯分布的加权和：

每个高斯有自己的均值 \(\mu_k\)、协方差 \(\Sigma_k\) 和权重 \(w_k\)。参数通过 EM 算法迭代估计：

• E 步：计算每个点属于每个簇的概率 \(r_{ik}\)
• M 步：根据 \(r_{ik}\) 更新 \(\mu_k, \Sigma_k, w_k\)

抽象变换器：从输入分布到输出分布

有了抽象域，下一步是定义抽象变换器——描述网络如何变换分布。这是整个框架的核心。

在具体语义中，网络 \(f\) 把输入 \(x\) 映射到输出 \(f(x)\)。在抽象语义中，变换器 \(f^\#\) 把输入的抽象表示（一组网格、一个分布函数、或一组质心）映射到输出的抽象表示。

对于聚类近似，变换器的逻辑是：每个质心 \(c_k^\#\) 通过网络变成 \(f(c_k^\#)\)，概率 \(p_{c_k^\#}\) 保持不变（质心代表的那组点，整体概率不变）。这看似简单，但关键在于——你不需要追踪每个点，只需要追踪 \(K\) 个质心。当 \(K \ll m\)（数据点数）时，计算量大幅降低。

对于分布近似，变换器更精妙：\(f^\#(y(x)) = y(f^{-1}(x))\)。这是说，输出分布在某个点 \(x\) 处的密度，等于输入分布在 \(f^{-1}(x)\) 处的密度。这要求 \(f\) 可逆——对神经网络来说，这通常需要额外处理（比如用网络的逆或近似逆）。

为什么这很重要

你可能会问：为什么要费这么大劲搞这些近似？直接跑网络不就行了吗？

区别在于"验证"和"测试"。测试是：你给网络一堆输入，看输出对不对。验证是：你证明网络在所有可能的输入上满足某个性质。测试只能覆盖有限样本，验证能覆盖整个输入空间。

但验证的难点在于输入空间太大。一个 224×224 的图像有 150528 个像素，每个像素 256 个值——可能输入数是 \(256^{150528}\)，比宇宙原子数还多。你不可能逐个验证。

抽象解释的价值在于：用抽象域近似输入空间，然后在抽象域上做验证。如果抽象域设计得好，验证结果可以推广到整个输入空间——这就是"soundness"（可靠性）保证。概率版本更进一步：不只告诉你"会不会出错"，而是"出错概率是多少"。

这篇论文的两种新方法给了验证者更多选择：

• 分布近似适合输入分布形状已知或可拟合的场景。比如，如果你知道输入扰动是高斯分布，直接用高斯 RBF 拟合就比切网格精确得多。
• 聚类近似适合输入有自然分组的场景。比如，对抗样本可能集中在某些"脆弱区域"，聚类能自动发现这些区域，而网格可能把它们切碎了。

局限与未来

论文很诚实地承认了局限：这些方法目前只在简单示例上验证过，"更多最先进的神经网络架构留待未来探索"。这是早期方法论文的常见特点——理论框架搭好了，工程实现和大规模实验是下一步。

另一个值得注意的点：分布近似需要假设输入分布能用某种函数族（多项式、RBF、傅里叶）拟合。如果真实分布不符合这些假设，近似质量会打折扣。聚类近似则更"数据驱动"——它不假设分布形状，但需要选择簇数 \(K\)，这本身是个超参数。

更大的图景

这篇论文处在一个更宏大的趋势中：用形式化方法给神经网络提供保证。这个领域叫神经网络安全验证（neural network verification），过去十年发展迅速。

经典方法如 AI2（ETH Zurich）、Reluplex、Marabou 用 SMT 求解器精确验证网络性质，但只能处理小网络。抽象解释方法（如 DeepPoly、Box）用区间或 zonotope 近似，能处理更大网络但精度较低。概率方法（如这篇论文）走第三条路——不追求确定性保证，而是给出概率性保证，这在统计意义上更有用。

分布近似和聚类近似的引入，让概率抽象解释框架更灵活了。你可以根据问题特点选择合适的抽象域——就像木匠根据木头硬度选不同的凿子。这种"工具箱"思路比"一刀切"方法更实际。

最后，这篇论文暗示了一个有趣的观点：神经网络的验证不必是确定性的。传统验证追求"100% 保证不会出错"，但这在实际中几乎不可能。概率验证追求"99.9% 的输入不会出错"——这更务实，也更适合部署。分布近似和聚类近似就是这种务实路线的体现：你接受近似带来的不确定性，换取可扩展性和灵活性。

在这个意义上，这篇论文不只是发明了两种新算法，更是拓展了"神经网络验证"这个概念本身的边界——从"证明"到"估计"，从"确定性"到"概率性"，从"逐点"到"逐流"。

---

论文: arXiv:2603.25273 作者: Zhuofan Zhang, Herbert Wiklicky (Imperial College London) 发布时间: 2026 年 3 月 领域: 神经网络验证 / 抽象解释 / 概率方法 开源代码: 无（理论论文，附简单示例）