Machine Learning

Motivation

Reinforcement learning methods estimate the value function $v_\pi$ of a policy $\pi$: the expected discounted sum of future rewards from each state. When the state space is large, $v_\pi$ cannot be stored as a table and is approximated by a parametrized function. The most studied case is linear function approximation, where each state $s$ carries a feature vector $\mathbf x(s) \in \mathbb R^d$ and the estimate is $\hat v(s, \mathbf w) = \mathbf w^\top \mathbf x(s)$. Temporal-difference learning with this approximation, linear semi-gradient TD(0), is one of the basic algorithms of the field, and Chapter 9 of Sutton and Barto's Reinforcement Learning: An Introduction (2nd ed., MIT Press, 2018) presents its analysis: where the algorithm can converge, why that point exists, and how good it is.

The history is short. Sutton (1988, doi:10.1007/BF00115009) introduced TD learning and showed positive definiteness of the matrix governing its expected update. Dayan (1992, doi:10.1007/BF00992701) extended convergence to TD(λ). Tsitsiklis and Van Roy (1997, doi:10.1109/9.580874) proved convergence with probability one for linear TD(λ) under on-policy sampling and bounded the error of the limit. Bradtke and Barto (1996) introduced least-squares TD (LSTD), which computes the same limit directly.

Setting

A finite Markov decision process has finite sets of states $\mathcal S$, actions $\mathcal A$ and rewards $\mathcal R \subset \mathbb R$, and dynamics $p(s', r \mid s, a)$, the probability of next state $s'$ and reward $r$ after action $a$ in state $s$. A policy $\pi(a \mid s)$ is a probability distribution over actions for each state. It induces a Markov chain on states with transition matrix $\mathbf P$, $\mathbf P(s, s') = p(s' \mid s) = \sum_a \pi(a \mid s) \sum_r p(s', r \mid s, a)$, and expected one-step reward $r_\pi(s)$. For a discount rate $0 \le \gamma < 1$, the true value is $v_\pi(s) = \sum_{k \ge 0} \gamma^k (\mathbf P^k r_\pi)(s)$, the expected discounted return.

A state distribution $\mu$ is stationary if $\mu^\top \mathbf P = \mu^\top$; write $\mathbf D = \mathrm{diag}(\mu)$. The feature matrix $\mathbf X$ is the $|\mathcal S| \times d$ matrix with rows $\mathbf x(s)$. The mean square value error of a weight vector is

$$\overline{\mathrm{VE}}(\mathbf w) = \sum_{s} \mu(s)\,[v_\pi(s) - \mathbf w^\top \mathbf x(s)]^2 .$$

Linear semi-gradient TD(0) updates $\mathbf w_{t+1} = \mathbf w_t + \alpha(R_{t+1} + \gamma \mathbf w_t^\top \mathbf x_{t+1} - \mathbf w_t^\top \mathbf x_t)\mathbf x_t$. In steady state its expected update involves

$$\mathbf b = \mathbb E[R_{t+1}\mathbf x_t], \qquad \mathbf A = \mathbb E[\mathbf x_t(\mathbf x_t - \gamma \mathbf x_{t+1})^\top],$$

and the TD fixed point is $\mathbf w_{\mathrm{TD}} = \mathbf A^{-1}\mathbf b$. A real square matrix $M$, not necessarily symmetric, is positive definite if $y^\top M y > 0$ for every $y \ne 0$. The key matrix is $\mathbf D(\mathbf I - \gamma\mathbf P)$.

Formalization targets

Goal: the TD fixed point exists and its error bound (9.12), (9.14)

Under the hypotheses above, with every $\mu(s) > 0$ and linearly independent feature columns, $\mathbf A$ is invertible, $\mathbf b = \mathbf A \mathbf w_{\mathrm{TD}}$, and

$$\overline{\mathrm{VE}}(\mathbf w_{\mathrm{TD}}) \le \frac{1}{1-\gamma}\min_{\mathbf w} \overline{\mathrm{VE}}(\mathbf w).$$

Milestones

1. The expected update (9.13): $\mathbb E[\mathbf w_{t+1} \mid \mathbf w_t] = (\mathbf I - \alpha \mathbf A)\mathbf w_t + \alpha \mathbf b$.
2. The matrix form $\mathbf A = \mathbf X^\top \mathbf D(\mathbf I - \gamma \mathbf P)\mathbf X$.
3. The criterion of Sutton (1988): positive diagonal, nonpositive off-diagonal entries, positive row sums and nonnegative column sums give positive definiteness.
4. The column sums of the key matrix, $\mathbf 1^\top \mathbf D(\mathbf I - \gamma \mathbf P) = (1-\gamma)\mu^\top$.
5. The key matrix and $\mathbf A$ are positive definite.
6. A positive definite $\mathbf A$ is invertible and $\mathbf A^{-1}\mathbf b$ is the unique solution of $\mathbf b = \mathbf A \mathbf w$ (9.12).
7. The Sherman–Morrison update (9.22) of the LSTD inverse $\hat{\mathbf A}_t^{-1}$.

Significance

Positive definiteness of $\mathbf A$ is the reason on-policy linear TD(0) is stable: it makes the expected iteration contract toward the fixed point for small step sizes, and it guarantees that the fixed point exists and is unique. The error bound (9.14) quantifies the price of bootstrapping: the limit of TD can be worse than the best linear approximation, but by at most the factor $1/(1-\gamma)$. The same objects $\mathbf A$, $\mathbf b$ and the key matrix reappear in LSTD, in the analysis of off-policy divergence (Chapter 11 of the book, where $\mathbf D$ is no longer the stationary distribution of $\mathbf P$ and positive definiteness fails), and in gradient-TD methods.

All results here are known. The book gives the positive definiteness argument in a box and cites (9.14) without proof. None of them has a machine-checked proof on the platform; the general Woodbury identity (FamousTheorems.woodbury_identity) is available, and (9.22) is its rank-one case written for the LSTD recursion. The mission produces a formal account of the finite-state theory of linear TD(0), with every hypothesis the book leaves implicit stated.

Difficulty

The key matrix $\mathbf D(\mathbf I - \gamma \mathbf P)$ is not symmetric, so the usual tools for symmetric positive definite matrices do not apply directly, and $\mathbf A$ is positive definite only because of the specific interplay between $\mathbf D$ and $\mathbf P$: if $\mu$ is replaced by a non-stationary distribution the claim is false (this is the off-policy counterexample of Chapter 11). The error bound (9.14) is not a consequence of positive definiteness alone. The TD fixed point is not the minimizer of $\overline{\mathrm{VE}}$, and $\overline{\mathrm{VE}}(\mathbf w_{\mathrm{TD}})$ has to be compared with the error of the $\mu$-weighted projection of $v_\pi$, which requires controlling $\mathbf P$ in the $\mu$-weighted norm. The book gives no argument for this step.

Formalization scope

The Lean development lives in the namespace SuttonBartoRL.LinearTD. The MDP has four-argument dynamics $p(s', r \mid s, a)$ with a finite reward set and one action set for all states; policies are stochastic. $v_\pi$ is defined from expected discounted returns as the series $\sum_k \gamma^k \mathbf P^k r_\pi$, never from a Bellman equation or from $\mathbf w_{\mathrm{TD}}$. $\mathbf A$ and $\mathbf b$ are defined as the book's steady-state expectations (9.11), as finite sums over $\mu$, $\pi$ and $p$; the matrix form is a milestone, not a definition. Features are a matrix Matrix S (Fin d) ℝ with rows $\mathbf x(s)$; linear independence of its columns is LinearIndependent ℝ Xᵀ. Positive definiteness is a custom predicate $\forall y \ne 0,\ 0 < y^\top M y$, not Mathlib's Matrix.PosDef, which requires symmetry. The minimum in (9.14) is expressed by quantifying over every $\mathbf w$. The matrix inverse is Mathlib's, which is zero on singular matrices; the goal therefore asserts invertibility of $\mathbf A$ explicitly.

Hypotheses the book leaves implicit and the statements make explicit: $0 \le \gamma < 1$ (the continuing case); $\mu$ a stationary distribution of the chain induced by $\pi$ with $\mu(s) > 0$ for every $s$ (otherwise the key matrix is only positive semidefinite); linearly independent feature columns (the book's "degenerate cases", p. 205). The box calls the off-diagonal entries of the key matrix "negative"; they are zero wherever $p(s' \mid s) = 0$, so the criterion is stated with nonpositive entries. The book's sentence that $\varepsilon\mathbf I$ "ensures that $\hat{\mathbf A}_t$ is always invertible" (p. 229) is false in general, because the summands $\mathbf x_k(\mathbf x_k - \gamma \mathbf x_{k+1})^\top$ are not positive semidefinite: with $d = 1$, $\varepsilon = 1/10$, $\gamma = 1/2$, $\mathbf x_0 = 1$, $\mathbf x_1 = 11/5$ one gets $\hat{\mathbf A}_1 = 0$. It is not stated; (9.22) carries invertibility of $\hat{\mathbf A}_{t-1}$ and a nonzero denominator as hypotheses.

A statement in which $v_\pi$ is defined as the solution of the projected equation, or in which $\mathbf A$ is assumed invertible or positive definite, would make the goal trivial or empty; neither is done. Convergence of the stochastic algorithm with probability one is not stated, since the book says it needs conditions and a step-size schedule it does not give. The bound for the episodic case and for other bootstrapping methods (p. 208) is stated only by reference in the book and is not a target.

Useful infrastructure: the $\mu$-weighted inner product and orthogonal projection onto the column space of $\mathbf X$, the non-expansiveness of a stochastic matrix in the norm of its stationary distribution, and the positive definiteness criterion for non-symmetric matrices. All of these are reusable in the off-policy and average-reward chapters of the book. Contributions of these lemmas, and of alternative proofs of the milestones, are welcome.

Selected references

• Richard S. Sutton and Andrew G. Barto, Reinforcement Learning: An Introduction, 2nd ed., MIT Press, 2018, ISBN 9780262039246, §§9.2, 9.4, 9.8.
• Richard S. Sutton, Learning to predict by the methods of temporal differences, Machine Learning 3, 1988. doi:10.1007/BF00115009
• John N. Tsitsiklis and Benjamin Van Roy, An analysis of temporal-difference learning with function approximation, IEEE Transactions on Automatic Control 42(5), 1997. doi:10.1109/9.580874
• Steven J. Bradtke and Andrew G. Barto, Linear least-squares algorithms for temporal difference learning, Machine Learning 22, 1996. doi:10.1007/BF00114723
• Richard S. Varga, Matrix Iterative Analysis, Prentice-Hall, 1962.

Motivation

Many problems in statistics and machine learning minimize an average of $n$ losses, one per data point, plus a regularizer: least squares, logistic regression, and their $\ell_1$- or $\ell_2$-penalized versions. When $n$ is large, a full gradient costs $n$ component gradients, while stochastic gradient descent, which uses one component per step, needs decreasing step sizes and converges slowly. Incremental gradient methods with variance reduction (SAG, SVRG, SDCA, Finito, MISO) use one component gradient per step but converge at the rate of a full-gradient method.

SAGA (Defazio, Bach and Lacoste-Julien, NIPS 2014, arXiv:1407.0202) is a method of this family. It handles a non-smooth regularizer through its proximal operator, and it comes with a guarantee when the losses are convex but not strongly convex. This mission covers that second guarantee, Theorem 2 of the paper. A companion mission covers the linear rate under strong convexity (Theorem 1, Corollary 1).

Timeline.

• 2012: SAG (Le Roux, Schmidt and Bach) gives a linear rate for smooth, strongly convex finite sums. Its analysis does not cover a proximal term.
• 2013: SVRG (Johnson and Zhang) gives a linear rate for the strongly convex case, using periodic full-gradient passes.
• 2013: SDCA (Shalev-Shwartz and Zhang) works on the dual and needs strong convexity.
• 2014: Prox-SVRG (Xiao and Zhang, arXiv:1403.4699) extends SVRG to composite objectives. Its key inequality is reused by SAGA's Theorem 2.
• 2014: SAGA proves both a linear rate under strong convexity and an $O(n/k)$ rate for the averaged iterate under convexity alone, for composite objectives.

Setting

Let $d\ge 0$ and $n\ge 1$. The components $f_1,\dots,f_n:\mathbb R^d\to\mathbb R$ are convex and differentiable, and each gradient $f_i'$ is $L$-Lipschitz ($L>0$). Write

$$f(x)=\frac1n\sum_{i=1}^n f_i(x),\qquad f'(x)=\frac1n\sum_{i=1}^n f_i'(x).$$

The regularizer $h:\mathbb R^d\to\mathbb R$ is convex but possibly non-differentiable. The objective is the composite function $F=f+h$, and $x^*$ is any minimizer of $F$. Minimizers need not be unique, and $f'(x^*)$ need not vanish.

The proximal operator with parameter $\gamma>0$ is

$$\mathrm{prox}_\gamma^h(y)=\arg\min_{x\in\mathbb R^d}\Big\{h(x)+\frac1{2\gamma}\|x-y\|^2\Big\}.$$

SAGA keeps an iterate $x^k$ and a table of points $\phi_1^k,\dots,\phi_n^k$, initialized as $\phi_i^0=x^0$. At step $k+1$ it draws an index $j$ uniformly from $\{1,\dots,n\}$, independently of the past, and sets

$$w^{k+1}=x^k-\gamma\Big[f_j'(x^k)-f_j'(\phi_j^k)+\frac1n\sum_{i=1}^n f_i'(\phi_i^k)\Big],\qquad x^{k+1}=\mathrm{prox}_\gamma^h(w^{k+1}).$$

It then sets $\phi_j^{k+1}=x^k$ and leaves the other table entries unchanged. The averaged iterate is $\bar x^k=\frac1k\sum_{t=1}^k x^t$, which excludes $x^0$.

Formalization targets

Goal: Theorem 2 (p. 11)

With step size $\gamma=1/(3L)$, for every $k\ge1$,

$$\mathbb E\big[F(\bar x^k)\big]-F(x^*)\le\frac{4n}{k}\Big[\frac{2L}{n}\|x^0-x^*\|^2+f(x^0)-\langle f'(x^*),x^0-x^*\rangle-f(x^*)\Big].$$

The expectation is over the indices $j^1,\dots,j^k$. The constants are those printed in the paper.

Milestones (in attack order)

1. Lemma 1 (p. 6) is an inner-product bound for averages of $\mu$-strongly convex functions with $L$-Lipschitz gradients. It is stated for $\mu\ge0$, and Theorem 2 uses the case $\mu=0$.
2. Lemma 2 (p. 7): $\frac1n\sum_i\|f_i'(\phi_i)-f_i'(x^*)\|^2\le 2L\big[\frac1n\sum_i f_i(\phi_i)-f(x^*)-\frac1n\sum_i\langle f_i'(x^*),\phi_i-x^*\rangle\big]$.
3. The bound on $\Delta$ (p. 12). Write $\Delta=-\frac1\gamma(w^{k+1}-x^k)-f'(x^k)$ for the gradient error. For every $\beta>0$, $\mathbb E\|\Delta\|^2\le(1+\beta^{-1})\mathbb E\|f_j'(\phi_j^k)-f_j'(x^*)\|^2+(1+\beta)\mathbb E\|f_j'(x^k)-f_j'(x^*)\|^2$.
4. The prox-SVRG inequality (p. 12): $\alpha\mathbb E\|x^{k+1}-x^*\|^2\le\alpha\|x^k-x^*\|^2-2\alpha\gamma\mathbb E[F(x^{k+1})-F(x^*)]+2\alpha\gamma^2\mathbb E\|\Delta\|^2$.
5. The one-step Lyapunov decrease (p. 12): $\mathbb E[T^{k+1}]-T^k\le-\frac1{4n}\mathbb E[F(x^{k+1})-F(x^*)]$. Here $T(x,\phi)=\frac1n\sum_i f_i(\phi_i)-f(x^*)-\frac1n\sum_i\langle f_i'(x^*),\phi_i-x^*\rangle+(c+\alpha)\|x-x^*\|^2$, with $c=\frac{3L}{2n}$ and $\alpha=\frac{3L}{8n}$.

In milestones 3–5, $\mathbb E$ is the expectation over the single index $j$ of the next step, given the current state.

Significance

The result. Theorem 2 shows that one method, with a step size that depends only on $L$, covers composite problems that are not strongly convex. Examples are $\ell_1$-regularized least squares and logistic regression without a ridge term. On these problems the method converges in expected objective value at rate $O(n/k)$. SAG has no proximal analysis, and SDCA requires strong convexity. With the same step size $1/(3L)$, the paper also states adaptivity to strong convexity, so no strong convexity constant has to be known in advance. The bound is in terms of $T^0$, a quantity computable from the starting point.

Formalizing it. The result is proved on paper, but the proof is not self-contained. Its central inequality (milestone 4) is quoted from the prox-SVRG analysis of Xiao and Zhang, with only the remark that their argument uses $\mathbb E[\Delta]=0$. A machine-checked proof must therefore reconstruct that argument for SAGA's estimator. To our knowledge, no machine-checked proof of SAGA, SVRG or prox-SVRG exists in Lean or Mathlib. The mission also produces reusable statements about convex functions with Lipschitz gradients (Lemmas 1 and 2) and an explicit finite model of a randomized incremental method.

Difficulty

The naive approach applies the non-expansiveness of the proximal operator to $\|x^{k+1}-x^*\|^2$, as in the strongly convex proof. That bounds distances, but it produces no term in $F(x^{k+1})-F(x^*)$. Without strong convexity, the distance terms cannot be traded for function values, so the argument yields no rate.

The function-value term comes from the prox-SVRG inequality (milestone 4), which the paper does not prove. Its difficulty is that $x^{k+1}$ depends on the same random index as $\Delta$, so the cross term between them does not vanish in expectation even though $\mathbb E[\Delta]=0$. A second difficulty is bookkeeping: $w^{k+1}$ uses the old table, the table entry $j$ receives $x^k$ and not $x^{k+1}$, and the constants must make three coefficients vanish exactly. A final step converts the bound on $\frac1k\sum_t\mathbb E[F(x^t)]$ into a bound on $\mathbb E[F(\bar x^k)]$, which requires Jensen's inequality for the convex $F$.

Formalization scope

• Space and indices. Points live in EuclideanSpace ℝ (Fin d). Components are indexed by Fin n (0-based), with $n\ge1$.
• Gradients and smoothness. The gradients are given maps f' with HasGradientAt (f i) (f' i x) x at every point. Smoothness is the Lipschitz bound $\|f_i'(x)-f_i'(y)\|\le L\|x-y\|$.
• Convexity. Convexity is ConvexOn ℝ Set.univ. Lemma 1 uses StrongConvexOn Set.univ μ, whose modulus $\frac\mu2\|x-y\|^2$ is the paper's.
• The regularizer. $h$ is real-valued and convex. Extended-valued regularizers such as indicator functions are outside the statement.
• The proximal map. The proximal operator enters as any map $P$ such that $P(y)$ minimizes $h(z)+\frac1{2\gamma}\|z-y\|^2$ for every $y$. For convex $h$ this determines $P=\mathrm{prox}_\gamma^h$.
• State and expectation. The state is the pair $(x^k,\phi^k)$. The expectation over $k$ steps is the uniform average over the $n^k$ index sequences, which is exactly the law of $k$ independent uniform indices.

Two trivializations are excluded. The averaged-iterate bound carries $k\ge1$, since at $k=0$ the factor $4n/k$ collapses to $0$. The left side is $F$ evaluated at the averaged point, not the average of $F(x^t)$, which is a weaker intermediate step.

A complete development needs the descent lemma and co-coercivity for convex functions with Lipschitz gradients, the characterization and non-expansiveness of the proximal operator, and finite-sum manipulations over index sequences. The lemmas on smooth convex functions and on proximal operators are reusable beyond this mission. Contributions are welcome at every level: proofs of the milestones, a reusable proximal-operator library, and the telescoping argument for the goal.

Selected references

• A. Defazio, F. Bach, S. Lacoste-Julien, SAGA: A Fast Incremental Gradient Method With Support for Non-Strongly Convex Composite Objectives, NIPS 2014. arXiv:1407.0202
• L. Xiao, T. Zhang, A Proximal Stochastic Gradient Method with Progressive Variance Reduction, SIAM J. Optim. 24(4), 2014. arXiv:1403.4699
• N. Le Roux, M. Schmidt, F. Bach, A Stochastic Gradient Method with an Exponential Convergence Rate for Finite Training Sets, NIPS 2012. arXiv:1202.6258
• R. Johnson, T. Zhang, Accelerating Stochastic Gradient Descent using Predictive Variance Reduction, NIPS 2013. NeurIPS proceedings
• S. Shalev-Shwartz, T. Zhang, Stochastic Dual Coordinate Ascent Methods for Regularized Loss Minimization, JMLR 14, 2013. arXiv:1209.1873
• Y. Nesterov, Introductory Lectures on Convex Optimization, Kluwer, 2004. doi:10.1007/978-1-4419-8853-9

Motivation

Reinforcement learning methods must explore in order to find good behaviour, yet the quantity they usually want to evaluate is the value of a different, often deterministic, policy. Off-policy prediction separates the two roles: episodes are generated by a behaviour policy $b$, and the goal is the value function $v_\pi$ of a target policy $\pi$. Almost every off-policy method in Sutton and Barto's Reinforcement Learning: An Introduction (2nd ed., MIT Press, 2018), and in the literature that follows it, rests on importance sampling: a return observed under $b$ is reweighted by the relative probability of its trajectory under $\pi$ and $b$. Section 5.5 of the book introduces the idea for Monte Carlo prediction, §5.6 gives the incremental form of the weighted estimator, and §§5.8–5.9 refine the weights using the internal structure of the return: discounting-aware importance sampling, after Sutton, Mahmood, Precup and van Hasselt (2014), and per-decision importance sampling, introduced by Precup, Sutton and Singh (2000). The book's remarks on the variance of the two estimators (p. 105) cite Precup, Sutton and Dasgupta (2001). Later chapters (7, 11, 12) reuse the same ratios for $n$-step, gradient-TD and eligibility-trace methods.

This mission is the fifth in a series formalizing the book's central mathematical claims. It covers §§5.5–5.9 (pp. 103–115).

Setting

A finite Markov decision process has finite sets of states $\mathcal S$ (terminal states included), actions $\mathcal A$ and rewards $\mathcal R \subset \mathbb R$, and dynamics $p(s', r \mid s, a)$: for each $(s, a)$ a probability distribution over next state and reward. The state-transition probability is $p(s' \mid s, a) = \sum_r p(s', r \mid s, a)$. A policy $\mu$ gives a distribution $\mu(\cdot \mid s)$ over actions in every state.

An episode from a start state $s$ is a sequence $S_0 = s, A_0, R_1, S_1, \dots, A_{T-1}, R_T, S_T$ in which $S_0, \dots, S_{T-1}$ are nonterminal and $S_T$ is terminal. Under $\mu$ it has probability $\prod_{k=0}^{T-1} \mu(A_k \mid S_k)\, p(S_{k+1}, R_{k+1} \mid S_k, A_k)$. The return is $G_0 = \sum_{k=0}^{T-1} \gamma^k R_{k+1}$ with discount rate $\gamma \in [0, 1]$, and the value $v_\pi(s)$ is the expected return of an episode generated by $\pi$ from $s$.

The behaviour policy covers the target policy if $\pi(a \mid s) > 0$ implies $b(a \mid s) > 0$. The importance-sampling ratio of decisions $0, \dots, j$ is

$$\rho_{0:j} = \prod_{k=0}^{j} \frac{\pi(A_k \mid S_k)}{b(A_k \mid S_k)},$$

and the per-decision return weights each reward only by the ratio of the decisions that precede it:

$$\tilde G_0 = \rho_{0:0} R_1 + \gamma \rho_{0:1} R_2 + \dots + \gamma^{T-1} \rho_{0:T-1} R_T .$$

The book writes these objects at a general time $t$ and conditions on $S_t = s$; by the Markov property this is the same as starting the episode at $s$, which is what the formal statements do.

Formalization targets

Goal: unbiasedness of ordinary and per-decision importance sampling

For episodes generated by $b$ from $s$,

$$\mathbb E_b\bigl[\rho_{0:T-1} G_0 \mid S_0 = s\bigr] = v_\pi(s) = \mathbb E_b\bigl[\tilde G_0 \mid S_0 = s\bigr].$$

The first equality is Eq. (5.4) (p. 104); the second is the statement $\mathbb E[\rho_{t:T-1}G_t] = \mathbb E[\tilde G_t]$ of §5.9 (p. 114).

Milestones

1. (5.3): the trajectory probability is a product, and the ratio of trajectory probabilities under $\pi$ and $b$ is $\rho_{0:T-1}$, independent of the dynamics.
2. (5.4) alone.
3. (5.13): $\sum_a b(a \mid x)\, \pi(a \mid x)/b(a \mid x) = \sum_a \pi(a \mid x) = 1$ under coverage.
4. (5.14) and its $k$-th form: $\mathbb E_b[\rho_{0:T-1} R_k] = \mathbb E_b[\rho_{0:k-1} R_k]$ for every $k \ge 1$ (Exercise 5.13).
5. Example 5.5: in a one-state MDP with a loop, $v_\pi(s) = 1$ and $\mathbb E_b[\rho_{0:T-1}G_0] = 1$, yet $\mathbb E_b[(\rho_{0:T-1}G_0)^2] = \infty$.
6. (5.7)–(5.8): the incremental rule $V_{n+1} = V_n + (W_n/C_n)(G_n - V_n)$ computes the weighted average $\sum_{k<n} W_k G_k / \sum_{k<n} W_k$ (Exercise 5.10).
7. §5.8: $G_t = (1-\gamma)\sum_{h=t+1}^{T-1}\gamma^{h-t-1}\bar G_{t:h} + \gamma^{T-t-1}\bar G_{t:T}$ with flat partial returns $\bar G_{t:h} = R_{t+1} + \dots + R_h$.

Significance

Eq. (5.4) is the reason the first-visit ordinary importance-sampling estimator (5.5) is unbiased, and it is the template for every importance-sampling correction in the rest of the book. The per-decision identity shows that an estimator with fewer ratio factors per reward, (5.15), has the same expectation, which is the starting point for per-decision and control-variate methods for multi-step off-policy learning (Precup, Sutton and Singh 2000). Example 5.5 shows that unbiasedness says nothing about variance: the ordinary estimator can have infinite variance on a two-action problem, which motivates weighted importance sampling and the incremental weighted update of §5.6.

The results of these sections are classical and proved informally in the book, partly as exercises (5.10, 5.13) left without solution. No machine-checked version exists on the platform: a search for importance sampling, off-policy and per-decision returned no statements. The mission produces a formal trajectory model of an episodic MDP under two policies, which later missions on $n$-step off-policy returns and off-policy traces can reuse.

Difficulty

Eq. (5.4) itself is a termwise identity: for every episode, $\Pr_b(\text{episode})\,\rho_{0:T-1} = \Pr_\pi(\text{episode})$ under coverage. The per-decision identity is not termwise. The later factors of $\rho_{0:T-1}$ multiply a reward that was received before the corresponding decisions, and removing them requires summing over all continuations of an episode prefix, of every remaining length, and using that each factor has conditional expectation one (5.13) and that the continuation terminates with probability one. The obvious attempt, cancelling the factors episode by episode, fails: on a single episode $\rho_{0:T-1}R_1$ and $\rho_{0:0}R_1$ differ.

In Example 5.5 the episodes have no length bound, so the expected square is an infinite series over episode lengths whose divergence must be shown directly.

Formalization scope

• States, actions and rewards are finite types; the terminal states are a finite subset of the state type. Policies are stochastic, one action set is used in every state, and $v_\pi$ is defined as an expected return, never as the solution of a Bellman equation.
• Expectations are series over episode lengths of finite sums over episodes. Lean assigns $0$ to a divergent series, so the goal and milestones 2 and 4 assume that under $b$ every episode from $s$ terminates within a fixed number $H$ of steps with probability one. The book leaves termination implicit; this bounded-horizon hypothesis is a restriction relative to the book's episodic setting and is stated as such. Example 5.5, whose episodes are unbounded, is stated without it, with the expected square in $[0, \infty]$.
• The discount rate is kept general in $[0, 1]$.
• The importance-sampling ratio uses real division; a factor with $b(A_k \mid S_k) = 0$ evaluates to $0$ in Lean, but such episodes have probability $0$ under $b$.
• The flat-partial-return decomposition is an algebraic identity and is stated for every real $\gamma$, which is more general than the book's "for any $\gamma \in [0,1)$".
• The incremental weighted update is stated with nonnegative weights and $W_1 > 0$. The book's $C_0 = 0$ makes (5.8) divide by zero at $n = 1$ when $W_1 = 0$; the hypothesis excludes that case.
• A trivializing formalization is ruled out: $v_\pi$ is the expected return of $\pi$'s own episodes, the ratio is computed from the episode, and the per-decision identity, which carries the chapter's content beyond (5.4), is part of the goal.
• Not stated: the bias and variance comparisons of ordinary and weighted importance sampling (p. 105) and the discounting-aware estimators (5.9)–(5.10) as estimators; these are statistical claims about estimators over a random number of visits that the book does not make precise.

Contributions welcome: proofs of the milestones, a general measure-theoretic version of the trajectory model without the bounded-horizon hypothesis, and variants for action values $q_\pi$ (Exercise 5.6).

Selected references

• R. S. Sutton and A. G. Barto, Reinforcement Learning: An Introduction, 2nd ed., MIT Press, 2018, ISBN 9780262039246, §§5.5–5.9, pp. 103–115. http://incompleteideas.net/book/the-book-2nd.html
• D. Precup, R. S. Sutton and S. Singh, Eligibility Traces for Off-Policy Policy Evaluation, Proceedings of the 17th International Conference on Machine Learning (ICML), 2000, pp. 759–766 (cited in the book's bibliography).
• D. Precup, R. S. Sutton and S. Dasgupta, Off-Policy Temporal-Difference Learning with Function Approximation, Proceedings of the 18th International Conference on Machine Learning (ICML), 2001, pp. 417–424 (cited in the book, p. 105).

Motivation

Many problems in machine learning and statistics are finite sums: an empirical risk $f(x)=\frac1n\sum_{i=1}^n f_i(x)$ over $n$ data points, often plus a regulariser $h$ such as an $\ell_1$ penalty. When $n$ is large, a full gradient of $f$ costs $n$ component gradients, while stochastic gradient descent uses one component per step but converges only sublinearly because its gradient estimate has non-vanishing variance. Incremental gradient methods with variance reduction keep the per-step cost of one component gradient and still converge linearly on strongly convex problems.

SAGA, introduced by Defazio, Bach and Lacoste-Julien at NIPS 2014 (arXiv:1407.0202), is one of the standard methods of this family, alongside SAG, SVRG, SDCA and Finito/MISO. It keeps a table of past component gradients and handles a non-smooth regulariser through its proximal operator.

Timeline. Le Roux, Schmidt and Bach (2012) gave SAG the first linear rate for strongly convex finite sums at the cost of one gradient per step. Shalev-Shwartz and Zhang (2013) proved linear rates for SDCA, a dual method. Johnson and Zhang (2013) introduced SVRG, with periodic full-gradient passes; Xiao and Zhang (2014) extended it to composite objectives (prox-SVRG). SAGA (2014) combines an unbiased SVRG-style estimator with a SAG-style table, and proves a linear rate in the composite strongly convex case with a simple Lyapunov argument.

Setting

Let $\mathbb R^d$ carry the Euclidean inner product. There are $n\ge1$ differentiable components $f_1,\dots,f_n:\mathbb R^d\to\mathbb R$ with gradients $f_i'$. Each $f_i$ is $\mu$-strongly convex ($\mu>0$): $f_i(ax+by)\le af_i(x)+bf_i(y)-ab\frac\mu2\|x-y\|^2$ for $a,b\ge0$, $a+b=1$. Each gradient is $L$-Lipschitz: $\|f_i'(x)-f_i'(y)\|\le L\|x-y\|$. Write $f=\frac1n\sum_i f_i$ and $f'=\frac1n\sum_i f_i'$. The regulariser $h:\mathbb R^d\to\mathbb R$ is convex, and the goal is to minimise the composite objective $F=f+h$; $x^*$ denotes its minimiser, which is unique.

The proximal operator with step $\gamma>0$ is

$$\operatorname{prox}^h_\gamma(y)=\operatorname*{argmin}_{x}\Big\{h(x)+\tfrac1{2\gamma}\|x-y\|^2\Big\}.$$

SAGA keeps an iterate $x^k$ and points $\phi_1^k,\dots,\phi_n^k$ at which the stored gradients $f_i'(\phi_i^k)$ were taken. It starts from $x^0$ with $\phi_i^0=x^0$. At iteration $k+1$ it draws $j$ uniformly from $\{1,\dots,n\}$, independently of the past, and sets

$$w^{k+1}=x^k-\gamma\Big[f_j'(x^k)-f_j'(\phi_j^k)+\frac1n\sum_{i=1}^n f_i'(\phi_i^k)\Big],\qquad x^{k+1}=\operatorname{prox}^h_\gamma(w^{k+1}),$$

then $\phi_j^{k+1}=x^k$, with every other entry unchanged.

The analysis uses the Lyapunov function

$$T(x,\{\phi_i\})=\frac1n\sum_i f_i(\phi_i)-f(x^*)-\frac1n\sum_i\langle f_i'(x^*),\phi_i-x^*\rangle+c\|x-x^*\|^2 .$$

Formalization targets

Goal: Corollary 1 (p. 8)

With $\gamma=\frac1{2(\mu n+L)}$, for every $k\ge0$,

$$\mathbb E\|x^k-x^*\|^2\le\Big(1-\frac{\mu}{2(\mu n+L)}\Big)^k\Big[\|x^0-x^*\|^2+\frac{n}{\mu n+L}\big(f(x^0)-\langle f'(x^*),x^0-x^*\rangle-f(x^*)\big)\Big],$$

where the expectation is over the indices drawn in the first $k$ iterations. The constants are the paper's.

Theorem 1 (p. 7)

With $\gamma$ as above, $c=\frac1{2\gamma(1-\gamma\mu)n}$ and $\kappa=\frac1{\gamma\mu}$, for every state $(x^k,\{\phi^k_i\})$,

$$\mathbb E\big[T^{k+1}\big]\le\Big(1-\frac1\kappa\Big)T^k ,$$

with the expectation over the next index only.

Supporting lemmas

Lemma 4 (p. 10), a lower bound combining strong convexity and smoothness; Lemma 1 (pp. 6–7), its average over the components; Lemma 2 (p. 7), which bounds the stale-gradient variance by the table part of $T$; and Lemma 3 (p. 7), a second-moment bound for the SAGA step.

Significance

The result. Corollary 1 gives an $\varepsilon$-accurate iterate in expectation after $O\big((n+L/\mu)\log(1/\varepsilon)\big)$ component-gradient evaluations. This is the complexity of full-gradient descent with the condition number decoupled from $n$, and it holds in the composite setting, so it covers the lasso and elastic-net problems that SAG's analysis does not reach. The paper notes that the rate improves on the published rates of SAG and SVRG and is within a factor 2 of SDCA's. Theorem 1 is the template of later Lyapunov analyses of variance-reduced methods.

Formalizing it. The result has been proved since 2014, and no machine-checked proof is known to this mission. The work left is to formalize the known proof: the convexity inequalities (Lemmas 4, 1, 2), the variance computation (Lemma 3), the one-step contraction (Theorem 1), and the passage from conditional to total expectation along the random index sequence (Corollary 1). The paper's Lemma 3 has a sign misprint, which the formalization corrects; see the scope section.

Difficulty

The obvious argument for SGD-type methods bounds $\mathbb E\|x^{k+1}-x^*\|^2$ in terms of $\|x^k-x^*\|^2$ alone. That fails here: the variance of the SAGA estimator depends on the stale table points $\phi_i^k$, which can be far from $x^*$ even when $x^k$ is close. One needs a potential that also measures the table. Balancing the terms of $T$ then requires the four round-bracket coefficients in the paper's display (10) to be non-positive for the specific $\gamma$, $c$ and an auxiliary $\beta=(2\mu n+L)/L$. Checking these coefficients is routine but long algebra in $\mu$, $L$, $n$. The composite case adds one step: since $f'(x^*)\neq0$ in general, the argument goes through the fixed-point identity $x^*=\operatorname{prox}^h_\gamma(x^*-\gamma f'(x^*))$ and the non-expansiveness of the proximal operator, neither of which is a numbered result of the paper.

Formalization scope

• Space and data. The space is EuclideanSpace ℝ (Fin d). Components are indexed by Fin n (0-based), with 0 < n. The gradients $f_i'$ are given maps with HasGradientAt (f i) (f' i x) x. Strong convexity is Mathlib's StrongConvexOn Set.univ μ, whose modulus $\frac\mu2\|x-y\|^2$ is the paper's.

• Regulariser and minimiser. $h$ is real-valued and convex; extended-valued regularisers are out of scope, as on the page. A minimiser $x^*$ of $f+h$ is a hypothesis.

• Proximal operator. It is any map $P$ such that $P(y)$ minimises $h(x)+\frac1{2\gamma}\|x-y\|^2$ for every $y$ (IsProxPoint). The minimiser is unique, so $P$ is $\operatorname{prox}^h_\gamma$.

• State and expectation. The state is the pair $(x,\phi)$. The run after $k$ steps is a deterministic function of the index sequence in Fin k → Fin n. The expectation in Corollary 1 is the average over all $n^k$ sequences, which is exactly the law of $k$ independent uniform indices; no measure theory is involved. Theorem 1's conditional expectation is the average over the next index.

• Constants and corrections. Constants are as printed and fixed, not "for some constant" and not "for all small enough steps". Lemma 4 carries the hypothesis $\mu<L$, which its fractions $1/(L-\mu)$ require. Lemma 3 is stated with $+\gamma f'(x^*)$, as in its proof and its use in Theorem 1; the printed $-\gamma f'(x^*)$ is false whenever $f'(x^*)\neq0$.

• Trivializing formalizations, ruled out. Taking the proximal step as merely non-expansive, fixing an index sequence instead of averaging over all of them, measuring $x^*$ against $f$ instead of $f+h$, or restricting Theorem 1 to reachable states changes the theorem and is excluded.

• Infrastructure. A complete development needs:

  • the co-coercivity inequality for convex functions with Lipschitz gradient;
  • existence, uniqueness and non-expansiveness of the proximal map of a finite convex function;
  • the optimality condition $x^*=\operatorname{prox}^h_\gamma(x^*-\gamma f'(x^*))$;
  • finite-sum variance identities.

  These pieces are reusable well beyond SAGA, by SVRG, SAG and proximal-gradient analyses. Contributions of any of them, or of proofs of the individual milestones, are welcome.

Selected references

• A. Defazio, F. Bach, S. Lacoste-Julien, SAGA: A Fast Incremental Gradient Method With Support for Non-Strongly Convex Composite Objectives, NIPS 2014. arXiv:1407.0202
• N. Le Roux, M. Schmidt, F. Bach, A Stochastic Gradient Method with an Exponential Convergence Rate for Finite Training Sets, NIPS 2012. arXiv:1202.6258
• R. Johnson, T. Zhang, Accelerating Stochastic Gradient Descent using Predictive Variance Reduction, NIPS 2013. NeurIPS proceedings
• L. Xiao, T. Zhang, A Proximal Stochastic Gradient Method with Progressive Variance Reduction, SIAM J. Optim. 24(4), 2014. arXiv:1403.4699
• S. Shalev-Shwartz, T. Zhang, Stochastic Dual Coordinate Ascent Methods for Regularized Loss Minimization, JMLR 14, 2013. arXiv:1209.1873
• Y. Nesterov, Introductory Lectures on Convex Optimization, Kluwer, 2004. doi:10.1007/978-1-4419-8853-9

Motivation

In many sequential decision problems the learner sees side information before acting. A news site chooses an article for a visitor whose history and location it knows; an ad server chooses an advertisement for a query. Only the reward of the chosen action is observed. These are contextual bandit problems, and Chapter 4 of Bubeck and Cesa-Bianchi's monograph Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems (arXiv:1204.5721v2) surveys several of their formal versions. In a contextual problem the learner is compared with the best policy, a map from contexts to arms, rather than with the best single arm.

This mission covers three of the chapter's models. The first marks each round with a context from a finite set. In the second, $N$ experts give advice, as in prediction with expert advice. The third is the bandit multiclass problem: a linear classifier predicts one of $K$ labels and then learns only whether its prediction was right. The goal is the mistake bound of the Banditron (Kakade, Shalev-Shwartz and Tewari, ICML 2008). The bound shows that one bit of feedback per round suffices to compete with every linear classifier, at regret $O(n^{2/3})$.

Setting

There are $K \ge 2$ arms (or labels) $\{1,\dots,K\}$ and rounds $t = 1, \dots, n$.

Adversarial losses. At round $t$ an adversary assigns losses $\ell_{i,t} \in [0,1]$ to the arms and may adapt to the forecaster's past plays $I_1, \dots, I_{t-1}$. The forecaster draws $I_t$ at random from a distribution $p_t$ that depends on what it has observed, and it observes only $\ell_{I_t,t}$. Expectations $\mathbb E$ are over the forecaster's draws.

Side information. Each round carries a context $s_t$ from a finite set $\mathcal S$, and the sequence $s_1, s_2, \dots$ is fixed in advance. The pseudo-regret against context-to-arm maps is

$$\overline R^{\mathcal S}_n = \max_{g:\mathcal S\to\{1,\dots,K\}} \mathbb E\Big[\sum_{t=1}^n \ell_{I_t,t} - \sum_{t=1}^n \ell_{g(s_t),t}\Big].$$

The S-Exp3 forecaster runs one instance of Exp3 (Section 3.1 of the book) on each context.

Expert advice. At each round each of $N$ experts $j$ proposes a distribution $\xi^j_t$ over arms, which may depend on the forecaster's past plays. The contextual pseudo-regret is

$$\overline R^{\mathrm{ctx}}_n = \max_{k=1,\dots,N}\mathbb E\Big[\sum_{t=1}^n \ell_{I_t,t} - \sum_{t=1}^n \mathbb E_{i\sim\xi^k_t}\ell_{i,t}\Big].$$

Exp4 (Fig. 4.1) runs exponential weights over the experts with importance-weighted loss estimates.

Bandit multiclass. The examples $(x_t, y_t) \in \mathbb R^d \times \{1,\dots,K\}$ are fixed in advance, with $\|x_t\| = 1$ (Euclidean). A $K\times d$ matrix $U$ classifies $x$ by $\arg\max_i (Ux)_i$. Its multiclass hinge loss on round $t$ is $\ell_t(U) = [1 - (Ux_t)_{y_t} + \max_{i\neq y_t}(Ux_t)_i]_+$. Write $L_n(U) = \sum_{t\le n}\ell_t(U)$ for the cumulative hinge loss, $\bar L_n(U) = L_n(U)/n$ for its average, and $\|U\|$ for the Frobenius norm. The multiclass Perceptron predicts $\hat y_t = \arg\max_i (W_tx_t)_i$ and, after seeing $y_t$, adds $x_t$ to row $y_t$ and subtracts it from row $\hat y_t$. The Banditron (p. 58) predicts $Y_t$ from $p_{i,t} = (1-\gamma)\mathbb 1_{\hat y_t = i} + \gamma/K$. It observes only $\mathbb 1_{Y_t = y_t}$ and updates $W_{t+1} = W_t + \widetilde X_t$, where $(\widetilde X_t)_{i,j} = x_{t,j}\big(\mathbb 1_{Y_t=y_t}\mathbb 1_{Y_t=i}/p_{i,t} - \mathbb 1_{\hat y_t=i}\big)$. Its number of mistakes is $M_n = \sum_{t\le n}\mathbb 1_{Y_t\neq y_t}$.

Formalization targets

Goal: Theorem 4.7 (Banditron)

For $n \ge 8K$, $\gamma = (K/n)^{1/3}$, every example sequence as above and every $K\times d$ matrix $U$,

$$\mathbb E\,M_n \le L_n(U) + \Big(1 + \|U\|\sqrt{2\bar L_n(U)}\Big)K^{1/3}n^{2/3} + 2\|U\|^2K^{2/3}n^{1/3} + \sqrt2\,\|U\|K^{1/6}n^{1/3}.$$

Milestones

1. Multiclass Perceptron bound (Section 4.4, p. 57). For every $n \ge 1$ and $U$, $\sum_{t\le n}\mathbb 1_{\hat y_t\ne y_t} \le L_n(U) + 2\|U\|^2 + \|U\|\sqrt{2n\bar L_n(U)}$.
2. Theorem 4.1 (p. 44). S-Exp3 satisfies $\overline R^{\mathcal S}_n \le \sqrt{2n|\mathcal S|K\ln K}$.
3. Theorem 4.2 (p. 46), with corrected constants. Exp4 without mixing satisfies $\overline R^{\mathrm{ctx}}_n \le \sqrt{2nK\ln N}$ for $\eta_t = \sqrt{2\ln N/(nK)}$, and $\overline R^{\mathrm{ctx}}_n \le 2\sqrt{nK\ln N}$ for $\eta_t = \sqrt{\ln N/(tK)}$.
4. Theorem 4.3 (p. 50), with corrected learning rate. Let the plays be drawn from distributions $q_t$ with $q_{i,t}\ge\varepsilon > 0$, and let Exp3 run on the estimates $\ell_{i,t}\mathbb 1_{I_t=i}/q_{i,t}$ with $\eta = \sqrt{2\varepsilon\ln K/n}$. Then $\max_k \mathbb E\big[\sum_t \mathbb E_{i\sim p_t}\ell_{i,t} - \sum_t\ell_{k,t}\big] \le \sqrt{(2n/\varepsilon)\ln K}$.

Significance

Theorem 4.7 shows that, on any sequence of examples, the bandit version of online multiclass classification costs at most $O(K^{1/3}n^{2/3})$ mistakes beyond the hinge loss of the best linear classifier. The full-information Perceptron, by comparison, pays $O(\sqrt n)$. The bound has no stochastic assumption and has explicit constants. Theorems 4.1–4.3 are the basic regret guarantees for side information and expert advice. Theorem 4.3 in particular lets learning algorithms serve as experts inside Exp4, which is the construction behind Theorem 4.5.

The mission produces machine-checked statements, and eventually proofs, of these results with fully explicit constants and an explicit model of adaptive adversaries and adaptive advice. To the curators' knowledge none of the Banditron, the multiclass Perceptron bound, S-Exp3 or Theorem 4.3 is formalized anywhere. The platform's Bandit Algorithms series has a proved Exp4 bound, but only for advice and rewards fixed in advance. The book proves all four milestones and the goal; two printed statements (4.2 and 4.3) contain misprints that this mission corrects.

Difficulty

The Banditron bound concerns a randomized process whose weight matrix depends on all earlier random predictions. The Perceptron argument tracks $\langle U, W_{n+1}\rangle$ and $\|W_{n+1}\|^2$. It carries over only in conditional expectation, and the second moment of the importance-weighted update is of order $K/\gamma$ on rounds where $\hat y_t \neq y_t$ and of order $\gamma$ otherwise. Combining these into one inequality for $\sum_t\mathbb P(\hat y_t\neq y_t)$ and then for $\mathbb E M_n$ requires solving a quadratic inequality in the presence of expectations, and the constants must come out as printed. For the Exp3/Exp4 results, the obstacle is that losses and advice adapt to past plays. The standard potential argument has to be run conditionally on the history, and a version that fixes the losses in advance proves a weaker theorem.

Formalization scope

• Rounds and laws. Rounds are numbered from $0$ in Lean (Lean round $t$ is the book's round $t+1$). Every forecaster is a sampling rule from past plays to weights on Fin K. The law of the first $n$ plays is the product $\prod_t p_t(\omega_t\mid\omega_{<t})$ over sequences $\omega : \mathrm{Fin}\,n\to\mathrm{Fin}\,K$, and expectations are finite sums against it. The adversary and the experts are deterministic functions of past plays; an independent randomized adversary is a mixture of these. The examples of the Banditron are fixed.
• Argmax. $\hat y_t$ uses any argmax selector; all tie-breaking rules are covered.
• Norms. $\|x_t\| = 1$ is the Euclidean condition $\sum_j x_{t,j}^2 = 1$; $\|U\|$ is the Frobenius norm written out explicitly.
• Infima and maxima. Each "$\inf_U$" and "$\max_k$" of the book is stated as "for every $U$" or "for every $k$", which is equivalent.
• Explicit constants. Every bound is the one printed or, for the corrected items, the one the proof yields. No $O(\cdot)$ appears.
• Corrected misprints. Theorem 4.7 prints the examples in $\mathbb R^d\times\{-1,+1\}$; labels are in $\{1,\dots,K\}$. Theorem 4.2 prints $\sqrt{2nN\ln K}$ and $2\sqrt{nN\ln K}$; the proof gives $\sqrt{2nK\ln N}$ and $2\sqrt{nK\ln N}$. Theorem 4.3 prints $\eta = \sqrt{2\ln K/(nK)}$; (4.7) follows from the proof with $\eta = \sqrt{2\varepsilon\ln K/n}$.
• Parameter range. At $n = 8K$ the Banditron's $\gamma$ equals $1/2$, outside the box's open interval $(0,1/2)$. The proof uses only $\gamma\le 1/2$, so $n = 8K$ is included.
• Ruling out trivial forms. Theorem 4.1 is stated for the explicit S-Exp3 forecaster, not as an existence claim, so no forecaster tuned to the losses can witness it. The losses and the advice are allowed to adapt, so a proof for oblivious sequences does not suffice.
• Left out. Theorem 4.4 (Exp4 with mixing) is proved in the book only by reference. The argument that reference suggests yields $\tfrac32\gamma n + K\ln N/\gamma$, not the printed $\gamma n/2 + K\ln N/\gamma$. Theorem 4.5 is stated with $O(\cdot)$, Theorem 4.6 "for some constant $c$", and Eq. (4.8) is left to the reader.

Useful reusable infrastructure: the path-law expectation for history-dependent sampling, the exponential-weights potential argument under adaptive losses, and Perceptron-type inner-product arguments for matrices. Proofs of any milestone and of the goal are welcome.

Selected references

• S. Bubeck, N. Cesa-Bianchi, Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems, Foundations and Trends in Machine Learning 5(1), 2012. arXiv:1204.5721v2. https://arxiv.org/abs/1204.5721 ; https://doi.org/10.1561/2200000024
• S. M. Kakade, S. Shalev-Shwartz, A. Tewari, Efficient Bandit Algorithms for Online Multiclass Prediction, ICML 2008. https://doi.org/10.1145/1390156.1390212
• P. Auer, N. Cesa-Bianchi, Y. Freund, R. E. Schapire, The Nonstochastic Multiarmed Bandit Problem, SIAM Journal on Computing 32(1), 2002. https://doi.org/10.1137/S0097539701398375
• O.-A. Maillard, R. Munos, Adaptive Bandits: Towards the Best History-Dependent Strategy, AISTATS 2011. https://proceedings.mlr.press/v15/maillard11a.html

Motivation

In bandit convex optimization a forecaster repeatedly picks a point $x_t$ of a convex set $\mathcal K\subseteq\mathbb R^d$, and an adversary picks a convex loss $\ell_t$. The forecaster pays $\ell_t(x_t)$ and observes only that number: it never sees the function, its gradient, or its value elsewhere. This is the model of online optimization with only function-value access, as in tuning a system online from measured costs, dynamic pricing with an unknown convex demand-cost curve, or routing with path costs observed only on the route taken. The question is how fast the forecaster can approach the best fixed point in hindsight.

Chapter 6 of Bubeck and Cesa-Bianchi's monograph (arXiv:1204.5721v2, Foundations and Trends in Machine Learning 5(1), 2012) treats the problem through spherical gradient estimates fed to projected gradient descent. The one-point method is due to Flaxman, Kalai and McMahan (SODA 2005, arXiv:cs/0408007), who obtained an $\mathcal O(n^{3/4})$ regret bound. Agarwal, Dekel and Xiao (COLT 2010) showed that two function evaluations per round allow $\mathcal O(\sqrt n)$. Whether one-point feedback admits $\sqrt n$ regret was open when the monograph was written (p. 94); Bubeck, Eldan and Lee (STOC 2017, arXiv:1607.03084) later obtained $\sqrt n$ regret up to logarithmic and polynomial-in-$d$ factors for convex losses, with a different and much more involved algorithm.

Setting

Let $\mathbb B=\{x\in\mathbb R^d:\|x\|\le1\}$ be the closed Euclidean unit ball and $\mathbb S=\{x:\|x\|=1\}$ the unit sphere, with unnormalized spherical measure $\sigma$, so that $\sigma(\mathbb S)=d\,\mathrm{Vol}(\mathbb B)$. Fix $\delta>0$. For a loss $\ell$, the smoothed loss is $\widetilde\ell(x)=\mathbb E\,\ell(x+\delta B)$ with $B$ uniform on $\mathbb B$.

The set $\mathcal K$ is closed and convex with $r\mathbb B\subseteq\mathcal K\subseteq R\mathbb B$. The losses $\ell_1,\ell_2,\dots:\mathbb R^d\to\mathbb R$ are $G$-Lipschitz, differentiable and convex, and are fixed before the game (an oblivious adversary).

OSGD (Online Stochastic Gradient Descent) on a set $\mathcal K'$ with learning rate $\eta$ starts at $x_1=0$ and sets $x_{t+1}=\operatorname{argmin}_{y\in\mathcal K'}\|y-(x_t-\eta\widetilde g_t(x_t))\|$, where $\widetilde g_t$ is a gradient estimate. With $S_1,S_2,\dots$ independent and uniform on $\mathbb S$:

• the two-point estimate (6.1) is $\widetilde g_t(x_t)=\frac d{2\delta}\big(\ell_t(X_t^+)-\ell_t(X_t^-)\big)S_t$ with $X_t^\pm=x_t\pm\delta S_t$; the played point is $X_t^+$ or $X_t^-$ by a fair coin;
• the one-point estimate (6.3) is $\widetilde g_t(x_t)=\frac d\delta\,\ell_t(\widetilde X_t)S_t$ with played point $\widetilde X_t=x_t+\delta S_t$.

OSGD runs on the shrunken set $\mathcal K'=(1-\delta/r)\mathcal K$, so that the perturbed points stay in $\mathcal K$. The pseudo-regret is

$$\overline R_n=\mathbb E\sum_{t=1}^n\ell_t(\widetilde X_t)-\min_{x\in\mathcal K}\sum_{t=1}^n\ell_t(x).$$

Formalization targets

Goal: Theorem 6.2, tuned

If in addition $|\ell_t|\le L$ on $\mathcal K$, and $\delta=(2n)^{-1/4}\sqrt{RdL/((3+R/r)G)}$, $\eta=(2n)^{-3/4}\sqrt{R^3/(dL(3+R/r)G)}$, then one-point OSGD satisfies

$$\overline R_n\le 4n^{3/4}\sqrt{RdL\,(3+R/r)\,G}.$$

Milestones

1. Lemma 6.1: $\nabla\int_{\mathbb B}\ell(x+\delta b)\,db=\frac1\delta\int_{\mathbb S}\ell(x+\delta s)s\,d\sigma(s)$.
2. Lemma 6.2: $\frac d\delta\mathbb E[\ell(x+\delta S)S]=\nabla\mathbb E\,\ell(x+\delta B)$.
3. Eq. (6.2): $|\ell(x)-\widetilde\ell(x)|\le\delta G$.
4. Lemma 6.3: the queried points' regret against $x$ is at most the smoothed regret of the iterates against $(1-\xi)x$, plus $3\delta Gn+\xi GRn$.
5. Theorem 6.1: two-point OSGD has $\overline R_n\le R^2/\eta+\eta(Gd)^2n+\delta(3+R/r)Gn$, and $\overline R_n\le 2RGd\sqrt n+\delta(3+R/r)Gn$ for $\eta=R/(Gd\sqrt n)$.
6. Theorem 6.2, first display: one-point OSGD has $\overline R_n\le R^2/\eta+\frac{(dL)^2}{\delta^2}\eta n+\delta(3+R/r)Gn$ for every $0<\delta\le r$ and $\eta>0$.

Significance

The $n^{3/4}$ bound shows that a single function value per round suffices for sublinear regret against any oblivious sequence of Lipschitz convex losses, with a forecaster whose only operations are a random perturbation and a Euclidean projection. The smoothing identity of Lemmas 6.1–6.2 is the basic tool of zeroth-order (derivative-free) optimization, used well beyond bandits, and Theorem 6.1 is the $\sqrt n$ benchmark for two-point methods.

All results are proved in the source. To the best of current knowledge none is formalized: the related items of the Introduction to Online Convex Optimization series on Prove2Me (Hazan's Lemma 6.7 and Theorem 6.9) were formalized with missing hypotheses and are recorded as disproved. This mission produces machine-checked statements with every hypothesis explicit, and the formal infrastructure (sphere measure calculus, a projected stochastic gradient analysis) for later zeroth-order results.

Difficulty

Two steps resist a direct formal treatment. First, Lemma 6.1 is a divergence-theorem identity on the ball; Mathlib has the sphere measure and polar coordinates, but its divergence theorem covers boxes rather than balls, so differentiating the ball average in $x$ requires either such a theorem or a direct argument about translates of the ball. Second, the regret analysis takes expectations of quantities that depend on the whole past: the iterate $x_t$ is a function of $S_1,\dots,S_{t-1}$, and unbiasedness $\mathbb E[\widetilde g_t\mid x_t]=\nabla\widetilde\ell_t(x_t)$ holds only conditionally, via independence of $S_t$ from the past. A pathwise gradient-descent inequality must be combined with this conditional expectation round by round, with measurability of the projected iterates established along the way. The naive approach of treating the estimate as the true gradient of $\ell_t$ fails: it is a gradient of $\widetilde\ell_t$, and the gap is handled only by Eq. (6.2) and Lemma 6.3.

Formalization scope

Points are in EuclideanSpace ℝ (Fin d) with $d\ge1$; rounds are $t=1,2,\dots$, sums run over Finset.Icc 1 n. $\sigma$ is Mathlib's Measure.toSphere of Lebesgue measure; the uniform laws are normalized restrictions. Randomness lives on an arbitrary probability space; the directions $S_t$ are measurable, mutually independent (iIndepFun) and uniform on $\mathbb S$, and in Theorem 6.1 the pairs $(S_t,C_t)$ are independent with $C_t$ a fair sign independent of $S_t$. A run of OSGD is a predicate (start at $0$, each iterate a Euclidean projection onto $(1-\delta/r)\mathcal K$), which determines the run uniquely, so the forecaster uses only observed values and its own randomness. The losses are Lipschitz, differentiable and convex on all of $\mathbb R^d$; the bound $|\ell_t|\le L$ is on $\mathcal K$, because a convex function bounded on $\mathbb R^d$ is constant. The minimum over $\mathcal K$ is an infimum over the subtype $\mathcal K$, attained in every theorem.

Conventions and corrections, each stated in the item's Formalization Note:

• Lemma 6.1 carries the factor $1/\delta$ that the printed statement omits and the proof contains (corrected misprint).
• Theorem 6.1's second display prints $\eta=R/(GD\sqrt n)$ and a limit "for $\delta\to0$"; the item states $\overline R_n\le 2RGd\sqrt n+\delta(3+R/r)Gn$ for $\eta=R/(Gd\sqrt n)$ and every admissible $\delta$, which implies the limit (corrected misprint).
• Theorems 6.1 and 6.2 add $0<\delta\le r$, which the proofs need for $X_t^\pm,\widetilde X_t\in\mathcal K$; for the tuned $\delta$ of the goal it is a condition on $n$.
• The goal adds $G,L>0$ and $n\ge1$, which its formulas for $\delta,\eta$ need; the constant $4$ is the book's rounding of $2\cdot2^{3/4}$ and is kept, as is the form $R^2/\eta$.

The statements cannot be satisfied trivially: the run is pinned by its recursion, the losses are fixed before the randomness, the expectations are of bounded measurable functions (no zero-valued Bochner integrals), and the minimum is over the nonempty compact $\mathcal K$. Section 6.3 (Lemma 6.4, Theorem 6.3) is not included, because its algorithm box and proof use different stage lengths and its unimodality condition is stated on a smaller set than the proof uses.

Needed infrastructure: calculus of ball averages and sphere integrals, symmetry of the uniform sphere law, nonexpansiveness of projections onto closed convex sets, and conditional-expectation bookkeeping for adapted iterates. Each is reusable for zeroth-order optimization; contributions of any of them as separate lemmas are welcome.

Selected references

• S. Bubeck, N. Cesa-Bianchi, Regret Analysis of Stochastic and Nonstochastic Multi-armed Bandit Problems, Foundations and Trends in Machine Learning 5(1), 2012. arXiv:1204.5721v2, doi:10.1561/2200000024
• A. Flaxman, A. Kalai, H. B. McMahan, Online convex optimization in the bandit setting: gradient descent without a gradient, SODA 2005. arXiv:cs/0408007
• A. Agarwal, O. Dekel, L. Xiao, Optimal algorithms for online convex optimization with multi-point bandit feedback, COLT 2010. link
• S. Bubeck, R. Eldan, Y. T. Lee, Kernel-based methods for bandit convex optimization, STOC 2017. arXiv:1607.03084