Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Computational Tradeoffs of Optimization-Based Bound Tightening in ReLU Networks

Fabian Badilla, Marcos Goycoolea, Gonzalo Muñoz, Thiago Serra

TL;DR

This work investigates the tradeoff between activation-bound tightness and MILP solve time in ReLU networks, focusing on how bound quality affects downstream optimization tasks like verification. It compares strong (exact/OBBT) and weak (LP-relaxed) bounds, as well as naive bounds, across architectures, regularization, and pruning, using a rigorous MNIST experimental setup. The findings show that LP-relaxation-based weak bounds often achieve a favorable balance between computational cost and bound quality, while strong bounds can dominate in deep networks for verification. The results provide actionable guidance for embedding neural networks in MILP-based optimization and verification pipelines, including hybrid bound strategies that adapt to layer depth and network conditioning.

Abstract

The use of Mixed-Integer Linear Programming (MILP) models to represent neural networks with Rectified Linear Unit (ReLU) activations has become increasingly widespread in the last decade. This has enabled the use of MILP technology to test-or stress-their behavior, to adversarially improve their training, and to embed them in optimization models leveraging their predictive power. Many of these MILP models rely on activation bounds. That is, bounds on the input values of each neuron. In this work, we explore the tradeoff between the tightness of these bounds and the computational effort of solving the resulting MILP models. We provide guidelines for implementing these models based on the impact of network structure, regularization, and rounding.

Computational Tradeoffs of Optimization-Based Bound Tightening in ReLU Networks

TL;DR

This work investigates the tradeoff between activation-bound tightness and MILP solve time in ReLU networks, focusing on how bound quality affects downstream optimization tasks like verification. It compares strong (exact/OBBT) and weak (LP-relaxed) bounds, as well as naive bounds, across architectures, regularization, and pruning, using a rigorous MNIST experimental setup. The findings show that LP-relaxation-based weak bounds often achieve a favorable balance between computational cost and bound quality, while strong bounds can dominate in deep networks for verification. The results provide actionable guidance for embedding neural networks in MILP-based optimization and verification pipelines, including hybrid bound strategies that adapt to layer depth and network conditioning.

Abstract

The use of Mixed-Integer Linear Programming (MILP) models to represent neural networks with Rectified Linear Unit (ReLU) activations has become increasingly widespread in the last decade. This has enabled the use of MILP technology to test-or stress-their behavior, to adversarially improve their training, and to embed them in optimization models leveraging their predictive power. Many of these MILP models rely on activation bounds. That is, bounds on the input values of each neuron. In this work, we explore the tradeoff between the tightness of these bounds and the computational effort of solving the resulting MILP models. We provide guidelines for implementing these models based on the impact of network structure, regularization, and rounding.
Paper Structure (12 sections, 1 theorem, 3 equations, 4 figures, 1 algorithm)

This paper contains 12 sections, 1 theorem, 3 equations, 4 figures, 1 algorithm.

Table of Contents

  1. Introduction
  2. Background
  3. Neural Networks
  4. Computing Activation Bounds
  5. Verification Problems
  6. Experimental Setup
  7. Results
  8. Strong Versus Weak Activation Bounds
  9. Solving Times
  10. Effectiveness On Verification Problems
  11. Conclusions
  12. Acknowledgments.

Key Result

proposition thmcounterproposition

Given $\hbox{UB}^{(l)}$ valid bounds for layer $l\geq 0$, then the following is a valid activation bound for every neuron on layer $l+1$:

Figures (4)

  • Figure 1: RBT for the lower bound on the last layer versus rounding threshold $\varepsilon$ for each architecture, regularization type (L1/L2) and level $\lambda$.
  • Figure 2: Running times of Algorithm \ref{['alg:bounder']} for strong and weak bounds in the L1 case (top) and the L2 case (bottom).
  • Figure 3: Comparison for the different bound types used.
  • Figure 4: Instances that reach a gap $1\%$ by network architecture.

Theorems & Definitions (1)

  • proposition thmcounterproposition: Naive Bound