Machine Learning

Why barycenters of histograms matter

A barycenter summarizes several objects by minimizing a weighted sum of distances to them. For probability histograms, ordinary coordinatewise averages depend strongly on how the bins are labeled. Optimal transport instead lets mass move between bins and charges for those moves through a cost matrix. The resulting Wasserstein barycenter can reflect the geometry of the bins: nearby bins can exchange mass at a lower cost than distant ones. Peyré and Cuturi use this construction in their treatment of variational transport problems, including shape interpolation and the representation of a measure as a barycenter of other measures. The finite histogram problem in this mission is the entropically regularized version developed in §9.2 of their textbook.

The computational question is how to connect three ways of describing the same solution: a histogram that is the barycenter, transport matrices coupling it to the inputs, and vectors of dual potentials. Proposition 9.1 on p. 530 identifies the dual potentials behind the scaling factors of the optimal transport matrices. This is the second proposition numbered 9.1 in the chapter; the one on p. 519 concerns derivatives with respect to histograms.

Finite histogram setting

There are $S$ input histograms. Source $s$ has $n_s$ bins and a probability vector $b_s$, while the barycenter has $n$ bins. The real matrix $C_s\in\mathbb R^{n\times n_s}$ gives the cost of transporting a unit of mass from barycenter bin $i$ to input bin $j$. A weight vector $\lambda\in\Sigma_S$ has nonnegative entries summing to one; $\Sigma_k$ denotes the probability simplex on $k$ bins. The unregularized barycenter problem (9.10) minimizes $\sum_s\lambda_s L_{C_s}(a,b_s)$ over $a\in\Sigma_n$, where $L_{C_s}$ is the minimum transport cost with marginals $a$ and $b_s$.

For a regularization parameter $\varepsilon>0$, the entropic transport cost $L^\varepsilon_{C_s}(a,b_s)$ minimizes $\langle C_s,P_s\rangle-\varepsilon H(P_s)$ over nonnegative coupling matrices $P_s$ with row marginal $a$ and column marginal $b_s$. Here $\langle C_s,P_s\rangle=\sum_{i,j}C_{s,ij}P_{s,ij}$ and $H(P_s)=\sum_{i,j}(-P_{s,ij}\log P_{s,ij}+P_{s,ij})$, with $0\log0=0$. The Gibbs kernel is $K_{s,ij}=e^{-C_{s,ij}/\varepsilon}$.

The book also writes the regularized barycenter as a weighted KL projection. Its variables are the matrices $(P_s)_s$; each matrix has column marginal $b_s$, and every matrix has the same row marginal. That shared row marginal is $a$, so the optimization can be expressed without carrying $a$ as a separate variable. The generalized matrix divergence is $\mathrm{KL}(P_s\mid K_s)=\sum_{i,j}[P_{s,ij}\log(P_{s,ij}/K_{s,ij})-P_{s,ij}+K_{s,ij}]$, using the continuous value at $P_{s,ij}=0$. See (9.15)–(9.17) in Peyré and Cuturi.

Formalization targets

The goal is Proposition 9.1 on p. 530. The dual variables are row potentials $f_s\in\mathbb R^n$ and column potentials $g_s\in\mathbb R^{n_s}$. They maximize

$$\sum_s\lambda_s\left[\langle g_s,b_s\rangle-\varepsilon\sum_{i,j}e^{f_{s,i}/\varepsilon}K_{s,ij}e^{g_{s,j}/\varepsilon}\right] \quad\text{subject to}\quad \sum_s\lambda_s f_s=0.$$

The theorem asserts that the primal and dual optima are attained, that every optimal primal family and every optimal dual family satisfy

$$P_{s,ij}=e^{f_{s,i}/\varepsilon}K_{s,ij}e^{g_{s,j}/\varepsilon},$$

and that the dual maximum is the minimum value of the entropic barycenter objective (9.15). The milestone targets are the scalar and matrix versions of the KL conjugate (9.22), followed by the closed form maximizer of one $g_s$ block, corresponding to the update (9.18). These statements retain the source's finite matrix setting and are listed in the order in which their concepts enter the dual formulation.

What the result supplies

The scaling formula turns the optimal couplings into a product of a row factor, a fixed positive kernel, and a column factor. It identifies those factors with exponentials of dual potentials and gives a constrained maximization problem whose value is the entropic barycenter cost. Thus a solver can reason about the couplings, the barycenter marginal, or the potentials while referring to one theorem that connects them. The book uses the same variables to describe the iterative scaling updates on pp. 529–531 and later illustrates barycenters of shapes and surface measures; those applications depend on interpreting the matrix factors correctly. Peyré and Cuturi give the mathematical proposition and its argument. A complete Lean proof of the proposition and its supporting KL identities is the work this mission calls for; the statements here are draft targets rather than machine-checked solutions.

Where the difficulty lies

The potential program is a constrained optimization problem, while the transport problem constrains nonnegative matrices by two kinds of marginals. Equality of their optimum values must preserve the normalization constants in generalized KL. The exponential form alone does not establish that a proposed matrix has the required marginals, nor does a feasible matrix alone identify dual potentials. In addition, the assertion concerns every optimizer: a choice of zero source weight would leave that source's coupling unconstrained by the objective, and a zero target entry would put a logarithmic column update on the boundary. These are substantive edge cases of the formulas, not merely notation.

Formalization scope

Lean uses Fin S, Fin n, and Fin (n_s) for the finite index sets; these are zero based versions of the book's one based indices. Histograms and potentials are real vectors, costs and couplings are real matrices, and the Gibbs kernel is defined entrywise. The theorem requires $S,n,n_s>0$, $\varepsilon>0$, strictly positive weights $\lambda_s$ that sum to one, and strictly positive input histograms $b_s$ that each sum to one. The strict positivity of weights and input entries is an explicit restriction beyond (9.15)–(9.21), needed for a statement about every optimizer and finite logarithmic potentials. Entropy uses $0\log0=0$ on nonnegative couplings. The shared row marginal is constructed by the constraints on the $P_s$; it is not a free histogram unrelated to them.

The definition layer includes finite matrix pairing, entropy, generalized KL, the Gibbs kernel, feasibility, and primal and dual objective functions. The KL conjugate identities and the block optimizer are separate theorem targets so they can be reused in other entropic transport developments. The main theorem asserts primal and dual attainment as well as their relationship; it does not assume strong duality or an optimal scaling as an input. The page has slips in the dimensions of the marginal equations and a missing subscript on $K$ in (9.17); the Lean statements use the dimensions specified by $P_s\in\mathbb R^{n\times n_s}$. The optional cost-gradient Proposition 9.2 on pp. 519–520 and the $f_s$ block update (9.19)–(9.20) lie outside this proposal.

Selected references

• Gabriel Peyré and Marco Cuturi, Computational Optimal Transport, Foundations and Trends in Machine Learning 11(5–6):355–607, 2019. DOI: 10.1561/2200000073.

Motivation

A multi-armed bandit learner repeatedly chooses one of several actions, observes only the loss of the chosen action, and tries to perform nearly as well as a single fixed action selected in hindsight. Two common loss models make different demands on the learner. In a stochastic model, each arm has a stable mean loss and the learner can gradually distinguish the best arm. In an adversarial model, losses may change with time and even respond to previous choices. A useful bandit algorithm should handle both without first being told which model generated the losses.

Zimmert and Seldin's Tsallis-INF paper analyzes one algorithm in both regimes. Its Theorem 1 gives a square-root guarantee against arbitrary adversarial losses and a logarithmic guarantee when the regret satisfies a self-bounding constraint. The latter condition includes the usual stochastic case with a unique best arm and also permits some adversarial deviations. This mission formalizes the reduced-variance (RV) estimator part of that theorem and six supporting statements from its analysis.

Setting

There are $K\ge1$ arms and rounds $t=1,2,\ldots$. At round $t$, the environment supplies a loss $\ell_{t,i}\in[0,1]$ for each arm $i$. The learner draws an arm $I_t$ from a probability vector $w_t$ and observes only $\ell_{t,I_t}$. The environment can base its current losses on the actions from earlier rounds. It may also randomize: a seed $\omega$ records its internal random choices, while its response to a history remains adaptive. The learner's random actions are then drawn successively from its history-dependent weight vectors. Expectations below average over both sources of randomness.

The pseudo-regret at horizon $T$ compares the learner's expected total loss with the lowest expected total loss of a fixed arm:

$$\operatorname{Reg}_T =\mathbb E\!\left[\sum_{t=1}^{T}\ell_{t,I_t}\right] -\min_i\mathbb E\!\left[\sum_{t=1}^{T}\ell_{t,i}\right].$$

For the algorithm studied here, $\widehat L_{t-1}$ is the vector of estimated losses accumulated before round $t$. The symmetric half-Tsallis regularizer is

$$\Psi_t(w)=-4\eta_t^{-1}\sum_{i=1}^{K}\left(\sqrt{w_i}-\tfrac12w_i\right), \qquad \eta_t=\frac4{\sqrt t}.$$

The vector $w_t$ maximizes $\langle w,-\widehat L_{t-1}\rangle-\Psi_t(w)$ over the probability simplex. With the RV loss estimator, arm $i$ has baseline $B_t(i)=\tfrac12\mathbf 1\{w_{t,i}\ge\eta_t^2\}$ and estimate $\widehat\ell_{t,i}=\mathbf 1\{I_t=i\}(\ell_{t,i}-B_t(i))/w_{t,i}+B_t(i)$. This is an estimator based on the one observed loss, even though its update is a vector.

The self-bounding condition chooses gaps $\Delta_i\in[0,1]$ with exactly one zero, at $i^*$, and a constant $C\ge0$, as defined in Section 2. It requires

$$\operatorname{Reg}_T\ge \mathbb E\!\left[\sum_{t=1}^{T}\sum_{i\ne i^*}w_{t,i}\Delta_i\right]-C.$$

The gaps measure how costly it is to place weight on each non-best arm. In a stochastic bandit with a unique best arm, the usual expected-loss gaps give this relation with $C=0$ Zimmert and Seldin, §2 and §4.1.

Formalization targets

Adversarial guarantee

The first target is an upper bound for every bounded, randomized adaptive adversary and every $T\ge1$:

$$\operatorname{Reg}_T\le 2\sqrt{KT}+14K\log T+16.$$

The paper prints $10K\log T$ in Theorem 1's display. Its proof yields $14K\log T$, the coefficient formalized here; the difference is recorded in the moderation notes. The theorem's other displayed bounds retain their printed constants.

Self-bounding guarantee

For $K\ge2$, set $\Delta_{\min}=\min_{i\ne i^*}\Delta_i$ and

$$X=\sum_{i\ne i^*}\frac{\log T+3}{\Delta_i}+\frac2{\Delta_{\min}}.$$

Under the self-bounding condition, the same algorithm must satisfy

$$\operatorname{Reg}_T\le X+28K\log T+\tfrac32\sqrt K+32+C.$$

When $C>X$, it must also satisfy $\operatorname{Reg}_T\le2\sqrt{XC}+28K\log T+\tfrac32\sqrt K+32$. The goal states both clauses together with the adversarial guarantee. Its six milestones give a pathwise stability bound from Lemma 19, two per-round stability bounds from Lemma 11, two accumulated penalty bounds from Lemma 12, and a finite tail-sum estimate from Lemma 15.

Significance

The adversarial clause limits the cost of learning even when no arm has a persistent advantage. The self-bounding clause gives gap-sensitive logarithmic growth when the learner receives enough information to identify a unique best arm, while allowing the additive deviation $C$. The two guarantees apply to the same weight rule and the same RV estimator Zimmert and Seldin, Theorem 1.

The paper proves its RV claims in prose and equations. A complete Lean proof would make the algorithm's randomized adaptive loss model, its path law, the estimator and the exact constants explicit in machine-checked form. The local theorem statements and definitions in this proposal compile with placeholder theorem proofs; the mission's mathematical results are therefore targets for formalization, not results already machine checked here. The setting definitions may also support formal analyses of other bandit algorithms with adaptive randomized losses.

Difficulty

The learner sees only one loss at each round, so the weight vector depends on estimates whose individual coordinates can be much larger than the observed losses. Bounding the change in the regularized potential by a simple worst-case estimate loses the dependence on the arm weights that the gap-sensitive result needs. The RV estimator reduces this difficulty but can take negative values, which changes the stability calculation. The self-bounding guarantee also compares the theorem's zero-gap arm with a best arm chosen in expectation at horizon $T$; for $C>0$ these need not coincide. That comparator issue is documented for audit.

Formalization scope

The arms are Fin K, with the paper's first arm represented by Lean index zero. Histories are functions on natural-number rounds; entry zero is unused. A referenced published adversarial protocol supplies bounded losses and dependence on past actions. A probability measure on adversary seeds and a finite sum over action paths define the run law. The algorithm is an argmax predicate whose estimates are computed from its own weights and the observed loss. The real-valued simplex supremum defines $\Phi_t$; $K\ge1$ makes that simplex nonempty, and its compactness bounds the objective. The goal requires measurable seeded losses, a probability measure, $T\ge1$, $C\ge0$ in the self-bounding regime, and $K\ge2$ where $\Delta_{\min}$ is used. The penalty milestones take conditionally unbiased estimators that depend only on actions through their own round, are measurable, and have finite expected absolute size, as required for a sequential run and genuine expectations. Positive, non-increasing learning rates are explicit.

The argmax is taken over every simplex weight vector, and the run law includes every action path with its product probability. These choices rule out an arbitrary weight rule or a zero-valued integral masquerading as the algorithm. The development needs reusable facts about the simplex, measurability and integrability of the finite-path law, positivity of Tsallis-INF weights, and bounds on the real potential. Contributions that establish those facts or close the six milestone theorems fit this mission.

Selected references

• Julian Zimmert and Yevgeny Seldin, Tsallis-INF: An Optimal Algorithm for Stochastic and Adversarial Bandits, Journal of Machine Learning Research 22(28), 2021; formalization follows arXiv:1807.07623v6, pp. 5–10, 18–21.

Motivation

Adam (Kingma and Ba, arXiv:1412.6980) is the default optimizer for training neural networks. It combines a stochastic gradient step with two exponential moving averages: a momentum term $m_n$ and a coordinatewise second-moment estimate $v_n$ that rescales each coordinate of the step. Its convergence theory is delicate: Reddi, Kale and Kumar (arXiv:1904.09237) exhibited convex problems on which Adam with constant hyperparameters fails to converge.

Barakat and Bianchi (arXiv:1810.02263, SIAM J. Math. Data Sci. 3(1), 2021) study Adam on nonconvex objectives through the ODE method of stochastic approximation. In the decreasing-stepsize regime, their Theorem 5.2 proves that the iterates converge almost surely to the critical points of the objective — provided the iterates are almost surely bounded. A stability hypothesis of this kind is standard in stochastic approximation (Benaïm, Dynamics of stochastic approximation algorithms, Séminaire de Probabilités XXXIII, 1999, doi:10.1007/BFb0096509), and it is often the hardest part to verify. Theorem 5.4 of the paper gives sufficient conditions, on the objective and the stepsizes only, under which almost sure boundedness holds. This mission formalizes that theorem.

Setting

Let $(\Omega,\mathcal F,\mathbb P)$ be a probability space and $(\Xi,\mathfrak S)$ a measurable space carrying a probability measure $\mu$. A loss $f:\mathbb R^d\times\Xi\to\mathbb R$ is given, with gradient $\nabla f(x,\xi)$ in $x$, and the objective is

$$F(x)=\mathbb E f(x,\xi)=\int_\Xi f(x,\xi)\,\mu(d\xi).$$

The samples $(\xi_n)_{n\ge1}$ are iid with law $\mu$ (Assumption 4.1). Vector operations below are coordinatewise.

Fix $\varepsilon>0$ and real sequences $(\gamma_n)$ (stepsizes), $(\alpha_n)$, $(\beta_n)$ (moment parameters). Algorithm 5.1 (Adam with decreasing stepsize) starts from $x_0\in\mathbb R^d$, $m_0=v_0=0$, $r_0=\bar r_0=0$, and for $n\ge1$ sets

$$\begin{aligned} m_n&=\alpha_nm_{n-1}+(1-\alpha_n)\nabla f(x_{n-1},\xi_n), & r_n&=\alpha_nr_{n-1}+(1-\alpha_n),\\ v_n&=\beta_nv_{n-1}+(1-\beta_n)\nabla f(x_{n-1},\xi_n)^{\odot2}, & \bar r_n&=\beta_n\bar r_{n-1}+(1-\beta_n),\\ x_n&=x_{n-1}-\gamma_n\,\hat m_n/(\varepsilon+\sqrt{\hat v_n}), & \hat m_n&=m_n/r_n,\quad \hat v_n=v_n/\bar r_n . \end{aligned}$$

The weights $r_n,\bar r_n$ implement the bias correction of Adam.

The hypotheses are: Assumption 2.2 ($f(x,\cdot)$ measurable, $f(\cdot,\xi)$ continuously differentiable for a.e. $\xi$, integrability at one point, and $\mathbb E\|\nabla f(x,\xi)-\nabla f(y,\xi)\|^2\le L_K^2\|x-y\|^2$ on each compact $K$); Assumption 2.3 ($F$ coercive); Assumption 4.2 i) with $p=4$ ($\sup_{x\in K}\mathbb E\|\nabla f(x,\xi)\|^4<\infty$ on compacts); Assumption 5.1 ($\gamma_n>0$, $\gamma_{n+1}/\gamma_n\to1$, $\sum\gamma_n=\infty$, $\sum\gamma_n^2<\infty$, $\alpha_n,\beta_n\in[0,1]$, $(1-\alpha_n)/\gamma_n\to a$, $(1-\beta_n)/\gamma_n\to b$ with $0<b<4a$); and Assumption 5.3 ($\nabla F$ Lipschitz, $\mathbb E\|\nabla f(x,\xi)\|^2\le C(1+F(x))$, and $\limsup_n\big(\gamma_n^{-1}-\frac{1-\alpha_{n+2}}{1-\alpha_{n+1}}\gamma_{n+1}^{-1}\big)<2(a-b/4)$).

Formalization targets

Goal: Theorem 5.4

Under Assumptions 2.2, 2.3, 4.1, 5.1, 5.3 and 4.2 i) with $p=4$,

$$\mathbb P\Big(\sup_{n\in\mathbb N}\|(x_n,m_n,v_n)\|<\infty\Big)=1 .$$

Milestones (in the order the proof of §9.2 uses them)

1. Lemma 9.1 i)–ii): $r_n=1-\prod_{i=1}^n\alpha_i$, and $(r_n)$ is nondecreasing with $r_n\to1$; likewise for $\bar r_n$.
2. (9.1): with $a_n=(1-\alpha_{n+1})/\gamma_n$ and $P_n=\frac1{2a_nr_n}\langle m_n^{\odot2},1/(\varepsilon+\sqrt{\hat v_n})\rangle$,

$$F(x_n)\le F(x_{n-1})-\gamma_n\Big\langle\nabla F(x_n),\frac{\hat m_n}{\varepsilon+\sqrt{\hat v_n}}\Big\rangle+C\gamma_n^2P_n .$$

3. (9.3): coordinatewise, $\sqrt{\hat v_n}-\sqrt{\hat v_{n+1}}\le c_{n+1}\sqrt{\hat v_{n+1}}$ with an explicit $c_{n+1}\sim b\gamma_n/2$.
4. (9.4): with $u_n=1-a_{n+1}/a_n$, for every $\delta>0$ and $n$ large,

$$\mathbb E_n\big(F(x_n)+P_{n+1}\big)\le F(x_{n-1})+P_n+u_n\mathbb E_nP_{n+1}-2\Big(a-\frac{b+\delta}4\Big)\gamma_nP_n+C\gamma_n^2\big(1+F(x_n)+P_n\big).$$

5. The Robbins–Siegmund inequality: $V_n=(1-C\gamma_{n-1}^2)F(x_{n-1})+(1-u_{n-1})P_n$ satisfies $\mathbb E_n(V_{n+1})\le(1+C'\gamma_n^2)V_n+C\gamma_n^2$ for $n$ large.

Significance

Theorem 5.2 of the paper, the almost sure convergence of decreasing-step Adam to the critical set, is conditional on almost sure boundedness. Theorem 5.4 removes that condition for objectives with Lipschitz gradient and quadratic gradient-noise growth, and so turns Theorem 5.2 into an unconditional convergence result in that class. The Lyapunov function $F(x_{n-1})+P_n$ — the objective plus a weighted kinetic energy of the momentum — is the discrete counterpart of the energy used for the continuous-time Adam ODE in the same paper; the condition $b<4a$ that keeps it decreasing is the discrete trace of the condition $b\le4a$ of the ODE analysis.

The result is proved in the paper; nothing about Adam is formalized on the platform. A formal proof produces a machine-checked stability theorem for an adaptive, momentum-based stochastic algorithm, together with reusable pieces: the Robbins–Siegmund almost-supermartingale theorem in the conditional-expectation form used here, and the bias-correction lemma, which applies to every exponential moving average with vanishing forgetting rate.

Difficulty

For plain stochastic gradient descent, boundedness follows from the descent lemma applied to $F$ alone: $F(x_n)$ is an almost supermartingale. For Adam this fails. The step $\hat m_n/(\varepsilon+\sqrt{\hat v_n})$ is not a descent direction for $F$: $m_n$ averages past gradients, so $\langle\nabla F(x_n),\hat m_n/(\varepsilon+\sqrt{\hat v_n})\rangle$ has no sign. The momentum must therefore enter the Lyapunov function, through $P_n$, and the coordinatewise preconditioner $1/(\varepsilon+\sqrt{\hat v_n})$ changes from step to step, so $P_{n+1}$ and $P_n$ are measured in different weighted norms. Controlling that change is what (9.3) does, and it costs a term of size $\frac b2\gamma_nP_n$ that must be absorbed by the friction $2a\gamma_nP_n$ of the momentum update; the margin is exactly $b<4a$. The time-varying weights $a_n$ and $r_n$ produce the further term $u_nP_{n+1}$, which is why Assumption 5.3 iii) is needed. Finally, the conditional expectations involve the next sample through both $m_{n+1}$ and $\hat v_{n+1}$, so the second-moment growth condition of Assumption 5.3 ii) has to be used with the right weights.

Formalization scope

Points of $\mathbb R^d$ are EuclideanSpace ℝ (Fin d); the state $(x,m,v)$ lives in the product $E\times E\times E$, whose Mathlib norm is the maximum of the three Euclidean norms (the same bounded sets). The gradient of $f$ is a function gf : E → Ξ → E that equals the true gradient for $\mu$-almost every $\xi$. The run of Algorithm 5.1 is defined along a sample path and then pathwise in $\omega$. Moments are lower Lebesgue integrals, so no hypothesis is vacuous through the convention that a non-integrable Bochner integral is $0$. Assumption 5.3 iii) is stated as "there is $c<2(a-b/4)$ bounding the bracket for all large $n$", which avoids a real limsup. The algorithm divides by $r_n$ and $\bar r_n$; the theorem therefore assumes $\alpha_1<1$ and $\beta_1<1$, which Algorithm 5.1 needs for $\hat m_1,\hat v_1$ to be defined. In the milestones, $\mathbb E_n$ applied to a function of the next state is the integral of that function over the next sample, $\int G(T_{n+1}(z_n,\xi))\,\mu(d\xi)$, a version of the conditional expectation under Assumption 4.1. In (9.4) the term printed as $u_nP_{n+1}$ is $u_n\mathbb E_nP_{n+1}$, the reading the derivation produces.

The goal asserts a single bound for the whole trajectory almost surely; finiteness of each iterate, boundedness of a projected variant of Adam, and boundedness under an almost-sure bound on $\nabla f(x,\xi)$ are all weaker statements and are not this theorem. The "without loss of generality $F\ge0$" of the proof appears only as a hypothesis of the last milestone.

A complete development needs the Robbins–Siegmund theorem (open on the platform as AdaptiveProtection.Convergence.lemma2_robbins_siegmund), differentiation under the integral sign for $F$, the descent lemma for Lipschitz gradients, and conditional expectations given $\sigma(\xi_1,\dots,\xi_n)$ for functions of an independent sample. Proofs of any milestone, and a proof of Robbins–Siegmund in the form used here, are welcome.

Selected references

• A. Barakat, P. Bianchi, Convergence and Dynamical Behavior of the ADAM Algorithm for Nonconvex Stochastic Optimization, SIAM J. Math. Data Sci. 3(1), 2021; arXiv:1810.02263v4. https://arxiv.org/abs/1810.02263
• D. P. Kingma, J. Ba, Adam: A Method for Stochastic Optimization, ICLR 2015. https://arxiv.org/abs/1412.6980
• S. J. Reddi, S. Kale, S. Kumar, On the Convergence of Adam and Beyond, ICLR 2018. https://arxiv.org/abs/1904.09237
• H. Robbins, D. Siegmund, A convergence theorem for non negative almost supermartingales and some applications, in Optimizing Methods in Statistics, Academic Press, 1971. https://doi.org/10.1016/B978-0-12-604550-5.50015-8
• M. Benaïm, Dynamics of stochastic approximation algorithms, Séminaire de Probabilités XXXIII, LNM 1709, Springer, 1999. https://doi.org/10.1007/BFb0096509

Motivation

Adam (Kingma and Ba, 2015) is the default optimizer for training neural networks: a stochastic gradient method that keeps an exponential moving average $m_n$ of past gradients and an exponential moving average $v_n$ of their coordinatewise squares, and divides the first by the square root of the second. Its practical success came well before any convergence theory for nonconvex objectives. Reddi, Kale and Kumar (2018) showed that Adam with constant momentum parameters can fail to converge even on convex problems, which made the question of under which parameter schedules Adam provably converges a live one.

Barakat and Bianchi (arXiv:1810.02263, SIAM J. Math. Data Sci. 2021) answer it through the ODE method of stochastic approximation (Benaïm, 1999). This mission takes the paper's almost-sure convergence theorem for Adam with decreasing stepsizes, Theorem 5.2. Under a stepsize schedule in which $1 - \alpha_n$ and $1 - \beta_n$ shrink in proportion to the stepsize $\gamma_n$, the iterates converge almost surely to the critical points of the objective, provided they stay bounded.

Setting

Let $\xi$ be a random variable on a measurable space $\Xi$ with law $\mu$, let $f : \mathbb R^d \times \Xi \to \mathbb R$ be an integrand with gradient $\nabla f(x, \xi)$ in $x$, and set

$$F(x) = \mathbb E f(x, \xi), \qquad S(x) = \mathbb E\big(\nabla f(x,\xi)^{\odot 2}\big), \qquad \mathcal S = \nabla F^{-1}(\{0\}),$$

where $\odot 2$ is the coordinatewise square and $\mathcal S$ is the critical set. Let $\xi_1, \xi_2, \dots$ be iid copies of $\xi$ on a probability space $(\Omega, \mathcal F, \mathbb P)$.

Algorithm 5.1 takes stepsizes $\gamma_n > 0$, weights $\alpha_n, \beta_n \in [0,1]$ and a constant $\varepsilon > 0$. Starting from $x_0 \in \mathbb R^d$, $m_0 = v_0 = 0$ and $r_0 = \bar r_0 = 0$, it computes for $n \ge 1$, with all vector operations coordinatewise:

$$\begin{aligned} m_n &= \alpha_n m_{n-1} + (1-\alpha_n)\nabla f(x_{n-1}, \xi_n), & v_n &= \beta_n v_{n-1} + (1-\beta_n)\nabla f(x_{n-1}, \xi_n)^{\odot 2},\\ r_n &= \alpha_n r_{n-1} + (1 - \alpha_n), & \bar r_n &= \beta_n \bar r_{n-1} + (1 - \beta_n),\\ x_n &= x_{n-1} - \gamma_n \frac{\hat m_n}{\varepsilon + \sqrt{\hat v_n}}, & \hat m_n &= m_n / r_n,\quad \hat v_n = v_n / \bar r_n . \end{aligned}$$

The divisions by $r_n$, $\bar r_n$ are the bias correction.

The stepsizes satisfy Assumption 5.1: $\gamma_{n+1}/\gamma_n \to 1$, $\sum_n \gamma_n = +\infty$, $\sum_n \gamma_n^2 < +\infty$, and there are $a, b$ with $0 < b < 4a$, $(1-\alpha_n)/\gamma_n \to a$ and $(1-\beta_n)/\gamma_n \to b$. The limiting dynamics is the autonomous ODE $\dot z = h_\infty(z)$ on $\mathcal Z_+ = \mathbb R^d \times \mathbb R^d \times [0,\infty)^d$, written $(\mathrm{ODE}_\infty)$, with

$$h_\infty(x, m, v) = \Big( -\frac{m}{\varepsilon + \sqrt v},\ a(\nabla F(x) - m),\ b(S(x) - v) \Big).$$

Formalization targets

Goal: Theorem 5.2

Assume Assumption 2.2 (regularity and moments of $f$), $F$ coercive (2.3), $S(x) > 0$ coordinatewise (2.4), iid samples (4.1), Assumption 5.1, $\sup_{x\in K}\mathbb E\|\nabla f(x,\xi)\|^4 < \infty$ on compacts (4.2 i) with $p = 4$), that $F(\mathcal S)$ has empty interior, and that $(x_n, m_n, v_n)$ is bounded with probability one. Then, almost surely,

$$d(x_n, \mathcal S) \to 0, \qquad m_n \to 0, \qquad S(x_n) - v_n \to 0,$$

and if $\mathcal S$ is countable, almost surely $(x_n, m_n, v_n) \to (x^*, 0, S(x^*))$ for some $x^* \in \mathcal S$.

Milestones

1. Lemma 9.1 i)–ii): $r_n = 1 - \prod_{i=1}^n \alpha_i$, and $r_n$ increases to $1$.
2. §9.1: in the decomposition $\bar z_{n+1} = \bar z_n + \gamma_{n+1} h_\infty(\bar z_n) + \gamma_{n+1}\chi_{n+1} + \gamma_{n+1}\varsigma_{n+1}$ of $\bar z_n = (x_{n-1}, m_n, v_n)$, the remainder satisfies $\varsigma_n \to 0$ almost surely.
3. §9.1: the piecewise-affine interpolation of $(\bar z_n)$ on the times $\tau_n = \sum_{k\le n}\gamma_k$ is almost surely a bounded asymptotic pseudotrajectory of the semiflow of $(\mathrm{ODE}_\infty)$.
4. Proposition 7.13: $(\mathrm{ODE}_\infty)$ is well posed on $\mathcal Z_+$ and defines a semiflow $\Phi$.
5. Proposition 7.14 (after Benaïm): the limit set of a relatively compact asymptotic pseudotrajectory of a semiflow with a strict Lyapunov function lies in the set of equilibria.
6. Proposition 7.15: on the closed hull of the orbits of a compact set, $W_\delta = V_\infty - \delta\langle\nabla F(x), m\rangle + \delta\|S(x) - v\|^2$ is a strict Lyapunov function for some $\delta > 0$.

Significance

The theorem identifies a regime of Adam's hyperparameters, $1 - \alpha_n \sim a\gamma_n$ and $1 - \beta_n \sim b\gamma_n$ with $b < 4a$, in which the algorithm behaves like a gradient method with vanishing noise: the iterates approach critical points, the momentum dies out, and the second-moment estimate converges to $S(x_n)$. The condition $b < 4a$ ties the two averaging rates together. It is the condition under which the paper's Lyapunov function for the continuous dynamics decreases (Lemma 7.5). The argument structure is also a template for other adaptive methods: once the limiting ODE has a strict Lyapunov function, almost-sure convergence of the iterates follows from the same steps.

The paper proves the result on paper; none of it is machine-checked. A formal proof would also be the first formal instance on Prove2Me of the full ODE method for a concrete stochastic algorithm. That pipeline runs from the iterates to a perturbed Euler scheme, then to an asymptotic pseudotrajectory and a limit-set theorem, and finally to convergence. Benaïm's general results are being formalized separately on the platform (the asymptotic-pseudotrajectory definition this mission reuses comes from that effort), so the two developments meet in milestone 3.

Difficulty

The obvious approach is to treat Adam as stochastic gradient descent with a preconditioner and run a descent-lemma argument on $F(x_n)$. This fails because the update direction $\hat m_n/(\varepsilon + \sqrt{\hat v_n})$ is not a descent direction for $F$: $m_n$ lags behind $\nabla F(x_n)$. Any Lyapunov function has to involve the momentum, and $F$ alone does not decrease. The continuous-time energy $V_\infty$ decreases only weakly, and only its perturbation $W_\delta$ is strict, and only on compact sets. A second difficulty is that the stepsize-dependent coefficients $(1-\alpha_{n+1})/\gamma_{n+1}$ and the bias corrections $r_n$, $\bar r_n$ make the recursion a non-autonomous perturbation of the Euler scheme of $h_\infty$. The remainder must be shown to vanish along almost every path before the general theory applies. Finally, the abstract limit-set theorem needs the semiflow to be well defined on the closed set $\mathcal Z_+$, where $h_\infty$ involves $\sqrt v$ and is not Lipschitz at $v = 0$.

Formalization scope

$\mathbb R^d$ is EuclideanSpace ℝ (Fin d). The state space $\mathcal Z$ is the product of three copies with Mathlib's max-of-factors norm, which is equivalent to the Euclidean norm of $\mathbb R^{3d}$ and leaves boundedness and limits unchanged. $F$ and $S$ are Bochner integrals against the law $\mu$. Assumption 2.2 makes the integrands integrable, so they are the true expectations. Moments are lower Lebesgue integrals. Algorithm 5.1 is a pathwise recursion adamIter, driven by a random sequence $\xi : \mathbb N \to \Omega \to \Xi$ whose index $0$ is unused. The iid hypothesis is iIndepFun with every $\xi_{n+1}$ of law $\mu$.

Two hypotheses are left implicit on the page and are added explicitly. The first is $\varepsilon > 0$. The second is $\alpha_1 < 1$ and $\beta_1 < 1$: Assumption 5.1 iii) permits $\alpha_1 = 1$, which gives $r_1 = 0$, and Lean's division by zero returns $0$. Lemma 9.1 is stated with $\gamma_n > 0$ and $\sum\gamma_n = \infty$, which its convergence claim needs. Semiflows are Flow ℝ≥0 on the subtype $\mathcal Z_+$, and the asymptotic pseudotrajectory and limit set are the published StochApproxDyn.LimitSet definitions. The ODE milestones 4–6 hold for abstract $F$, $S$ under Assumptions 7.1–7.2 with $0 < b \le 4a$, as in the paper's §7.

The goal concerns the iterates of Algorithm 5.1 itself. A statement about trajectories of $(\mathrm{ODE}_\infty)$, or one that replaces almost-sure boundedness by a bound uniform in $\omega$ together with deterministic gradients, is a different and much weaker theorem and is ruled out. The interior condition on $F(\mathcal S)$ and the countability of $\mathcal S$ enter exactly as on the page.

A complete development needs the following:

• well-posedness of the ODE on a closed set with a non-Lipschitz field;
• the Benaïm machinery: martingale-noise control via Doob's convergence theorem, and the passage from vanishing perturbations to asymptotic pseudotrajectories;
• the limit-set theorem for strict Lyapunov functions.

The last two are reusable for any stochastic approximation scheme, and contributions to them are welcome independently of Adam.

Selected references

• A. Barakat, P. Bianchi, Convergence and Dynamical Behavior of the ADAM Algorithm for Nonconvex Stochastic Optimization, SIAM J. Math. Data Sci. 3(1), 2021; arXiv:1810.02263v4. https://arxiv.org/abs/1810.02263
• M. Benaïm, Dynamics of stochastic approximation algorithms, Séminaire de Probabilités XXXIII, LNM 1709, Springer, 1999. https://doi.org/10.1007/BFb0096509
• D. P. Kingma, J. Ba, Adam: A Method for Stochastic Optimization, ICLR 2015. https://arxiv.org/abs/1412.6980
• S. J. Reddi, S. Kale, S. Kumar, On the Convergence of Adam and Beyond, ICLR 2018. https://arxiv.org/abs/1904.09237

Motivation

Regularized loss minimization covers support vector machines, logistic and ridge regression, and the absolute-deviation regression of robust statistics. Stochastic dual coordinate ascent (SDCA) solves these problems by maximizing the Fenchel dual one randomly chosen coordinate at a time. Shalev-Shwartz and Zhang (arXiv:1209.1873, JMLR 2013) gave the first analysis of SDCA in terms of the duality gap. For smooth losses their rate is linear; for Lipschitz but non-smooth losses such as the hinge loss it is of order $1/\epsilon$, which is no better than stochastic gradient descent, although SDCA is observed to converge much faster than SGD on SVM problems asymptotically.

Section 5 of the paper explains that observation. Many non-smooth losses are smooth at most points: the hinge loss $\max(0,1-uy_i)$ fails to be smooth only at $uy_i=1$. If, at the optimum, most margins stay away from the kink, the dual is strongly concave in most coordinates, and SDCA converges linearly in the dual objective. Earlier linear-rate results for dual coordinate ascent on SVMs (Luo and Tseng, 1992) depend on the smallest nonzero eigenvalue of the data Gram matrix, which can be arbitrarily small when two data points are close; the condition of Section 5 avoids the Gram matrix.

Setting

Data $x_1,\dots,x_n\in\mathbb R^d$ (Euclidean norm), scalar convex losses $\varphi_1,\dots,\varphi_n:\mathbb R\to\mathbb R$ and $\lambda>0$ define the primal problem

$$\min_{w\in\mathbb R^d} P(w),\qquad P(w)=\frac1n\sum_{i=1}^n\varphi_i(w^\top x_i)+\frac\lambda2\|w\|^2 .$$

The convex conjugate of $\varphi_i$ is $\varphi_i^*(u)=\sup_z(zu-\varphi_i(z))\in(-\infty,+\infty]$. The dual problem is $\max_{\alpha\in\mathbb R^n}D(\alpha)$ with

$$D(\alpha)=\frac1n\sum_{i=1}^n-\varphi_i^*(-\alpha_i)-\frac\lambda2\|w(\alpha)\|^2,\qquad w(\alpha)=\frac{1}{\lambda n}\sum_{i=1}^n\alpha_ix_i .$$

A dual variable is feasible when every $\varphi_i^*(-\alpha_i)$ is finite. A function is $L$-Lipschitz if $|\varphi_i(a)-\varphi_i(b)|\le L|a-b|$. The standing assumptions are $\|x_i\|\le1$, $\varphi_i\ge0$ and $\varphi_i(0)\le1$.

Procedure SDCA starts from $\alpha^{(0)}=0$. At iteration $t$ it picks $i$ uniformly at random, independently of the past, chooses $\Delta\alpha_i$ maximizing $-\varphi_i^*(-(\alpha_i^{(t-1)}+\Delta\alpha_i))-\frac{\lambda n}{2}\|w(\alpha^{(t-1)})+(\lambda n)^{-1}\Delta\alpha_ix_i\|^2$, and sets $\alpha^{(t)}=\alpha^{(t-1)}+\Delta\alpha_ie_i$. Let $\alpha^*$ be a dual optimum and $w^*=w(\alpha^*)$.

The refined dual strong convexity condition (Definition 2, (4)) asks for functions $\gamma_i(\cdot)\ge0$ with

$$\varphi_i^*(-a)-\varphi_i^*(-b)+u(a-b)\ge\gamma_i(u)|a-b|^2\qquad\text{for all }a,b\text{ and }u\in\partial\varphi_i^*(-b).$$

For the hinge loss one may take $\gamma_i(u)=|uy_i-1|$. With constants $\gamma_i\ge0$, the dual strong convexity inequality (5) is

$$D(\alpha^*)-D(\alpha)\ge\frac1n\sum_{i=1}^n\gamma_i|\alpha_i-\alpha_i^*|^2+\frac\lambda2\|w(\alpha)-w^*\|^2\quad\text{for every feasible }\alpha,$$

and $N(u)=\#\{i:\gamma_i<u\}$ counts the coordinates with small modulus.

Formalization targets

Goal: Theorem 5 (p. 9)

Assume convex $L$-Lipschitz losses, the standing assumptions, and (5) with constants $\gamma_i\ge0$. For every $\epsilon_D>0$ and $s\in(0,1]$ with $\epsilon_D\ge 8L^2\frac{s}{\lambda n}N(\frac{s}{\lambda n})/n$,

$$t\ge2\frac ns\log\frac2{\epsilon_D}\quad\Longrightarrow\quad\mathbb E\bigl[D(\alpha^*)-D(\alpha^{(t)})\bigr]\le\epsilon_D .$$

The constants $2$ and $8$ are the paper's.

Milestones

1. Proposition 1 (pp. 8–9): condition (4), with $\gamma_i=\gamma_i(w^{*\top}x_i)$, implies (5), and $|(w^*-w)^\top x_i|\ge\gamma_i|a_i-\alpha_i^*|$ whenever $-a_i\in\partial\varphi_i(w^\top x_i)$ (6).
2. Lemma 5 (p. 19): under (5), one step raises the expected dual by at least $\frac{s}{2n}$ times the dual sub-optimality, plus $\frac{3s\lambda}{4n}\|w^*-w\|^2$, minus $(\frac sn)^2G_*(s)/(2\lambda)$ with $G_*(s)=\frac1n\sum_i(\|x_i\|^2-\gamma_i\lambda n/s)(\alpha_i^*-\alpha_i)^2$.
3. Lemma 3 (p. 15): the conjugate of an $L$-Lipschitz function is $+\infty$ outside $[-L,L]$.
4. Lemma 6 (p. 20): $G_*(s)\le4L^2N(s/(\lambda n))/n$.
5. Dual recursion (§7.6, p. 20): $\epsilon_D^{(t)}\le(1-\frac s{2n})\epsilon_D^{(t-1)}+(\frac sn)^2\frac{G_*(s)}{2\lambda}$ and $\epsilon_D^{(t)}\le(1-\frac s{2n})^t\epsilon_D^{(0)}+\frac sn\frac{G_*(s)}\lambda$, with $G_*(s)=4L^2N(s/(\lambda n))/n$.
6. Lemma 2 (p. 13): $D(\alpha)\le P(w^*)\le P(0)\le1$ and $D(0)\ge0$.

Significance

Theorem 5 gives a linear rate for the dual sub-optimality of SDCA on non-smooth losses whenever few constants $\gamma_i$ are small. If $N(s_0/(\lambda n))=0$ for some $s_0>0$ (for the SVM, $\lambda n|w^{*\top}x_iy_i-1|\ge s_0$ for all $i$), the iteration count is $(2n/s_0)\log(2/\epsilon_D)$, compared with order $n+L^2/(\lambda\epsilon)$ from the Lipschitz analysis of Theorem 1 of the same paper. The paper uses Theorem 5 to explain the observed asymptotic advantage of SDCA over SGD, and its Theorem 6 converts it into a duality-gap bound.

The result is proved in the paper. It has not been formalized: no SDCA convergence result is on Prove2Me, and Mathlib has no conjugate-duality theory for this problem class. The mission produces a formal account of the dual objective in extended reals, of the exact coordinate maximization step, and of the averaging over uniformly random coordinate sequences, together with a checked proof of the rate. The companion missions of this series cover Theorem 1 (Lipschitz losses) and Theorem 2 (smooth losses).

Difficulty

Condition (5) gives a modulus $\gamma_i$ per coordinate, and some $\gamma_i$ may be zero, so the dual is not strongly concave and the standard linear-rate argument for strongly concave coordinate ascent does not apply. The per-step progress has a variance term with the sign of $\|x_i\|^2-\gamma_i\lambda n/s$, which is positive exactly on the coordinates with small modulus; that term must be controlled by bounding the dual variables themselves, which requires the Lipschitz structure through the conjugate. The extended-real-valued conjugate is a second source of work: every quantity must be shown finite along the run before it can be manipulated as a real number.

Formalization scope

Lean works in EuclideanSpace ℝ (Fin d), with $n$ data points indexed by Fin n, $n>0$. The conjugate is an EReal supremum and $D$ is EReal-valued, $-\infty$ exactly at infeasible points. Real-valued expectations of dual values appear only together with a conjunct stating their finiteness. The SDCA step is a map $\Delta$ with the hypothesis that $\Delta(\alpha,i)$ is an exact maximizer of the coordinate objective. The run is a fold over the sequence of chosen coordinates, and the expectation is the uniform average over all sequences of length $t$ (SAGA.Convex.expectIdx, a published definition). The optimum $\alpha^*$ is a hypothesis $D(\beta)\le D(\alpha^*)$ for all $\beta$; in (5), $w^*$ is $w(\alpha^*)$. Inequality (5) quantifies over feasible $\alpha$ only. Lemmas 5 and 6 are stated for an arbitrary feasible current state, which is stronger than the history-averaged form printed. The paper's range $s\in[0,1]$ becomes $s\in(0,1]$, because at $s=0$ the iteration bound $2(n/s)\log(2/\epsilon_D)$ is undefined. A formalization that admits $s=0$ would evaluate it to $0$ and claim the bound at $t=0$, which is false.

The development needs elementary facts about conjugates of scalar functions in EReal (convexity, the Fenchel–Young inequality, the Lipschitz domain bound), the weak duality inequality $D\le P$, and finite averages over coordinate sequences. The conjugate facts and the expectation calculus are reusable by the other two missions of the series. Proofs of individual milestones are welcome independently.

Selected references

• S. Shalev-Shwartz and T. Zhang, Stochastic Dual Coordinate Ascent Methods for Regularized Loss Minimization, Journal of Machine Learning Research 14 (2013), 567–599; preprint arXiv:1209.1873v2. https://arxiv.org/abs/1209.1873
• Z.-Q. Luo and P. Tseng, On the convergence of coordinate descent method for convex differentiable minimization, Journal of Optimization Theory and Applications 72 (1992), 7–35. https://doi.org/10.1007/BF00939948
• C.-J. Hsieh, K.-W. Chang, C.-J. Lin, S. S. Keerthi and S. Sundararajan, A dual coordinate descent method for large-scale linear SVM, ICML 2008. https://doi.org/10.1145/1390156.1390208