131. Exact Verification of First-Order Methods via Mixed-Integer Linear Programming
Invited abstract in session MC-8: Systematic and computer-aided analyses II: Systematic algorithmic design approaches, stream Systematic and computer-aided analyses of optimization algorithms.
Monday, 14:00-16:00Room: B100/7007
Authors (first author is the speaker)
| 1. | Vinit Ranjan
|
| Princeton | |
| 2. | Jisun Park
|
| Operations Research and Financial Engineering, Princeton University | |
| 3. | Stefano Gualandi
|
| Matematica, Università di Pavia | |
| 4. | Andrea Lodi
|
| D.E.I.S., University of Bologna | |
| 5. | Bartolomeo Stellato
|
| Operations Research and Financial Engineering, Princeton University |
Abstract
We present exact mixed-integer linear programming formulations for verifying the performance of first-order methods for parametric quadratic optimization. We formulate the verification problem as a mixed-integer linear program where the objective is to maximize the infinity norm of the fixed-point residual after a given number of iterations. Our approach captures a wide range of gradient, projection, proximal iterations through affine or piecewise affine constraints. We derive tight polyhedral convex hull formulations of the constraints representing the algorithm iterations. To improve the scalability, we develop a custom bound tightening technique combining interval propagation, operator theory, and optimization-based bound tightening. Numerical examples, including linear and quadratic programs from network optimization, sparse coding using Lasso, and optimal control, show that our method provides several orders of magnitude reductions in the worst-case fixed-point residuals, closely matching the true worst-case performance.
Keywords
- Computer-aided algorithm analysis
- First-order optimization
Status: accepted
Back to the list of papers