Clip-and-Verify: Linear Constraint-Driven Domain Clipping for Accelerating Neural Network Verification¶

会议: NeurIPS 2025
arXiv: 2512.11087
代码: https://github.com/Verified-Intelligence/Clip_and_Verify (有)
领域: AI安全/神经网络验证
关键词: 神经网络验证, branch-and-bound, 线性约束, 域裁剪, α,β-CROWN

一句话总结¶

提出Clip-and-Verify框架，通过利用线性界传播产生的约束来裁剪输入空间和收紧中间层界，包含完全裁剪（坐标上升求解对偶问题）和松弛裁剪（收缩输入盒）两种GPU高效算法，最多减少96%的BaB子问题数量，是VNN-COMP 2025获胜验证器的核心组件。

研究背景与动机¶

领域现状：神经网络验证旨在形式化证明网络在给定输入域上满足安全性质。主流方法为分支定界(BaB)+界传播（如α,β-CROWN），通过递归松弛非线性激活来计算中间层界。
现有痛点：BaB子问题指数增长；中间层界初始化后固定不更新（因逐层更新开销太大），导致松弛质量受限；使用LP求解器太贵。
核心矛盾：BaB分支产生的线性约束蕴含收紧可行域的机会，但现有框架无法高效利用。
本文要解决什么？ 以极低开销利用"免费"线性约束收紧所有层的界。
切入角度：将约束优化问题转化为1D对偶问题，发现其与连续背包问题等价，可GPU并行精确求解。
核心idea一句话：利用界传播"免费"产生的线性约束，通过GPU并行坐标上升求解对偶问题来裁剪输入域和收紧中间界。

方法详解¶

整体框架¶

在α,β-CROWN验证器的BaB流程中嵌入domain clipping环节。每个BaB节点处收集线性约束，用完全裁剪直接优化中间层界或用松弛裁剪收缩输入盒后重新具体化界。

关键设计¶

完全裁剪（Complete Clipping）:
做什么：在线性约束 \(\mathbf{g}^\top \mathbf{x} + h \leq 0\) 下优化盒域上的线性目标
核心思路：Lagrangian对偶将n维LP转化为1D凹分段线性函数最大化 \(L^* = \max_{\beta \geq 0} D(\beta)\)，通过排序断点精确求解（\(\mathcal{O}(n \log n)\)）。多约束用坐标上升
设计动机：比Gurobi LP快880× (0.0028s vs 2.47s)，精度相当
松弛裁剪（Relaxed Clipping）:
做什么：利用约束逐维收缩输入盒，重新具体化已缓存的线性界
核心思路：对每个约束和每个输入维度，闭式计算新界限，取与原界限的交集
设计动机：几乎零开销，可每步BaB执行
约束来源：线性界传播本身在所有层产生的界平面可直接作为裁剪约束，是"free lunch"

实验关键数据¶

主实验¶

基准	子问题减少率	核心优势
多项VNN-COMP基准	最高96%	一致性提升
vs Gurobi LP	880×加速	精度相当(0.00085 vs 0.0007)

消融实验¶

配置	关键指标	说明
仅松弛裁剪	低开销中等提升	快速迭代
仅完全裁剪	更强提升	困难子问题
两者结合	最佳综合	完整版Clip-and-Verify

关键发现¶

完全裁剪等价于连续背包问题，可高效精确求解
方法是VNN-COMP 2025获胜α,β-CROWN验证器的一部分
早期不可行检测可跳过大量子问题

亮点与洞察¶

1D对偶转化是核心贡献——避免外部LP求解器，实现GPU原生高效求解
"免费约束"洞察巧妙——界传播自身产物作为裁剪输入，零额外计算

局限性 / 可改进方向¶

坐标上升对多约束不保证全局最优
仅适用于前馈网络和盒域约束

评分¶

新颖性: ⭐⭐⭐⭐ 对偶-坐标上升框架新颖，连续背包等价性优雅
实验充分度: ⭐⭐⭐⭐⭐ VNN-COMP获胜验证实用性
写作质量: ⭐⭐⭐⭐ 理论推导清晰
价值: ⭐⭐⭐⭐⭐ 工程价值极高