Convex Optimization

Motivation

Many optimization problems in machine learning minimize an average of losses, one loss for each observation. A full gradient step examines every observation, while a stochastic gradient step examines one. The latter is cheaper per step, but its sampled gradient can remain noisy even near the optimum. Section 6.3 of Bubeck's monograph studies stochastic variance reduced gradient descent (SVRG), which periodically computes a full gradient at an anchor point and uses it to correct subsequent sampled gradients. The question for this mission is whether that correction gives a geometric reduction of the expected objective gap at the constants printed in Theorem 6.5.

Bubeck places this method alongside full gradient descent and stochastic gradient descent for finite sums. The section records that earlier stochastic average gradient and dual coordinate ascent methods attain a gradient-computation cost of order $(m+\kappa)\log(1/\varepsilon)$ for the same regime, where $m$ is the number of components and $\kappa$ is a condition number. The target here is the precise SVRG convergence statement in the book, rather than a comparison of implementation costs. The source's discussion on pp. 334–336 gives the context and the algorithm.

Setting

Let $f_1,\ldots,f_m:\mathbb R^n\to\mathbb R$ be differentiable convex functions, with $m\ge1$, and define the finite-sum objective and its gradient by

Each component is $\beta$-smooth when its gradient is $\beta$-Lipschitz in the Euclidean norm: $\|\nabla f_i(x)-\nabla f_i(z)\|_2\le\beta\|x-z\|_2$ for all $x,z$. The average $f$ is $\alpha$-strongly convex, meaning that for all $x,z$ it lies at least $\frac\alpha2\|z-x\|_2^2$ above its first-order affine approximation at $x$. The constants $\alpha$ and $\beta$ are positive, $x^*$ minimizes $f$ over $\mathbb R^n$, and $\kappa=\beta/\alpha$.

An epoch begins at an anchor $y$. Its first inner iterate is $x_1=y$. For $t=1,\ldots,k$, draw $i_t$ uniformly from $\{1,\ldots,m\}$, independently across steps and epochs, and update

The next anchor is the average $y^+=k^{-1}\sum_{t=1}^k x_t$. In particular, this average uses $x_1$ through $x_k$, while the last updated point $x_{k+1}$ is excluded. Starting from an arbitrary $y^{(1)}$ and repeating the epoch produces $y^{(s+1)}$. The expectation of $f(y^{(s+1)})$ is over all $sk$ sampled indices in the first $s$ epochs.

Formalization targets

Goal: geometric contraction across epochs

Theorem 6.5 sets $\eta=1/(10\beta)$ and $k=20\kappa$ and asserts, for every $s\ge1$,

The epoch length is a count, so the statement takes $k\in\mathbb N$ and explicitly requires $k=20\beta/\alpha$. The goal uses exactly the book's step size, epoch length, and contraction factor.

Milestones: second moments and a single epoch

Lemma 6.4 bounds $\mathbb E_i\|\nabla f_i(x)-\nabla f_i(x^*)\|_2^2$ by $2\beta(f(x)-f(x^*))$. Equation (6.3) bounds the second moment of the corrected sampled direction by the objective gaps at the current point and the anchor. Equation (6.2), the unbiased-direction display, and the one-step display express how that direction changes squared distance to $x^*$. The later display on p. 338 bounds one epoch for any positive step size with $2\beta\eta<1$. Finally, equation (6.1) substitutes the stated constants to obtain the factor $0.9$ for one epoch. These seven source claims form the milestone list in reading order.

Significance

The theorem gives an explicit accuracy guarantee after a specified number of epochs: an initial gap $D$ falls below $0.9^sD$ in expectation. Because each epoch uses a full gradient at its anchor as well as sampled component gradients, the result makes clear which quantity contracts and which operations are counted. It is a concrete linear-rate statement for a method whose individual stochastic gradients need not approach zero at the optimum. Bubeck, §6.3 discusses this issue when introducing the correction term.

The mathematical result is already proved in the monograph. The remaining task is to produce machine-checked proofs of its precise finite-sum model, the single-index estimates, the epoch inequality, and the full repeated-epoch guarantee. The mission drafts those statements and definitions; no proof is claimed for the open theorem items. The finite uniform-average representation and the separation between a conditional one-step average and the full multi-epoch average can be reused in other finite-sum stochastic algorithms.

Difficulty

The sampled component gradient $\nabla f_{i_t}(x_t)$ need not be small when $x_t$ is near $x^*$, so a bound using only its norm does not yield the desired fixed-step contraction. The correction $-\nabla f_{i_t}(y)+G(y)$ has mean zero relative to the full gradient at the current iterate, but its second moment still depends on both $x_t$ and $y$. The proof must control those two gaps while respecting the fact that $x_t$ depends on earlier samples. A single-index estimate with $x_t$ held fixed and an expectation over complete sample histories are different statements; confusing them would make the goal weaker or false.

Formalization scope

The carrier is EuclideanSpace ℝ (Fin n) with its usual inner product and norm. The Fin m components and every sample array are finite. A real-valued uniform average is an ordinary finite sum divided by the number of arrays, and $m\ge1$ and $k\ge1$ prevent an empty average. Independent uniform sampling is represented by averaging over every function from step positions to component indices. The multi-epoch sample space has one such block for every epoch. There are no integrals or measurability side conditions.

The component assumptions include differentiability with an explicit gradient map, convexity on all of $\mathbb R^n$, and the book's gradient-Lipschitz version of smoothness. Strong convexity is imposed on the average objective alone, using the published OnlineConvexOpt.ConvexBasics.StronglyConvexOn definition on the whole space. The book's standing notation assumes a minimizing $x^*$ exists; this is explicit. Positivity of $\alpha$ and $\beta$, and integrality of $20\beta/\alpha$, make the displayed divisions and epoch length meaningful. The general epoch bound also requires $0<\eta$ and $2\beta\eta<1$. Dimension zero is allowed: the theorem remains a statement about the unique point of $\mathbb R^0$ and its zero objective gap.

The direction always contains the sampled difference $\nabla f_{i_t}(x_t)-\nabla f_{i_t}(y)$ and the full anchor gradient $G(y)$. Replacing that direction with $G(x_t)$ would define gradient descent and would not satisfy this mission's algorithm. Contributions are welcome for the finite averaging identities, the component-gradient estimate, the conditional one-step calculation, the epoch inequality, and the induction across epochs.

Selected references

• Sébastien Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4), 2015, pp. 231–358. arXiv:1405.4980v2
• Rie Johnson and Tong Zhang, Accelerating Stochastic Gradient Descent using Predictive Variance Reduction, Advances in Neural Information Processing Systems 26 (NIPS), 2013 (the origin of SVRG, cited by Bubeck on p. 335). https://proceedings.neurips.cc/paper/2013/hash/ac1dd209cbcc5e5d1c6e28598e8cbbe8-Abstract.html

Motivation

MAXCUT asks for a partition of the vertices of a weighted graph into two sets that maximizes the total weight of the edges between them. It is one of Karp's original NP-hard problems, so no polynomial-time exact algorithm is expected, and the natural question is how close a polynomial-time algorithm can come to the optimum. Sampling a uniformly random partition already achieves, in expectation, half of the optimal value. For two decades this factor $1/2$ was essentially the best known.

Goemans and Williamson (J. ACM 42(6), 1995) replaced the combinatorial problem by a semidefinite relaxation, solvable in polynomial time by interior point methods, and rounded its solution with a random Gaussian hyperplane. They proved that the resulting cut has expected weight at least $0.878$ times the maximum. The technique founded the use of semidefinite programming in approximation algorithms. Khot, Kindler, Mossel and O'Donnell (SIAM J. Comput. 37(1), 2007) showed that, assuming the Unique Games Conjecture, no polynomial-time algorithm achieves a better constant. Nesterov (Optim. Methods Softw. 9, 1998) extended the rounding analysis to maximizing any positive semidefinite quadratic form over the hypercube, with the constant $2/\pi$.

This mission formalizes the presentation of these results in §6.6 of S. Bubeck, Convex Optimization: Algorithms and Complexity (arXiv:1405.4980v2), pp. 343–347.

Setting

Let $n\ge 0$ and let $A\in\mathbb R^{n\times n}$ be a symmetric matrix with non-negative entries; $A_{i,j}$ is the weight between points $i$ and $j$. The graph Laplacian is $L=D-A$, where $D$ is the diagonal matrix with entries $\sum_{j=1}^n A_{i,j}$. For $x\in\{-1,1\}^n$ the vector $x$ encodes a partition, and MAXCUT is (6.7)

Write $\langle M,X\rangle=\operatorname{Tr}(M^\top X)$ for the Frobenius inner product and $\mathbb S^n_+$ for the symmetric positive semidefinite matrices. Since $x^\top Lx=\langle L,xx^\top\rangle$ and $xx^\top\in\mathbb S^n_+$ has unit diagonal, MAXCUT is bounded above by the SDP relaxation

A solution $\Sigma$ of the relaxation is any feasible matrix attaining this maximum. The rounding draws $\xi\sim\mathcal N(0,\Sigma)$, a centered Gaussian vector with covariance $\Sigma$, and outputs $\zeta=\operatorname{sign}(\xi)\in\{-1,1\}^n$ coordinatewise.

Formalization targets

Goal: Theorem 6.11 (Goemans–Williamson)

For $A$ symmetric with non-negative entries, $L=D-A$, $\Sigma$ any solution of the relaxation, $\xi\sim\mathcal N(0,\Sigma)$ and $\zeta=\operatorname{sign}(\xi)$:

Milestones

1. Bounded entries. If $\Sigma\in\mathbb S^n_+$ and $\Sigma_{i,i}=1$, then $|\Sigma_{i,j}|\le 1$ (remark in the proof of Lemma 6.12).
2. Lemma 6.12 (Sheppard's formula). If $\xi\sim\mathcal N(0,\Sigma)$ with $\Sigma_{i,i}=1$ and $\zeta=\operatorname{sign}(\xi)$, then $\mathbb E\,\zeta_i\zeta_j=\frac{2}{\pi}\arcsin(\Sigma_{i,j})$.
3. Inequality (6.8). $1-\frac{2}{\pi}\arcsin(t)\ge 0.878(1-t)$ for all $t\in[-1,1]$.
4. Relaxation inequality. $\max_{x}x^\top Lx=\max_x\langle L,xx^\top\rangle\le\langle L,\Sigma\rangle$ for every solution $\Sigma$.

The separately stated Laplacian identity on p. 346 is also included as a theorem item: if $X_{i,i}=1$ for all $i$, then $\langle L,X\rangle=\sum_{i,j}A_{i,j}(1-X_{i,j})$; for $x\in\{-1,1\}^n$, $x^\top Lx=\sum_{i,j}A_{i,j}(1-x_ix_j)$.

Companion: Theorem 6.13 (Nesterov)

For $B\in\mathbb S^n_+$, $\Sigma$ a solution of $\max\{\langle B,X\rangle : X\in\mathbb S^n_+,\ X_{i,i}=1\}$, $\xi\sim\mathcal N(0,\Sigma)$ and $\zeta=\operatorname{sign}(\xi)$:

Significance

The result. Theorem 6.11 is a polynomial-time randomized $0.878$-approximation for MAXCUT: the relaxation is a semidefinite program, and sampling a Gaussian vector and taking signs is cheap. Repeated sampling turns the bound in expectation into a cut of value close to $0.878$ times the optimum with high probability. The same scheme of relaxation followed by randomized rounding underlies approximation algorithms for MAX-2SAT, correlation clustering and quadratic programs over the hypercube, and Nesterov's Theorem 6.13 is the version for an arbitrary positive semidefinite objective.

Formalizing it. Both theorems were proved long ago. To our knowledge neither has a machine-checked proof in Mathlib. The platform has related statements from other books, in different forms: Grothendieck's identity for a standard Gaussian and two unit vectors, and the relaxation guarantee with a Grothendieck constant. This mission states the textbook's results for a Gaussian with a possibly singular covariance matrix, which is the form the rounding uses. A complete development needs Sheppard's formula for a degenerate bivariate Gaussian, an elementary but careful real-variable inequality, and a link between Mathlib's multivariate Gaussian and Gram factorizations of $\Sigma$. All three are reusable.

Difficulty

The algebra (the Laplacian identity and milestone 4) is routine. The probabilistic core is Lemma 6.12. The textbook argument reduces it to the probability that a uniformly random direction separates two unit vectors, which is "a quick picture" on paper. In Lean this requires showing that the pair $(\xi_i,\xi_j)$ has the law of $(\langle V_i,\varepsilon\rangle,\langle V_j,\varepsilon\rangle)$ for a standard Gaussian $\varepsilon$, and then computing an angular measure in the plane, including the degenerate cases $\Sigma_{i,j}=\pm1$, where the pair is supported on a line. A density-based argument fails there, because $\mathcal N(0,\Sigma)$ has no density when $\Sigma$ is singular, and singular solutions of the relaxation occur (for instance $\Sigma=xx^\top$). Inequality (6.8) is a statement about a transcendental function on a closed interval with a tight constant ($0.878$ against the true minimum $\approx0.87856$), so crude estimates do not suffice near the minimizer $t\approx-0.689$.

Formalization scope

• Matrices are Matrix (Fin n) (Fin n) ℝ, vectors Fin n → ℝ. $\mathbb S^n_+$ is Matrix.PosSemidef, which includes symmetry, and $\langle M,X\rangle$ is trace (Mᵀ * X).
• $\mathcal N(0,\Sigma)$ is Mathlib's ProbabilityTheory.multivariateGaussian 0 Σ on EuclideanSpace ℝ (Fin n), defined for every positive semidefinite $\Sigma$, singular ones included. Expectations are Bochner integrals against it, and each theorem also asserts integrability of its (bounded) integrand.
• The sign is $\{-1,1\}$-valued: $\operatorname{sign}(r)=1$ for $r\ge0$ and $-1$ for $r<0$. Mathlib's Real.sign would give $\operatorname{sign}(0)=0$, which takes $\zeta$ out of $\{-1,1\}^n$; the two agree almost surely because $\Sigma_{i,i}=1$.
• The maximum over the hypercube is a finite maximum (Finset.sup') over the $2^n$ Boolean vectors read as $\pm1$ vectors, so it is never a junk value. "The solution" of the relaxation means any maximizer, and maximizers exist since the feasible set is compact and contains the identity.
• Standing hypotheses: in Theorem 6.11, $A$ symmetric with non-negative entries (the book's MAXCUT setting); in Lemma 6.12, $\Sigma$ positive semidefinite (implicit in "$\xi\sim\mathcal N(0,\Sigma)$"); in Theorem 6.13, $B$ positive semidefinite. The identities of milestones 4 and 5 hold for every real matrix $A$ and are stated without hypotheses on $A$.
• Ruled out: tying $\xi$'s law to anything other than $\Sigma$, or dropping optimality of $\Sigma$, would make the goal false or vacuous; here the law is exactly $\mathcal N(0,\Sigma)$ and $\Sigma$ is a maximizer.
• Welcome contributions: Sheppard's formula in Mathlib's multivariate Gaussian language, a proof of (6.8), and the Schur product theorem ($A,B\succeq0\Rightarrow A\circ B\succeq0$) used in Theorem 6.13.

Selected references

• S. Bubeck, Convex Optimization: Algorithms and Complexity, Foundations and Trends in Machine Learning 8(3–4):231–358, 2015. arXiv:1405.4980v2
• M. X. Goemans, D. P. Williamson, Improved approximation algorithms for maximum cut and satisfiability problems using semidefinite programming, J. ACM 42(6):1115–1145, 1995. doi:10.1145/227683.227684
• Yu. Nesterov, Semidefinite relaxation and nonconvex quadratic optimization, Optim. Methods Softw. 9(1–3):141–160, 1998. doi:10.1080/10556789808805690
• S. Khot, G. Kindler, E. Mossel, R. O'Donnell, Optimal inapproximability results for MAX-CUT and other 2-variable CSPs?, SIAM J. Comput. 37(1):319–357, 2007. doi:10.1137/S0097539705447372
• W. F. Sheppard, On the application of the theory of error to cases of normal distribution and normal correlation, Phil. Trans. R. Soc. A 192:101–167, 1899. doi:10.1098/rsta.1899.0003