Bound Tightening using Rolling-Horizon Decomposition for Neural Network Verification

TL;DR

This paper presents a novel rolling-horizon decomposition method for neural network verification that improves bound tightness and computational tractability, demonstrated through extensive experiments on benchmark instances.

Contribution

It introduces a new mixed-integer programming approach leveraging layered network structure for tighter bounds in neural network verification.

Findings

Significantly improved bounds over existing methods.

Effective parallelization for solving open verification problems.

Open-source implementation integrated into Gravity tool.

Abstract

Neural network verification aims at providing formal guarantees on the output of trained neural networks, to ensure their robustness against adversarial examples and enable their deployment in safety-critical applications. This paper introduces a new approach to neural network verification using a novel mixed-integer programming rolling-horizon decomposition method. The algorithm leverages the layered structure of neural networks, by employing optimization-based bound-tightening on smaller sub-graphs of the original network in a rolling-horizon fashion. This strategy strikes a balance between achieving tighter bounds and ensuring the tractability of the underlying mixed-integer programs. Extensive numerical experiments, conducted on instances from the VNN-COMP benchmark library, demonstrate that the proposed approach yields significantly improved bounds compared to existing effective bound propagation methods. Notably, the parallelizable nature of the proposed method proves effective in solving open verification problems. Our code is built and released as part of the open-source mathematical modeling tool Gravity (https://github.com/coin-or/Gravity), which is extended to support generic neural network models.