New verification method tightens bounds for neural networks with real-world constraints

Verifying that neural networks behave correctly across all possible inputs is a critical challenge in deep learning safety. A new research paper presents an approach designed to handle verification problems where the input space involves multiple overlapping constraints—a scenario far more common in practice than the simplified uniform regions most tools assume.

The verification challenge#

Existing neural network verification (NNV) tools work by computing a conservative estimate of how a network responds across a given input region. The quality of this estimate directly affects whether the tool can confirm a network is safe or must report inconclusive results. Current methods restrict input regions to simple geometric shapes like Lp-norm balls (e.g., all inputs within a fixed distance from a reference point), which are mathematically convenient but rarely match real-world scenarios. Many practical applications require input regions defined by multiple convex constraints simultaneously—for instance, combining a motion-blur perturbation with both halfspace and L2-ball bounds—resulting in loose approximations that produce false positives or missed verifications.

How CLAD works#

The proposed method, Constrained Lagrangian Abstract Domain (CLAD), extends existing abstraction-based verification to handle constrained input regions. Rather than attempting to directly optimize bounds across a complex intersection of constraints, CLAD reformulates the problem using Lagrange multipliers, transforming each constraint into a penalty term in an objective function. This allows the method to solve a max-min problem iteratively: it takes projected gradient steps on the input domain while updating the multiplier weights to tighten bounds over only the truly feasible region. The approach is flexible enough to work with any convex constraint that supplies a subgradient, including those computed automatically via standard differentiation tools.

Experimental results#

Testing on nearly 2,000 verification instances across four convolutional networks, CLAD performed competitively with the baseline tool GCPCROWN on standard unconstrained verification problems while dramatically improving on constrained scenarios. When verifying properties involving L2-ball constraints, CLAD succeeded on 60% more instances. Across all constrained test cases, it verified 22% more problems than existing approaches, suggesting meaningful gains for real-world robustness certification tasks.