# Global Optimization of Objective Functions Represented by ReLU Networks

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

## Key facts

- Cited by 24 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 7 Oct 2020.

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

- [Marabou 2.0: A Versatile Formal Analyzer of Neural Networks](https://mlsanity.com/paper/2401.14461/) (2024)
- [Towards Formal XAI: Formally Approximate Minimal Explanations of Neural Networks](https://mlsanity.com/paper/2210.13915/) (2022)
- [When Deep Learning Meets Polyhedral Theory: A Survey](https://mlsanity.com/paper/2305.00241/) (2023)
- [Towards Scalable Verification of Deep Reinforcement Learning](https://mlsanity.com/paper/2105.11931/) (2021)
- [Verifying Learning-Based Robotic Navigation Systems](https://mlsanity.com/paper/2205.13536/) (2022)
- [Verification of Image-based Neural Network Controllers Using Generative Models](https://mlsanity.com/paper/2105.07091/) (2021)
- [An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks](https://mlsanity.com/paper/2201.01978/) (2022)
- [Neural Network Verification with Proof Production](https://mlsanity.com/paper/2206.00512/) (2022)
- [Pruning and Slicing Neural Networks using Formal Verification](https://mlsanity.com/paper/2105.13649/) (2021)
- [Infinite Time Horizon Safety of Bayesian Neural Networks](https://mlsanity.com/paper/2111.03165/) (2021)
- [veriFIRE: Verifying an Industrial, Learning-Based Wildfire Detection System](https://mlsanity.com/paper/2212.03287/) (2022)
- [Constrained Reinforcement Learning for Robotics via Scenario-Based Programming](https://mlsanity.com/paper/2206.09603/) (2022)
- [Verifying Generalization in Deep Learning](https://mlsanity.com/paper/2302.05745/) (2023)
- [Optimization Over Trained Neural Networks: Taking a Relaxing Walk](https://mlsanity.com/paper/2401.03451/) (2024)
- [Tighter Abstract Queries in Neural Network Verification](https://mlsanity.com/paper/2210.12871/) (2022)
- [On Optimizing Back-Substitution Methods for Neural Network Verification](https://mlsanity.com/paper/2208.07669/) (2022)
- [A Robust Optimisation Perspective on Counterexample-Guided Repair of Neural Networks](https://mlsanity.com/paper/2301.11342/) (2023)
- [DelBugV: Delta-Debugging Neural Network Verifiers](https://mlsanity.com/paper/2305.18558/) (2023)
- [ZoPE: A Fast Optimizer for ReLU Networks with Low-Dimensional Inputs](https://mlsanity.com/paper/2106.05325/) (2021)
- [Verifying the Generalization of Deep Learning to Out-of-Distribution Domains](https://mlsanity.com/paper/2406.02024/) (2024)
- [Incremental Neural Network Verification via Learned Conflicts](https://mlsanity.com/paper/2603.12232/) (2026)
- [Nonmyopic Global Optimisation via Approximate Dynamic Programming](https://mlsanity.com/paper/2412.04882/) (2024)
- [Optimization over Trained (and Sparse) Neural Networks: A Surrogate within a Surrogate](https://mlsanity.com/paper/2505.01985/) (2025)
- [Mining Verdict Boundaries for Neural Network Verification](https://mlsanity.com/paper/2607.28954/) (2026)

## Abstract (arXiv)

Neural networks can learn complex, non-convex functions, and it is challenging to guarantee their correct behavior in safety-critical contexts. Many approaches exist to find failures in networks (e.g., adversarial examples), but these cannot guarantee the absence of failures. Verification algorithms address this need and provide formal guarantees about a neural network by answering "yes or no" questions. For example, they can answer whether a violation exists within certain bounds. However, individual "yes or no" questions cannot answer qualitative questions such as "what is the largest error within these bounds"; the answers to these lie in the domain of optimization. Therefore, we propose strategies to extend existing verifiers to perform optimization and find: (i) the most extreme failure in a given input region and (ii) the minimum input perturbation required to cause a failure. A naive approach using a bisection search with an off-the-shelf verifier results in many expensive and overlapping calls to the verifier. Instead, we propose an approach that tightly integrates the optimization process into the verification procedure, achieving better runtime performance than the naive approach. We evaluate our approach implemented as an extension of Marabou, a state-of-the-art neural network verifier, and compare its performance with the bisection approach and MIPVerify, an optimization-based verifier. We observe complementary performance between our extension of Marabou and MIPVerify.