arXiv：cs.LG· Hai Duong, Thanh Le, ThanhVu Nguyen·· 7 小时前AI 评分35
CLAD：面向神经网络验证的约束抽象域
CLAD: Constrained Abstract Domain for Neural Network Verification
AI 导读
研究人员提出约束拉格朗日抽象域（CLAD），可在由多个凸约束组合定义的输入区域上对神经网络做可靠的过近似，并通过对偶投影法求解无闭式解的神经元边界问题。在四个卷积网络、1,944 个运动模糊结构化扰动实例上，CLAD 在标准无约束 Linf 属性下验证数量与 GCPCROWN 相当、运行时间相近；在约束属性下，L2-ball 属性验证数量比 GCPCROWN 多 60%，总计多 22%。
正文
Abstract:Neural network verification (NNV) formally verifies that a network satisfies a specified property for all inputs within a defined region. Modern NNV tools employ abstract domains to compute a sound over-approximation of the network's behavior from the given input region, thus the tightness of these abstractions essentially determines efficiency. A long line of increasingly precise domains has been developed, but they all describe the valid input region in the same restrictive way, e.g., an Lp-norm ball. A practical input region is rarely a simple Lp ball, but rather a combination Lp ball with additional constraints. Verifying a network over such a region with existing abstraction produces a loose over-approximation, which results in either failing to verify a property or spurious counterexamples. We introduce Constrained Lagrangian Abstract Domain (CLAD), a new abstract domain that computes a sound over-approximation of neural networks over input regions defined by a combination of convex constraints. CLAD propagates these constraints and tightens bounds over the true feasible region. However, bounding a neuron over the intersection of these constraints has no closed-form solution, so CLAD relaxes each constraint into the objective with a Lagrange multiplier and solves the resulting max-min problem with a projected primal-dual method, alternating a projected gradient step on the input with a multiplier update. CLAD supports any convex constraint with a subgradient, e.g., from automatic differentiation. We evaluate CLAD on 1,944 instances across four convolutional networks with motion-blur structured perturbations with halfspace or L2-ball constraints. On standard unconstrained Linf property, CLAD verifies as many instances as GCPCROWN at a similar runtime. On constrained properties, CLAD verifies 60% more instances than GCPCROWN on L2-ball properties, and 22% more in total.
| Subjects: | Software Engineering (cs.SE); Machine Learning (cs.LG) |
| Cite as: | arXiv:2609.34628 [cs.SE] |
| (or arXiv:2609.34628v2 [cs.SE] for this version) | |
| https://doi.org/10.48550/arXiv.2609.34628 arXiv-issued DOI via DataCite |
Submission history
From: Thanh Le [view email]
[v1]
Mon, 28 Sep 2026 08:48:41 UTC (751 KB)
[v2]
Tue, 6 Oct 2026 04:08:26 UTC (752 KB)
来源：arXiv：cs.LG · arxiv.org