🤖 machine learning

Formally Verifying Analog Neural Networks Under Process Variations Using Polynomial Zonotopes

本文提出了一种基于多项式 zonotopes 和多项式模型的模拟神经网络工艺变化形式化验证方法，该方法在不依赖蒙特卡洛模拟的情况下，能够准确覆盖 99% 的变化样本，并将验证时间从数天显著缩短至数秒。

原作者： Yasmine Abu-Haeyeh, Tobias Ladner, Matthias Althoff, Lars Hedrich

发布于 2026-05-12

📖 1 分钟阅读☕ 轻松阅读

原作者： Yasmine Abu-Haeyeh, Tobias Ladner, Matthias Althoff, Lars Hedrich

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一下，你正在用微小的电子电路而非软件代码，构建一个超高速、高能效的大脑。这就是模拟神经网络的承诺。与你手机中使用严格“开/关”开关（0 和 1）的数字计算机不同，这些模拟电路利用平滑流动的电流来模仿真实神经元的工作方式。它们速度极快且耗电极少，使其成为可穿戴设备和传感器的理想选择。

然而，其中有一个陷阱。因为这些是由沙子（硅）制成的物理电路，它们对制造工艺极其敏感。这就好比烘焙蛋糕：即使你完美地遵循了食谱，烤箱温度的微小波动、湿度的变化或量勺尺寸的细微差别，都可能改变最终结果。在芯片制造中，这些“差异”意味着没有两个晶体管是完全相同的。一个可能稍宽，另一个可能稍厚。

对于数字计算机而言，微小的差异无关紧要；1 仍然是 1。但对于模拟大脑，微小的差异可能导致整个系统做出错误的判断。

问题：“蒙特卡洛”陷阱

为了确保这些模拟大脑在存在制造缺陷的情况下仍能正常工作，工程师通常使用一种称为蒙特卡洛模拟的方法。

想象你想知道一座新桥能否在风暴中屹立不倒。传统的方法是建造一个模型，然后用略微不同的风速和降雨强度模拟风暴 1,000 次。你反复这样做，以观察桥梁是否会倒塌。

论文的主张：对模拟神经网络这样做，就像试图为复杂大脑的每一层都模拟 1,000 次风暴。这需要数天的计算时间。对于简单的图像识别任务（如识别手写数字），论文指出，研究人员在标准计算机上运行这些模拟就花费了近29,000 秒（约 8 小时）。

解决方案：“多项式 Zonotope"

这篇论文的作者提出了一种更聪明的方法。与其模拟风暴 1,000 次，不如创建一个数学地图，一次性覆盖所有可能的风暴。

以下是他们如何做到的，分解为简单步骤：

1. 找出“主要元凶”
首先，他们检查了电路，意识到虽然有许多变量可能出错（如导线厚度或电压），但只有两个特定变量实际上造成了最大的麻烦。这就像意识到在汽车中，只有轮胎压力和发动机温度真正关乎安全；座椅的颜色则无关紧要。他们将注意力集中在这两个“主导”因素上。

2. 为误差创建“形状”
他们不使用检查单个点的方法，而是使用一种称为多项式 Zonotope的数学形状。

类比：想象你试图捕捉一群飞行模式混乱且不可预测的鸟。
- 旧方法（蒙特卡洛）：你试图一只一只地抓鸟。这需要永恒的时间，而且你可能会漏掉几只。
- 新方法（多项式 Zonotope）：你张开一张巨大的、灵活的、透明的网，覆盖整个鸟群。这张网被塑造成完美地包裹住鸟群的移动，并考虑了风（制造差异）如何推动它们。
- 这张“网”就是多项式 Zonotope。它是一种特殊的形状，能够弯曲和扭曲以适应误差所采取的复杂曲线路径，而更简单的形状（如直盒子）则无法做到这一点。

3. “验证”测试
一旦拥有了这张网，他们就不需要模拟电路数千次。他们只需检查：“这张网是否保持在‘安全区’内？”

如果这张网（代表所有可能的结果）从未触及“不安全区”（大脑会犯错的地方），那么无论制造如何变化，该电路都保证是安全的。

结果：从数天到数秒

论文在三个不同的任务上测试了这种方法：

乳腺癌检测：区分良性肿瘤和恶性肿瘤。
鸢尾花分类：识别不同类型的鲜花。
MNIST：识别手写数字（0-9）。

结果：

速度：旧方法需要数小时甚至数天。新方法仅需数秒。
- 对于手写数字（MNIST），旧方法耗时约 8 小时。新方法仅需1.77 秒。
准确性：新方法极其精确。它成功“捕捉”了**99%**的所有可能变化。换句话说，如果你制造 100 个这样的芯片，这张数学网保证其中 99 个能正常工作。

为什么这很重要（根据论文）

作者强调，这不仅仅是关于速度；更是关于可行性。

可扩展性：由于该方法如此快速，工程师现在可以设计更大、更复杂的模拟大脑，而无需等待数周进行验证。
鲁棒性：它允许设计人员确切地看到芯片在失效前能处理多少变化。例如，他们发现，虽然具有微小变化（1 或 2 个标准差）的芯片仍然工作良好，但具有巨大变化（3 个标准差）的芯片开始失效。这有助于设计人员确定界限。

总结

简而言之，这篇论文提出了一种新的“数学网”（多项式 Zonotope），使工程师能够在数秒内而非数天内验证模拟神经网络的安全性。通过关注最重要的制造缺陷并将它们包裹在灵活的数学形状中，他们证明了这些高能效电路即使在由不完美材料制造时，也能被信任正常工作。

技术摘要：基于多项式 Zonotopes 的工艺变化下模拟神经网络的形式化验证

问题陈述

与数字对应物相比，模拟神经网络（ANNs）在功耗、处理速度和芯片面积方面具有显著优势，使其成为能源受限的物联网（IoT）应用的理想选择。然而，作为物理电路，ANNs 极易受到制造工艺变化（如栅极宽度、阈值电压、氧化层厚度）的影响。这些变化会导致其偏离标称模型，从而可能损害网络的安全性和准确性。

传统的验证方法依赖耗时的蒙特卡洛（Monte Carlo）模拟来验证电路在这些变化下的功能。对于复杂的网络（如卷积神经网络 CNNs），此类模拟可能需要数天才能完成，从而在设计周期中形成了瓶颈。此外，现有的建模方法往往无法捕捉完整的系统级行为，或缺乏跨不同网络架构的可扩展性。

方法论

作者提出了一种形式化验证框架，利用基于集合的可达性分析（使用多项式 Zonotopes）来替代蒙特卡洛模拟。该方法包含三个主要阶段：

1. 灵敏度分析与参数缩减

作者使用 PSP 晶体管模型分析了 130 nm CMOS 模拟神经元电路。通过对 50 多个工艺参数的灵敏度分析，他们发现只有两个主导参数（ $\phi_1$ 和 $\phi_2$ ）——即影响 NMOS 晶体管表面电位的参数——会显著影响电路性能。其他参数被发现影响微乎其微，或者被电路拓扑结构（例如电流镜）所抑制。

2. 基于多项式的参数化建模

作者推导了一个多项式模型来抽象神经元的行为，而不是针对每种变化模拟完整的电路物理特性。

权重建模： 权重（ $\tilde{W}_k$ ）被建模为主导参数 $\phi_1$ 和 $\phi_2$ 的三阶多项式。
偏置与噪声： 偏置项被视为可忽略，而剩余的微小变化由单个三阶噪声符号（ $d_3$ ）捕获。
公式化： 网络行为被表示为这些参数的函数，使得权重可以表示为集合而非固定值。具体而言，权重建模为：
$\tilde{W}_k = \sum_{i=0}^{3} \sum_{j=0}^{3} A_{k,i,j} \phi_1^i \phi_2^j + d_3$
其中系数是通过对每个量化权重的蒙特卡洛数据进行多项式回归确定的。

3. 基于多项式 Zonotopes 的可达性分析

验证过程使用多项式 Zonotopes将输入集合通过网络进行传播，这是一种能够处理变量间依赖关系的集合表示法。

集合传播： 输入集合逐层传播。线性层涉及与多项式权重集合的矩阵乘法。
非线性处理： ReLU 激活函数使用集合计算的标准技术进行包裹（enclosed）。
验证： 对最终输出集合进行包裹。如果该包裹不与“不安全”输出集合（例如错误的分类边界）相交，则该网络在指定的变化范围（例如 $\pm 3\sigma$ ）内被形式化验证为安全。

主要贡献

优化的多项式模型： 一种参数化模型，仅使用两个主导参数和一个噪声项，精确抽象了工艺变化下的模拟神经元性能，在保持准确性的同时降低了复杂度。
系统级形式化验证： 将基于多项式 Zonotopes 的可达性分析应用于工艺变化下的电路级模型验证，避免了 exhaustive 蒙特卡洛模拟的需求。
可扩展性： 该方法被证明在不同架构中具有可扩展性，包括全连接和卷积神经网络（CNNs）。
效率： 该方法大幅减少了验证时间，同时包裹了高比例的变体样本。

实验结果

该方法在三个数据集上进行了评估：威斯康星乳腺癌数据集、鸢尾花（Iris）数据集和 MNIST 数据集（包括全连接和 CNN 架构）。

验证时间： 所提出的方法将验证时间从数天缩短至数秒。
- MNIST CNN： Cadence 蒙特卡洛模拟耗时约 29,592 秒（约 8.2 小时）；所提出的方法耗时 3.37 秒。
- Iris： 模拟耗时约 865 秒；所提出的方法耗时 1.15 秒。
包裹精度： 多项式 Zonotope 包裹在所有数据集中成功捕获了约 99% 的蒙特卡洛变体样本（范围从 97.77% 到 99.51%）。
模型必要性： 一项将多项式 Zonotopes 与标准 Zonotopes（线性松弛）进行比较的消融研究表明，线性模型是不够的。标准 Zonotopes 产生的包裹跨越了决策边界，无法验证安全性，而多项式 Zonotopes 提供了紧密的包裹，成功验证了规范。

意义与主张

该论文声称其主要意义在于能够在计算可行的时间范围内实现工艺变化下模拟神经网络的形式化验证。通过将统计模拟（蒙特卡洛）转变为确定性基于集合的分析，作者实现了：

快速设计周期： 设计人员可以快速评估模拟电路对制造变化的鲁棒性，而无需等待数天的模拟。
安全保证： 该方法提供了形式化保证，即网络将在指定的变化范围内（例如 99% 的样本）正确运行，这对于安全关键的物联网应用至关重要。
鲁棒性评估： 该方法允许量化多少制造出的电路可能存在故障（例如，识别出偏离超过 $2\sigma$ 的电路可能会失去准确性），从而指导对更鲁棒电路设计的需求。

作者指出，虽然当前的模型相对较小，但这主要是模拟电路物理鲁棒性的限制，而非验证方法本身的限制。他们得出结论，这种方法可以显著加快更大、更鲁棒的模拟推理电路的设计周期。