Neural network verification improves with flexible input region constraints
CLAD: Constrained Abstract Domain for Neural Network Verification
Software EngineeringMachine Learning
Summary
Verifying that neural networks work correctly for all inputs is hard, especially when input conditions are complex. Current methods often assume simple shapes for input regions, which can lead to errors or missed problems. The authors introduce CLAD, a new technique that handles more complex input conditions by combining multiple constraints. This approach better matches real-world scenarios and helps verify more properties accurately, particularly when inputs have combined restrictions.
What this means in practice
- •For machine learning engineers: Verify neural network robustness under complex real-world input conditions combining multiple convex constraints like motion blur plus shape limits.
- •For autonomous vehicle developers: Test neural network models against safety properties that consider combined environmental effects, improving confidence in perception modules.
Authors
Hai Duong, Thanh Le, ThanhVu Nguyen
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.