Scaling Mixed-Integer Programming for Certification of Neural Network Controllers Using Bounds Tightening

TL;DR

This paper improves the scalability of neural network certification for control systems by applying bound-tightening techniques to reduce mixed-integer program complexity, enabling more efficient safety verification.

Contribution

It introduces and evaluates bound-tightening strategies to enhance the scalability of mixed-integer programming for neural network certification in control applications.

Findings

Bound-tightening significantly reduces optimization time.

Tighter bounds improve certification accuracy.

Strategies vary in complexity and effectiveness.

Abstract

Neural networks offer a computationally efficient approximation of model predictive control, but they lack guarantees on the resulting controlled system's properties. Formal certification of neural networks is crucial for ensuring safety, particularly in safety-critical domains such as autonomous vehicles. One approach to formally certify properties of neural networks is to solve a mixed-integer program based on the network. This approach suffers from scalability issues due to the complexity of solving the resulting mixed-integer programs. Nevertheless, these issues can be (partially) mitigated via bound-tightening techniques prior to forming the mixed-integer program, which results in tighter formulations and faster optimisation. This paper presents bound-tightening techniques in the context of neural network explicit control policies. Bound tightening is particularly important when considering problems spanning multiple time steps of a controlled system, as the bounds must be propagated through the problem depth. Several strategies for bound tightening are evaluated in terms of both computational complexity and tightness of the bounds.