Exact Verification of First-Order Methods via Mixed-Integer Linear Programming

TL;DR

This paper introduces an exact mixed-integer linear programming approach to verify the performance of first-order optimization algorithms, enabling precise worst-case analysis across various applications.

Contribution

It develops a novel MILP formulation for verifying first-order methods, including tight convex hulls and scalable bound tightening techniques, improving accuracy and efficiency.

Findings

Significant reduction in worst-case fixed-point residuals

Accurate worst-case performance matching true bounds

Applicable to diverse optimization problems

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.