CLAD：用于神经网络验证的约束抽象域

中文摘要 AI 辅助

神经网络验证（NNV）形式化地验证网络在给定输入区域内是否对所有输入满足特定属性。现代NNV工具采用抽象域来计算网络行为从给定输入区域出发的可靠过度近似，因此这些抽象的紧致性本质上决定了效率。已有大量日益精确的域被开发出来，但它们都以同样受限的方式描述有效输入区域，例如Lp范数球。实际输入区域很少是简单的Lp球，而是Lp球与额外约束的组合。使用现有抽象在此类区域上验证网络会产生松散的过度近似，导致要么无法验证属性，要么产生虚假反例。我们引入了约束拉格朗日抽象域（CLAD），一种新的抽象域，用于在由凸约束组合定义的输入区域上计算神经网络的可靠过度近似。CLAD传播这些约束并在真实可行区域上收紧边界。然而，在约束交集上对神经元进行边界计算没有闭式解，因此CLAD将每个约束松弛到目标函数中，使用拉格朗日乘子，并通过投影原始-对偶方法求解所得的极大极小问题，交替进行输入上的投影梯度步骤和乘子更新。CLAD支持任何具有次梯度的凸约束，例如来自自动微分的约束。我们在四个卷积网络上，使用带有半空间或L2球约束的运动模糊结构化扰动，对1,944个实例评估了CLAD。在标准的无约束L∞属性上，CLAD验证的实例数量与GCPCROWN相当，运行时间相近。在约束属性上，CLAD在L2球属性上比GCPCROWN多验证60%的实例，总计多22%。

英文摘要

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.

发表机构

• George Mason University（乔治梅森大学）

机构由 AI 辅助整理，请以论文原文为准。