概率神经符号系统的可扩展鲁棒性验证：松弛近似的胜利

论文概览

神经符号（NeSy）AI 把神经网络感知和符号推理结合起来，在自动驾驶、医疗等关键领域被视为"既能泛化又能解释"的希望之星。但概率型 NeSy 系统——神经网络先从图像中抽取离散概念，概率逻辑推理层再基于这些概念做推理——的鲁棒性验证一直是个硬骨头。本文研究的核心问题是：

给定一个概率 NeSy 系统和一个输入扰动 $\epsilon$，如何形式化地验证：所有 $\epsilon$-邻域内的输入都不会改变系统的概率推理输出？

Lomuscio 团队（Imperial + NCSR Demokritos）给出的回答分三步：

1. 理论分析：精确求解的核心计算 E-WMC 是 NP^PP-完备（复杂度类在多线性多项式顶点展开与 #P 计数预言机之间），因此精确验证不可行；
2. 方法突破：把整个 NeSy 系统（NN + 算术电路形式的概率逻辑）编译成单一可微计算图，导出 ONNX，直接喂给现成的 NN 验证器（autoLiRPA），用 IBP（区间传播） 在端到端层面做松弛近似；
3. 实验验证：在多位数 MNIST 加法基准上比求解器方法指数级更快；在 ROAD-R 自动驾驶真实数据集上成功验证了一个由两个 6 层 CNN 构成的安全系统，3×240×320 行车记录仪图像，验证耗时仅 ~0.09 s/样本。

[译注]：Lomuscio 是 NN 验证领域的资深学者（Reluplex、VeriNet 等都出自其组），与 AARM 框架关注的形式化保证方向高度契合。本文最值得玩味的不是又一个验证工具，而是它揭示的"NeSy 系统的精确验证天然 NP^PP 难"——这是该方向第一个正式的复杂度上界。

核心贡献

概率 NeSy 系统：背景与问题

一个概率 NeSy 系统分两步工作（Marconato et al. 2024）：

1. 感知层：神经网络 $p_\theta(c \mid x)$ 从输入 $x \in \mathbb{R}^n$ 抽取 $k$ 个潜在概念的离散概率；
2. 推理层：用符号知识 $K$（一般是概率逻辑公式）做推理，得到 $p(y \mid c; K)$。

输出 $y$ 是查询的概率。系统的关键特征是整个计算图是可微的——这是把松弛传播推过去的代数基础。

鲁棒性定义

给定输入 $x$ 与扰动半径 $\epsilon$，鲁棒性即要求所有 $x' \in \mathbb{B}_\epsilon(x)$ 都保持相同输出。形式化上要计算：

\left[ \min_{x'}\, p(y_i \mid x'),\ \max_{x'}\, p(y_i \mid x') \right]\quad \forall x' \text{ s.t. } \|x' - x\| \leq \epsilon \tag{2}

[译注]：式 (2) 是松弛验证的"目标函数"——只要每个输出类的概率区间都和真实标签保持一致，且最小值仍大于阈值 $T$，实例就鲁棒。本文取 $T=0.5$。

知识编译 + WMC：NeSy 推理的算术化

概率 NeSy 系统的推理通常用加权模型计数（WMC） 归约：

\mathrm{WMC}(\varphi, p) = \sum_{\omega \models \varphi} \prod_{i \in \omega} p_i \prod_{i \notin \omega} (1 - p_i) \tag{1}

• $\varphi$ 是命题逻辑公式；
• $p_i$ 是变量 $v_i$ 为真的概率；
• $\omega$ 是满足 $\varphi$ 的世界（赋值）。

WMC 通过知识编译（KC） 高效求解：先把 $\varphi$ 编译成决定性图（SDD） 等"易处理表示"，再在推理阶段用算术电路（AC） 把布尔运算转成算术运算：

这就是所谓的 NAT 半环（Maene and De Raedt 2025）。编译一次后可摊销大量查询——这是 NeSy 系统运行时高效的根源。

E-WMC：精确求解为什么 NP^PP 难？

要把 NN 输出（已经被 IBP 推成概率区间）传到符号层，核心问题是 E-WMC（"存在" WMC）：

定义 1（E-WMC） 给定布尔公式 $\varphi(v)$、变量概率区间 $I_i = [l_i, u_i] \subseteq [0,1]$、阈值 $T$，是否存在 $w \in I_1 \times \dots \times I_k$ 使 $\mathrm{WMC}(\varphi, w) \geq T$？

命题 2：E-WMC 是 NP^PP-完备。

• 上界（NP 成员）：算术电路是变量的多线性多项式（Choi et al. 2020），多线性多项式在闭区间上极值在顶点取得（Laneve et al. 2010），所以搜索空间是 $2^n$ 个顶点组合，每次检查是 #P 查询。组合搜索（NP 部分）+ #P 预言机 = NP^#P = NP^PP（Monniaux 2022）。
• 下界（NP 困难）：从 E-MAJSAT 归约——这是概率规划的 SAT 完备问题。

[译注]：NP^PP 比 NP 高一阶（含 #P 计数），比 PSPACE 低（包含 PP）。它的直观含义是"在组合空间里搜，每次搜都要做计数查询"——NeSy 验证天生落在这里。

框架总览：端到端松弛传播

精确传播不可行 → 论文的解法是把 NeSy 系统的神经部分和算术电路部分统一编为单一可微计算图，再导出 ONNX：

整个流程（左→右）：

1. 输入层：$x \in \mathbb{R}^n$，扰动 $\|x' - x\| \leq \varepsilon$；
2. 神经感知层（可多个）：$p_\theta(c \mid x)$ → 概率向量；
3. 概率逻辑层：知识编译（SDD）→ 算术电路（AC）→ $\mathrm{WMC}(\varphi, p)$；
4. 整体编译：把 NN+AC 编为单一 ONNX 图；
5. 验证器复用：autoLiRPA（IBP 松弛）/ Marabou（SMT 精确）/ R+SLV（混合）；
6. 输出：$\left[\min\,p(y \mid x'), \max\,p(y \mid x')\right]$；实例鲁棒当且仅当 $\min > 0.5$。

关键洞察

• 代数一致性：算术电路只是多线性多项式，与 NN 的代数结构天然兼容，可以端到端反向传播；
• 摊销开销：编译一次（KC）→ 多次区间查询 → 适合大规模数据集；
• 工具复用：导出 ONNX 直接对接所有主流 NN 验证器，避免重复造轮子。

实验 1：多位数 MNIST 加法

任务：每个样本是若干张 MNIST 数字图像，系统把它们加起来求和（参见 Manhaeve et al. 2018 的 DeepProbLog 设置）。CNN 识别单数字（98% 准确率），逻辑层用 KC 编译多位数加法规则。#digits 越大，符号电路越复杂。

基线：

• E2E-R：本文方法，端到端 autoLiRPA+IBP；
• R+SLV：混合方法——NN 部分用 IBP，符号部分把 AC 转多项式交给 Gurobi 解约束优化；
• Marabou：精确 SMT 验证器，但当前版本不支持 Softmax 与张量索引——所以只能验证 CNN 子任务。

可扩展性（图 2，对数坐标）：

观察：

• R+SLV 在 $\epsilon = 10^{-2}$ 下，#digits=5、6 时全部超时（72h 单样本），#digits=6、$\epsilon = 10^{-3}$ 时<5% 样本在超时内完成；
• E2E-R 三种 $\epsilon$ 下的运行时间都在 0.01–0.3 s 量级，与 R+SLV 差距随 #digits 增大呈指数级扩大；
• Marabou 仅 CNN 子任务（不包含符号层）即需 314 s/样本——比 E2E-R 慢 4 个数量级。

结果质量（表 1，$\epsilon = 0.001$）：

[译注]：E2E-R 区间略宽（误差累积在端到端图上传播），但鲁棒率几乎与 R+SLV 重合——说明在工程意义上，松弛带来的精度损失可以忽略。这是松弛验证的核心价值：极少精度的代价，换来指数级的可扩展性。

实验 2：ROAD-R 自动驾驶

把方法搬到真实场景。ROAD-R（Giunchiglia et al. 2023）是 22 段行车记录仪视频的逐帧标注（边界框）。安全属性：

$\phi_1: \text{red light} \lor \text{car in front} \Rightarrow \text{brake}, \quad \phi_2: \text{accelerate} \Leftrightarrow \neg \text{brake}$

实验选 3143 帧，标签为 4 个二值量（红灯/前车/停车/前进）。系统结构：

• 目标检测 CNN：6 层卷积（4 conv + max-pool + 2 linear + sigmoid），准确率 97.2%；
• 动作选择 CNN：6 层卷积（4 conv + max-pool + 2 linear + softmax），准确率 96.3%；
• 输入：3×240×320 图像（标准行车记录仪分辨率）。

结果（表 2）：

观察：

• 鲁棒率随扰动增长急剧下降——这正是神经网络易受攻击的体现；
• 验证耗时几乎与扰动大小无关（~0.09 s），证明松弛传播的计算开销主要花在网络层数上，而不是扰动范围；
• E2E-R 与 R+SLV 在此任务上结果几乎相同（论文省略）——因为符号电路小、神经部分占主导，松弛在 NN 层已有控制。

[译注]：这个"验证耗时与扰动无关"的现象很重要。工程上意味着一旦模型部署上线，验证预算就基本固定——不像求解器方法那样被扰动大小严重影响。

相关工作对比

核心差异：本文第一个支持概率逻辑语义的 NeSy 验证——之前的工具只能验证确定性逻辑。代价是松弛（不完备），但通过 KC 把 WMC 嵌进 AC，再把 AC 视作多线性多项式，与 NN 的代数流无缝衔接。

启示与思考

1. 复杂度诚实性比"看起来完整"更重要

NP^PP-完备的判据让"完整验证 NeSy"在理论层面被宣判死刑。这个判据不是工程限制，而是结构性障碍。承认这一点，论文才有底气转向松弛并讨论精度权衡。

2. 知识编译是 NeSy 系统的"系统边界"

KC 的核心价值是把"模型"和"查询"分离——编译一次、查询 N 次。这与 AARM 框架的"意图授权 / 执行隔离 / 副作用验证"分层思想同构：编译产物是可重用的中间表示，对应 AARM 里的规范层。

3. 松弛的工程意义远超理论

E2E-R 的鲁棒率与 R+SLV 几乎一致（差距<2%），但速度指数级快。这意味着在自动驾驶这种实时性约束的场景，松弛验证是唯一可行的工程路径。

4. 对 AARM 框架的潜在价值

• WMC 形式化可作为"数据学习行为模型"的形式化底座——L3 副作用验证若用概率逻辑约束表达，复杂度就锁定在 NP^PP 这一类；
• 可微计算图 + IBP 与 AgentMonitor 的"事件溯源 + 区间传播"思路同构；
• AC → ONNX 编译 模式可作为"工具链适配"的方法论——不要为新逻辑重写验证器，让主流工具直接消费。

参考

• 论文：Manginas et al. A Scalable Approach to Probabilistic Neuro-Symbolic Robustness Verification. NeSy 2025, PMLR.
• arXiv：2502.03274v2 (29 Jul 2025)
• 代码：https://github.com/EVENFLOW-project-EU/nesy-veri
• 资助：EU Horizon EVENFLOW (101070430) + Royal Academy of Engineering Chair

关键参考文献

• Chavira & Darwiche (2008). On probabilistic inference by weighted model counting. AIJ.
• Choi, Vergari, Van den Broeck (2020). Probabilistic circuits: A unifying framework. UCLA Tech Report.
• Darwiche & Marquis (2002). A knowledge compilation map. JAIR.
• Ehlers (2017). Formal verification of piece-wise linear feed-forward neural networks. ATVA.
• Giunchiglia et al. (2023). ROAD-R: the autonomous driving dataset with logical requirements. Machine Learning.
• Henriksen & Lomuscio (2020). Efficient neural network verification via adaptive refinement and adversarial search. ECAI.
• Katz et al. (2017). Reluplex: An efficient SMT solver for verifying deep neural networks. CAV.
• Katz et al. (2019). The Marabou framework for verification and analysis of deep neural networks. CAV.
• Littman, Goldsmith, Mundhenk (1998). The computational complexity of probabilistic planning. JAIR.
• Manhaeve et al. (2018). DeepProbLog: Neural probabilistic logic programming. NeurIPS.
• Monniaux (2022). NP^#P = ∃PP and other remarks about maximized counting.
• Wong et al. (2018). Scaling provable adversarial defenses. NeurIPS.
• Xu et al. (2020). Automatic perturbation analysis on general computational graphs (autoLiRPA). arXiv:2002.12920.