线性界传播LBP

可视化演示

动态演示线性界传播LBP的核心机制，通过采集/分析/决策/反馈四种模式展示关键概念与交互流程。

概念起源：一家面包房的质检难题

如果你是一家面包房的质检员，忽然接了一张苛刻的订单：客户要求一整批面包，每一只的重量都必须落在300克的正负15克内。面粉供应商只能承诺“每袋500克，误差不超过5克”，车间温度和水质也不是恒定的。你不可能把几万袋面粉的每一种搭配都揉成面包——那样工厂要停工十年。你需要一种更聪明的验收方式：不逐个试做，而是把“所有可能的误差”装进一个数学信封里。

深度学习模型落地时遇到的是同一道题。医疗影像模型上线前，医生最担心的是：输入图片只要被噪声、光线甚至对抗扰动改动一点点，模型就把“良性”判成“恶性”？暴力测试永远只能覆盖有限个样本，而安全攸关场景需要的是数学上的保证——对一整类可能的输入给出确定性结论。这正是形式化验证（Formal Verification）登场的动机：用逻辑和代数证明“无论输入怎么变，输出都不会跨过红线”。

LBP（Linear Bound Propagation，线性界传播）就是形式化验证中最直观的一类方法。它不逐个检查输入，而是把每一层神经元可能的输出值“包”成一个区间，像账本一样逐层往后传。这套方法在认证防御（Certified Defense）中扮演质检员角色：用可证实的上下界，给模型盖下“通过”或“待查”的章。它不依赖具体攻击方式，因此不会出现“挡住攻击者A、漏掉攻击者B”的假安全感。

小李的账本，就是LBP的化身。区别只在于，账本上记的不是面团克数，而是张量每个维度上的上下界。接下来的每一节，我们都沿着这条流水线，把这本账一页页翻开。

问题建模：给一批面粉圈出范围

走进车间前，小李做的第一件事是找面粉供应商要一份“波动承诺书”：每袋面粉的克数和标签值的偏差，绝不超过5克。有了这个承诺，他才敢在账本第一页写上：所有面粉的可能重量属于 [495, 505] 克。AI验证也一样，第一步不是训练模型，而是把“输入可能怎么变”用数学语言锁死。

数学上，这个承诺被写成输入扰动域。给定原始样本 \(x_0\)（标准标签重量）和半径 \(\epsilon\)（供应商承诺的误差上限），我们关心 \(x_0\) 的 \(\epsilon\)-邻域：

仅圈出范围还不够，还要定义什么是“合格”。在分类问题中，鲁棒性属性通常表述为：对扰动域内所有输入，模型给出的真实类别分数必须严格高于其他所有类别。这等价于“每一只面包，无论面粉如何波动，都落回300±15克的合格区间”。扰动域是账本的第一页，鲁棒性属性是挂在墙上的质检标准。两者都齐了，小李才敢开始翻页。

核心原理：揉面机里的精确账本

第一道工序是揉面。配方固定：加50克水、甩掉20克损耗、再拉伸到1.2倍。每一个输入的变化都按同一个线性规则被放大或缩小。既然规则是线性的，小李的账本就能做到分毫不差——输入的波动范围有多大，算出来的新范围就有多准。

神经网络中的仿射层 \(h_i = W h_{i-1} + b\) 就是那道“揉了揉又拉长”的工序。难点在于权重矩阵 \(W\) 里的每个元素有正有负：正权重让“输入下界”产生最小的输出，负权重则让“输入下界”产生最大的输出。于是需要把权重拆成正部 \(W^+\) 和负部 \(W^-\)，再分别搭配相应的界值：

这也是“线性界”名字的由来：在仿射层上，边界跟着矩阵走，等价于把每个神经元的取值范围看作一维区间，做一次区间算术的前向传递。计算复杂度是 \(O(\text{层参数量})\)，和一次普通前向传播相当。小李在这一页上写的数字，每一克都经得起复称。真正让账本需要“留余量”的，是下一道不讲道理的发酵工序。

关键实现：发酵工序的大帐篷

发酵是不讲道理的：有的面团发不起来，重量只减不增；有的正常鼓起，重量线性上浮。真实的变化曲线是一条“先平后升”的折线——账本没法精确记一条折线。小李的解决办法是掏出一个三角形帐篷，把整条折线罩在下面。帐篷比真实范围略大，但至少保证“真实值一定在帐篷里”。

ReLU激活函数 \(f(x)=\max(x,0)\) 就是这道发酵工序。设上一层传来的区间为 \([l,u]\)，分三种情形处理：

引入过近似意味着账本记录的范围会比真实范围宽，多出来的部分叫“松弛”（slack）。松弛让验证结论可能变保守——原本安全的一批面料，账本上看着像越界。但它换来巨大的计算收益：每个神经元只需几次乘法和比较，就可以把非线性激活“线性化”，让整个网络保持可被区间算术处理的形式。帐篷比货物大一点没关系，重要的是货物一定在帐篷里。

验证判定：翻到最后一页盖质检章

经过六道工序，小李终于翻到账本最后一页。上面写着“全批次面包的可能重量：[285, 309]克”。上界309克仍低于315克红线——很好，整批放行！如果账本写的是[285, 322]克，那322越线了，不能盖章：要么真的有问题，要么某个帐篷搭得太大，需要复查。

对分类模型，验证目标被写成类别间距：

实现时，LBP把 \(f_c(x)\) 与 \(\max_{j\neq c} f_j(x)\) 的组合当作一个“输出层”，再做一次区间传播，得到间距的保守下界。若下界大于0，就拿到了数学保证：扰动域内每一个输入，模型都会给出正确类别。注意“验证未通过”和“存在对抗样本”并不等价——界太松、帐篷太大也会让下界跌破0。因此工程上往往把LBP当第一道筛子：通过了直接发“鲁棒性认证证书”；不通过再用分支定界、反例搜索等更精细的手段复核。这就好比账本上越界的面粉，未必真的超标，但稳妥起见还是要开袋复称。

局限挑战：帐篷越搭越多

流水线上有六道工序，每道都要搭帐篷。帐篷A套帐篷B，边界一层层放宽。到了最后，账本上写的是[280, 330]克——可实际上每种配方的面包都在合格范围内。小李知道，不是面包不合格，是“帐篷叠帐篷”让账本太保守了。凡是被账本拦下的批次，都得花时间复查，这就是过近似误差累积的代价。

在LBP中，仿射层不引入任何过近似误差，因此误差的唯一来源是ReLU层的三角近似。每经过一个跨零的ReLU，界就宽一点；网络越深、跨零神经元越多，松弛累积越严重。理论研究表明，在最坏情况下LBP的界可能随网络深度指数级膨胀。此外，网络权重的尺度也直接影响界的紧致性：权重越大，输入范围的放大倍数越大，后续ReLU越容易跨零，界就越松。

缓解的核心思路是让模型“训练感知验证”：在训练损失中加入LBP界宽或间距下界的惩罚项，强制网络把决策边界与扰动域拉开距离，由此得到的模型往往有显著更紧的界。代价是训练时间变长、超参数变多。工程上总要在“界紧不紧”和“算得快不快”之间权衡——这也解释了为什么LBP适合做快速初筛，而硬核认证会给它配上更重的分析器。小李的账本越保守，工厂越不敢直接依赖它。真正好用的质检方案，得让帐篷尽量贴合货物。

工程应用：把账本变成工厂SOP

故事的最后，面包房把小李的方法固化成标准作业流程：新品上线之前必须先过账本；新供应商的面粉必须附上波动承诺书；每个月写一份全品类质量报告给大客户。账本从个人绝活变成了组织能力。在AI工程里，LBP也正经历同样的“制度化”过程。

其三种典型用法是：第一，鲁棒性认证。模型发布前，对测试集每个样本计算给定半径 \(\epsilon\) 下的验证结果，汇总成“认证鲁棒率”（Certified Robust Accuracy），写进模型卡，让使用方明确知道“这个模型在多大扰动下保证不变”。

第二，对抗防御评估。对抗训练等防御方法效果如何？只看普通准确率会被攻击强度欺骗——攻击不够强时，防御模型看似准确率很高。用LBP认证得到的鲁棒率不依赖攻击方式，是更可信的横向对比指标。第三，模型筛选与监控。在数据可信层，对候选模型批量运行LBP，挑选稳健者上线，再对线上输入扰动情况定期复核。开源工具链如ERAN、\(\alpha,\beta\)-CROWN 已经把LBP工程化，支持CNN、Transformer等主流架构，并用GPU加速和分支定界大幅提升可扩展性。从一张手写账本到一套自动化质检SOP，LBP完成了从论文到生产线的旅程。下次有人问“AI被对抗样本骗了怎么办”，你可以递上这本账本。

AI 应用场景

Python 演示

# -*- coding: utf-8 -*-"""LBP 线性界传播的玩具实现: 验证两层ReLU网络在输入扰动下的鲁棒性"""import numpy as np  class ToyNet:    """2维输入 -> 3个隐层神经元(ReLU) -> 2类输出"""     def __init__(self):        self.W1 = np.array([[1.0, -0.5],                            [-1.0, 0.8],                            [0.6, 0.6]])        self.b1 = np.array([0.2, 0.1, -0.1])        self.W2 = np.array([[1.0, -1.0, 0.5],                            [-0.5, 0.8, -1.0]])        self.b2 = np.array([0.1, 0.2])     def forward(self, x):        h = np.maximum(0, self.W1 @ x + self.b1)        return self.W2 @ h + self.b2     def margin(self, x):        out = self.forward(x)        return out[0] - out[1]     def lbp_margin_lb(self, x0, eps):        """返回 margin 的 LBP 保守下界"""        l0 = x0 - eps        u0 = x0 + eps        # 第1层: 仿射精确传播        pos_w = np.maximum(self.W1, 0.0)        neg_w = np.minimum(self.W1, 0.0)        l1 = pos_w @ l0 + neg_w @ u0 + self.b1        u1 = pos_w @ u0 + neg_w @ l0 + self.b1        # ReLU: 三角过近似        l2 = np.where(l1 >= 0, l1, 0.0)        u2 = np.where(u1 <= 0, 0.0, u1)        # 输出层: 先对margin做线性组合, 再精确传播        w_m = self.W2[0] - self.W2[1]        b_m = self.b2[0] - self.b2[1]        pos_wm = np.maximum(w_m, 0.0)        neg_wm = np.minimum(w_m, 0.0)        ml = pos_wm @ l2 + neg_wm @ u2 + b_m        return ml     def lbp_verify(self, x0, eps):        ml = self.lbp_margin_lb(x0, eps)        return ml > 0, ml  def mc_estimate(net, x0, eps, n=20000):    """蒙特卡洛采样估计, 只作对比, 不能给出保证"""    cnt = 0    rng = np.random.default_rng(42)    for _ in range(n):        x = x0 + rng.uniform(-eps, eps, size=x0.shape)        if net.margin(x) > 0:            cnt += 1    return cnt / n  def main():    net = ToyNet()    x0 = np.array([0.5, -0.3])    for eps in [0.1, 0.2, 0.35, 0.5]:        ok, ml = net.lbp_verify(x0, eps)        rate = mc_estimate(net, x0, eps)        print("eps=%.2f margin_lb=%.4f verified=%s mc_rate=%.2f%%"              % (eps, ml, ok, rate * 100))  if __name__ == "__main__":    main()

1. pos_w = np.maximum(self.W1, 0.0)把权重矩阵切成“正部”，负权重补零，这是仿射层界传播的基石。
2. l1 = pos_w @ l0 + neg_w @ u0 + self.b1正权重乘下界、负权重乘上界，加偏置得到新的下界。
3. u1 = pos_w @ u0 + neg_w @ l0 + self.b1正权重乘上界、负权重乘下界，对称地得到新的上界。
4. l2 = np.where(l1 >= 0, l1, 0.0)ReLU的三角近似下界：完全导通时保留原值，其余情况一律截到0。
5. u2 = np.where(u1 <= 0, 0.0, u1)ReLU的三角近似上界：完全关闭时为0，否则保留原上界。
6. w_m = self.W2[0] - self.W2[1]把“类别间距”合并成一个线性层，再走一次精确的仿射传播。
7. ml = pos_wm @ l2 + neg_wm @ u2 + b_m得到margin的保守下界，大于0即可通过验证。
8. if net.margin(x) > 0:蒙特卡洛采样逐个判断，只能给出概率估计，无法覆盖全部输入。
9. for eps in [0.1, 0.2, 0.35, 0.5]:逐步加大扰动半径，观察LBP验证从通过到拒绝的临界变化。

常见误区

面试题