Machine Learning

Why stability bounds

A learning algorithm is judged by its generalization error, its expected loss on a fresh example, which cannot be computed because the data distribution is unknown. Practitioners estimate it either by the empirical error on the training set or by the leave-one-out error, which retrains the algorithm once per example. Classical learning theory justifies these estimates through uniform convergence over the whole hypothesis space (VC dimension, covering numbers). That route says nothing useful about algorithms such as nearest-neighbour rules or regularized kernel methods, whose effective hypothesis space is huge or unknown.

An alternative is to bound the deviation through a property of the algorithm itself: how much its output changes when one training example is removed. This idea goes back to Rogers and Wagner (1978) and Devroye and Wagner (1979) for local rules, and Kearns and Ron (1999) gave it a name. Bousquet and Elisseeff (JMLR 2002) systematized it with several stability notions and corresponding bounds; their paper is the standard reference for algorithmic stability in learning theory. This mission formalizes its first family of results, the polynomial bounds of §4.1.

Setting

Let $Z = X \times Y$ and let $D$ be a probability distribution on $Z$. A training set $S = \{z_1, \dots, z_m\}$ consists of $m$ examples drawn i.i.d. from $D$. A learning algorithm $A$ maps a training set $S$ to a hypothesis $A_S : X \to Y'$; it is deterministic and symmetric, meaning it does not depend on the order of the examples. A cost $c$ with $0 \le c(y', y) \le M$ defines the loss $\ell(f, z) = c(f(x), y)$ of a hypothesis $f$ at $z = (x, y)$.

For each index $i$, $S^{\setminus i}$ is $S$ with $z_i$ removed, and $S^i$ is $S$ with $z_i$ replaced by an independent fresh draw $z'_i \sim D$. The three error quantities are

Two stability notions (Definitions 3 and 4) control them. $A$ has hypothesis stability $\beta_1$ if $\mathbb E_{S,z}[|\ell(A_S,z) - \ell(A_{S^{\setminus i}},z)|] \le \beta_1$ for every $i$, and pointwise hypothesis stability $\beta_2$ if $\mathbb E_{S}[|\ell(A_S,z_i) - \ell(A_{S^{\setminus i}},z_i)|] \le \beta_2$ for every $i$.

Formalization targets

Goal: Theorem 11

For $m \ge 1$, under hypothesis stability $\beta_1$ and pointwise hypothesis stability $\beta_2$, for every $\delta > 0$, each of the following holds with probability at least $1 - \delta$ over $S \sim D^m$:

Milestones

1. Lemma 25 (p. 520), a generalized Rogers–Wagner identity: upper bounds on $\mathbb E_S[(R - R_{\mathrm{emp}})^2]$ and $\mathbb E_S[(R - R_{\mathrm{loo}})^2]$ by correlations of the loss.
2. Lemma 9, (8) and (9) (p. 505): $\mathbb E_S[(R - R_{\mathrm{emp}})^2] \le \frac{M^2}{2m} + 3M\,\mathbb E_{S,z'_i}[|\ell(A_S,z_i) - \ell(A_{S^i},z_i)|]$ and $\mathbb E_S[(R - R_{\mathrm{loo}})^2] \le \frac{M^2}{2m} + 3M\,\mathbb E_{S,z}[|\ell(A_S,z) - \ell(A_{S^{\setminus i}},z)|]$.
3. The replace-one term (proof of Theorem 11): $\mathbb E_{S,z'_i}[|\ell(A_S,z_i) - \ell(A_{S^i},z_i)|] \le \beta_1 + \beta_2$.
4. The second-moment bounds (proof of Theorem 11): $\mathbb E_S[(R - R_{\mathrm{emp}})^2] \le \frac{M^2}{2m} + 3M(\beta_1+\beta_2)$ and $\mathbb E_S[(R - R_{\mathrm{loo}})^2] \le \frac{M^2}{2m} + 3M\beta_1$.

Significance

Theorem 11 is the weakest-assumption bound in the paper: it requires only average-case stability, not the uniform (worst-case) stability behind the exponential bounds of §4.2. It shows that both the resubstitution and the deleted estimate are within $O(1/\sqrt{m\delta})$ of the risk whenever the stability parameters decay like $1/m$, with no reference to the size of the hypothesis class. It also extends Devroye and Wagner's leave-one-out analysis for classification to bounded regression losses and to the empirical estimator. Later work on average stability and on generalization of stochastic gradient methods (for example Hardt, Recht and Singer, 2016) starts from these notions.

The result is proved in the paper; as far as is known it has no machine-checked proof. A formal development has two concrete payoffs. First, it fixes the constants: in checking the argument, two printed slips were found (the empirical constant in Theorem 11 and the third term of Lemma 25's first inequality), and the formal statements record the versions that the paper's proof actually establishes. Second, the Lemma 25 and Lemma 9 machinery — exchangeability of i.i.d. samples under renaming, and second-moment control through stability — is reusable for any later stability result.

Difficulty

The obvious route is the Efron–Stein (Steele) variance inequality, Theorem 1 of the paper. It bounds the variance of $R - R_{\mathrm{emp}}$, not its second moment, and leaves the bias to be handled separately; the paper notes that it gives worse constants. The direct route of Appendix A instead expands $\mathbb E_S[(R - R_{\mathrm{emp}})^2]$ and rewrites each correlation term by renaming i.i.d. variables: training points, fresh test points and replacement points are exchanged with one another, and the algorithm is retrained on sets $T \cup \{z, z'\}$ with $T = S^{\setminus \{i,j\}}$. Every renaming is a measure-preserving map on a product of $m + 2$ copies of $D$, and each must be justified by the symmetry of $A$. Doing this rigorously, rather than as "a matter of renaming", is the core of the work. The leave-one-out case is only sketched in the paper ("it is easy to see"), so its formal proof has to be reconstructed.

Formalization scope

• An algorithm is a function Multiset (X × Y) → (X → Y'). Symmetry in the training set is built into the type, and the same algorithm acts on sets of every size, as $S$ and $S^{\setminus i}$ require. A sample is S : Fin m → X × Y with law $D^m$ (Measure.pi); fresh points $z$, $z'$, $z'_i$ are further independent coordinates, via product measures $D^m \otimes D$ and $(D^m \otimes D) \otimes D$.
• The loss, empirical error and generalization error are the published FoundationsML.Stability definitions (Loss, EmpiricalError, GeneralizationError).
• The cost satisfies $0 \le c \le M$ everywhere. The paper's assumption that "all functions are measurable" becomes one hypothesis: for every $n$, $(S, z) \mapsto \ell(A_S, z)$ is measurable on $(X \times Y)^n \times (X \times Y)$. Both stability definitions also require their integrands to be integrable. Together these rule out the trivializing reading in which a non-integrable expectation equals Lean's default value $0$ and the stability hypotheses hold vacuously.
• "With probability $1 - \delta$" is stated as a bound on the failure event: $D^m\{S : R > R_{\mathrm{emp}} + \cdots\} \le \delta$ for every $\delta > 0$, separately for each estimator.
• $m \ge 2$ is assumed in Lemmas 9 and 25 and in the two second-moment steps of the proof, because the lemmas refer to two distinct indices. Theorem 11 itself is stated for every $m \ge 1$, as printed.
• Corrected statements. (i) Theorem 11's empirical bound is stated with $6Mm(\beta_1+\beta_2)$, not the printed $12Mm\beta_2$: the proof bounds a hypothesis-stability term by $\beta_2$ when it is bounded by $\beta_1$. The two coincide when $\beta_1 = \beta_2$. Accordingly the replace-one milestone is stated as $\le \beta_1 + \beta_2$ (printed $2\beta_2$), and the empirical second-moment bound as $\frac{M^2}{2m} + 3M(\beta_1+\beta_2)$ (printed $6M\beta_2$). (ii) Lemma 25's empirical inequality has $\mathbb E_S[\ell(A_S,z_i)\ell(A_S,z_j)]$ as its third term, as its proof gives, not the printed leave-one-out term. (iii) The leave-one-out second-moment bound follows from (9), not from (10) as printed.

Contributions are welcome at every level: proofs of the milestones, a general exchangeability lemma for symmetric algorithms on product measures, and Markov/Chebyshev glue for the final step.

Selected references

• O. Bousquet and A. Elisseeff, Stability and Generalization, Journal of Machine Learning Research 2 (2002), 499–526. https://www.jmlr.org/papers/v2/bousquet02a.html
• W. H. Rogers and T. J. Wagner, A finite sample distribution-free performance bound for local discrimination rules, Annals of Statistics 6(3) (1978), 506–514. https://doi.org/10.1214/aos/1176344196
• L. Devroye and T. J. Wagner, Distribution-free performance bounds for potential function rules, IEEE Transactions on Information Theory 25(5) (1979), 601–604. https://doi.org/10.1109/TIT.1979.1056087
• M. Kearns and D. Ron, Algorithmic stability and sanity-check bounds for leave-one-out cross-validation, Neural Computation 11(6) (1999), 1427–1453. https://doi.org/10.1162/089976699300016304
• M. Hardt, B. Recht and Y. Singer, Train faster, generalize better: stability of stochastic gradient descent, ICML 2016. https://arxiv.org/abs/1509.01240

Motivation

Learning from a finite sample is useful only if changing the sample has a controlled effect on the learned predictor. Uniform stability asks for a bound on the change in loss at every test point when one training example is removed. Bousquet and Elisseeff use this property to obtain generalization bounds for learning algorithms, and identify regularization as a source of stability in methods built from reproducing kernels. The present mission isolates their result for a squared norm penalty in a reproducing kernel Hilbert space (RKHS). It concerns the sensitivity of the optimizer itself, before any probability bound on a random training sample is applied. The result is Theorem 22 of Bousquet and Elisseeff (2002).

Setting

Let $X$ be an input space, $Y$ a label space, and $H$ a real reproducing kernel Hilbert space of real-valued predictors on $X$. A kernel $K:X\times X\to\mathbb R$ and a feature representative $\Phi(x)\in H$ express the reproducing identity $f(x)=\langle f,\Phi(x)\rangle_H$ and $K(x,x')=\langle\Phi(x),\Phi(x')\rangle_H$. Thus $K(x,x)=\|\Phi(x)\|_H^2$. The source assumes that all diagonal kernel values satisfy $K(x,x)\le\kappa^2$.

A labeled example is $z=(x,y)\in X\times Y$. Its loss under $f$ is $\ell(f,z)=c(f(x),y)$, where $c$ is a real-valued cost. Let $D_H$ be the set of predictions that some element of $H$ can produce at some input. The loss is $\sigma$-admissible when $c(\cdot,y)$ is convex for every label $y$ and $|c(a,y)-c(b,y)|\le\sigma|a-b|$ for all $a,b\in D_H$ and $y\in Y$. Here $\sigma$ is a nonnegative Lipschitz constant. The definition compares any two attainable predictions, even when they arise at different inputs.

Fix a sample $S=(z_1,\ldots,z_m)$, a deleted index $i$, and a regularization weight $\lambda>0$. The paper's full and truncated objectives, with squared RKHS norm regularization, are

The factor in both objectives is $1/m$. Let $f$ and $f^{\setminus i}$ be minimizers of these respective objectives over all of $H$. The statements allow any minimizer satisfying the relevant global optimality condition; they do not choose one by an arbitrary fallback rule.

Formalization targets

The central target is the explicit deletion stability estimate of Theorem 22. For every test point $z\in X\times Y$,

Its four milestones follow the paper's route through Lemma 20, the point-evaluation inequality (25), and the two quantitative inequalities displayed in the proof of Theorem 22. In particular, the intermediate RKHS distance bound is $\|f^{\setminus i}-f\|_H\le\kappa\sigma/(2\lambda m)$ when $\kappa\ge0$. The main theorem uses $\kappa^2$, so it does not need a choice of sign for $\kappa$. These numerical constants are part of the target, rather than placeholders for unspecified bounds.

Significance

The theorem supplies a deterministic, uniform sensitivity estimate for kernel methods trained by squared norm regularization. The bound applies simultaneously to every test example and decreases as either the sample size or the regularization weight increases. It is one of the ingredients that lets the paper apply its earlier stability-to-generalization results to concrete learning procedures. The loss need not be bounded for this theorem; bounding it is a separate question addressed later in the paper.

The result is proved in the source article. This mission asks for a machine-checked version of its exact pairwise claim and the reusable infrastructure around it: the paper's admissibility condition, the two objectives, the general regularizer inequality, and the RKHS evaluation bound. The existing Prove2Me library already has definitions for loss, empirical error, and the RKHS reproducing identity, so the new definitions concentrate on what is specific to these pages. The related replace-one estimate in Mohri, Rostamizadeh and Talwalkar's Foundations of Machine Learning uses a different perturbation and constant; it is not interchangeable with this result.

Difficulty

The two minimizers solve different objectives, and the deleted example appears in only one of them. A comparison of their objective values alone does not directly give a bound on their distance in the Hilbert norm. The source also distinguishes an abstract convex class of functions in Lemma 20 from the full RKHS used in Theorem 22. A proof must keep those domains straight while preserving the precise normalization of the truncated objective. Another delicate point is that the kernel bound controls evaluations through the reproducing identity; a bound on $K(x,x)$ is not by itself a bound on loss unless the admissibility condition is also used.

Formalization scope

The Lean model uses an abstract complete real inner product space $H$, an evaluation map $\operatorname{ev}:H\to(X\to\mathbb R)$, a feature map $\Phi:X\to H$, and the published IsRKHSOf predicate tying these to $K$. The completeness instance matches the source's Hilbert-space assumption. Samples have type Fin m → X × Y, so an index i : Fin m already forces $m\ge1$. Minimization ranges over the entire $H$ for Theorem 22 and over the declared convex class for Lemma 20. The objective definitions use the published Loss and EmpiricalError objects. No probability measure or measurability assumption is needed for these deterministic assertions.

There is a printed mismatch that affects what “deletion” means. Theorem 22 names an algorithm defined by equation (26), which, run afresh on $m-1$ points, would normalize its data term by $1/(m-1)$. Lemma 20 and the proof of Theorem 22 instead compare the full objective with equation (20), whose data term uses $1/m$. The formalized goal states that comparison, with its explicit constant, and records the discrepancy for audit. This excludes the tempting shortcut of treating the two normalizations as identical. The regularizer is the genuine squared norm and the second minimizer is required to minimize the genuine truncated objective; neither a restricted hypothesis ball nor an artificially assumed distance bound enters the goal. Contributions that establish minimizer existence or connect the pairwise bound to an algorithmic selection would extend this core without changing its statement.

Selected references

• Olivier Bousquet and André Elisseeff, Stability and Generalization, Journal of Machine Learning Research 2 (2002), 499–526. Article and PDF.
• Mehryar Mohri, Afshin Rostamizadeh, and Ameet Talwalkar, Foundations of Machine Learning, second edition, MIT Press, 2018, Chapter 14. Book information.

Motivation

Eligibility traces are one of the basic mechanisms of reinforcement learning. A trace is a short-term memory vector $z_t$ with one component per weight. It records which components contributed to recent value estimates, so that an error observed now can be credited to the right components without storing the past. Chapter 12 of Sutton and Barto's Reinforcement Learning: An Introduction (2nd ed., 2018) organizes the topic around two ways of describing an algorithm. A forward view updates each state toward a target built from rewards that arrive later. A backward view makes an update at every step from the current error and the trace.

The chapter proves one exact equivalence between the two views itself, in §12.6: "This is the only equivalence of forward- and backward-views that we explicitly demonstrate in this book" (p. 301). The setting is linear Monte Carlo prediction, and the backward view uses a dutch trace. The same trace appears in true online TD($\lambda$), whose exact equivalence to the online $\lambda$-return algorithm (van Seijen and Sutton, 2014; van Seijen et al., 2016) the book cites without proof. Of that proof, §12.6 "gives some of the flavor ... but is much simpler" (p. 301).

The older equivalence of §§12.1–12.2 goes back to Sutton (1988). If the weights are held fixed during an episode, the summed updates of TD($\lambda$) with accumulating traces equal the summed updates of the off-line $\lambda$-return algorithm. The book leaves it as Exercises 12.3–12.4.

Setting

Fix a dimension $d$, a step size $\alpha$ and an episode of length $T \ge 1$ with feature vectors $x_0, \dots, x_{T-1} \in \mathbb R^d$. The episode ends with a single return $G \in \mathbb R$ ("a single reward received at the end of the episode ... and ... no discounting", p. 301). The forward view is the linear gradient Monte Carlo, or LMS, rule (12.13): from an initial $w_0$,

Let $F_t = I - \alpha x_t x_t^\top$ be the fading matrix. The backward view keeps two vectors that are updated at each step in $O(d)$ time without knowledge of $G$. The dutch trace is $z_0 = x_0$, $z_t = z_{t-1} + (1 - \alpha z_{t-1}^\top x_t)\,x_t$. The auxiliary vector is $a_t = a_{t-1} - \alpha x_t x_t^\top a_{t-1}$, with $a_0 = F_0 w_0$.

For the second part, an episode $S_0, R_1, S_1, \dots, R_T, S_T$ carries states and rewards, and $\hat v(s, w)$ is a differentiable value function with $\hat v(\text{terminal}, \cdot) = 0$. For one fixed weight vector $w$, define the following, with $\gamma \in [0,1]$ and $\lambda \in [0,1)$:

• the return $G_t$;
• the $n$-step return $G_{t:t+n}$ (12.1), with $G_{t:t+n} = G_t$ once $t + n \ge T$;
• the $\lambda$-return $G^\lambda_t = (1-\lambda)\sum_{n \ge 1}\lambda^{n-1} G_{t:t+n}$ (12.2);
• the TD error $\delta_t = R_{t+1} + \gamma\hat v(S_{t+1}, w) - \hat v(S_t, w)$ (12.6);
• the accumulating trace $z_{-1} = 0$, $z_t = \gamma\lambda z_{t-1} + \nabla\hat v(S_t, w)$ (12.5).

Formalization targets

Goal: the dutch-trace equivalence (12.14), corrected

The left side is the forward view after $T$ LMS updates. On the right, $a_{T-1}$ and $z_{T-1}$ are produced by the incremental recursions above. The goal is about the two algorithms, not only about the closed-form product identity.

Milestones on the goal's path (§12.6, p. 302)

1. $w_{t+1} = F_t w_t + \alpha G x_t$.
2. $w_T = F_{T-1}\cdots F_0 w_0 + \alpha G \sum_{k=0}^{T-1} F_{T-1}\cdots F_{k+1} x_k$, the first line of (12.14).
3. $z_t = \sum_{k=0}^{t} F_t \cdots F_{k+1} x_k$ for the dutch-trace recursion.
4. $a_t = F_t \cdots F_0 w_0$ for the auxiliary-vector recursion (corrected initialization).

Milestones on the $\lambda$-return (§§12.1–12.2)

5. (12.3): $G^\lambda_t = (1-\lambda)\sum_{n=1}^{T-t-1}\lambda^{n-1}G_{t:t+n} + \lambda^{T-t-1}G_t$ for $t < T$.
6. Exercise 12.1: $G^\lambda_t = R_{t+1} + \gamma[(1-\lambda)\hat v(S_{t+1}, w) + \lambda G^\lambda_{t+1}]$.
7. Exercise 12.3: $G^\lambda_t - \hat v(S_t, w) = \sum_{k=t}^{T-1}(\gamma\lambda)^{k-t}\delta_k$.
8. Exercise 12.4: $\sum_{t<T}\alpha\delta_t z_t = \sum_{t<T}\alpha[G^\lambda_t - \hat v(S_t, w)]\nabla\hat v(S_t, w)$.

Significance

The goal says that an $O(d)$-per-step algorithm reproduces the Monte Carlo/LMS result exactly. That algorithm never stores the feature vectors or the $T$ intermediate weight vectors. The book draws the conclusion that eligibility traces "are not specific to TD learning at all" (p. 303). The dutch trace in the case $\gamma\lambda = 1$ is the same object that true online TD($\lambda$) (12.11) uses for general $\gamma\lambda$. The fading-matrix products and their incremental forms are therefore the vocabulary of any later formalization of true online TD($\lambda$) and of the online $\lambda$-return algorithm.

Exercises 12.3–12.4 are the fixed-weight equivalence of TD($\lambda$) and the off-line $\lambda$-return algorithm. They are the standard justification for calling TD($\lambda$) an approximation of the $\lambda$-return algorithm. Exercise 12.1 and (12.3) are the identities the rest of the chapter uses to manipulate $\lambda$-returns.

On status: all of these results are known and elementary on paper, and the book prints the derivation of (12.14). To our knowledge none of them has a machine-checked proof, and the platform has no statement about $\lambda$-returns, eligibility traces or TD($\lambda$). What this mission adds is formal statements with every convention fixed, including one correction to the printed text. It also adds reusable definitions of $n$-step returns, $\lambda$-returns and traces.

Difficulty

The algebra is elementary. The difficulty lies in the conventions, and a careless reading of the page produces a false statement. The book initializes $a_0 = w_0$, and taken literally that makes the goal false. The $\lambda$-return is an infinite series, whose tail collapses only because every $n$-step return that reaches past termination equals the full return. That convention has to be built into the definition of $G_{t:t+n}$, together with the terminal value $\hat v(\text{terminal}, \cdot) = 0$. Exercises 12.3 and 12.4 are true only when the weights stay fixed. With the algorithms' changing weights $w_t$ the $n$-step returns (12.1) use $w_{t+n-1}$, and neither identity holds. The boundary indices ($t = T-1$, the empty product at $k = T-1$, $G^\lambda_T = 0$) must come out right.

Formalization scope

Namespace SuttonBartoRL.Traces. Vectors of §12.6 are Fin d → ℝ, matrices Matrix (Fin d) (Fin d) ℝ, and $x x^\top$ is Matrix.vecMulVec x x. The ordered product fadeProd α x j t is $F_t \cdots F_j$, the identity when $t < j$. Feature sequences are indexed by $\mathbb N$; only $x_0, \dots, x_{T-1}$ enter. $T \ge 1$ is a hypothesis wherever $T - 1$ appears. The identities of §12.6 are stated for every real $\alpha$ and $G$, a harmless strengthening of the book's positive step size.

For §§12.1–12.2, weights are EuclideanSpace ℝ (Fin d), $\nabla$ is Mathlib's gradient, and each $\hat v(s,\cdot)$ is assumed differentiable in Exercise 12.4. An episode is a length $T$, states and rewards. The value at time $t \ge T$ is $0$. (12.2) is a tsum over $n \ge 0$ of $\lambda^n G_{t:t+n+1}$, and $\lambda \in [0,1)$, the range the book gives with (12.2). Milestone 5 concludes summability, so the junk value of a divergent tsum cannot make it trivial. Exercises 12.3–12.4 take one weight binder w, used in every return, TD error and gradient. That is the book's fixed-$w$ assumption, stated in the binders.

Correction. The printed initialization $a_0 = w_0$ (p. 302) contradicts the printed definition $a_t \doteq F_t\cdots F_0 w_0$ and (12.14). The counterexample is $d = 1$, $T = 1$, $x_0 = 1$, $\alpha = 1/2$, $w_0 = 1$, $G = 0$: the forward view gives $w_1 = 1/2$, while $a_0 + \alpha G z_0 = 1$. The mission states the corrected result with $a_0 = F_0 w_0$, equivalently the same recursion started from $a_{-1} = w_0$. The printed text is kept verbatim in the milestone.

A trivializing formalization is ruled out: the goal is not the closed-form identity with $a_{T-1}$ and $z_{T-1}$ defined as the products and sums. Those vectors are defined by their $G$-free incremental recursions, and the closed forms are separate milestones.

Out of scope: the equivalence of true online TD($\lambda$) and the online $\lambda$-return algorithm (cited, p. 300), the truncated-return identity (12.10), the error bound (12.8), and all convergence claims. Proofs of the milestones, and reuse of the definitions in later missions on true online TD($\lambda$), are welcome.

Selected references

• R. S. Sutton and A. G. Barto, Reinforcement Learning: An Introduction, 2nd ed., MIT Press, 2018, ISBN 9780262039246, Chapter 12, pp. 287–320. http://incompleteideas.net/book/the-book-2nd.html
• R. S. Sutton, "Learning to predict by the methods of temporal differences", Machine Learning 3 (1988), 9–44. https://doi.org/10.1007/BF00115009
• H. van Seijen and R. S. Sutton, "True online TD(λ)", Proceedings of ICML 2014, PMLR 32, 692–700. https://proceedings.mlr.press/v32/seijen14.html
• H. van Seijen, A. R. Mahmood, P. M. Pilarski, M. C. Machado and R. S. Sutton, "True online temporal-difference learning", Journal of Machine Learning Research 17 (2016), 1–40. https://jmlr.org/papers/v17/15-599.html

Motivation

An agent learning to control an unknown environment must balance rewards it can collect now against information that improves later decisions. In a finite Markov decision process (MDP), every action changes the distribution of the next state, so a mistaken transition estimate can affect decisions many steps later. Regret measures this loss against a policy that already knows the transition probabilities. The paper of Azar, Osband and Munos gives high-probability regret bounds for two variants of upper confidence bound value iteration (UCBVI) in finite-horizon reinforcement learning. This mission targets its Chernoff–Hoeffding variant, UCBVI-CH, whose bonus depends only on the horizon and the visit count. Theorem 1 improves the paper's cited earlier dependence on the number of states from $S$ to $\sqrt S$ in the leading term for sufficiently many interactions. Azar, Osband and Munos, 2017, pp. 2, 4–5.

The paper was released in 2017 alongside work on the attainable dependence of episodic regret on the horizon $H$, state count $S$, action count $A$, and total interaction time $T$. Its second algorithm, UCBVI-BF, uses a variance-dependent bonus and is the subject of the next mission in this series. UCBVI-CH has a simpler bonus and its own explicit bound, making it a distinct mathematical target. Azar, Osband and Munos, 2017, pp. 1–5.

Setting

The state set $\mathcal S$ and action set $\mathcal A$ are finite and nonempty, with cardinalities $S$ and $A$. A stationary transition kernel $P(y\mid x,a)$ gives the probability of moving to state $y$ after action $a$ in state $x$; each row is nonnegative and sums to one. The known, deterministic reward $R(x,a)$ lies in $[0,1]$. An episode lasts $H\ge1$ steps. The environment chooses its starting state $x_{k,1}$ before episode $k$ and may base that choice on earlier episodes. It cannot see the current episode's future random draws. Azar, Osband and Munos, 2017, §2 and Assumption 1, pp. 2–3.

A policy $\pi$ selects an action from the current state and the step number. Its value $V_h^\pi(x)$ is the expected sum of rewards from step $h$ through step $H$ when starting in state $x$. The terminal value is $V_{H+1}^\pi=0$, and $V_h^*(x)$ is the maximum of $V_h^\pi(x)$ over all such policies. Since the state, action and step sets are finite, this maximum is over a finite nonempty policy class. The paper's sentence describing $H-h$ rewards uses a shifted terminal convention; this series follows the $H$ reward steps of Algorithms 1–2. Azar, Osband and Munos, 2017, pp. 3–4.

At the start of episode $k$, UCBVI-CH forms visit counts $N_k(x,a,y)$ and $N_k(x,a)$ from earlier completed transitions. On a visited pair it uses the empirical row $\widehat P_k(y\mid x,a)=N_k(x,a,y)/N_k(x,a)$. Algorithm 2 computes values backward from zero at the terminal step. For a visited pair, $Q_{k,h}(x,a)$ is the minimum of the preceding episode's $Q_{k-1,h}(x,a)$, $H$, and the empirical Bellman value plus Algorithm 3's bonus. For an unvisited pair, $Q_{k,h}(x,a)=H$. A maximizing action is chosen at every state, including states outside the realized path. Azar, Osband and Munos, 2017, Algorithms 1–3, pp. 3–4.

Formalization targets

Theorem 1: UCBVI-CH regret

For $K$ episodes and $T=KH$, regret sums the gap $V_1^*(x_{k,1})-V_1^{\pi_k}(x_{k,1})$. The goal is the paper's printed bound, with its constants:

Algorithm 3 itself uses $L_{\rm alg}=\ln(5SAT/\delta)$ in its bonus $7HL_{\rm alg}/\sqrt{N_k(x,a)}$. Both logarithms remain as printed. The probability is over the MDP's next-state draws, for every admissible starting-state rule and every way of breaking ties between maximizing actions. Azar, Osband and Munos, 2017, Algorithm 3, p. 4; Theorem 1, p. 5.

Supporting results

Four milestones retain the source's indexed attack path: the Bernstein bound (9) for the empirical value error, the count-deviation display before (11), Lemma 18 on optimism, and the weighted recursion displayed in the proof of Lemma 3. The last milestone preserves the signed weights that appear before the paper's final simplification. Azar, Osband and Munos, 2017, pp. 17, 20–21, 28.

Significance

Theorem 1 gives a finite-sample failure probability with explicit dependence on $H,S,A,K$ and $\delta$. It covers a learner whose initial state can change between episodes, a feature that matters in episodic learning where the experimenter does not fix a single starting distribution. For the regime stated after Theorem 1, the leading rate is $\widetilde O(H\sqrt{SAT})$. This is a result claimed by the paper; the present Lean declarations are open proof targets, not machine-checked proofs of that claim. Azar, Osband and Munos, 2017, p. 5.

Formalizing the result creates reusable finite objects for adaptive interaction: a constructed probability law on complete paths, empirical transition counts pooled across steps, a policy value defined by its expected reward, and confidence events with their domains stated explicitly. The concentration and optimism milestones can then be investigated independently of the final regret bound. The later UCBVI-BF mission uses the same paper's model with a different bonus. Azar, Osband and Munos, 2017, pp. 3–5, 14–17.

Difficulty

The visit count $N_k(x,a)$ is random and depends on earlier observations and decisions. A concentration inequality for a predetermined number of samples therefore does not immediately give a statement that holds at every episode start. The algorithm also reuses the previous episode's $Q$ estimate through a minimum. Any optimism claim must account for this dependence across episodes as well as the backward dependence across steps. In the regret analysis, the terms called martingale differences can have either sign, so replacing a positive weight by a larger common bound can reverse an inequality. These are concrete obstacles to the printed chain of estimates. Azar, Osband and Munos, 2017, pp. 4, 17, 20–21, 28.

Formalization scope

States, actions, steps, episodes and complete outcome arrays are finite. Probabilities are finite sums of products of transition rows. The transition-row predicate is a published general definition; this mission defines the paper-specific reward-bounded MDP, policies, UCBVI-CH recursion, and path law on top of it. The starting-state rule can inspect only earlier episodes. Greedy tie-breaking is universally quantified. $V^*$ is a maximum over policies, and the bonus is read only at positive counts. A model that assigns an arbitrary probability law, fixes one starting state, or omits Algorithm 2's minimum does not represent this target. Azar, Osband and Munos, 2017, pp. 2–4.

Lean uses steps $0,\dots,H-1$ and terminal index $H$ in place of the paper's algorithmic $1,\dots,H+1$. The appendix sometimes puts the terminal value at $H$. The weighted recursion therefore runs through the final reward step, rather than ending one step early. Its typical-state threshold is $4H^2L$, as required by (34)–(36), whereas Appendix B.1 prints $2H^2L$. The proof's correction term $c_4$ dominates its other terms under $A\ge2$, which is made explicit in that milestone. The printed (11) loses a factor of two from the count display before it; only the preceding display is a milestone. Lemma 18 is stated under the empirical-model part of the confidence event and $\delta\le1$, the domain on which its bonus comparison holds. The weighted milestone retains its coefficients because the bracketed martingale terms can be negative. Azar, Osband and Munos, 2017, pp. 14–17, 20–21, 28.

The goal retains Theorem 1's constant $20$. Appendix C.1 cites Lemmas 15 and 18, but the sketch of Lemma 15 does not track that constant explicitly. Formalizing the printed bound may therefore expose a gap in its proof; the mission records the claim without weakening its constants. Contributions establishing or repairing the explicit bound, as well as the four stated milestones and reusable finite concentration results, are within scope. Azar, Osband and Munos, 2017, pp. 5, 27, 29.

Selected references

• M. G. Azar, I. Osband and R. Munos, Minimax Regret Bounds for Reinforcement Learning, arXiv:1703.05449v2, 2017. Pinned preprint.

Motivation

Online decision makers often have to choose an action before seeing the cost assigned to it. A no-regret algorithm performs almost as well, in total, as the best single action that could have been chosen after the costs were known. In a related repeated-game problem, Blackwell approachability asks a player to keep the average of vector payoffs close to a desired set despite an adversary's choices. These two performance criteria look different: one compares scalar costs to a fixed benchmark, while the other measures a geometric distance. Abernethy, Bartlett, and Hazan establish algorithmic reductions between them, with explicit finite-horizon bounds in their COLT 2011 paper. This mission isolates the direction that turns an approachability algorithm into an online linear optimization algorithm.

The bound matters even when the input algorithm has no known rate. It relates the regret of the resulting online algorithm to the actual distance attained on the corresponding sequence. Any subsequent guarantee on that distance then yields a regret guarantee through the same reduction. The paper also gives the reverse reduction and an application to calibrated forecasting; those are separate missions in this series.

Setting

Fix a dimension $d$ and a nonempty compact convex decision set $K\subseteq\mathbb R^d$. On round $t$, an algorithm selects $x_t\in K$ using only the preceding cost vectors $f_1,\ldots,f_{t-1}$. The adversary then reveals $f_t$ in the Euclidean unit ball $B_2(1)$. The incurred linear cost is $\langle f_t,x_t\rangle$. For a horizon $T$, regret compares these costs with the cost of the best single point of $K$ evaluated on all $T$ rounds:

The minimum exists because $K$ is nonempty and compact. No probabilistic model for the cost sequence is assumed. The round index begins at one, and $x_t$ cannot depend on $f_t$.

The reduction uses $\kappa=\max_{x\in K}\|x\|$, the maximum norm of a decision. Write $a\oplus x$ for Euclidean concatenation of a scalar and a vector, an element of $\mathbb R^{d+1}$. The generated cone of a set $M$ consists of its nonnegative scalar multiples, $\operatorname{cone}(M)=\{\alpha m:\alpha\ge0,\ m\in M\}$. For a set $C$, its polar cone is $C^0=\{\theta:\langle\theta,z\rangle\le0\text{ for every }z\in C\}$. This negative-sign convention is fixed throughout the mission.

Algorithm 1 of the paper constructs a vector-payoff game. Its player actions are $K$, its adversary actions are $B_2(1)$, its payoff and target are

A Blackwell approachability algorithm for this game chooses each $x_t$ from the preceding adversary moves. Its finite-horizon approachability rate on a given sequence is $D_T(A)=\operatorname{dist}(T^{-1}\sum_{t=1}^T u(x_t,f_t),S)$, where distance means the Euclidean distance from a point to a set. The online algorithm created by Algorithm 1 uses precisely the same choices $x_t$.

Formalization targets

The goal is Theorem 16 of the paper. For every admissible history-based algorithm, every sequence of unit-ball costs, and every $T\ge1$, it asserts

This is a statement about the rate actually obtained on the chosen cost sequence. It assumes no upper bound on $D_T(A)$ and does not require an oracle call in the statement. Thus it also covers algorithms whose behavior is specified directly rather than through an implementation of the oracle.

The milestone targets are the distance formula of Lemma 13, the conic distance identity in display (8) of Theorem 16's proof, and the existence of a valid halfspace oracle in Lemma 15. Lemma 13 says distance to a nonempty convex cone equals the attained maximum of a linear functional over the polar cone's unit ball. Display (8) specializes this geometry to Algorithm 1's lifted target. Lemma 15 says that every halfspace containing that target admits a player action whose payoff remains in the halfspace against every permitted adversary move. Together these statements specify the geometry and the oracle needed by the reduction.

Significance

Theorem 16 gives a numerical transfer rule: a bound on approachability distance for Algorithm 1's game immediately bounds average regret for the same sequence. Its factor depends only on the size $\kappa$ of the decision set. This permits comparison of algorithms in a common finite-horizon language, without replacing the online cost sequence by a distribution or an asymptotic limit. The source paper uses this direction as one half of its equivalence between approachability and no-regret learning Abernethy, Bartlett, and Hazan, 2011.

The mathematical results are established in that paper; the goal here is a machine-checked Lean development of their statements and eventually their proofs. The mission also supplies reusable definitions of generated and polar cones, a Euclidean lift, a finite-history online algorithm, and regret over a compact decision set. Lemma 13 is useful outside this reduction whenever distance to a cone is compared with linear functionals on its polar. The proposed theorem items currently carry open proofs, while their statements and definition files are checked for elaboration in the pinned Lean environment.

Difficulty

The main obstacle is the change of viewpoint from a scalar regret comparison to distance from a set of lifted vector payoffs. A direct comparison of individual round costs does not describe that distance. The target is a polar cone in one additional Euclidean dimension, so a faithful account must keep the lift's geometry, the cone's sign convention, and the normalization by $\kappa$ aligned. The distance formula also asserts that its maximum is attained. An encoding that merely writes an infimum or supremum with default values can silently make an edge case look valid without representing the paper's claim.

The oracle milestone has a separate quantifier demand. One selected action must work against every adversary move for each halfspace containing the target. It cannot be replaced by a possibly different action for each move, or by a claim only about tangent halfspaces. The theorem includes halfspaces with arbitrary offsets and zero normals because the source oracle accepts any containing halfspace.

Formalization scope

Vectors live in EuclideanSpace ℝ (Fin d), and $a\oplus x$ lives in EuclideanSpace ℝ (Fin (d+1)) with the Euclidean norm. The generated cone uses exactly one nonnegative multiple of a point of the generating set, as in Definition 11. The polar uses $\langle\theta,z\rangle\le0$, the opposite sign from a positive dual-cone convention. Distances are Euclidean point-to-set distances. All arithmetic is over exact real numbers, and the regret minimum ranges over the image of the nonempty compact set $K$.

The statements require $\kappa>0$ because the source payoff divides by $\kappa$. This excludes the degenerate case $K=\{0\}$, in which the source instance is undefined. They require $T\ge1$ wherever an average is formed. Admissible histories consist of unit-ball adversary moves, and each round's decision belongs to $K$. The dimension may be zero syntactically, but the positive-$\kappa$ hypothesis excludes that case in results using Algorithm 1. These conditions keep the bound from being satisfied through Lean's default values for division by zero, distance to an empty set, or infima over empty sets.

The paper's display (8) writes $\operatorname{cone}(\kappa\oplus K)$ and labels its unit ball with dimension $d$; the formalization uses the cone of $\{\kappa\}\times K$ in $\mathbb R^{d+1}$, matching Algorithm 1. Lemma 12's printed bipolar claim omits closedness; this mission does not use that uncorrected sentence as a milestone. The oracle statement covers all containing halfspaces. Contributions are welcome for the distance identity, the oracle existence result, and the final regret inequality, as well as geometric lemmas supporting those proofs.

Selected references

• Jacob Abernethy, Peter L. Bartlett, and Elad Hazan, Blackwell Approachability and No-Regret Learning are Equivalent, Proceedings of the 24th Annual Conference on Learning Theory, JMLR Workshop and Conference Proceedings 19, 2011, pp. 27–46. Published paper.