An efficient nonconvex reformulation of stagewise convex optimization problems
Rudy Bunel, Oliver Hinder, Srinadh Bhojanapalli, Krishnamurthy Dvijotham
Abstract
Convex optimization problems with staged structure appear in several contexts, including optimal control, verification of deep neural networks, and isotonic regression. Off-the-shelf solvers can solve these problems but may scale poorly. We develop a nonconvex reformulation designed to exploit this staged structure. Our reformulation has only simple bound constraints, enabling solution via projected gradient methods and their accelerated variants. The method automatically generates a sequence of primal and dual feasible solutions to the original convex problem, making optimality certification easy. We establish theoretical properties of the nonconvex formulation, showing that it is (almost) free of spurious local minima and has the same global optimum as the convex problem. We modify PGD to avoid spurious local minimizers so it always converges to the global minimizer. For neural network verification, our approach obtains small duality gaps in only a few gradient steps. Consequently, it can quickly solve large-scale verification problems faster than both off-the-shelf and specialized solvers. Introduction This paper studies efficient algorithms for a particular class of stage-wise optimization problems: minimize where n and m are positive integers, S ⊆ R m , the function f has domain S × R n and range R, the functions µ i and η i have domain S × R i-1 and range R. Given a vector z, we use the notation z 1:i to denote the vector [z 1 , . . . , z i ]. We let z 1:0 be a vector of length zero. Throughout the paper we assume that η 1 , . . . , η n are proper concave functions, f , µ 1 , . . . , µ n are proper convex functions, and S is a nonempty convex set. Problems that fall into this problem class are ubiquitous. They appear in optimal control [1], finite horizon Markov decision processes with cost function controlled by an adversary [2], generalized Isotonic regression [3, 4], and verification of neural networks [5-7]. Details explaining how these problems can be written in the form of (1) are given in Appendix A. Here we briefly outline how neural network verification falls into (1b). Letting s represent the input image and z the activation values, neural networks verification can be written (unconventionally) as minimize (s,z)∈S×R n f (s, z) s.t. z i = σ([s, z 1:i-1 ] • w i ),
Ask about this paper
Your agent reads all of it.
Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.
Cited by top-tier papers8
- The Convex Relaxation Barrier, Revisited: Tightened Single-Neuron Relaxations for Neural Network VerificationChristian Tjandraatmadja, Ross Anderson, Joey Huchette, Will Ma et al.NeurIPS 2020 · 102 citations
- PRIMA: general and precise neural network certification via scalable convex hull approximationsMark Niklas Müller, Gleb Makarchuk, Gagandeep Singh, Markus Püschel et al.POPL 2022 · 75 citations
- Make Sure You're Unsure: A Framework for Verifying Probabilistic SpecificationsLeonard Berrada, Sumanth Dathathri, Krishnamurthy Dvijotham, Robert Stanforth et al.NeurIPS 2021 · 22 citations
- Optimizing over trained GNNs via symmetry breakingShiqiang Zhang, Juan S. Campos, Christian Feldmann, David Walz et al.NeurIPS 2023 · 14 citations
- Input-Relational Verification of Deep Neural NetworksDebangshu Banerjee, Changming Xu, Gagandeep SinghPLDI 2024 · 9 citations
Builds on2
Related papers
- Zonotope Domains for Lagrangian Neural Network VerificationMatt Jordan, Jonathan Hayase, Alex Dimakis, Sewoong OhNeurIPS 2022 · 6 citations
- Fast Convex Optimization for Two-Layer ReLU Networks: Equivalent Model Classes and Cone DecompositionsAaron Mishkin, Arda Sahiner, Mert PilanciICML 2022 · 35 citations
- Scaling the Convex Barrier with Active SetsAlessandro De Palma, Harkirat S. Behl, Rudy Bunel, Philip H. S. Torr et al.ICLR 2021 · 66 citations
- Out of the Shadows: Exploring a Latent Space for Neural Network VerificationLukas Koller, Tobias Ladner, Matthias AlthoffICLR 2026 · 6 citations
- ReLU Hull ApproximationZhongkui Ma, Jiaying Li, Guangdong BaiPOPL 2024 · 7 citations
