math.LO — Logic

The Logical Anatomy of Optimization: Reverse Mathematics, Proof Mining, and the Price of Convergence

Contributed by Xiaoyu Li

Optimization theory proves three kinds of theorems: that optimal points exist, that algorithms converge to them, and that optimality can be certified by duality. We measure how much mathematics each kind needs, using reverse mathematics, Weihrauch complexity and proof mining, and assemble the answers, old and new, into one map stated in the language of optimization. Compactness makes existence cost weak Kőnig's lemma, but convexity (and, format by format, tameness) makes it cheap: we show that $\mathsf{RCA}_0$ proves that convex functions on $[0,1]$ attain their minima (and on $[0,1]^n$, for each fixed $n$, given a modulus of uniform continuity), and that $\mathsf{RCA}_0$ proves linear programming duality and the minimax theorem for real data of every size. Convergence costs more: it follows from results of Kohlenbach and Neumann that convergence of gradient descent for convex smooth functions on $\mathbb{R}$ is equivalent to $\mathsf{ACA}_0$. We explain this by a selection principle: what costs is the particular minimizer the algorithm selects, and uniqueness or an error bound removes the cost. Below convergence lies finitary information. Gradient descent in $\mathbb{R}^d$ has at most $2C_dD/\varepsilon$ fluctuations of size $\varepsilon$, with $C_d$ depending only on $d$, which yields rates of metastability; no such bound is dimension-free, by the span-restriction argument behind performance estimation; and the limits of gradient descent on computable instances have d.c.e. coordinates, a proper subclass of the limit-computable reals. The map also covers Ekeland's variational principle (up to $\Pi^1_1\text{-}\mathsf{CA}_0$), separation theorems, Kőnig duality ($\mathsf{ATR}_0$), proof-mined rates for fixed-point iterations, and the feasible world, where local search captures the $\mathsf{NP}$ search problems provably total in $T^1_2$ and approximate stationary points of smooth functions are complete for $\mathsf{CLS}=\mathsf{PPAD}\cap\mathsf{PLS}$. We close with five principles and open problems.