Verifying Neural Networks with Reinforcement Learning¶

会议: NeurIPS 2026
arXiv: 2609.34553
领域: 强化学习
关键词: 神经网络验证、分支定界、启发式重加权、双后继强化学习、图神经网络

一句话总结¶

Rsb 用图结构观测与 actor-critic 学习重加权 Fsb 的神经元分支分数，在不替代验证逻辑的前提下，将 600 个困难测试实例中的求解数量从 148 提高到 165，但奖励定义、特征掩码和部分统计存在原文不一致，需与性能收益分开理解。

研究背景与动机¶

神经网络形式化验证不是检查若干测试输入，而是判断给定输入集合内是否存在违反输出性质的输入。分支定界（branch-and-bound，BaB）先用抽象计算界；如果当前界无法排除反例，就将一个不稳定神经元的状态进一步固定，产生两个子问题。对 ReLU 而言，不稳定意味着激活前区间跨过零，因此需要区分激活与不激活两种情况。界计算负责证明，分支选择则决定证明需要走多远，两者不能混为一谈。

Fsb 根据潜在界改善给候选神经元打分，是成熟验证器中常用的分支启发式。其困难不在于完全没有专业知识，而在于局部界改善未必对应更小的后续搜索树：某个分支只消除一个局部不确定性，另一个分支却可能同时稳定多个下游神经元。直接学习一个替代打分器容易丢失已有启发式积累的知识，也需要应对网络大小变化、候选集收缩和昂贵的验证交互。

本文因此选择学习已有分数的修正，而不是重新实现验证器。GNN 提供神经元之间的结构关联，局部区间特征反映当前性质与分支约束，策略再根据后续搜索的反馈改变候选优先级。核心 idea：让学习负责“先分谁更省搜索”，让已有可靠验证器继续负责“是否真的证明了性质”，并在价值学习中同时考虑一次分支产生的两个后继。

方法详解¶

整体框架¶

输入是待验证网络、输入约束、输出性质和当前累计分支约束；输出仍是原验证器的性质判定，而不是 actor 的分类预测。对尚未被界计算解决的子问题，Rsb 构造候选观测，生成权重，与 Fsb 分数逐项相乘，然后选择最高分神经元进行分支。两个子问题仍交给原有界计算与队列管理处理。

训练与验证推理需要明确分开。训练时，GCN 先用 Fsb 分数做监督预训练，actor 与双 critic 再从验证交互的双后继经验中学习；测试时权重冻结，没有逐网络微调，critic 和奖励也不承担性质判定。下面实线表示验证数据流，虚线表示训练监督或参数更新。

%%{init: {'flowchart': {'rankSpacing': 24, 'nodeSpacing': 28, 'padding': 6, 'wrappingWidth': 400}}}%%
flowchart TD
    I["网络、性质<br/>当前分支约束"] --> A["结构增强观测"]
    S["Fsb 分数<br/>仅 GCN 预训练监督"] -.-> A
    A --> B["可变长分数重加权"]
    H["当前 Fsb 分数"] --> B
    B --> D["原验证器<br/>分支并计算两侧界"]
    D -->|未解决子问题| A
    D --> O["证明、反例<br/>或预算耗尽未决"]
    D -.->|训练奖励与双后继| C["双后继价值学习"]
    C -.->|仅训练更新 actor| B

图中的三个设计依次对应观测、动作和价值学习；原验证器是保留的脚手架，不是本文新发明的证明模块。策略可以改变将要分支的神经元，但不能把一个界仍未解决的子问题自行宣布为已证明。

关键设计¶

1. 结构增强观测：同时看当前区间和神经元关联

同一网络面对不同输入域或输出性质，隐藏层区间可能不同，所以单纯缓存一个静态拓扑嵌入不足以描述验证状态。本文将所有神经元作为图节点，网络连接作为边，以激活前下界、上界、偏置和二值掩码作为节点原始特征。GCN 在不稳定神经元上回归 Fsb 分数，预训练目标是均方误差；随后取这些候选节点的嵌入供策略使用。这不是拿“正确分支标签”监督 actor，而是先让结构表示吸收已有启发式的信号。

原始特征只有 4 维，而结构嵌入更宽。论文先把原始特征投影到嵌入宽度，再与 GCN 嵌入拼接并再次投影，避免局部区间信息在高维结构表示中被弱化。最终策略输入只保留当前不稳定候选，因此网络规模与每轮候选数量可以变化；但 GCN 图包含所有神经元，不能据此宣称整体计算只发生在候选子图上。

这里有一个实际影响复现的命名问题：示例明确写掩码为“不稳定取 1、稳定取 0”，附录 Table 3 也称其为 unstable mask；§4 和 §5.1 又描述为已分支状态。稳定性和历史分支状态不是一般意义上的同一个变量，不能把这些表述悄悄统一。本笔记采用“二值神经元掩码”这一中性名称，记录两种定义；没有代码证据，不能确定实际实现选择了哪一种。它也不能与训练中表示后继是否继续搜索的掩码混用。

2. 可变长分数重加权：保留 Fsb 知识，只改变优先级

actor 使用 PointerNet 式编码器—解码器，而非固定维度输出层。编码器读取候选观测，解码器查询候选引用向量，经注意力得到每个候选的权重；附录还说明使用 LSTM、attention glimpses、截断到正负 10 的 logits 和候选上的 softmax。被选神经元的特征进入下一解码状态，让后续决策能利用此前选择的信息。候选数量缩小时，指针机制仍能直接给现有候选打权重。

真正执行的神经元选择是：

\[ n^{*}=\arg\max_{n\in\mathcal{N}_{u}}\omega_n a_n. \]

其中 \(\omega_n\) 是原启发式分数，\(a_n\) 是 actor 权重。注意力不是直接替代验证分数，也不是某个神经元“满足性质的概率”：实际优先级由两者乘积决定。这样可以压低原先高分但后续代价大的候选，同时保留 Fsb 对当前界的专业估计。实验具体评估的是 Fsb 重加权；论文提出可以接入其他启发式，不等于已经实证展示所有启发式都受益。

双 critic 也采用 PointerNet 式结构，参数彼此独立，并利用 actor 当前解码状态初始化各自解码器。正文描述其为各候选输出 Q 值，附录又强调 branch-child pair 的标量输出；可确认的核心是它们评估候选分支的未来收益，而不是输出性质证明。附录使用双 Q 网络与保守目标缓解过估计，目标网络通过缓慢移动平均更新。

改变分支顺序不改变两个分支覆盖原问题的事实，也不改变界计算的可靠性。论文的 soundness/completeness 论证依赖底层 BaB 保持原有逻辑并穷尽必要分支；这不是对有限时间内必然结束的保证。在 120 秒预算下超时只能解释为未决，不能解释为性质不成立。SAT 必须有底层验证器找到的反例，UNSAT 必须来自可靠的排除或证明过程。

3. 双后继价值学习：一次分支的代价要覆盖两侧子树

普通轨迹经验常保存“当前状态、动作、奖励、一个下一状态”。BaB 则在一次神经元分支后生成正负两个后继，证明性质通常需要同时排除两侧，而不是随机选择一侧继续就可以代表全部工作。Rsb 的 replay buffer 因此在同一条经验中保存两个后继观测和各自掩码，让价值目标包含两侧仍需搜索的成本。这是训练适配搜索树的关键，不应描述成普通单后继 rollout。

为解释 Eq. 10 的机制，可以用以下概念性目标；它不是对缓存中损坏排版公式的逐字重建：

\[ y_t=r_t+\gamma\left(c_{+}V_{\mathrm{target}}(o_{+})+c_{-}V_{\mathrm{target}}(o_{-})\right). \]

这里 \(c_{+},c_{-}\) 表示“该侧仍未解决则为 1，否则为 0”，\(V_{\mathrm{target}}\) 表示目标 critic 在策略下的预期价值。正文 Eq. 10 后也明确说其掩码为 0 时该侧已经解决、没有未来价值；然而前面的经验描述将掩码称为 termination mask，语义并不清楚。因此理解实现时应检查到底是继续掩码还是终止掩码，不能机械地把“终止取 1”代入这条目标。

奖励还存在更实质的不一致。§4 Eq. 8 与后续文字给每个已解决子问题加 1，并声称最大化折扣回报等价于最少子问题；Alg. 2 第 11 行及 §5.3 却使用“未解决后继数量的负值”。附录 C.1 只补充按固定最大访问子问题数归一化，附录 B 只给一般 actor-critic 目标，均没有澄清两种奖励如何对应。

独立分析表明，即使每次恰有两个后继，“已解决数”与“负未解决数”也只是单步相差常数 2。不同策略会改变分支次数和折扣长度，因此不能直接推导两种累计目标等价；在完整二叉 UNSAT 树、无额外提前终止的简化情形中，增加分支还会增加终端叶子数量。故本笔记保留论文的设计意图——惩罚后续搜索负担——但不把正奖励的等价性当作已验证定理，也不擅自修订作者公式。

一个完整示例¶

论文 Fig. 1 的小网络要证明：当 \(x_1\in[-2,2]\)、\(x_2\in[-1,1]\) 时，输出始终满足 \(y_1>y_2\)。初始抽象留下三个不稳定 ReLU：\(n_{11},n_{21},n_{22}\)。本例用于解释优先级改变，不代表统计实验中的平均收益。

Fsb 初始分数依次为 0.3、0.5、0.1，因此先分 \(n_{21}\)。其负侧可直接排除，正侧仍未解决；下一轮再分 \(n_{11}\) 才完成证明，总计两次分支、四个分支后继。

Rsb 给三个候选的权重依次为 0.6、0.3、0.1，乘积变成 0.18、0.15、0.01，于是先分 \(n_{11}\)。在该示例中两侧都能被原界计算解决，因此只需要一次分支、两个后继。关键不是 actor 声称网络更安全，而是它把能同时约束下游多个神经元的分支提前了，随后由相同验证逻辑确认结论。

训练看到的经验也不同：第一种选择存在一个需要继续搜索的后继，第二种选择的两个后继都没有未来搜索成本。双后继价值目标可以表达这一差异；若只采一个已解决后继，第一种选择就可能看起来与第二种一样好。

损失函数 / 训练策略¶

critic 以双后继 Bellman 目标的平方误差学习价值，actor 则最大化 critic 估计的动作价值，目标可写为：

\[ \mathcal{L}_{\pi}(\psi)=\mathbb{E}_{o\sim\mathcal{D},\,a\sim\pi_{\psi}(\cdot\mid o)}[-Q_{\phi}(o,a)]. \]

附录称其为 SAC 变体，保留 off-policy 经验复用与双 Q 网络；列出的 actor 目标没有标准最大熵 SAC 的显式熵项，因此不应凭算法引用自行补出温度参数或熵损失。

作者生成 480,960 个 FNN 验证实例，先通过 PGD 剔除发现反例的实例，再用 LiRPA 剔除容易证明的实例，留下 14,454 个困难训练实例。攻击未发现反例并不自动证明 UNSAT；这里的两级过滤旨在富集需要非平凡分支的任务，不是新的完备判定程序。训练共 100,000 个 episode，单 GPU 需要数天。

GCN 预训练采用两层、隐藏宽度 128、ReLU，Adam 学习率 \(3\times10^{-4}\)，5 个 epoch，batch size 512。RL 采用 AdamW，actor 与 critic 学习率均为 \(4\times10^{-4}\)，折扣 \(\gamma=0.99\)，replay 容量为 \(10^5\)，batch size 512，并累积 8 个 minibatch。

每次策略更新前进行 2 次 critic 更新，目标移动平均系数为 \(10^{-4}\)。前 \(10^3\) 环境步使用启发式 warm-up，附录还允许 buffer 半满时提前开始优化，并在之后偶尔插入启发式动作。测试阶段冻结权重，所有实例共享同一策略；没有测试时 critic 更新或逐网络适配。

实验关键数据¶

主实验¶

测试包含 FNN、CNN、Sigmoid 各 200 个困难实例，总计 600 个；后两类网络没有用于训练。FNN 测试与训练共享网络架构但性质不同，不宜称为全新网络泛化。所有启发式统一接入 NeuralSAT，在 Threadripper 32 核、128 GB RAM、RTX 4090 上运行，每实例上限 120 秒。

下表取自原文 Table 2。其时间和分支统计限定于“至少被一个方法求解的实例”这一子集，不是整个 600 实例全集的无条件总耗时；分支列单位为百万。

基准	方法	求解数	时间（秒）	分支数（百万）
FNN	Polarity	1	6064.32	170.81
FNN	Upb	23	4359.36	27.17
FNN	Fsb	43	2679.00	6.65
FNN	Rsb	50	2051.94	1.86
CNN	Polarity	0	8662.55	583.01
CNN	Upb	71	2387.48	1.73
CNN	Fsb	71	2295.89	1.81
CNN	Rsb	72	2419.58	1.69
Sigmoid	Polarity	10	6027.70	62.98
Sigmoid	Upb	39	3963.69	8.59
Sigmoid	Fsb	34	4336.73	8.99
Sigmoid	Rsb	43	3450.80	5.14

按该表求和，Rsb 为 165，Fsb 为 148，增加 17 个、约 11.5%；分支数由 17.45M 降到 8.69M，约少 50.2%。这些是本笔记根据表格计算的比率，论文将其概括为 11% 和 50%。

Upb 的表格求和是 \(23+71+39=133\)，但 §6.2 正文写总计 110；110 又恰是其 CNN 与 Sigmoid 之和。原文没有确认错误来源，本笔记保留表内数字并显式记录冲突，不将正文的 110 当作全基准总计。

消融实验¶

论文没有提供去掉 GCN、去掉原始特征、取消重加权或改成单后继训练的模块消融表。以下是 §6.4 的统计与效率分析，不冒充因果消融；五次运行改变的是基准生成种子，不能改称五个训练随机种子。

分析项	Rsb	对照	证据与边界
五次运行求解数中位数	150	Fsb 140；Upb 125	Fig. 5 / §6.4；不是 Table 2 的 165
每步决策时间	约 0.11 秒	Fsb、Upb 约 0.13 秒	文中近似值，包含当前工作负载差异
活跃子问题批量示例	32	64	作者用于解释评分开销差异的示例，非固定参数
分支分布中位数量级	约 \(10^4\)	Fsb 约 \(10^4\)	Rsb 分布更低更集中；不是总分支数
unseen 网络求解数	115	Fsb 105；Upb 110	CNN 与 Sigmoid 合计，非全集
模块独立贡献	未报告	未报告	无法确定 GCN、重加权、双后继各贡献多少

关键发现¶

增益集中在 FNN 和 Sigmoid：分别多解 7 个和 9 个；CNN 只多解 1 个。它支持跨所测架构的迁移，但不足以证明对任意规模或激活函数的普遍泛化。
CNN 的 Rsb 时间为 2419.58 秒，高于 Fsb 的 2295.89 秒，尽管分支少一些。因此不能概括为“每种基准都更快”，更小搜索树也不保证更低墙钟时间。
每步决策时间较低的解释是策略使队列和评分批量变小，而不是额外神经网络前向本身免费。若固定同一子问题批量比较，是否仍更快，本文没有独立控制实验。
作者报告五次运行的分布稳定性，但没有给出正式显著性检验或置信区间；“统计分析”不应升级为严格统计显著性的证明。

亮点与洞察¶

学习与证明的责任分离：策略出错首先影响计算量，而不是让它拥有否定或肯定性质的权力。这种接口适合将学习加入具有明确可靠性边界的求解系统。
学习修正而非从零替代：Fsb 已经编码对界改善的专业判断，重加权保留了这个参照。其可迁移之处是学习启发式的状态依赖偏好，而非仅拟合一个更复杂的静态评分器。
搜索树不等于轨迹：证明型搜索的两个子问题都可能消耗资源。经验结构和价值备份必须匹配实际工作展开方式，而不能直接套用单后继训练模板。

局限与展望¶

奖励正负表述、累计等价性与掩码语义尚未对齐，影响训练目标的可复现性。应公布具体实现、回报定义和完整停止条件，并验证分支数量与所优化回报之间的关系。
缺少关键模块消融，不能从最终性能推断哪一部分最重要。可在统一实例与预算下分别取消结构嵌入、原始特征投影、Fsb 乘法和双后继备份。
困难实例筛选使实验对分支策略有针对性，但不代表一般验证任务的平均收益。论文自己指出 VNN-COMP’25 常规赛道 2700 个实例中 2473 个无需分支或只需很少分支，部署评估应同时报告完整分布。
训练耗时数天，现有实验未量化成本摊销，也没有大规模现代网络的广泛覆盖。新增候选带来的学习推理与图处理开销仍需单独测量。
作者提出输入空间分支和验证时在线适配作为未来方向；它们不是当前结果。在线适配尤其应继续保持证明内核不受学习输出直接替代的边界。

评分¶

新颖性: 4/5 — 启发式重加权与双后继价值学习的结合清晰，学习分支本身已有先例。
实验充分度: 3/5 — 有 600 个困难实例及跨架构分析，但缺少模块消融、目标核验与完整成本分析。
写作质量: 2/5 — 主流程容易理解，奖励、掩码、Upb 总数及泛化措辞的不一致妨碍精确复现。
价值: 4/5 — 展示学习可以在不接管证明逻辑的情况下改善成熟验证器的搜索效率。