We introduce a numerical framework to verify the finite step convergence of first-order methods for parametric convex quadratic optimization. We formulate the verification problem as a mathematical optimization problem where we maximize a performance metric (e.g., fixed-point residual at the last iteration) subject to constraints representing proximal algorithm steps (e.g., linear system solutions, projections, or gradient steps). Our framework is highly modular because we encode a wide range of proximal algorithms as variations of two primitive steps: affine steps and element-wise maximum steps. Compared to standard convergence analysis and performance estimation techniques, we can explicitly quantify the effects of warm-starting by directly representing the sets where the initial iterates and parameters live. We show that the verification problem is NP-hard, and we construct strong semidefinite programming relaxations using various constraint tightening techniques. Numerical examples in nonnegative least squares, network utility maximization, Lasso, and optimal control show a significant reduction in pessimism of our framework compared to standard worst-case convergence analysis techniques.
We introduce a new technique for solving uni-parametric versions of linear programs, convex quadratic programs, and linear complementarity problems in which a single parameter is permitted to be present in any of the input data. We demonstrate the use of our method on a small, motivating example and present the results of a small number of computational tests demonstrating its utility for larger scale problems.
We consider parametric Markov decision processes (pMDPs) that are augmented with unknown probability distributions over parameter values. The problem is to compute the probability to satisfy a temporal logic specification with any concrete MDP that corresponds to a sample from these distributions. As solving this problem precisely is infeasible, we resort to sampling techniques that exploit the so-called scenario approach. Based on a finite number of samples of the parameters, the proposed method yields high-confidence bounds on the probability of satisfying the specification. The number of sa…
This paper studies symmetric constrained linear-quadratic optimal control problems and their parametric solutions. The parametric solution of such a problem is a piecewise-affine feedback law that can be equivalently expressed as a set of active sets. We show symmetries of the optimal control problem entail symmetries of the active sets, which can be used to simplify finding the set of active sets considerably. Specifically, we improve a recently proposed method for the dynamic-programming-based enumeration of all active sets. The achieved reduction of the computational effort is illustrated w…
Certifying the safety or robustness of neural networks against input uncertainties and adversarial attacks is an emerging challenge in the area of safe machine learning and control. To provide such a guarantee, one must be able to bound the output of neural networks when their input changes within a bounded set. In this paper, we propose a semidefinite programming (SDP) framework to address this problem for feed-forward neural networks with general activation functions and input uncertainty sets. Our main idea is to abstract various properties of activation functions (e.g., monotonicity, bound…
Compact Optimality Verification for Optimization Proxies
Georgia Institute of Technology（佐治亚理工学院）；NSF Artificial Intelligence Research Institute for Advances in Optimization (AI4OPT)（美国国家科学基金会优化人工智能研究所（AI4OPT））
本文针对优化代理的最优性验证问题，提出了一种紧凑公式和基于梯度的原始启发式方法，显著提升了计算效率并适用于非凸优化，在大规模 DC Optimal Power Flow 和 knapsack 问题上验证了其优势。
