Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Philip Sosnin, Calvin Tsay

TL;DR

This work targets formal certification of neural network controllers that approximate MPC policies by encoding the combined NN and MPC into a mixed-integer program (MIP). Recognizing that MIP scalability hinges on tight intermediate bounds, the authors evaluate multiple bound-tightening strategies—IBP, CROWN, OBBT (MIP- and LP-based), and layer-wise OBBT—and apply them to multi-step horizon problems by unrolling the dynamics into an augmented network. Through a case study on a 4D linear system with two NN controllers and horizon $N=9$, they show that tighter bounds dramatically reduce MIP solve times for reachability (and improve worst-case error certifiability), while multi-step problems accentuate the importance of bound quality. The results suggest that combining tight bound propagation with suitable MIP formulations enables scalable, formal NN certification for explicit MPC, with LP-OBBT and layer-wise OBBT offering strong speed–tightness trade-offs for practical use.

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.

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

TL;DR

This work targets formal certification of neural network controllers that approximate MPC policies by encoding the combined NN and MPC into a mixed-integer program (MIP). Recognizing that MIP scalability hinges on tight intermediate bounds, the authors evaluate multiple bound-tightening strategies—IBP, CROWN, OBBT (MIP- and LP-based), and layer-wise OBBT—and apply them to multi-step horizon problems by unrolling the dynamics into an augmented network. Through a case study on a 4D linear system with two NN controllers and horizon , they show that tighter bounds dramatically reduce MIP solve times for reachability (and improve worst-case error certifiability), while multi-step problems accentuate the importance of bound quality. The results suggest that combining tight bound propagation with suitable MIP formulations enables scalable, formal NN certification for explicit MPC, with LP-OBBT and layer-wise OBBT offering strong speed–tightness trade-offs for practical use.

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.
Paper Structure (17 sections, 11 equations, 1 figure, 2 tables)

This paper contains 17 sections, 11 equations, 1 figure, 2 tables.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Model predictive control (MPC)
  4. Explicit MPC using neural networks (NNs)
  5. Mixed-integer programming (MIP) formulations
  6. Certification problem statement
  7. Deriving and tightening bounds
  8. Interval bound propagation (IBP)
  9. Linear bound propagation (CROWN)
  10. Optimization-based bounds tightening (OBBT)
  11. Layer-wise OBBT
  12. Combining bound tightening methods
  13. Bounding multi-timestep problems
  14. Case study
  15. Worst-case error results
  16. ...and 2 more sections

Figures (1)

  • Figure 1: Comparison of bound tightening methods on a 4-layer NN controller over $K=3$ time-steps (note log-scale y-axis).