Machine Learning

Motivation

Policy gradient methods optimize a parameterized policy of a Markov decision process by gradient ascent on its expected discounted return. They are among the most widely used methods in reinforcement learning, from REINFORCE (Williams 1992) and the policy gradient theorem to natural policy gradient and trust-region methods. The objective is not concave in the policy, even when the policy is a raw table of action probabilities, so standard optimization theory guarantees at best convergence to a stationary point, and it was long unclear whether or how fast these methods find an optimal policy.

Agarwal, Kakade, Lee and Mahajan (JMLR 2021) give a systematic answer for the tabular and function-approximation settings. This mission formalizes their warm-up result, Theorem 4.1: projected gradient ascent over the simplex of stochastic policies reaches an $\epsilon$-optimal policy after a number of iterations polynomial in the sizes of the MDP, the effective horizon $1/(1-\gamma)$, $1/\epsilon$, and a distribution mismatch coefficient. The gradient domination idea it rests on goes back to the analysis of conservative policy iteration by Kakade and Langford (2002) and to Scherrer and Geist (2014).

Setting

A finite discounted MDP consists of finite sets $\mathcal S$ of states and $\mathcal A$ of actions, a transition kernel $P(s'\mid s,a)$, rewards $r(s,a)\in[0,1]$ and a discount factor $\gamma\in[0,1)$. A policy $\pi$ assigns to each state a probability distribution $\pi(\cdot\mid s)$ over actions. Its value from a start state $s_0$ is

$$V^\pi(s_0)=\mathbb E\Big[\sum_{t=0}^\infty\gamma^t r(s_t,a_t)\,\Big|\,s_0\Big],\qquad a_t\sim\pi(\cdot\mid s_t),\ s_{t+1}\sim P(\cdot\mid s_t,a_t),$$

and for a start distribution $\rho$, $V^\pi(\rho)=\sum_s\rho(s)V^\pi(s)$. The action value is $Q^\pi(s,a)=r(s,a)+\gamma\sum_{s'}P(s'\mid s,a)V^\pi(s')$ and the advantage is $A^\pi(s,a)=Q^\pi(s,a)-V^\pi(s)$. The discounted state visitation distribution is $d^\pi_\rho(s)=(1-\gamma)\sum_{t\ge0}\gamma^t\Pr^\pi(s_t=s\mid s_0\sim\rho)$. An optimal policy $\pi^\star$ maximizes $V^\pi(s)$ at every state simultaneously; $V^\star=V^{\pi^\star}$.

In the direct parameterization the parameter is the table itself, $\pi_{s,a}=\pi(a\mid s)$, a point of the product simplex $\Delta(\mathcal A)^{|\mathcal S|}\subseteq\mathbb R^{\mathcal S\times\mathcal A}$. The algorithm optimizes $V^\pi(\mu)$ for a chosen start distribution $\mu$ by projected gradient ascent

$$\pi^{(t+1)}=P_{\Delta(\mathcal A)^{|\mathcal S|}}\big(\pi^{(t)}+\eta\nabla_\pi V^{(t)}(\mu)\big),$$

where $P_{\Delta(\mathcal A)^{|\mathcal S|}}$ is the Euclidean projection and $V^{(t)}=V^{\pi^{(t)}}$. Performance is measured under a possibly different distribution $\rho$, and the distribution mismatch coefficient $\|d^{\pi^\star}_\rho/\mu\|_\infty$ (componentwise ratio) measures how well $\mu$ covers the states an optimal policy visits from $\rho$.

Formalization targets

Goal: Theorem 4.1

With step size $\eta=(1-\gamma)^3/(2\gamma|\mathcal A|)$, from any initial policy, for every $\rho\in\Delta(\mathcal S)$ and $\epsilon>0$,

$$\min_{t\le T}\big\{V^\star(\rho)-V^{(t)}(\rho)\big\}\le\epsilon\qquad\text{whenever}\qquad T>\frac{64\gamma|\mathcal S||\mathcal A|}{(1-\gamma)^6\epsilon^2}\Big\|\frac{d^{\pi^\star}_\rho}{\mu}\Big\|_\infty^2 .$$

Milestones, in the order of the proof

1. Lemma 3.2 (performance difference): $V^\pi(s_0)-V^{\pi'}(s_0)=\frac1{1-\gamma}\mathbb E_{s\sim d^\pi_{s_0}}\mathbb E_{a\sim\pi(\cdot\mid s)}[A^{\pi'}(s,a)]$.
2. (7), the gradient of the direct parameterization: $\partial V^\pi(\mu)/\partial\pi(a\mid s)=\frac1{1-\gamma}d^\pi_\mu(s)Q^\pi(s,a)$.
3. Lemma 4.1 (gradient domination): $V^\star(\rho)-V^\pi(\rho)\le\frac1{1-\gamma}\|d^{\pi^\star}_\rho/\mu\|_\infty\max_{\bar\pi}(\bar\pi-\pi)^\top\nabla_\pi V^\pi(\mu)$, together with the sharper form with $d^\pi_\mu$ in place of $(1-\gamma)\mu$.
4. Lemma D.3 (smoothness): $\|\nabla_\pi V^\pi(s_0)-\nabla_\pi V^{\pi'}(s_0)\|_2\le\frac{2\gamma|\mathcal A|}{(1-\gamma)^3}\|\pi-\pi'\|_2$.
5. Theorem E.1(3) (Beck 2017, Theorem 10.15): projected gradient descent with step $1/\beta$ on a $\beta$-smooth function over a closed convex set has $\min_{t<T}\|G^\eta(x_t)\|\le\sqrt{2\beta(f(x_0)-f(x^*))}/\sqrt T$, with $G^\eta$ the gradient mapping.
6. Proposition B.1: a gradient mapping of norm at most $\epsilon$ at $\pi$ makes the next iterate $\pi^+$ $\epsilon(\eta\beta+1)$-stationary over feasible unit directions.

Significance

The theorem shows that, for the simplest constrained parameterization, a first-order method finds a globally optimal policy at a polynomial rate in spite of non-concavity. The guarantee holds for every performance distribution $\rho$ at once, and it isolates the role of exploration in a single quantity, the mismatch coefficient; Section 4.3 of the paper shows that without a well-covering $\mu$ gradient methods can need exponentially many steps. Lemma 4.1 and the smoothness bound are reused across the rest of the paper, and the performance difference lemma underlies essentially all of its analyses.

All results here are proved in the paper, with Theorem E.1 and Theorem E.2 cited from Beck (2017) and Ghadimi–Lan (2016). None of them has a machine-checked proof on the platform. A formal development provides a verified link between the policy gradient expression of the direct parameterization and a standard nonconvex projected-gradient rate, and a reusable formal library of discounted visitation distributions, the performance difference identity, and projected gradient methods on Euclidean spaces.

Difficulty

The obvious argument, "projected gradient ascent converges to a stationary point, and stationary points are optimal", fails on both counts as stated. Stationary points of $V^\pi(\mu)$ need not be optimal when $\mu$ does not cover the relevant states; the quantitative replacement is gradient domination, which only controls suboptimality through the mismatch coefficient. The convergence rate itself requires smoothness of the value as a function of the policy table, which is a bound on second derivatives of a matrix inverse $(I-\gamma P_\pi)^{-1}$ with the dependence $(1-\gamma)^{-3}$ and the factor $|\mathcal A|$ made explicit. Finally, the near-stationarity delivered by the gradient-mapping rate is at the next iterate, not the current one, which is why the conclusion is over $t\in\{0,\dots,T\}$. On the Lean side, the value is an infinite series in the policy entries, so its differentiability and the exact gradient formula have to be established for a function defined on the whole parameter space.

Formalization scope

Policies are parameter vectors in EuclideanSpace ℝ (S × A), so norms are $\ell_2$ and Mathlib's gradient is $\nabla_\pi$; the objective $\pi\mapsto V^\pi(\mu)$ is defined on the whole space and is only ever evaluated, with its gradient, at policies. The MDP layer (transition kernels, policies, $V^\pi$, $Q^\pi$, occupation distributions, optimal policies) is the published FoundationsML.ReinforcementLearning library; $V^\pi$ is the unnormalized discounted sum. The projection is any map satisfying the nearest-point property. The optimal policy is a hypothesis IsOptimalPolicy (optimal from every state), not a supremum over all functions.

Conventions committed to:

• The mismatch coefficient is any constant $D$ with $d^{\pi^\star}_\rho(s)\le D\mu(s)$ for all $s$; this avoids Lean's $x/0=0$ and is equivalent to the page's statement when the coefficient is finite.
• $\gamma>0$ and $\epsilon>0$ are explicit hypotheses of the goal (the step size divides by $\gamma$, the threshold by $\epsilon$).
• The goal concludes $\exists\,t\le T$. The printed $\min_{t<T}$ fails at $T=1$ (one state, two actions with rewards $1$ and $0$, $\gamma=0.001$, $\epsilon=1/2$, initial policy on the bad action); the proof on p. 50 establishes the range $0\le t\le T$.
• Proposition B.1 bounds the directions feasible at $\pi^+$, as its proof does; Theorem E.1 assumes smoothness on $C$ only and uses the radicand $2\beta(f(x_0)-f(x^*))$ of Beck and of p. 49.

A formalization that defines the update through formula (7), that assumes gradient domination or smoothness as hypotheses of the goal, or that takes the gradient off the simplex where the value series may diverge, would trivialize the goal; the goal mentions none of these, and (7) is a milestone theorem.

A complete development needs: summability and differentiability of the value series near the simplex; the performance difference lemma; the Euclidean projection inequality on a closed convex set; the descent lemma for functions smooth on a convex set; and the gradient-mapping argument. The projection and gradient-mapping results are independent of reinforcement learning and reusable. Contributions to any milestone are welcome, as are proofs of Theorem E.2 (Ghadimi–Lan) as a stepping stone to Proposition B.1.

Selected references

• A. Agarwal, S. M. Kakade, J. D. Lee, G. Mahajan, On the Theory of Policy Gradient Methods: Optimality, Approximation, and Distribution Shift, JMLR 22(98), 2021; arXiv:1908.00261v5. https://arxiv.org/abs/1908.00261
• A. Beck, First-Order Methods in Optimization, MOS-SIAM Series on Optimization, SIAM, 2017. https://doi.org/10.1137/1.9781611974997
• S. Ghadimi, G. Lan, Accelerated gradient methods for nonconvex nonlinear and stochastic programming, Mathematical Programming 156, 2016. https://doi.org/10.1007/s10107-015-0871-8
• S. Kakade, J. Langford, Approximately optimal approximate reinforcement learning, ICML 2002. https://dl.acm.org/doi/10.5555/645531.656005
• B. Scherrer, M. Geist, Local Policy Search in a Convex Space and Conservative Policy Iteration as Boosted Policy Search, ECML PKDD 2014, pp. 35–50 (arXiv version: https://arxiv.org/abs/1306.1520)
• R. J. Williams, Simple statistical gradient-following algorithms for connectionist reinforcement learning, Machine Learning 8, 1992. https://doi.org/10.1007/BF00992696

Motivation

Regularized least squares is the standard tool of high-dimensional linear regression. The square-root LASSO of Belloni, Chernozhukov and Wang (Biometrika, 2011) minimizes $\sqrt{\mathrm{MSE}_n(\beta)} + \lambda\|\beta\|_1$. Unlike the LASSO, its optimal regularization parameter does not depend on the unknown noise level. Regularization is usually justified through sparsity or bias–variance arguments. Blanchet, Kang and Murthy (arXiv:1610.05627, J. Appl. Probab. 56(3), 2019) give a different justification. The square-root LASSO, and every $\ell_p$-penalized square-root least-squares estimator, is exactly a distributionally robust estimator. It minimizes the worst-case expected square loss over all data distributions within a given optimal-transport distance of the empirical distribution.

The rest of the paper builds on this representation: the radius of the transport ball is the regularization parameter, which the paper's Robust Wasserstein Profile function selects by a statistical criterion (mission 3 of this series). The duality theorem underneath, Proposition 1, is due to Blanchet and Murthy (Math. Oper. Res., 2019). Closely related representations for logistic regression appear in Shafieezadeh-Abadeh, Mohajerin Esfahani and Kuhn (NeurIPS 2015), where they are approximate. The cost function introduced in this paper makes them exact.

Setting

The training data are $n \ge 1$ pairs $(X_1, Y_1), \dots, (X_n, Y_n)$ with predictors $X_i \in \mathbb R^d$ and responses $Y_i \in \mathbb R$. No distributional assumption is made; the data are fixed vectors. The empirical distribution is $P_n = \frac1n \sum_{i=1}^n \delta_{(X_i, Y_i)}$. For $\beta \in \mathbb R^d$ the square loss is $l(x, y; \beta) = (y - \beta^T x)^2$ and the mean square error is $\mathrm{MSE}_n(\beta) = \frac1n\sum_{i=1}^n (Y_i - \beta^T X_i)^2$.

A cost function $c$ assigns to two points $z, w$ of $\mathbb R^d \times \mathbb R$ a value $c(z, w) \in [0, \infty]$, the cost of moving a unit of mass from $z$ to $w$. The optimal transport cost between probability measures $P$ and $Q$ is

$$D_c(P, Q) = \inf\Big\{ \mathbb E_\pi[c(U, W)] : \pi \text{ a probability measure on pairs } (U, W),\ \pi_U = P,\ \pi_W = Q \Big\}. \qquad (7)$$

The worst-case expected loss at radius $\delta \ge 0$ is $\sup_{P : D_c(P, P_n) \le \delta} \mathbb E_P[l(X, Y; \beta)]$, and the distributionally robust regression problem (8) minimizes it over $\beta$.

Two costs are used. With $q \in (1, \infty]$:

• the squared $\ell_q$ cost on $\mathbb R^{d+1}$, $c((x, y), (u, v)) = \|(x, y) - (u, v)\|_q^2$ (Proposition 2);
• the cost $N_q^2$, where (14) $N_q((x, y), (u, v)) = \|x - u\|_q$ if $y = v$ and $+\infty$ otherwise. Under this cost the responses cannot be moved, and only the predictors are perturbed (Theorem 1).

The exponent $p$ is the dual of $q$, $1/p + 1/q = 1$, and $\bar\beta = (-\beta, 1)$.

Formalization targets

Goal: Theorem 1 (p. 11)

For the cost $c = N_q^2$, every $\delta \ge 0$ and every $\beta \in \mathbb R^d$,

$$\sup_{P :\, D_c(P, P_n) \le \delta} \mathbb E_P\big[(Y - \beta^T X)^2\big] = \Big(\sqrt{\mathrm{MSE}_n(\beta)} + \sqrt\delta\,\|\beta\|_p\Big)^2 ,$$

and consequently

$$\inf_{\beta \in \mathbb R^d} \sup_{P :\, D_c(P, P_n) \le \delta} \mathbb E_P\big[(Y - \beta^T X)^2\big] = \inf_{\beta \in \mathbb R^d} \Big(\sqrt{\mathrm{MSE}_n(\beta)} + \sqrt\delta\,\|\beta\|_p\Big)^2 .$$

The second identity is the printed theorem; the first is what its proof establishes for each $\beta$. The goal states both.

Milestones

1. Proposition 1 (p. 10): strong duality. For a lower semicontinuous cost vanishing on the diagonal, an upper semicontinuous loss and $\delta > 0$, the worst-case expected loss equals $\min_{\gamma \ge 0} \{\gamma\delta + \frac1n \sum_i \varphi_\gamma(X_i, Y_i)\}$, with $\varphi_\gamma(z) = \sup_u \{l(u) - \gamma c(u, z)\}$ (11).
2. (28) (pp. 28–29): the closed form of $\varphi_\gamma$ for the square loss and the squared $\ell_q$ cost.
3. (29) and the display after it (p. 29): $\inf_{\gamma > b^2} \{\gamma\delta + \frac{\gamma}{\gamma - b^2} M\} = (\sqrt M + b\sqrt\delta)^2$ for $M, b, \delta \ge 0$.
4. Proposition 2 (p. 10): the analogue of the goal for the squared $\ell_q$ cost, with $\|\bar\beta\|_p$ in place of $\|\beta\|_p$ (13).
5. Outline of the proof of Theorem 1, last display (p. 29): the closed form of $\varphi_\gamma$ for the cost $N_q^2$.

Significance

The result. Theorem 1 identifies $\ell_p$-penalized square-root least squares with a min–max problem over data distributions. For $q = \infty$, $p = 1$ the minimizers are those of the square-root LASSO with $\lambda = \sqrt\delta$. The regularization parameter therefore acquires a meaning: it is the square root of the transport budget an adversary may spend perturbing the predictors. This is the basis of the paper's choice of $\delta$ by the Robust Wasserstein Profile function (§4), and of the interpretation of regularized estimators as robust to covariate perturbations. Proposition 2 shows that letting the adversary also move the responses changes the penalty to $\|(-\beta, 1)\|_p$, which is why the label-preserving cost $N_q$ is needed for an exact match.

Formalizing it. All results are proved on paper; none is formalized. A complete development gives a machine-checked strong-duality theorem for optimal-transport balls with possibly infinite costs (Proposition 1), two explicit worst-case computations, and corrected boundary cases of the closed forms (28) and the outline display, which print $+\infty$ for all $\gamma \le \|\bar\beta\|_p^2$ although the value can be finite at equality. The corrections do not affect the theorems.

Difficulty

The obvious argument fails in two places. The first is the duality step: the supremum ranges over all Borel probability measures on $\mathbb R^{d+1}$ within transport cost $\delta$, an infinite-dimensional set that is not compact in any convenient topology, with a loss that is unbounded above. Exchanging the supremum with the Lagrange multiplier of the budget constraint is Proposition 1, a theorem in its own right (Blanchet–Murthy), and its attainment claim needs $\delta > 0$.

The second is the cost $N_q$, which is $+\infty$ off $\{y = v\}$, so the standard Wasserstein duality theorems, which assume a finite metric cost, do not apply. The degenerate cases $\beta = 0$, $\mathrm{MSE}_n(\beta) = 0$, $\delta = 0$, where the objective in $\gamma$ does not blow up at both ends, must be covered separately.

Formalization scope

• Spaces. A data point is a pair in (Fin d → ℝ) × ℝ with the product σ-algebra and topology. Proposition 2's cost uses the stacked vector in Fin (d+1) → ℝ (response last, built with Fin.snoc), and $\bar\beta$ is the stacked vector of $(-\beta, 1)$.
• Norms. $\|\cdot\|_q$ and $\|\cdot\|_p$ are the norms of PiLp, with exponents in ℝ≥0∞, so $q = \infty$ (the square-root LASSO case) is included. The exponents are linked by p.HolderConjugate q, and $q \in (1, \infty]$ throughout. Theorem 1 does not print a range for $q$; the range is taken from Proposition 2, which the paper calls essentially the same result.
• Transport cost and worst case. Costs are ℝ≥0∞-valued, and $D_c$ is an infimum over probability couplings with both marginals fixed. Expectations of the nonnegative losses are lower Lebesgue integrals, and the worst case is a supremum in ℝ≥0∞ over all probability measures in the ball. No integrability side condition removes measures from the ball. Identities with a real right-hand side are stated after embedding it with ENNReal.ofReal.
• The empirical distribution is the published definition WassersteinDRO.Regularization.empiricalDistribution, applied to $i \mapsto (X_i, Y_i)$, with $n > 0$.
• $\varphi_\gamma$. A point at infinite cost contributes $-\infty$ for every $\gamma \ge 0$, including $\gamma = 0$, as in the paper's treatment of $N_q$. With the convention $0 \cdot \infty = 0$ instead, Proposition 1's minimum would not be attained for the cost $N_q^2$ at $\beta = 0$.
• Proposition 1 is stated for a nonnegative loss and $\delta > 0$; both are restrictions of the page, recorded in the item.
• Corrections. (28) and the outline display are stated with their corrected boundary cases. The one-dimensional lemma behind (29) is stated as a greatest lower bound over $\gamma > b^2$, including $b = 0$, $M = 0$, $\delta = 0$.

A formalization in which the transport infimum did not fix both marginals, allowed sub-probability couplings, or used a Bochner integral would make the worst case trivially $+\infty$ or $0$. The conventions above rule this out: at $\delta = 0$ the ball is $\{P_n\}$ and both sides of the goal equal $\mathrm{MSE}_n(\beta)$.

The work needs Kantorovich-type duality for lower semicontinuous costs on $\mathbb R^m$ (absent from Mathlib), Hölder's inequality with its equality case for PiLp, and elementary one-variable optimization. The duality theorem and the transport-cost definition are reusable beyond this mission: mission 2 of this series (classification) uses Proposition 1 with the cost $N_q$, $\rho = 1$. Contributions that prove Proposition 1, or its weak-duality half, are particularly welcome.

Selected references

• J. Blanchet, Y. Kang, K. Murthy, Robust Wasserstein Profile Inference and Applications to Machine Learning, J. Appl. Probab. 56(3), 2019; arXiv:1610.05627v4. https://arxiv.org/abs/1610.05627
• J. Blanchet, K. Murthy, Quantifying distributional model risk via optimal transport, Math. Oper. Res. 44(2), 2019. https://doi.org/10.1287/moor.2018.0936
• A. Belloni, V. Chernozhukov, L. Wang, Square-root lasso: pivotal recovery of sparse signals via conic programming, Biometrika 98(4), 2011. https://doi.org/10.1093/biomet/asr043
• S. Shafieezadeh-Abadeh, P. Mohajerin Esfahani, D. Kuhn, Distributionally robust logistic regression, NeurIPS 2015. https://arxiv.org/abs/1509.09259
• C. Villani, Optimal Transport: Old and New, Springer, 2009. https://doi.org/10.1007/978-3-540-71050-9

Motivation

Robust optimization protects a decision against every realization of uncertain data in a prescribed uncertainty set. The standard approach replaces the uncertain constraints by a deterministic robust counterpart and solves that counterpart directly (Ben-Tal, El Ghaoui, Nemirovski, Robust Optimization, 2009). The counterpart is often a harder problem than the original: a robust linear program with ellipsoidal uncertainty becomes a second-order cone program, and a robust quadratic program can become a semidefinite program. A practitioner who has an efficient, specialised solver for the nominal problem may therefore have no efficient solver for its robust version.

Ben-Tal, Hazan, Koren and Mannor (arXiv:1402.6361, Operations Research 2015) ask whether the robust problem can be solved by repeatedly calling a solver of the nominal problem, with the number of calls independent of the dimension. Their first answer, the dual-subgradient meta-algorithm of §3.1, does so whenever the constraints are concave in the noise and the uncertainty set is convex. It is a primal–dual scheme: an online-learning algorithm picks the noise, and the nominal solver answers. This mission formalizes that result, Theorem 3.

Setting

Let $\mathcal D\subseteq\mathbb R^n$ be a convex domain, $\mathcal U\subseteq\mathbb R^d$ a convex uncertainty set, and $f_1,\dots,f_m:\mathbb R^n\times\mathbb R^d\to\mathbb R$ constraint functions. The robust feasibility problem (3) is

$$\exists\,x\in\mathcal D:\qquad f_i(x,u_i)\le 0\quad\forall u_i\in\mathcal U,\ i=1,\dots,m .$$

(An objective is handled by binary search on its value, so feasibility is the core question.) A point $x\in\mathcal D$ is an $\epsilon$-approximate solution if $f_i(x,u)\le\epsilon$ for all $u\in\mathcal U$ and all $i$.

An $\epsilon$-approximate oracle $\mathcal O_\epsilon$ (Figure 1) takes a noise vector $u=(u_1,\dots,u_m)\in\mathcal U^m$ and either returns some $x\in\mathcal D$ with $f_i(x,u_i)\le\epsilon$ for all $i$, or answers "infeasible", which it may do only if no $x\in\mathcal D$ has $f_i(x,u_i)\le 0$ for all $i$.

The standing assumptions of §3.1 are: each $f_i(\cdot,u)$ is convex on $\mathcal D$; each $f_i(x,\cdot)$ is concave on $\mathcal U$ for $x\in\mathcal D$; $D\ge\|u-v\|_2$ for all $u,v\in\mathcal U$; and $\|\nabla_u f_i(x,u)\|_2\le G$ for $x\in\mathcal D$, $u\in\mathcal U$. Write $P$ for the Euclidean projection onto $\mathcal U$.

Algorithm 1 sets $T=\lceil G^2D^2/\epsilon^2\rceil$ and $\eta=D/(G\sqrt T)$, starts from $u^0_1,\dots,u^0_m\in\mathcal U$, and for $t=1,\dots,T$ updates

$$u^t_i=P\bigl(u^{t-1}_i+\eta\,\nabla_u f_i(x^{t-1},u^{t-1}_i)\bigr),\qquad x^t=\mathcal O_\epsilon(u^t_1,\dots,u^t_m),$$

stopping with "infeasible" as soon as the oracle says so, and otherwise returning $\bar x=\frac1T\sum_{t=1}^T x^t$. In Lean these are alg1T, alg1Eta, alg1U, alg1X, alg1Output and alg1Calls in the namespace OracleRO.DualSubgrad.

Formalization targets

Goal: Theorem 3 (p. 7)

For every $\epsilon$-approximate oracle,

$$\text{output}=\text{"infeasible"}\ \Longrightarrow\ \neg\,\exists x\in\mathcal D\ \forall i\ \forall u\in\mathcal U:\ f_i(x,u)\le 0,$$ $$\text{output}=\bar x\ \Longrightarrow\ \bar x\in\mathcal D\ \text{ and }\ f_i(\bar x,u)\le 2\epsilon\ \ \forall i,\ \forall u\in\mathcal U,$$

and the number of oracle calls is at most $\lceil G^2D^2/\epsilon^2\rceil$.

Milestones

1. Lemma 1 (p. 5, Zinkevich 2003): projected online gradient ascent with step $\eta=D/(G\sqrt T)$ on concave rewards has regret $\sum_t f_t(x^*)-\sum_t f_t(x_t)\le GD\sqrt T$ for every $x^*$ in the decision set.
2. (6) (p. 7): if a point is returned, $\frac1T\sum_{t=1}^T f_i(x^t,u^t_i)\le\epsilon$ for every $i$.
3. (7) (p. 8): for every $i$ and $u\in\mathcal U$, $\frac1T\sum_t f_i(x^t,u)-\frac1T\sum_t f_i(x^t,u^t_i)\le GD/\sqrt T\le\epsilon$.
4. Final inequality of the proof (p. 8): $f_i(\bar x,u)\le\frac1T\sum_t f_i(x^t,u)$ for $u\in\mathcal U$.

Significance

The result. Theorem 3 turns any approximate solver of the nominal problem into an approximate solver of its robust counterpart, at a cost of $\lceil G^2D^2/\epsilon^2\rceil$ solver calls, a number that depends on the geometry of $\mathcal U$ and the sensitivity of the constraints to the noise but not on $n$, $d$ or $m$. It is the prototype of the paper's oracle-based reductions: the same primal–dual template, with a different online learner, gives the dual-perturbation algorithm of §3.2–3.3 for non-convex uncertainty sets, and the applications of §4 (robust linear programs, quadratic programs, semidefinite programs) instantiate it.

Formalizing it. The theorem is proved in the paper; none of it is machine-checked. A formal development adds a checked statement of the reduction with an explicit call count in place of the paper's $O(\cdot)$, and a reusable regret bound for projected online gradient ascent on concave rewards (Lemma 1), which the paper quotes from Zinkevich without proof and which many other online-learning results rest on.

Difficulty

The obvious argument for the dual side fails at one point: in round $t$ the primal point $x^t$ is computed from $u^t$, so the reward $f_i(x^t,\cdot)$ that the dual player faces depends on its own current move. A regret bound that assumed rewards fixed in advance, or drawn independently of the learner's play, would not apply. Lemma 1 must be used in its adversarial form, valid for every sequence of reward functions, including adaptively chosen ones. A second point is that the projection step requires the variational characterization of a nearest point in a convex set, which a mere "map into $\mathcal U$" does not provide.

Formalization scope

Points are elements of EuclideanSpace ℝ (Fin k), so every norm is the $\ell_2$ norm. The projection is a predicate IsProjOnto U P (each $P(y)$ is a nearest point of $\mathcal U$ to $y$), not a construction; the oracle is a function (Fin m → E d) → Option (E n) with none for "infeasible", constrained by the predicate IsApproxOracle on inputs in $\mathcal U^m$. The goal is quantified over every oracle meeting that specification. The gradient $\nabla_u f_i(x,u)$ is a given map gradU with HasGradientAt at points of $\mathcal U$; no differentiability in $x$ is assumed. Rounds are indexed by natural numbers with index $0$ for the initialization; the starting primal point $x^0\in\mathcal D$, used by the first update and left undefined by the algorithm, is an input. Hypotheses $D>0$ and $G>0$ are added so that $\eta$ and $T\ge1$ are meaningful. Maxima over $\mathcal U$ are stated as "for every $u\in\mathcal U$".

Explicit instantiations and corrections:

• The paper's "$O(G^2D^2/\epsilon^2)$ calls" is stated as at most $\lceil G^2D^2/\epsilon^2\rceil$ calls (one call per round, $T$ rounds).
• Lemma 1's "$G\ge\max_t\|f_t(x_t)\|$" is read as the gradient bound $\|\nabla f_t(x_t)\|\le G$, as the same sentence describes it.
• The proof's "Combining (10) and (12)" refers to (6) and (7).

Trivializing formalizations are ruled out: an oracle specification under which "infeasible" is never returned, or an output that is not the average of the oracle's answers, would not be Theorem 3. The "infeasible" conclusion is about the robust problem, not the nominal one.

A complete development needs the variational inequality for nearest points in a convex set, the gradient (supergradient) inequality for a concave function differentiable at a point of a convex set, Zinkevich's telescoping argument, and Jensen's inequality for finite averages. The first two and Lemma 1 are reusable beyond this mission. Proofs of the milestones, in any order, are welcome.

Selected references

• A. Ben-Tal, E. Hazan, T. Koren, S. Mannor, Oracle-Based Robust Optimization via Online Learning, arXiv:1402.6361v1, 2014; Operations Research 63(3), 2015. https://arxiv.org/abs/1402.6361v1
• M. Zinkevich, Online Convex Programming and Generalized Infinitesimal Gradient Ascent, ICML 2003. https://dl.acm.org/doi/10.5555/3041838.3041955
• A. Ben-Tal, L. El Ghaoui, A. Nemirovski, Robust Optimization, Princeton University Press, 2009. https://doi.org/10.1515/9781400831050
• E. Hazan, Introduction to Online Convex Optimization, Foundations and Trends in Optimization, 2016. https://arxiv.org/abs/1909.05207

Motivation

Data-dependent risk bounds in statistical learning replace combinatorial quantities such as the VC dimension with averages of how well a function class can fit random noise on the observed sample. Bartlett and Mendelson's article (JMLR 3, 2002) established these averages, the Rademacher and Gaussian complexities, as a general tool: a risk bound (their Theorem 8) holds with a complexity penalty, and the complexity of a complicated class can be bounded through structural results that relate it to the complexities of simpler classes.

This mission formalizes two of those structural results, both stated for Gaussian complexities. The first (Theorem 14) controls a Lipschitz function of several real-valued classes at once, the vector-valued analogue of the classical contraction principle. The second (Theorem 16) controls an arbitrary fixed boolean combination of classes of classifiers, such as intersections, unions or majority votes of a fixed number of base classifiers, by the sum of the complexities of the components. Such combinations arise whenever a classifier is assembled from simpler ones, for instance in decision lists, small decision trees over a base class, or voting schemes.

Setting

Let $\mathcal X$ be a set, $\mu$ a probability measure on it, and $n \ge 1$ a sample size. For a class $F$ of functions $\mathcal X \to \mathbb R$ and a sample $x = (x_1, \dots, x_n)$, the empirical Gaussian complexity is

$$\hat G_n(F)(x) = \mathbb E\left[\sup_{f\in F}\left|\frac2n\sum_{i=1}^n g_i f(x_i)\right|\right],$$

with $g_1, \dots, g_n$ independent standard Gaussian $N(0,1)$ variables, and the Gaussian complexity is $G_n(F) = \mathbb E\, \hat G_n(F)(X_1, \dots, X_n)$ for $X_1, \dots, X_n$ i.i.d. with law $\mu$ (Definition 2, p. 464). In Lean these are empiricalGaussian n F x and gaussianComplexity μ n F.

Three constructions of classes appear.

• Direct sum. With $\mathcal A = \mathbb R^m$ carrying the Euclidean distance, a class $F$ of maps $\mathcal X \to \mathcal A$ is a subset of the direct sum of real classes $F_1, \dots, F_m$ when each $f \in F$ is $x \mapsto (f_1(x), \dots, f_m(x))$ with $f_i \in F_i$ (SubsetDirectSum F Fi).
• Composition. For $\phi : \mathcal Y \times \mathcal A \to \mathbb R$, $\phi \circ f$ is $(x, y) \mapsto \phi(y, f(x))$ and $\phi\circ F$ collects these (compClass φ F).
• Boolean combination. For $g : \{\pm1\}^k \to \{\pm1\}$ and classes $F_1, \dots, F_k$ of $\{\pm1\}$-valued functions, $g(F_1, \dots, F_k) = \{x \mapsto g(f_1(x), \dots, f_k(x)) : f_j \in F_j\}$ (boolComb g F).

A centred Gaussian process indexed by a finite set $I$ is a family $(X_i)_{i \in I}$ of real random variables whose finite-dimensional laws are jointly Gaussian with mean zero; $\|X_i - X_j\|_2 = (\mathbb E(X_i - X_j)^2)^{1/2}$.

Formalization targets

Goal: Theorem 16 (p. 472)

For a fixed boolean function $g : \{\pm1\}^k \to \{\pm1\}$ with $k \ge 1$ and classes $F_1, \dots, F_k$ of $\{\pm1\}$-valued functions,

$$G_n\bigl(g(F_1, \dots, F_k)\bigr) \le 2 \sum_{j=1}^k G_n(F_j).$$

Milestones

1. Lemma 13 (p. 471), the comparison of Gaussian processes as printed: if $\|X_i - X_j\|_2 \le \|Y_i - Y_j\|_2$ for all $i, j$, then $\mathbb E\sup_i X_i \le 2\,\mathbb E\sup_i Y_i$.
2. Theorem 14 (p. 471): if each $\phi(y, \cdot)$ is $L$-Lipschitz for the Euclidean distance, passes through the origin, and $\phi$ is uniformly bounded, then for every sample $(x_k, y_k)_{k \le n}$,

$$\hat G_n(\phi \circ F) \le 2L \sum_{i=1}^m \hat G_n(F_i).$$

3. The extension of $g$ (proof of Theorem 16, p. 472): $g(x) = (1 - \|x - a\|)g(a)$ when $\|x - a\| < 1$ for a cube vertex $a$, and $0$ otherwise, is well defined, extends $g$, maps into $[-1,1]$, vanishes at $0$ and is $1$-Lipschitz.

Significance

Theorem 16 turns any bound on the Gaussian complexity of base classes into a bound for a fixed boolean combination of them, at the cost of a factor $2$ on the sum of their complexities, whatever $g$ and $k$ are. Together with the comparison between Gaussian and Rademacher complexities (Lemma 4 of the paper) and the risk bound of Theorem 8, it yields generalization bounds for classifiers built as combinations of base classifiers. Theorem 14 is the general tool: it handles any Lipschitz loss of a vector-valued predictor, such as multiclass margins, through the complexities of its coordinate classes.

All three results are proved in the paper (Lemma 13 is classical and cited from Pisier). None of them is formalized on Prove2Me; the finite-dimensional Sudakov–Fernique inequality, with constant $1$, is (HighDimProb.RandomProcesses.sudakov_fernique_finite_dim). This mission produces machine-checked versions of the vector contraction for Gaussian averages and of the boolean-combination bound, and records the corrections the printed statements need.

Difficulty

The obvious approach to Theorem 14 compares two Gaussian processes indexed by the class, but Definition 2 takes the supremum of an absolute value scaled by $2/n$, while Gaussian comparison inequalities bound the expected supremum of the process itself. The printed proof equates the two; done carefully, the comparison with the printed constant $2$ of Lemma 13 gives only $4L$. Reaching the printed $2L$ requires a comparison with constant $1$ and an argument that handles the absolute value. A second difficulty is that the classes may be infinite and unbounded, so expected suprema must be handled as extended-valued quantities, and the reduction to finite classes ("without loss of generality") must be justified. For Theorem 16 the extension of $g$ must be checked to be Lipschitz across the boundaries of the tents in the Euclidean, not the sup, norm.

Formalization scope

The source is the published JMLR article (vol. 3, 2002, pp. 463–482), not the COLT 2001 version, whose numbering differs.

• Complexities in $[0, \infty]$. $\hat G_n$ and $G_n$ are lower Lebesgue integrals of an ENNReal supremum against $N(0,1)^{\otimes n}$ and $\mu^{\otimes n}$. An unbounded class has complexity $+\infty$; a real-valued supremum or Bochner integral would silently return $0$ there and make the upper bounds false, so that encoding is ruled out. No finiteness or boundedness of any class is assumed.
• $\mathcal A = \mathbb R^m$ is EuclideanSpace ℝ (Fin m), so "Lipschitz" refers to the Euclidean distance as printed. Using Fin m → ℝ (the sup distance) would change the theorem.
• $\{\pm1\}$ is encoded as $\mathbb Z^\times$ coerced to $\mathbb R$.
• Lemma 13: centred processes added. As printed the lemma is false: $X_i \equiv 5$, $Y_i \equiv 0$ satisfy the hypothesis. Both processes are assumed mean zero, as in Slepian's lemma. The two processes may live on different probability spaces; the index set is any finite nonempty type. The constant $2$ is kept as printed.
• Theorem 14: printed proof loose, statement kept. The constant $2L$ is kept as printed; the statement is true via the constant-$1$ comparison. The uniform-boundedness hypothesis on $\phi$ is kept as printed although the extended-valued formulation does not need it.
• Theorem 16 and the extension: $k \ge 1$ added. For $k = 0$ the boolean function is a constant $\pm1$, the right side is $0$, and the left side is $\mathbb E\frac2n|\sum_i g_i| > 0$; also the extension would have $g(0) = \pm1$.
• Theorem 16: measurability guard. Each $\hat G_n(F_j)$ is assumed almost-everywhere measurable as a function of the sample, so that the expectation of $\sum_j \hat G_n(F_j)$ is the sum of the expectations. The paper does not discuss measurability.

A complete development needs Gaussian comparison for finite index sets (available on the platform), the reduction from infinite to finite classes for extended-valued suprema, and elementary Euclidean geometry of the cube. The first two are reusable for every Gaussian-average argument in learning theory. Proofs of any milestone, and of the constant-$1$ variant of Lemma 13 transported between probability spaces, are welcome.

Selected references

• P. L. Bartlett, S. Mendelson, Rademacher and Gaussian Complexities: Risk Bounds and Structural Results, Journal of Machine Learning Research 3 (2002), 463–482. https://www.jmlr.org/papers/v3/bartlett02a.html
• G. Pisier, The Volume of Convex Bodies and Banach Space Geometry, Cambridge University Press, 1989. https://doi.org/10.1017/CBO9780511662454
• M. Ledoux, M. Talagrand, Probability in Banach Spaces: Isoperimetry and Processes, Springer, 1991. https://doi.org/10.1007/978-3-642-20212-4

Motivation

A robust Markov decision process (robust MDP) evaluates a policy against the worst transition kernel and reward in an uncertainty set around a nominal model $(P_0, r_0)$. It is the standard model for planning when the dynamics are estimated from data (Iyengar 2005; Nilim and El Ghaoui 2005; Wiesemann, Kuhn and Rustem 2013). Its Bellman update contains an inner optimization over the uncertainty set at every state, which makes robust planning costly when the sets are not $(s,a)$-rectangular.

Derman, Geist and Mannor (arXiv:2110.06267, NeurIPS 2021) show that, for $s$-rectangular ball uncertainty sets, this inner optimization can be replaced by an explicit penalty that depends both on the policy and on the value function. The resulting twice regularized (R²) MDPs have Bellman operators with no inner optimization over models. The first mission of this series formalizes the robust–regularized equivalence (Theorem 4.1 of the paper). This mission formalizes Section 5: the R² Bellman operators are monotone and contracting under a bound on the transition radius, and the greedy policy of the R² optimal value is optimal.

Setting

Let $\mathcal S$ and $\mathcal A$ be finite nonempty sets of states and actions, $\gamma\in(0,1)$ a discount factor, $P_0(s'\mid s,a)$ a transition kernel and $r_0(s,a)$ a reward. A policy $\pi\in\Delta_{\mathcal A}^{\mathcal S}$ assigns to each state a probability distribution $\pi_s$ on $\mathcal A$. For $v\in\mathbb R^{\mathcal S}$ write $q_s(a)=r_0(s,a)+\gamma\sum_{s'}P_0(s'\mid s,a)v(s')$ and

$$[T^\pi_{(P_0,r_0)}v](s)=\sum_a\pi_s(a)\,q_s(a).$$

All norms $\|\cdot\|$ below are $\ell_2$-norms, $\|a\|=\big(\sum_z a(z)^2\big)^{1/2}$; $\|\cdot\|_\infty$ is the sup norm.

Fix nonnegative radii $\alpha^r_s,\alpha^P_s$ for each state. The R² regularizer is $\Omega_{v,\mathrm R^2}(\pi_s)=\|\pi_s\|\,(\alpha^r_s+\alpha^P_s\gamma\|v\|)$, and the R² Bellman operators are

$$[T^{\pi,\mathrm R^2}v](s)=[T^\pi_{(P_0,r_0)}v](s)-\Omega_{v,\mathrm R^2}(\pi_s),\qquad [T^{*,\mathrm R^2}v](s)=\max_{\pi\in\Delta^{\mathcal S}_{\mathcal A}}[T^{\pi,\mathrm R^2}v](s).$$

A policy $\pi$ is greedy for $v$ when $T^{\pi,\mathrm R^2}v=T^{*,\mathrm R^2}v$.

Assumption 5.1 (bounded radius). For each $s$ there is $\epsilon_s>0$ with

$$\alpha^P_s\le\min\Big(\frac{1-\gamma-\epsilon_s}{\gamma\sqrt{|\mathcal S|}}\ ;\ \min_{u\in\mathbb R^{\mathcal A}_+,\|u\|=1,\ w\in\mathbb R^{\mathcal S}_+,\|w\|=1}\ \sum_{a,s'}u(a)P_0(s'\mid s,a)w(s')\Big),$$

and $\epsilon_*=\min_s\epsilon_s$. The R² value function $v^{\pi,\mathrm R^2}$ of a policy and the R² optimal value $v^{*,\mathrm R^2}$ are the fixed points of $T^{\pi,\mathrm R^2}$ and $T^{*,\mathrm R^2}$.

Formalization targets

Goal: Theorem 5.1 (p. 8)

Under Assumption 5.1, $T^{*,\mathrm R^2}$ and every $T^{\pi,\mathrm R^2}$ have unique fixed points; a greedy policy $\pi^{*,\mathrm R^2}$ for $v^{*,\mathrm R^2}$ exists, and every such policy satisfies

$$v^{\pi^{*,\mathrm R^2},\mathrm R^2}=v^{*,\mathrm R^2}\ \ge\ v^{\pi,\mathrm R^2}\qquad\text{for all }\pi\in\Delta^{\mathcal S}_{\mathcal A};$$

every optimal policy is greedy; and when $\alpha^r_s>0$ for all $s$ the greedy policy is unique, hence the unique optimal R² policy.

Milestones

1. Proposition 2.1 (p. 3): for $\Omega$ strongly convex on the simplex, $\Omega^*(y)=\max_{a\in\Delta}\langle a,y\rangle-\Omega(a)$ is differentiable with Lipschitz gradient equal to the unique maximizer, satisfies $\Omega^*(y+c\mathbb 1)=\Omega^*(y)+c$, and is non-decreasing.
2. Proposition 5.1 (i) (p. 8): $v_1\le v_2$ implies $T^{\pi,\mathrm R^2}v_1\le T^{\pi,\mathrm R^2}v_2$ and $T^{*,\mathrm R^2}v_1\le T^{*,\mathrm R^2}v_2$.
3. Proposition 5.1 (iii) (p. 8):

$$\|T^{\pi,\mathrm R^2}v_1-T^{\pi,\mathrm R^2}v_2\|_\infty\le(1-\epsilon_*)\|v_1-v_2\|_\infty,\qquad \|T^{*,\mathrm R^2}v_1-T^{*,\mathrm R^2}v_2\|_\infty\le(1-\epsilon_*)\|v_1-v_2\|_\infty.$$

Significance

Theorem 5.1 is the R² counterpart of the fundamental theorem of discounted dynamic programming: optimal R² values are achieved by stationary policies obtained by a single greedy step. Together with the contraction of Proposition 5.1 (iii) it justifies the R² modified policy iteration algorithm of the paper, whose greedy step is a projection onto the simplex rather than a robust max–min problem. Combined with the first mission of the series, which identifies the robust value of an $s$-rectangular ball-constrained MDP with the optimum of an R²-regularized program, it gives a route to robust planning at the cost of regularized planning.

The results are proved in the paper (App. C), partly by reference to Geist, Scherrer and Pietquin (2019) for the optimality operator. No machine-checked proof of any of them exists; this mission produces the first. Prop. 2.1 is a general fact of convex analysis (Danskin-type smoothness of a conjugate on the simplex) that is reusable for any regularized MDP or entropy-regularized game.

Difficulty

The R² evaluation operator is not affine: the value regularizer $-\alpha^P_s\gamma\|\pi_s\|\,\|v\|$ is concave in $v$ and decreases as $\|v\|$ grows. Monotonicity therefore does not follow from the positivity of $P_0$ as in the standard case; it requires the second bound of Assumption 5.1, which compares the $\ell_2$ variation of $\|v\|$ with the minimal nonnegative bilinear form of $P_0(\cdot\mid s,\cdot)$. Likewise the contraction modulus is not $\gamma$ but $1-\epsilon_*$, because the regularizer is $\sqrt{|\mathcal S|}$-Lipschitz between the $\ell_2$ and sup norms. The optimality step of the classical proof uses linearity of $T^\pi$ when comparing values of policies; here only monotonicity and contraction are available. Uniqueness of the greedy policy rests on strict concavity on the simplex, which holds only when the regularization weight is positive.

Formalization scope

States and actions are finite nonempty types; transitions are arrays P₀ : S → A → S → ℝ with the published predicate IsTransitionKernel; value functions are S → ℝ with the pointwise order. The $\ell_2$-norm is an explicit l2norm (Mathlib's norm on S → ℝ is the sup norm, used only for $\|\cdot\|_\infty$). $T^{*,\mathrm R^2}v(s)$ is the real supremum over the simplex $\Delta_{\mathcal A}$ (attained), and the inner minimum of Assumption 5.1 is the real infimum over nonnegative $\ell_2$-unit vectors; the witnesses $\epsilon_s$ are explicit. Greedy policies are a predicate, never a function, and the R² value functions are not defined by choice: the goal asserts their existence and uniqueness and speaks about the fixed points.

Disclosed deviations from the page. Assumption 5.1 is a hypothesis of Theorem 5.1 (its proof assumes it). The uniqueness clause of Theorem 5.1 additionally assumes $\alpha^r_s>0$ for all $s$: with one state, two actions, zero reward and zero radii every policy is greedy and optimal. Proposition 2.1 assumes $\Omega$ continuous on the simplex, without which the maximum need not be attained, and strong convexity is Mathlib's StrongConvexOn for some modulus (norm-independent in finite dimension). Proposition 5.1 (ii) is false as printed and is not drafted: with one state, one action, $P_0=1$, $r_0=0$, $\gamma=1/2$, $\alpha^r=0$, $\alpha^P=1/2$, $\epsilon=1/4$, one has $Tv=v/2-|v|/4$, and $v_1=-1$, $c=1$ give $T(v_1+c)=0>-1/4=Tv_1+\gamma c$. Remark 5.1, Algorithm 1 and the $\ell_p$ variant of App. C.1 are out of scope. The inner minimum of Assumption 5.1 is $0$ whenever some $P_0(s'\mid s,a)=0$, forcing $\alpha^P_s=0$; this is the assumption as printed.

A formalization in which $\|\cdot\|$ is the sup norm, the inner minimum ranges over all unit vectors (making the assumption unsatisfiable), or the value functions are postulated rather than shown to exist would be trivial or wrong; the drafted statements avoid all three. Contributions welcome: Prop. 2.1 as a general convex-analysis lemma, Banach fixed-point plumbing for S → ℝ with the sup norm, and the strict concavity of $p\mapsto\langle p,q\rangle-c\|p\|$ on the simplex.

Selected references

• E. Derman, M. Geist, S. Mannor, Twice regularized MDPs and the equivalence between robustness and regularization, NeurIPS 2021. arXiv:2110.06267v1
• M. Geist, B. Scherrer, O. Pietquin, A theory of regularized Markov decision processes, ICML 2019. arXiv:1901.11275
• A. Nilim, L. El Ghaoui, Robust control of Markov decision processes with uncertain transition matrices, Operations Research 53(5), 2005. doi:10.1287/opre.1050.0216
• G. N. Iyengar, Robust dynamic programming, Mathematics of Operations Research 30(2), 2005. doi:10.1287/moor.1040.0129
• W. Wiesemann, D. Kuhn, B. Rustem, Robust Markov decision processes, Mathematics of Operations Research 38(1), 2013. doi:10.1287/moor.1120.0566
• A. Mensch, M. Blondel, Differentiable dynamic programming for structured prediction and attention, ICML 2018. arXiv:1802.03676

Motivation

The stochastic multi-armed bandit is the basic model of sequential decisions under uncertainty with partial feedback: a forecaster repeatedly picks one of $K$ options and observes only the reward of the option it picked. It models clinical trials, ad placement, routing and dynamic pricing, and is the building block of many reinforcement-learning algorithms. The question is how much reward is lost, compared with always playing the best option, through having to learn which option is best.

Chapter 2 of Bubeck and Cesa-Bianchi's monograph (arXiv:1204.5721v2) answers this for upper confidence bound (UCB) strategies.

• Lai and Robbins (1985) introduced upper confidence bounds and proved that the number of pulls of a suboptimal arm must grow at least logarithmically, with an explicit constant, for consistent strategies (doi:10.1016/0196-8858(85)90002-8).
• Agrawal (1995) gave simpler sample-mean-based index policies with logarithmic regret (doi:10.2307/1427934).
• Auer, Cesa-Bianchi and Fischer (2002) gave the finite-time analysis of UCB1 for bounded rewards (doi:10.1023/A:1013689704352).
• Bubeck and Cesa-Bianchi (2012) present the $(\alpha,\psi)$-UCB family, whose analysis needs only a bound $\psi$ on the cumulant generating function of the rewards, and the Lai–Robbins lower bound for Bernoulli rewards.

Setting

There are $K\ge2$ arms. Arm $i$ has an unknown reward distribution $\nu_i$ with mean $\mu_i$. At each round $t=1,2,\dots$ the forecaster selects an arm $I_t$ based on the past and receives a reward drawn from $\nu_{I_t}$, independently of the past. Write $\mu^*=\max_i\mu_i$, $\Delta_i=\mu^*-\mu_i$ for the gap of arm $i$, and $T_i(n)$ for the number of times arm $i$ is selected in rounds $1,\dots,n$. The pseudo-regret is

$$\overline R_n=n\mu^*-\mathbb E\sum_{t=1}^n\mu_{I_t}=\sum_{i=1}^K\Delta_i\,\mathbb E\,T_i(n).$$

Moment condition (2.2). There is a convex $\psi:\mathbb R\to\mathbb R$ with $\ln\mathbb E\,e^{\lambda(X-\mathbb EX)}\le\psi(\lambda)$ and $\ln\mathbb E\,e^{\lambda(\mathbb EX-X)}\le\psi(\lambda)$ for all $\lambda\ge0$ and every arm's reward $X$. Its Legendre–Fenchel transform is $\psi^*(\varepsilon)=\sup_{\lambda\in\mathbb R}(\lambda\varepsilon-\psi(\lambda))$. For $[0,1]$ rewards one may take $\psi(\lambda)=\lambda^2/8$, for which $\psi^*(\varepsilon)=2\varepsilon^2$.

$(\alpha,\psi)$-UCB. With $\hat\mu_{i,s}$ the mean of the first $s$ rewards of arm $i$, at round $t$ select

$$I_t\in\operatorname*{argmax}_{i}\Big[\hat\mu_{i,T_i(t-1)}+(\psi^*)^{-1}\Big(\frac{\alpha\ln t}{T_i(t-1)}\Big)\Big].$$

Formalization targets

Goal: Theorem 2.1 (p. 11)

If the rewards satisfy (2.2), then $(\alpha,\psi)$-UCB with $\alpha>2$ satisfies, for every $n$,

$$\overline R_n\le\sum_{i:\Delta_i>0}\Delta_i\Big(\frac{\alpha\ln n}{\psi^*(\Delta_i/2)}+\frac{\alpha}{\alpha-2}\Big).$$

This is the bound the book's proof establishes. The printed statement has $\alpha/(\alpha-2)$ in place of $\Delta_i\,\alpha/(\alpha-2)$; see Formalization scope.

Milestones

• The decomposition $\overline R_n=\sum_i\Delta_i\,\mathbb E\,T_i(n)$ (p. 9).
• The Cramér–Chernoff bound (2.3): $\mathbb P(\mu_i-\hat\mu_{i,s}>\varepsilon)\le e^{-s\psi^*(\varepsilon)}$.
• The three-event lemma (2.5)–(2.7) from the proof of Theorem 2.1.
• The bounded-reward bound (2.4): $\overline R_n\le\sum_{i:\Delta_i>0}\big(\frac{2\alpha}{\Delta_i}\ln n+\frac{\alpha}{\alpha-2}\big)$.
• The comparison (2.8): $2(p-q)^2\le\mathrm{kl}(p,q)\le(p-q)^2/(q(1-q))$.
• Theorem 2.2: for every strategy with $\mathbb E\,T_i(n)=o(n^a)$ on all Bernoulli instances, $\liminf_n\overline R_n/\ln n\ge\sum_{i:\Delta_i>0}\Delta_i/\mathrm{kl}(\mu_i,\mu^*)$.

Significance

Theorem 2.1 says that the cost of learning grows only logarithmically in the horizon, with a constant set by how well each suboptimal arm can be told apart from the best one. Theorem 2.2 shows that, up to constants, this cannot be improved: for Bernoulli rewards any strategy that is good on every instance must pay $\ln n$ per suboptimal arm, with constant $\Delta_i/\mathrm{kl}(\mu_i,\mu^*)$. By (2.8) this constant is at least of order $1/\Delta_i$, matching (2.4). Together they are the template for the analysis of most optimistic algorithms: KL-UCB, linear and contextual UCB, and UCB-style reinforcement learning.

All results of the chapter are classical and proved on paper. This mission makes them machine-checked in a common model. That model has an explicit pseudo-regret, an explicit (generalized) inverse of $\psi^*$, an explicit initialization rule for the algorithm, and a randomized-strategy model for the lower bound. Later chapters of the series and later papers on optimistic algorithms can build on it.

Difficulty

The deterministic part of the upper bound is short, so the main difficulty is probabilistic. The sample mean $\hat\mu_{i,T_i(t-1)}$ is taken over a random number of samples that depends on the algorithm's past. A Chernoff bound for a fixed sample size does not apply to it directly. The proof needs a union bound over all possible sample sizes, together with the representation in which the $s$-th reward of each arm is a fixed random variable. Summing the resulting tail $t^{1-\alpha}$ over rounds is where $\alpha>2$ enters.

The lower bound needs a change-of-measure argument between two Bernoulli instances, applied to a forecaster that may be randomized and never knows the horizon. Expressing "the forecaster cannot distinguish the instances" requires the law of the whole interaction under two environments.

Formalization scope

Model. Arms are Fin K with $2\le K$, rounds are $1,2,\dots$, and the natural logarithm is used. Rewards are a stack: $X_{i,k}$ is the reward of the $(k+1)$-st pull of arm $i$, all mutually independent, identically distributed per arm. For every strategy this gives the same law of arms and rewards as the book's protocol. $\mu^*$, $\Delta_i$ and $T_i(t)$ are the published definitions of ImprovedLinBandits.UCBDelta.armModel. The pseudo-regret is (2.1), $n\mu^*-\mathbb E\sum_t\mu_{I_t}$, not the expected regret. The arms played are measurable random variables, so that every expectation is genuine.

$\psi^*$ and its inverse. $\psi^*$ takes values in the extended reals. $(\psi^*)^{-1}(y)=\inf\{\varepsilon\ge0:\psi^*(\varepsilon)\ge y\}$.

Algorithm. The index is undefined while $T_i(t-1)=0$. Unplayed arms are therefore played first, so each arm is played once in rounds $1,\dots,K$. Ties are broken arbitrarily.

Corrected misprint. The book prints Theorem 2.1 with constant term $\alpha/(\alpha-2)$. Its proof yields $\Delta_i\,\alpha/(\alpha-2)$ (bound on $\mathbb E\,T_i(n)$ times $\Delta_i$). The printed form is false for Gaussian rewards with large gaps. The goal states the proof's version. (2.4) is correct as printed because $\Delta_i\le1$.

Constants. No O(·) appears in the chapter's statements. The constants are the book's: $\alpha/(\alpha-2)$ in Theorem 2.1 and (2.4), and the factor $2$ in (2.4) and (2.8).

Conventions made explicit.

1. $\psi(\lambda)\ge\psi(0)$ for $\lambda\le0$. Condition (2.2) constrains $\psi$ only on $\lambda\ge0$, while $\psi^*$ takes the supremum over all of $\mathbb R$. Without this convention, (2.3) and Theorem 2.1 are false (for example $\psi(\lambda)=c\lambda+\lambda^2/8$ with large $c$).
2. $\psi^*$ is finite on $[0,\infty)$.
3. $\psi^*(\Delta_i/2)>0$ for suboptimal arms.
4. $\varepsilon\ge0$ in (2.3).
5. $q\in(0,1)$ in (2.8).

Conventions 1–3 hold for every $\psi$ the book uses.

Theorem 2.2. The forecaster is a measurable rule from the history and a fresh uniform seed to an arm. It does not depend on the horizon. Consistency is required on every Bernoulli instance, every suboptimal arm and every $a>0$. A term with $\mu^*=1$ ($\mathrm{kl}=+\infty$) is $0$, and the $\liminf$ is taken in the extended reals. The book proves only $K=2$.

Ruled out. The algorithm cannot see unplayed rewards (its index uses only the sample means of rewards already received). Non-measurable arm choices, which would make the expectations vanish in Lean, are excluded. Consistency cannot be assumed only on the instance of the conclusion.

Needed infrastructure. Cramér–Chernoff bounds for sums of i.i.d. variables, Hoeffding's lemma, the stack representation of bandit interactions, and the divergence decomposition for randomized strategies. All are reusable beyond this mission, and contributions of any of them 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
• T. L. Lai, H. Robbins, Asymptotically efficient adaptive allocation rules, Advances in Applied Mathematics 6, 1985. doi:10.1016/0196-8858(85)90002-8
• R. Agrawal, Sample mean based index policies with O(log n) regret for the multi-armed bandit problem, Advances in Applied Probability 27, 1995. doi:10.2307/1427934
• P. Auer, N. Cesa-Bianchi, P. Fischer, Finite-time analysis of the multiarmed bandit problem, Machine Learning 47, 2002. doi:10.1023/A:1013689704352