Machine Learning

Motivation

Lower bounds for interactive decision making (bandits, reinforcement learning, and the general decision making with structured observations framework of Foster, Kakade, Qian and Rakhlin, arXiv:2112.13487) compare what a learner observes under two different environments. A learner's whole interaction history is generated one step at a time: each observation is drawn from a conditional law that depends on everything seen before. Statistical estimation guarantees, by contrast, are stated one step at a time, as bounds on the divergence between the conditional laws at each round. Passing from the per-step guarantees to a statement about the laws of entire histories requires a chain rule for the divergence in use.

For the Kullback–Leibler divergence the chain rule is an identity. The paper's guarantees, however, are stated in the squared Hellinger distance, which is bounded, symmetric, and the natural loss for density estimation with the logarithmic loss. Hellinger distance has no exact chain rule. Lemma A.13 of the paper (App. A.2, p. 73) supplies an approximate one, losing a factor logarithmic in the number of steps, and the paper uses it in the proof of its main regret lower bound (Theorem 3.2, via App. C.1.3).

Setting

Fix $n \in \mathbb N$ and finite sets $\mathcal X_1, \dots, \mathcal X_n$. A sequence is $x = (x_1, \dots, x_n)$ with $x_i \in \mathcal X_i$, and $x_{1:i-1} = (x_1, \dots, x_{i-1})$ denotes its prefix; $\mathcal X^{(i-1)} = \prod_{t=1}^{i-1} \mathcal X_t$.

For probability distributions $p, q$ on a finite set, the squared Hellinger distance, the Hellinger distance and the Kullback–Leibler divergence are

the last one set to $+\infty$ when $p$ charges a point that $q$ does not. Note that the paper's $D^2_{\mathrm H}$ carries no factor $\tfrac12$, so $0 \le D^2_{\mathrm H} \le 2$.

A family of sequential kernels $P = (P^{(i)})_{i=1}^n$ assigns to each $i$ and each prefix $x_{1:i-1}$ a probability distribution $P^{(i)}(\cdot \mid x_{1:i-1})$ on $\mathcal X_i$. Its sequential law is the law of $X_1, \dots, X_n$ under $X_i \sim P^{(i)}(\cdot \mid X_{1:i-1})$:

For a second family $Q$ with law $\mathbb Q$, the quantity controlled by per-step estimation is

In Lean these are IsSeqKernel, seqLaw and condHellingerSum, with hellingerSq and klDivDiscrete the published discrete divergences.

Formalization targets

Goal: Lemma A.13, (97), for $n \ge 2$

The constant $10^2$ is the paper's; the shape that matters downstream is the logarithmic dependence on $n$ with no assumption on the kernels beyond their being probability kernels.

Companion: Lemma A.13, (98)

If $V \ge e$ and $P^{(i)}(A \mid x_{1:i-1}) \le V\, Q^{(i)}(A \mid x_{1:i-1})$ for every $i$, prefix and event $A$, then $D^2_{\mathrm H}(\mathbb P, \mathbb Q) \le 3\log(V) \cdot \mathbb E_{\mathbb P}[\sum_i D^2_{\mathrm H}(P^{(i)}, Q^{(i)})]$.

Milestones

1. Lemma A.10 (p. 72): $D_{\mathrm{KL}}(p\,\|\,q) \le (2 + \log V)\, D^2_{\mathrm H}(p, q)$ under a likelihood-ratio bound $V$ (referenced, finite case).
2. Lemma A.5 (p. 71): $D^2_{\mathrm{TV}} \le D^2_{\mathrm H} \le D_{\mathrm{KL}}$ (referenced, finite case).
3. The triangle inequality for $D_{\mathrm H}$ (proof of Lemma A.13, p. 73).
4. The chain rule $D_{\mathrm{KL}}(\mathbb Q\,\|\,\mathbb P) = \mathbb E_{\mathbb Q}[\sum_i D_{\mathrm{KL}}(Q^{(i)}\,\|\,P^{(i)})]$ for sequential laws (p. 73).
5. Convexity of $D^2_{\mathrm H}$ in its second argument (p. 74).
6. Lemma A.11 (p. 72), the multiplicative Pinsker-type inequality: $|\mathbb E_P h - \mathbb E_Q h| \le \sqrt{2R(\mathbb E_P h + \mathbb E_Q h) D^2_{\mathrm H}(P, Q)}$ and $\mathbb E_P h \le 3\mathbb E_Q h + 4R\, D^2_{\mathrm H}(P, Q)$ for $0 \le h \le R$.

Significance

The result. Inequality (97) converts per-round Hellinger estimation error into a bound on the Hellinger distance between the laws of complete interaction histories, under no boundedness assumption on likelihood ratios. In the paper this is the step that lets the lower bound of Theorem 3.2 relate any algorithm's behaviour under a reference model to its behaviour under alternatives, and hence express the minimax regret through the decision-estimation coefficient. Without it, only the KL chain rule is available, which requires bounded likelihood ratios (the situation of (98)) or loses more than a logarithmic factor. Lemma A.11, a milestone here, is used independently in the same lower bound and in the paper's tabular reinforcement learning analysis.

Formalizing it. The lemma is proved in the paper; no machine-checked proof exists. The published layer on the platform has the discrete divergences and the comparisons of Lemmas A.5 and A.10; the sequential-law objects, the triangle inequality, the convexity of $D^2_{\mathrm H}$, the discrete chain rule and Lemma A.11 are new. A completed development gives a reusable chain-rule toolkit for any later formalization of lower bounds over adaptive interaction histories.

Difficulty

The squared Hellinger distance does not tensorize along adaptive sequences: the natural attempt to write $1 - \tfrac12 D^2_{\mathrm H}(\mathbb P, \mathbb Q)$ as a product of conditional affinities fails because the conditional affinities are random, depending on the prefix, and their expectation does not factor. Bounding $D^2_{\mathrm H}$ by $D_{\mathrm{KL}}$ and applying the KL chain rule fails in the other direction: the conditional KL divergences are not controlled by the conditional Hellinger distances unless the likelihood ratios are bounded, and in (97) they are not. The difficulty is to obtain a bound that pays only $\log n$ for an unbounded ratio, with explicit constants that survive the final numerical comparison.

Formalization scope

• Finite alphabets. The paper works over measurable spaces. This mission formalizes the finite-alphabet case, as the published FoundationsRL divergence layer does: each $\mathcal X_i$ is a Fintype, distributions are probability vectors, expectations are finite sums. Coordinates are indexed by Fin n (0-based) and the alphabets may differ from coordinate to coordinate.
• Kernels. A kernel family is a function P i x of the whole sequence that is a probability vector and depends only on the coordinates j < i; this is what makes seqLaw P the law the paper describes.
• Added hypothesis $n \ge 2$ in (97). The paper states (97) for every $n$; at $n = 1$ the right side vanishes because $\log 1 = 0$ while the left side is positive whenever $P^{(1)} \ne Q^{(1)}$, and the proof's last step $2(6\log(96n) + \tfrac{18}{96n}) \le 10^2\log n$ holds only for $n \ge 2$. The goal is stated for $n \ge 2$, with the constant unchanged.
• Likelihood ratios are stated multiplicatively, $P(A) \le V\,Q(A)$, so that a zero denominator does not make a hypothesis vacuous; KL divergences are compared to Hellinger distances in $[0, \infty]$.
• Lemma A.11 holds "almost surely under $P$ and $Q$", which becomes: $0 \le h \le R$ at every point charged by $P$ or $Q$.
• Ruling out trivial forms. The goal's hypotheses are satisfiable with $\mathbb P \ne \mathbb Q$ and $n \ge 2$ (checked in a sanity file). A formalization in which the kernels may read coordinates beyond the prefix, in which $\log$ is applied to $n \le 1$, or in which the ratio bound of (98) is checked through a quotient that is vacuous at zero denominators, is not the paper's statement.

Contributions welcome: proofs of any milestone and of the fact that seqLaw is a probability vector.

Selected references

• D. J. Foster, S. M. Kakade, J. Qian, A. Rakhlin, The Statistical Complexity of Interactive Decision Making, arXiv:2112.13487v3, 2023. https://arxiv.org/abs/2112.13487
• Y. Yang, A. Barron, An asymptotic property of model selection criteria, IEEE Transactions on Information Theory 44(1), 1998. https://doi.org/10.1109/18.650993
• Y. Polyanskiy, Y. Wu, Lecture Notes on Information Theory, 2014. https://people.lids.mit.edu/yp/homepage/data/itlectures_v5.pdf
• D. J. Foster, A. Rakhlin, Foundations of Reinforcement Learning and Interactive Decision Making, arXiv:2312.16730v1, 2023. https://arxiv.org/abs/2312.16730

Motivation

Neural networks trained by empirical risk minimization are sensitive to small, deliberately chosen perturbations of their inputs ("adversarial examples"). A standard defence is adversarial training: at each step, perturb the training example to increase the loss, then take a gradient step at the perturbed point. Sinha, Namkoong, Volpi and Duchi (arXiv:1710.10571, ICLR 2018) recast adversarial training as distributionally robust optimization over a Wasserstein ball around the data distribution, and replaced the hard ball constraint by a Lagrangian penalty. The resulting procedure perturbs each example by solving a penalized inner maximization, and the paper shows that, when the penalty is large enough relative to the smoothness of the loss, this inner problem is strongly concave and therefore tractable.

This mission formalizes the paper's computational guarantee, Theorem 2: stochastic gradient descent on the penalized robust objective, with an inexact adversary, reaches an approximate stationary point at the rate of smooth nonconvex stochastic optimization. The analysis follows Ghadimi and Lan's argument for nonconvex SGD (arXiv:1309.5549), adapted to a gradient oracle that is biased by the inexact inner maximization.

Setting

Parameters $\theta$ live in $\Theta=\mathbb R^d$ and data in a set $Z\subseteq\mathbb R^m$; both spaces carry the Euclidean norm $\|\cdot\|_2$. Data are drawn from a probability distribution $P_0$ on $Z$.

A transportation cost $c:Z\times Z\to[0,\infty)$ measures how expensive it is to move a data point $z_0$ to $z$. Assumption A: $c$ is continuous, $c(z,z)=0$, and for each $z_0\in Z$ the map $z\mapsto c(z,z_0)$ is $1$-strongly convex. The canonical example is $c(z,z_0)=\tfrac12\|z-z_0\|_2^2$.

A loss $\ell(\theta;z)$ has partial gradients $\nabla_\theta\ell$ and $\nabla_z\ell$. Assumption B: these gradients are Lipschitz in each argument,

For a penalty $\gamma>0$, the robust surrogate and the robust objective are

By Wasserstein duality, $F(\theta)$ equals the worst-case expected loss over all distributions $P$, penalized by $\gamma$ times the transport distance from $P$ to $P_0$.

Algorithm 1 (with $\Theta=\mathbb R^d$ and constant stepsize $\alpha$): from $\theta^0$, for $t=0,\dots,T-1$, draw $z^t\sim P_0$ independently, find an $\epsilon$-approximate maximizer $\hat z^t\in Z$, meaning $\ell(\theta^t;\hat z^t)-\gamma c(\hat z^t,z^t)\ge\varphi_\gamma(\theta^t;z^t)-\epsilon$, and set $\theta^{t+1}=\theta^t-\alpha\nabla_\theta\ell(\theta^t;\hat z^t)$.

Formalization targets

Goal: Theorem 2 (p. 6)

Let $\gamma>L_{zz}$, $L_\varphi=L_{\theta\theta}+L_{\theta z}L_{z\theta}/(\gamma-L_{zz})$, $\Delta_F\ge F(\theta^0)-\inf_\theta F(\theta)$, and assume $\mathbb E\|\nabla F(\theta)-\nabla_\theta\varphi_\gamma(\theta;Z)\|_2^2\le\sigma^2$ for all $\theta$. With $\alpha=\sqrt{\Delta_F/(L_\varphi T\sigma^2)}$ and $T\ge L_\varphi\Delta_F/\sigma^2$,

Milestones

1. (4), p. 4: for $\gamma\ge L_{zz}$, $z\mapsto\ell(\theta;z)-\gamma c(z,z_0)$ is $(\gamma-L_{zz})$-strongly concave.
2. Lemma 1, p. 5: the supremum $\bar f(\theta)=\sup_{z\in Z}f(\theta,z)$ of a $\lambda$-strongly concave family satisfying Assumption B is differentiable, with $\nabla\bar f(\theta)=\nabla_\theta f(\theta,z_\star(\theta))$, a $(L_{z\theta}/\lambda)$-Lipschitz maximizer and a $(L_{\theta\theta}+L_{\theta z}L_{z\theta}/\lambda)$-Lipschitz gradient.
3. §2.1, p. 6: $\varphi_\gamma(\cdot;z_0)$ has $L_\varphi$-Lipschitz gradient $\nabla_\theta\varphi_\gamma(\theta;z_0)=\nabla_\theta\ell(\theta;z_\star(z_0,\theta))$.
4. (31) and (32), p. 40: the descent inequality for an $L_\varphi$-smooth objective, and its form with the bias $\delta=g-\nabla_\theta\varphi_\gamma$ separated, for $\alpha\le1/L_\varphi$.
5. The bias bound, p. 41: $\|\delta\|_2^2\le 2L_{\theta z}^2\epsilon/(\gamma-L_{zz})$.
6. The one-step bound in conditional expectation and the averaged bound, p. 41:

for every constant stepsize $0<\alpha\le1/L_\varphi$. The goal is this bound at the balancing stepsize.

Significance

The result. Theorem 2 certifies that the robust training procedure is no harder, in iteration count, than ordinary nonconvex SGD: the stationarity measure decays as $T^{-1/2}$, and the inexactness of the adversary enters only as an additive term proportional to $\epsilon$, independent of $T$. This is what licenses running a few steps of gradient ascent for the inner problem rather than solving it exactly. It also explains the role of the penalty: the guarantee requires $\gamma>L_{zz}$, so smoothness of the loss in the data (smooth activations rather than ReLUs) is what makes the robust problem tractable.

Formalizing it. The result and its proof are published; nothing here is open. To our knowledge none of it is machine-checked. A formal proof would add a verified Danskin-type theorem for strongly concave suprema with explicit Lipschitz constants (Lemma 1), which is reusable well beyond this paper, and a verified nonconvex SGD analysis with a biased oracle, including the measure-theoretic bookkeeping (independence of the fresh sample from the current iterate, differentiation under the integral) that the paper's proof compresses into one line.

Difficulty

The deterministic inequalities (31), (32) and the bias bound are short. The weight sits elsewhere. First, Lemma 1 requires differentiability of a supremum over a possibly unbounded set, with the maximizer depending on $\theta$; the paper invokes a Danskin-type theorem that is not in Mathlib, and the cost $c$ is not assumed differentiable, so the first-order optimality conditions for the inner problem must be derived from strong convexity alone. Second, the expectation step uses $\mathbb E[\nabla_\theta\varphi_\gamma(\theta^t;z^t)\mid\theta^t]=\nabla F(\theta^t)$, which needs both differentiation under the integral sign for $F$ and the independence of $z^t$ from $\theta^t$ along the run. Third, finiteness of every expectation along the run is not assumed and must be propagated from step to step.

Formalization scope

Lean representation: $\Theta$ and $\mathbb R^m$ are EuclideanSpace ℝ (Fin d) and EuclideanSpace ℝ (Fin m); $Z$ is a set in the latter. The loss is a function on all of $\mathbb R^d\times\mathbb R^m$; its partial gradients are required at points of $Z$ and the Lipschitz conditions on $Z$ only. Strong convexity is Mathlib's StrongConvexOn, whose modulus convention matches the paper. Suprema are sSup over the image of $Z$. $F$ is a Bochner integral, and $\varphi_\gamma(\theta;\cdot)$ is assumed $P_0$-integrable for every $\theta$. The run is driven by $(z^0,\dots,z^{T-1})\sim P_0^{\otimes T}$ (Measure.pi). The expectations in the conclusion and in the variance hypothesis are lower Lebesgue integrals in $[0,\infty]$; the $\epsilon$-term of Theorem 2 is moved to the right-hand side.

Hypotheses made explicit that the paper leaves implicit: $\gamma>L_{zz}$ (the paper writes $\gamma\ge L_{zz}$ but divides by $\gamma-L_{zz}$); $Z$ nonempty, convex and closed; Lipschitz constants nonnegative; $\sigma>0$, $\Delta_F>0$, $T\ge1$, $\epsilon\ge0$; $F$ bounded below (so $\inf_\theta F$ is a real number); integrability of $\varphi_\gamma(\theta;\cdot)$; $P_0(Z)=1$; joint measurability of the oracle $(\theta,z_0)\mapsto\hat z(\theta,z_0)$; and, in (32) and the later milestones, $0<\alpha\le1/L_\varphi$, which the paper assumes "in the rest of the proof". Lemma 1 is specialized to the Euclidean norm, the case Theorem 2 uses. The cost $c$ is not assumed differentiable.

A trivializing formalization is ruled out: the run uses an oracle tied to $\varphi_\gamma$ by the $\epsilon$-gap and to $Z$ by membership, $\varphi_\gamma$ is the supremum of the penalized loss over $Z$, $F$ is its $P_0$-integral, and the hypotheses are satisfiable (for instance $\ell(\theta;z)=\tfrac12\|\theta\|^2$, $c(z,z_0)=\tfrac12\|z-z_0\|^2$, $Z=\mathbb R^m$, $P_0$ a point mass, $\epsilon=0$). Expectations as lower integrals prevent a non-integrable $\|\nabla F(\theta^t)\|^2$ from being read as $0$.

Infrastructure a complete development needs: the descent lemma for functions with Lipschitz gradient; first-order characterizations of strong concavity on a convex set; a Danskin/envelope theorem for strongly concave suprema; differentiation under the integral for $F$; and conditional-expectation bookkeeping for Markov-type recursions driven by i.i.d. samples on a finite product space. The first three are reusable in any minimax or bilevel analysis. Contributions to any milestone, or to these supporting facts as separate lemmas, are welcome.

Selected references

• A. Sinha, H. Namkoong, R. Volpi, J. Duchi, Certifying Some Distributional Robustness with Principled Adversarial Training, ICLR 2018; arXiv:1710.10571v5, 2020. https://arxiv.org/abs/1710.10571
• S. Ghadimi, G. Lan, Stochastic First- and Zeroth-Order Methods for Nonconvex Stochastic Programming, SIAM Journal on Optimization 23(4), 2013. https://doi.org/10.1137/120880811
• J. F. Bonnans, A. Shapiro, Perturbation Analysis of Optimization Problems, Springer, 2000. https://doi.org/10.1007/978-1-4612-1394-9
• R. Gao, A. Kleywegt, Distributionally Robust Stochastic Optimization with Wasserstein Distance, Mathematics of Operations Research 48(2), 2023; arXiv:1604.02199. https://arxiv.org/abs/1604.02199

Motivation

Online combinatorial optimization is a repeated game in which a learner selects, round after round, a structured object (a subset of fixed size, a path, a matching, a spanning tree) encoded as a 0/1 vector, and an adversary assigns a cost to every coordinate. It models routing, ranking, scheduling and many other sequential decision problems in operations research and machine learning, and it contains prediction with expert advice as the special case of one-hot vectors.

The most widely used algorithm for this game is the exponentially weighted forecaster, which keeps a weight on every action and multiplies it by $\exp(-\eta\cdot\text{loss})$ after each round. Applied to a combinatorial action set it is called EXP2 (Audibert, Bubeck and Lugosi), or Expanded Hedge in the full-information case (Koolen, Warmuth and Kivinen, COLT 2010). Its standard analysis gives regret of order $m^{3/2}\sqrt{n\log(d/m)}$, while online mirror descent with the negative entropy (Component Hedge) achieves $m\sqrt{n\log(d/m)}$, which is optimal. Koolen, Warmuth and Kivinen left open whether a better tuning or a better analysis of EXP2 could close this gap.

Timeline.

• 1997: Freund and Schapire analyse Hedge for experts.
• 2010: Koolen, Warmuth and Kivinen introduce Component Hedge, prove the $m\sqrt{n\log(d/m)}$ bound, and ask whether Expanded Hedge can match it.
• 2012–2014: Audibert, Bubeck and Lugosi (arXiv:1204.4710; Math. Oper. Res. 39(1), 2014) answer negatively: Theorem 1 exhibits an action set on which EXP2's full-information regret is at least $0.01\,d^{3/2}\sqrt n$ for every learning rate.

Setting

Fix integers $d$ (the dimension) and $n$ (the number of rounds). An action set is a nonempty finite set $\mathcal A\subseteq\{0,1\}^d$ whose elements all have the same number $m$ of ones: $\|a\|_1=m$ for every $a\in\mathcal A$. At each round $t=1,\dots,n$:

1. the player chooses a probability distribution $p_t$ on $\mathcal A$ and draws $a_t\sim p_t$;
2. simultaneously, the adversary chooses a loss vector $z_t\in[0,1]^d$;
3. the player pays $a_t^\top z_t$ and, in the full-information game, observes $z_t$.

The regret after $n$ rounds is

EXP2 with learning rate $\eta$ starts from the uniform distribution $p_1$ on $\mathcal A$ and updates, for every $a\in\mathcal A$,

In the Lean development IsBinaryActionSet A m is the action-set condition, exp2Weights A η z t is $p_{t+1}$, and exp2Regret A η z n is $R_n$ against a fixed loss sequence $z$. thmOneSet d, adv1 d and adv2 d ε are the action set and the two adversaries of the paper's proof.

Formalization targets

Goal: Theorem 1 (p. 6)

For $n\ge d$ with $d$ a multiple of $4$, there is an action set $\mathcal A\subseteq\{0,1\}^d$ with constant $\|a\|_1$ such that for every $\eta\ge0$ some adversary with losses in $[0,1]^d$ makes EXP2 pay

The action set is chosen before the learning rate, and the adversary after it.

Milestones (App. A and App. C)

1. Lemma 3 (p. 19): for $k\ge1$ and $1\le c\le 2$,

2. First adversary (p. 15): on the action set of App. A, against the alternating adversary, $R_n=\frac{nd}{16}\tanh\frac{\eta d}{8}$ for $n$ even.
3. Second adversary (p. 16): against the constant adversary with $\varepsilon=\min(\log2/(\eta n),1)$, $R_n\ge\min\bigl(\frac{d\log2}{12\eta},\frac{nd}{12}\bigr)$ for $\eta>0$.
4. Optimization over $\eta$ (pp. 14–15): for every $\eta>0$,

Significance

The result. Theorem 1 shows that the gap between EXP2 and mirror descent with the negative entropy is not an artefact of the analysis: on an action set with $m=d/2$, where the optimal rate is of order $d\sqrt n$, no learning rate brings EXP2 below $0.01\,d^{3/2}\sqrt n$. Exponential weights over the actions are therefore provably suboptimal in online combinatorial optimization, which motivates working with the convex hull of $\mathcal A$ (mirror descent) rather than with the actions themselves. The construction is also a template for algorithm-specific lower bounds: two adversaries, one punishing large and one punishing small learning rates.

Formalizing it. The result is proved in the paper (App. A, with Lemma 3 in App. C); to our knowledge none of it is machine-checked. A formalization yields a checked algorithm-specific lower bound for exponential weights, an exact closed-form regret computation for EXP2 on a structured action set, and a rigorous proof of Lemma 3, whose printed proof checks $k\le10^6$ numerically before an asymptotic argument with Stirling's formula.

Difficulty

The statements are elementary, but each step hides a real computation. The first adversary requires the exact distribution of EXP2 on a set of $2\binom{d/2}{d/4}$ actions over alternating rounds, and a regret identity rather than a bound. The second requires controlling EXP2's expected loss over all $n$ rounds against a constant adversary on the same exponentially large set. Lemma 3 is the hardest piece: at $c=2$ it is tight at $k=1$, while the ratio tends to $1-\sqrt2/(1+\sqrt2)\approx0.414$ as $k\to\infty$; the printed proof verifies $k\le10^6$ numerically, so a formal proof needs an argument valid for every $k$. A naive attempt to prove the goal with a single adversary fails: one adversary only defeats either large or small learning rates.

Formalization scope

• Actions are real vectors Fin d → ℝ with entries in $\{0,1\}$, so $a^\top z$ is the dot product. Coordinates and rounds are 0-based: the paper's odd rounds are the even indices.
• EXP2 is defined by the recursion of Figure 2 with $\tilde z_t=z_t$, starting uniform on $\mathcal A$; its closed form $p_t(a)\propto\exp(-\eta\sum_{s<t}a^\top z_s)$ is a consequence, not the definition.
• The regret is defined against a deterministic, oblivious loss sequence, for which the expectation is a finite sum. Exhibiting such an adversary proves the paper's $\sup_{\text{adversary}}$, since it is a special case of the paper's adaptive adversaries.
• The minimum over $\mathcal A$ is a Finset.inf'; every statement requires $\mathcal A$ nonempty, so no junk value enters.
• Added hypotheses: $4\mid d$ in the goal (the proof's own simplifying assumption; the printed statement fails at $d=1$, where any constant-norm $\mathcal A$ is a singleton); $\eta>0$ and $n\ge1$ wherever $1/\eta$ or $1/(\eta n)$ appears. The goal does not assume $n$ even, although App. A does; the second-adversary milestone does not need it either.
• The action set of App. A is printed with "or"; it is formalized with exactly one of the two intervals filled, as the prose and the constant norm $\|a\|_1=d/2$ require.
• Ruled out: an existential over $\eta$, an adversary chosen before $\eta$, an action set depending on $\eta$, unbounded losses, and an empty action set with a junk minimum would each make the goal trivial or different; the statement quantifies as above.

Contributions welcome: proofs of the milestones, a proof of Lemma 3 by any method, and reusable lemmas on exponential weights (normalization, closed form, monotonicity of weights along a constant adversary). The paper's proofs are in its App. A and App. C.

Selected references

• J.-Y. Audibert, S. Bubeck, G. Lugosi, Regret in Online Combinatorial Optimization, Math. Oper. Res. 39(1), 2014; arXiv:1204.4710v2. https://arxiv.org/abs/1204.4710
• W. M. Koolen, M. K. Warmuth, J. Kivinen, Hedging Structured Concepts, Proceedings of COLT 2010 (reference [26] of the paper above).
• Y. Freund, R. E. Schapire, A Decision-Theoretic Generalization of On-Line Learning and an Application to Boosting, J. Comput. Syst. Sci. 55(1), 1997. https://doi.org/10.1006/jcss.1997.1504
• S. Bubeck, N. Cesa-Bianchi, Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems, Found. Trends Mach. Learn. 5(1), 2012; arXiv:1204.5721. https://arxiv.org/abs/1204.5721

Motivation

Stochastic gradient methods are the standard tool for minimizing an objective that can only be accessed through noisy gradient samples. Training a machine-learning model on sampled data, simulation-based optimization, and stochastic programs with endogenous uncertainty are all of this kind. In many of these applications the objective is nonconvex: the loss or the regularizer of a learning problem may be nonconvex, as may the expected cost of a simulation model.

Before 2013 the complexity theory of stochastic approximation (SA) was essentially a convex theory. Robbins and Monro (1951) introduced the method. Polyak and Juditsky (1992) and Nemirovski, Juditsky, Lan and Shapiro (2009) established optimal rates for convex problems, and Lan (2012) unified the smooth, nonsmooth and stochastic convex cases. None of these results covered nonconvex objectives. Ghadimi and Lan (2013) gave the first non-asymptotic complexity bound for a stochastic gradient method on a smooth nonconvex problem. The bound is stated for the expected squared gradient norm at a randomly chosen iterate, and it is the result this mission formalizes.

Setting

The problem is

where $f:\mathbb R^n\to\mathbb R$ is differentiable and bounded below, and its gradient is $L$-Lipschitz: $\|\nabla f(y)-\nabla f(x)\|\le L\|y-x\|$ for all $x,y$. This class is written $\mathcal C^{1,1}_L(\mathbb R^n)$. The function need not be convex.

The gradient is accessible only through a stochastic first-order oracle: at the $k$-th query point $x_k$ it returns $G(x_k,\xi_k)$, where $\xi_1,\xi_2,\dots$ are random variables and $G$ is a Borel function. Assumption A1 asks that for every $k\ge1$, conditionally on the past, $G(x_k,\xi_k)$ is an unbiased estimate of $\nabla f(x_k)$, and that its error $\delta_k=G(x_k,\xi_k)-\nabla f(x_k)$ has second moment $\mathbb E\|\delta_k\|^2\le\sigma^2$. The noise variables need not be independent of each other or of the iterates.

The randomized stochastic gradient (RSG) method takes an initial point $x_1$, an iteration limit $N$, stepsizes $\gamma_k$ and a probability mass function $P_R$ on $\{1,\dots,N\}$. It draws a random index $R\sim P_R$, runs

and outputs $x_R$. The mass function used in the main theorem is

The constants are $D_f=[2(f(x_1)-f^*)/L]^{1/2}$ and, in the convex case with minimizer $x^*$, $D_X=\|x_1-x^*\|$.

Formalization targets

Goal: Theorem 2.1 a)

If $0<\gamma_k<2/L$ for $k=1,\dots,N$, $N\ge1$, and $R$ has the mass function above, then under Assumption A1

where the expectation is over $R$ and the noise. Any stepsize sequence below $2/L$ is allowed, so the goal does not fix a step rule, and the step rules of the paper's corollaries follow from it.

Milestones

1. The quadratic bound (1.6): $|f(y)-f(x)-\langle\nabla f(x),y-x\rangle|\le\frac L2\|y-x\|^2$ (already proved on the platform).
2. The one-step inequality (2.8) and its pathwise sum (2.9).
3. The conditional mean-zero property (2.10), $\mathbb E[\langle\nabla f(x_k),\delta_k\rangle\mid\xi_{[k-1]}]=0$.
4. The averaged bound (2.11), $\sum_k(\gamma_k-\frac L2\gamma_k^2)\,\mathbb E\|\nabla f(x_k)\|^2\le f(x_1)-f^*+\frac{L\sigma^2}{2}\sum_k\gamma_k^2$.
5. The weighting identity: $\mathbb E\|\nabla f(x_R)\|^2$ equals the $P_R$-weighted average of $\mathbb E\|\nabla f(x_k)\|^2$.
6. For the convex companion: co-coercivity (1.8) (already proved on the platform) and its consequence (2.12), $\frac1L\|\nabla f(y)\|^2\le\langle\nabla f(y),y-x^*\rangle$ when $\nabla f(x^*)=0$.

Companion statements

Theorem 2.1 b) bounds $\mathbb E[f(x_R)-f^*]$ by $(D_X^2+\sigma^2\sum\gamma_k^2)/\sum(2\gamma_k-L\gamma_k^2)$ when $f$ is convex with a minimizer. Corollary 2.2 specializes both bounds to the stepsizes $\gamma_k=\min\{1/L,\tilde D/(\sigma\sqrt N)\}$:

and the analogous bound with $D_X$ for $\mathbb E[f(x_R)-f^*]$ in the convex case.

Significance

Theorem 2.1 a) is the basic guarantee for stochastic gradient descent on smooth nonconvex objectives. With the stepsizes of Corollary 2.2 it shows that $O(\sigma^2/\epsilon^2)$ oracle calls suffice to reach $\mathbb E\|\nabla f(x_R)\|^2\le\epsilon$. The paper builds two further methods on it: a two-phase variant with large-deviation guarantees, and a zeroth-order variant (RSGF) that uses Gaussian smoothing when only function values are available. Later analyses of variance-reduced and adaptive stochastic methods for nonconvex problems measure their improvements against this bound.

The result is proved on paper; no machine-checked proof of it is known. A formalized fixed-step bound of the form "some iterate among the first $K$ has small expected squared gradient" exists, but it is a different statement: it has no randomized output and no general stepsizes. A complete formalization would check the measure-theoretic content that the paper treats informally: integrability of the iterates' gradients, the conditional-expectation step under dependent noise, and the role of the independence of $R$.

Difficulty

The algebra of (2.8)–(2.9) is routine. The difficulty is in the probability. The noise may depend on the past, so the cross term $\langle\nabla f(x_k),\delta_k\rangle$ vanishes only in conditional expectation, and only once $x_k$ is known to be measurable with respect to the past. Its integrability is not assumed anywhere: $\nabla f(x_k)$ must be shown to have a finite second moment from the recursion, the Lipschitz gradient and Assumption A1. The randomized output adds a second step, where $\mathbb E\|\nabla f(x_R)\|^2$ is rewritten as a weighted average. This needs $R$ independent of the noise, and $\|\nabla f(x_k)\|^2$ has to be exhibited as a measurable function of the noise sequence. A proof that replaces $x_R$ by the deterministic weighted average skips exactly this step.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n). $f\in\mathcal C^{1,1}_L$ is the published predicate ConvexOptAlg.SmoothGD.IsBetaSmooth f g L, with the gradient given as a map $g$. $f^*$ is the greatest lower bound of the range of $f$, not an arbitrary lower bound.
• Indices are 1-based. The iterates satisfy $x_1$ given and $x_{k+1}=x_k-\gamma_kG(x_k,\xi_k)$ for $k\ge1$, pointwise on the sample space. The noise takes values in a general measurable space.
• Assumption A1 is stated along the trajectory and in conditional form, with respect to any filtration to which the noise is adapted. The paper's history filtration $\sigma(\xi_1,\dots,\xi_k)$ is one admissible choice. Every conditional expectation and every integral in a hypothesis comes with an integrability clause. Every bounded expectation in a conclusion comes with an integrability conjunct.
• The output index $R$ is a measurable random variable with values in $\{1,\dots,N\}$ and law $P_R$. It is assumed independent of the whole noise sequence; the paper leaves this implicit (Step 0 draws $R$ before any oracle call).
• Added hypotheses, all implicit on the page: $L>0$; $\gamma_k>0$; independence of $R$. In Corollary 2.2 the stepsize (2.13) is read as $\gamma_k=1/L$ when $\sigma=0$, the paper's convention $\tilde D/0=+\infty$, because Lean's $\tilde D/0=0$ would otherwise give $\gamma_k=0$.
• The goal concerns the integral of $\|\nabla f(x_{R(\omega)}(\omega))\|^2$ over the sample space. A statement about the weighted sum of $\mathbb E\|\nabla f(x_k)\|^2$ with $R$ removed, or one that drops the integrability conjunct, would trivialize the randomized output and does not formalize the goal.
• Infrastructure: measurability of the iterates as functions of the noise, the pull-out property of conditional expectation for inner products, and a second-moment induction along the recursion. These are reusable for the paper's two-phase and zeroth-order methods and for other stochastic-approximation analyses. Proofs of any milestone, or of the integrability lemmas on their own, are welcome.

Selected references

• S. Ghadimi and G. Lan, Stochastic first- and zeroth-order methods for nonconvex stochastic programming, SIAM J. Optim. 23(4), 2341–2368, 2013. Preprint arXiv:1309.5549v1 (cited version). https://arxiv.org/abs/1309.5549
• H. Robbins and S. Monro, A stochastic approximation method, Ann. Math. Statist. 22(3), 400–407, 1951. https://doi.org/10.1214/aoms/1177729586
• B. T. Polyak and A. B. Juditsky, Acceleration of stochastic approximation by averaging, SIAM J. Control Optim. 30(4), 838–855, 1992. https://doi.org/10.1137/0330046
• A. Nemirovski, A. Juditsky, G. Lan and A. Shapiro, Robust stochastic approximation approach to stochastic programming, SIAM J. Optim. 19(4), 1574–1609, 2009. https://doi.org/10.1137/070704277
• G. Lan, An optimal method for stochastic composite optimization, Math. Program. 133, 365–397, 2012. https://doi.org/10.1007/s10107-010-0434-y
• Y. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9

Motivation

Many optimization problems in machine learning, signal processing and distributed computation have an objective that is a sum of a large number $m$ of component functions: one per data point, per sensor, or per processor. Evaluating the whole sum, or a subgradient of it, at every iteration is expensive when $m$ is large. Incremental methods process one component at a time, cycling through the components or sampling them, and update the iterate after each one. Incremental gradient and subgradient methods go back to the training of neural networks and to least squares; incremental proximal methods replace the subgradient step of a component by a proximal step, which is more stable and handles nonsmooth terms exactly.

Bertsekas (LIDS-P-2847, 2010, rev. 2011; Math. Program. 129 (2011)) proposed a unified family that mixes the two: each component is split as $F_i=f_i+h_i$, a proximal step is taken on $f_i$ and a subgradient step on $h_i$, followed by a projection onto the constraint set. This mission formalizes the convergence analysis of that family under the cyclic order of component selection.

Timeline. Incremental subgradient methods were analysed by Nedić and Bertsekas (SIAM J. Optim. 12 (2001)) for cyclic and randomized orders. Incremental proximal methods were studied by Bertsekas (Optimization for Machine Learning, 2011, ch. 4). The 2011 paper combines the two analyses; its cyclic-order results are Propositions 3–6.

Setting

Let $\mathbb R^n$ carry the Euclidean norm $\|\cdot\|$ and inner product $x'y$. The data are a nonempty closed convex set $X\subseteq\mathbb R^n$ and real-valued convex functions $f_i,h_i:\mathbb R^n\to\mathbb R$, $i=1,\dots,m$. The problem is

with optimal value $F^*=\inf_{x\in X}F(x)$, possibly $-\infty$, and optimal set $X^*=\{x^*\in X:F(x^*)=F^*\}$, possibly empty.