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

arXiv: https://arxiv.org/abs/2403.17874 · HTML: https://mlsanity.com/paper/2403.17874/

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 26 Mar 2024.

## Built on by (most cited first, 6 of 6)

- [Certified Robustness to Data Poisoning in Gradient-Based Training](https://mlsanity.com/paper/2406.05670/) (2024)
- [Certification for Differentially Private Prediction in Gradient-Based Training](https://mlsanity.com/paper/2406.13433/) (2024)
- [Exact Certification of Data-Poisoning Attacks Using Mixed-Integer Programming](https://mlsanity.com/paper/2602.16944/) (2026)
- [Relaxation-Informed Training of Neural Network Surrogate Models](https://mlsanity.com/paper/2604.22746/) (2026)
- [Optimization over Trained (and Sparse) Neural Networks: A Surrogate within a Surrogate](https://mlsanity.com/paper/2505.01985/) (2025)
- [DCEmbed: Scalable Optimization over Neural Surrogates](https://mlsanity.com/paper/2609.33879/) (2026)

## Abstract (arXiv)

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.