当神经网络遇见概率抽象解释：用分布与聚类丈量不可丈量之物
一座你想保护的城市
想象你是一座城市的防空指挥官。城里有几百万栋建筑，每栋建筑都可能受到不同强度的冲击。你不可能逐栋建筑去模拟——那太慢了；你也不能只看一栋就下结论——那太冒险了。你需要的是一张"概率地图"：哪些区域在哪些冲击强度下会怎样变形，整个城市的脆弱性分布是什么样的。
神经网络验证面临的就是这个问题。一个训练好的神经网络接受输入、产出输出，但输入空间是连续的、无限的——所有可能的图像、所有可能的文本、所有可能的扰动。你想知道的不是"这张熊猫图片会被分类成什么"，而是"所有看起来像熊猫的图片，被这个网络分类后，输出分布是什么样"。
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\|)$，整体拟合是这些钟形函数的加权和：
$$y = \sum_{i=1}^{N} a_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$ 个高斯分布的加权和：
$$p(x|\lambda) = \sum_{k=1}^{K} w_k \mathcal{N}(x|\mu_k, \Sigma_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 月 领域: 神经网络验证 / 抽象解释 / 概率方法 开源代码: 无（理论论文，附简单示例）