神经网络的形式化验证：从抽象解释到 SMT 驱动的鲁棒性证明

在自动驾驶的视觉感知模块被一个像素的扰动欺骗、信贷审批模型对特定群体隐性歧视、对话模型被精心构造的提示词越狱之后，工程师们开始意识到：测试通过不等于系统正确。当 AI 系统从辅助工具升级为核心基础设施，我们需要比准确率、F1 值更严格的保证——数学意义上的正确性证明。

一、为什么 AI 系统需要形式化验证？

传统软件测试的覆盖率理论建立在程序逻辑有限且确定的事实之上。一个 Web 服务的输入空间可以被等价类划分和边界值分析覆盖，但深度神经网络的输入空间是连续且高维的：一张 224×224 的 RGB 图像拥有 250,880 个像素通道值，其输入空间大小为 256^150,528，穷举测试在宇宙寿命内都不可能完成。

更深层的问题在于神经网络的行为不可分解。传统程序的正确性可以通过分解为函数、模块、类来分别验证，而深度网络是典型的黑箱系统——数百万参数共同决定输出，单个神经元的行为无法独立解释。面对这种系统，我们需要一种能从全局角度保证性质成立的验证方法。

形式化验证的核心思想是：用数学语言描述系统应满足的性质，然后用严密的数学推理证明这些性质对所有允许的输入都成立。这意味着穷举所有可能的输入而非采样，给出\"不存在反例\"而非\"未发现反例\"的保证。

二、规格描述：我们到底要验证什么？

在动手写验证器之前，首先需要用精确数学语言描述\"正确性\"。神经网络验证领域已经发展出几类核心规格：

2.1 局部鲁棒性（Local Robustness）

给定输入 x 和分类结果 c，保证所有在 x 的 ε-邻域内的输入 x'（‖x' - x‖_p ≤ ε）都被分类为 c。这是对抗样本防御的数学基础。

∀x' : ‖x' - x‖_∞ ≤ ε → argmax(f(x')) = argmax(f(x))

2.2 安全不变量（Safety Invariants）

对于给定的安全约束集合 S，保证网络在任何合法输入下都不违反约束：

∀x ∈ S : g(f(x)) ≤ 0

其中 g 是安全约束函数。典型场景包括自动驾驶中\"障碍物距离必须大于安全阈值\"。

2.3 公平性约束（Fairness Constraints）

形式化公平性要求模型在不同人口群体上的行为满足统计平价或均等赔率：

|P(ŷ=1|z=0, y=1) - P(ŷ=1|z=1, y=1)| ≤ δ

其中 z 是受保护属性，y 是真实标签，ŷ 是预测标签，δ 是可接受偏差。

三、抽象解释：可扩展验证的数学框架

抽象解释（Abstract Interpretation）是形式化验证的核心理论框架，由 Patrick Radhia Cousot 在 1977 年提出。其核心思想很简单：与其在具体域（如实数向量组成的输入空间）上执行计算（不可行），不如在一个精心选择的抽象域上执行，使得抽象计算既足够高效、又能给出真实计算的上近似。

3.1 区间抽象域

最简单的抽象域是区间抽象：每一维神经元值用区间 [l, u] 表示。考虑 ReLU 激活函数：

def relu_abstract(l, u):     \"\"\"区间传播经过 ReLU 抽象转换\"\"\"     return max(0, l), max(0, u)

区间传播虽然计算高效（每层只需线性时间），代价是松弛过大——它无法捕捉神经元之间的相关性，导致对深层网络的验证结果过于保守。

3.2 Zonotope 抽象域

Zonotope（区域体）是区间抽象的推广，它通过噪声符号 ε_i 追踪神经元之间的线性关系：

x̂ = c   Σ α_i · ε_i    where α_i ∈ [-1, 1]

import numpy as np  class Zonotope:     \"\"\"Zonotope 抽象域：中心向量   生成器矩阵\"\"\"     def __init__(self, center, generators):         # center: shape (n,)         # generators: shape (n, m)，每列是一个噪声符号的系数         self.c = center         self.G = generators      def relu_abstract(self):         \"\"\"Zonotope 上的 ReLU 抽象转换\"\"\"         n = self.c.shape[0]         new_G = np.hstack([self.G, np.zeros((n, 1))])         new_c = self.c.copy()          for i in range(n):             l, u = self.bounds_of(i)             if l