Bandit Algorithms

Motivation

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

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

Setting

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

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

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

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

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

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

Formalization targets

Goal: Theorem 6.2, tuned

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

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

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

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

Selected references

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

Motivation

The multi-armed bandit is the simplest setting in which a learner must trade off exploiting what it knows against exploring what it does not: one situation, $k$ actions, and a reward drawn from an unknown distribution each time an action is taken. Chapter 2 of Sutton and Barto's Reinforcement Learning: An Introduction (2nd ed., MIT Press, 2018) uses it to introduce, in the smallest possible setting, ideas that run through the rest of the book: incremental estimation with a step size, the bias introduced by the initial estimate, soft-max policies over learned preferences, and learning by following the gradient of expected reward.

The chapter ends with the gradient bandit algorithm (§2.8), which learns a numerical preference for each action instead of a value estimate. A shaded box on pp. 38–40 shows that its expected update is exactly a gradient-ascent step on the expected reward, so the algorithm is an instance of stochastic gradient ascent. The same argument, a score-function (likelihood-ratio) identity with a baseline, reappears in Chapter 13 as the REINFORCE algorithm and the policy gradient theorem. The bandit case is where the book first carries it out in full.

Setting

Actions are $1, \dots, k$. Each action $x$ has a reward distribution $\nu_x$ on $\mathbb R$ with finite mean $q_*(x)$, the true action value. At each step the learner holds a vector of action preferences $H = (H(1), \dots, H(k)) \in \mathbb R^k$ and selects action $A$ with the soft-max probability

$$\pi(a) = \frac{e^{H(a)}}{\sum_{b=1}^k e^{H(b)}} \qquad (2.11).$$

Given $A = x$, a reward $R \sim \nu_x$ is received. The expected reward is $\mathbb E[R] = \sum_x \pi(x)\, q_*(x)$, a smooth function of $H$. With a step size $\alpha > 0$ and a baseline $B \in \mathbb R$, the gradient bandit update (2.12) is

$$H'(A) = H(A) + \alpha (R - B)(1 - \pi(A)), \qquad H'(a) = H(a) - \alpha (R - B)\,\pi(a) \ \ (a \ne A).$$

The chapter's estimation sections use a single action's rewards $R_1, R_2, \dots$. The sample average after $n-1$ selections is $Q_n = (R_1 + \cdots + R_{n-1})/(n-1)$, with an arbitrary initial value $Q_1$. A constant step size $\alpha \in (0,1]$ updates $Q_{n+1} = Q_n + \alpha [R_n - Q_n]$ (2.5). The trace of one $\bar o_0 = 0$, $\bar o_n = \bar o_{n-1} + \alpha (1 - \bar o_{n-1})$ defines the step size $\beta_n = \alpha / \bar o_n$ (2.8)–(2.9).

Formalization targets

Goal: the expected update is the gradient step

For every action $a$, with $A \sim \pi$ and $R \mid A = x \sim \nu_x$,

$$\mathbb E\bigl[H'(a)\bigr] = H(a) + \alpha\, \frac{\partial\, \mathbb E[R]}{\partial H(a)} ,$$

that is, the update (2.12) equals the exact gradient-ascent step (2.13) in expected value, for every baseline $B$ that does not depend on the selected action.

Milestones

1. (2.3): $Q_{n+1} = Q_n + \tfrac1n [R_n - Q_n]$ for $n \ge 1$, including $Q_2 = R_1$ for arbitrary $Q_1$.
2. (2.6): $Q_{n+1} = (1-\alpha)^n Q_1 + \sum_{i=1}^n \alpha(1-\alpha)^{n-i} R_i$, with weights summing to one.
3. Exercise 2.7: with $\beta_n = \alpha/\bar o_n$, $Q_{n+1} = \sum_{i=1}^n \frac{\alpha(1-\alpha)^{n-i}}{\bar o_n} R_i$ for $n \ge 1$, weights summing to one, and no dependence on $Q_1$.
4. Shift invariance (p. 37): adding a constant $c$ to every preference leaves $\pi$ unchanged.
5. Exercise 2.9: for $k = 2$, $\pi(1) = \sigma(H(1) - H(2))$ with $\sigma(x) = 1/(1+e^{-x})$.
6. Soft-max derivative (p. 40): $\partial \pi(x)/\partial H(a) = \pi(x)(\mathbb 1_{a=x} - \pi(a))$.
7. Zero-sum gradient (p. 39): $\sum_x \partial \pi(x)/\partial H(a) = 0$.
8. Performance gradient as an expectation (p. 39): $\partial \mathbb E[R]/\partial H(a) = \mathbb E[(R - B)(\mathbb 1_{a=A} - \pi(a))]$.

Significance

The result. The identity makes a model-free algorithm, which uses only the sampled action and reward, an unbiased estimator of the gradient of a quantity that depends on the unknown $q_*$. It therefore places the gradient bandit algorithm within stochastic approximation, where convergence theory for stochastic gradient methods applies. It also explains the role of the baseline: any baseline independent of the action leaves the expected update unchanged, so the choice of baseline can only affect the variance of the update, as Figure 2.5 shows empirically. The estimation milestones make precise two claims the chapter uses repeatedly: sample averages can be maintained incrementally, and constant step sizes produce an exponentially recency-weighted average biased by $Q_1$. Exercise 2.7 removes that bias.

Formalizing it. All of these results are elementary and proved (or left as routine exercises) in the book. None of them is formalized on Prove2Me or, as far as is known, in Mathlib. What this mission adds is a machine-checked version of the book's argument with the reward model and baseline condition stated precisely, and a reusable soft-max layer (definition, partial derivatives, shift invariance) for later missions of this series, in particular the policy gradient theorem of Chapter 13.

Difficulty

The mathematics is beginning calculus, as the book says. The formal difficulty lies elsewhere. The goal is an identity between an expectation over a two-stage random experiment (an action from $\pi$, then a reward from $\nu_A$) and a partial derivative in one coordinate of a vector-valued parameter. A proof has to justify exchanging the finite sum with the derivative and splitting the reward integral, and it has to use integrability of each $\nu_x$. It also needs the fact that the baseline term vanishes because $\sum_x \partial\pi(x)/\partial H(a) = 0$. A scalar-parameter version of the log-sum-exp derivative does not suffice: the book differentiates in one coordinate $H(a)$ while all other preferences are held fixed. For Exercise 2.7 the obvious unrolling of (2.6) does not apply directly, because the step size $\beta_n$ varies with $n$ and the book states neither the weights nor the range of $\alpha$.

Formalization scope

• Actions are Fin k. Every statement quantifies over some action, so $k \ge 1$ whenever it has content. Preferences are vectors Fin k → ℝ. The partial derivative in coordinate $a$ is the derivative of $h \mapsto f(\text{update } H\ a\ h)$ at $H(a)$. The soft-max derivative milestone is stated with HasDerivAt, so it also asserts differentiability.
• Rewards: each $\nu_x$ is a probability measure on $\mathbb R$ with Integrable identity and mean $q_*(x)$. The expectation of a function of $(A, R)$ is $\sum_x \pi(x) \int \cdot \, d\nu_x$. The book's normal-distribution testbed is only an example.
• The baseline is a fixed real $B$, the book's "any scalar that does not depend on" the action (pp. 39–40). The book's $B_t = \bar R_t$, the average of past rewards, is covered once one conditions on the past. Footnote 1 on p. 37 states that the chapter's experiments used a $\bar R_t$ that also included $R_t$. That baseline depends on $A_t$, and the identity does not cover it.
• Rewards of one action are a sequence indexed from $1$. $Q_1$ is arbitrary, and $0^0 = 1$ as in the book (p. 33), so $\alpha = 1$ is included in (2.6).
• Exercise 2.7 speaks of "a conventional constant step size $\alpha > 0$". The formalization takes $\alpha \in (0,1]$, the range of the constant step size in (2.5). For $\alpha = 2$ the trace $\bar o_n$ vanishes at every even $n$ and $\beta_n$ is undefined. "Without initial bias" is read as "for $n \ge 1$, $Q_{n+1}$ is the displayed weighted average of $R_1, \dots, R_n$ with weights summing to one", which in particular does not involve $Q_1$.
• Exercise 2.9 is read as the two equalities $\pi(1) = \sigma(H(1)-H(2))$ and $\pi(2) = \sigma(H(2)-H(1))$.
• A trivializing formalization is ruled out: the goal is about the expected value of the algorithm's update (2.12) under the joint law of action and reward, not the soft-max derivative alone and not a version in which the reward is replaced by its mean or the expectation is taken over $A$ only.
• Not formalized: the UCB rule (2.10) and the 10-armed testbed, which carry no provable claim in the chapter, and the stochastic-approximation conditions (2.7), which the book cites without proof.
• Welcome contributions: a general soft-max library (derivatives, Jacobian, log-sum-exp) over a finite type, reusable for Chapter 13, and proofs of the milestones in the listed order.

Selected references

• R. S. Sutton, A. G. Barto, Reinforcement Learning: An Introduction, 2nd ed., MIT Press, 2018, ISBN 9780262039246, Chapter 2, pp. 25–46. http://incompleteideas.net/book/the-book-2nd.html
• R. J. Williams, Simple statistical gradient-following algorithms for connectionist reinforcement learning, Machine Learning 8 (1992) 229–256. https://doi.org/10.1007/BF00992696
• H. Robbins, S. Monro, A stochastic approximation method, Annals of Mathematical Statistics 22 (1951) 400–407. https://doi.org/10.1214/aoms/1177729586

Motivation

In best arm identification with fixed confidence, a learner samples $K$ unknown distributions ("arms") sequentially and must name the arm with the largest mean, with error probability at most a prescribed $\delta$, using as few samples as possible. Garivier and Kaufmann (arXiv:1602.04589, COLT 2016) showed that every $\delta$-PAC strategy needs, in expectation, at least $T^*(\boldsymbol\mu)\,\mathrm{kl}(\delta,1-\delta)$ samples, where the characteristic time $T^*(\boldsymbol\mu)$ is the value of a max–min optimization problem over the proportions of draws allocated to the arms. The maximizer of that problem, $w^*(\boldsymbol\mu)$, is the allocation any asymptotically optimal strategy must follow; the Track-and-Stop algorithm of the same paper computes $w^*(\hat{\boldsymbol\mu})$ at plug-in estimates and tracks it.

A strategy can only track $w^*$ if $w^*$ can be computed. This mission formalizes the part of the paper (Section 2.2 and Appendix A) that turns the abstract max–min problem into an explicit recipe: a closed form for the inner infimum, and a characterization of $w^*$ through the root of one increasing scalar function. The problem had been solved in closed form before only for special cases, such as Poisson rewards with all suboptimal arms equal (Vaidhyan and Sundaresan, 2015); the paper's result covers every one-parameter exponential family.

Setting

A canonical one-parameter exponential family is a family of laws $\nu_\theta$, $\theta\in\Theta$, on $\mathbb R$ with density $\exp(\theta x-b(\theta))$ with respect to a reference measure $\xi$. The law $\nu_\theta$ has mean $\dot b(\theta)$; the set of attainable means is the mean space $\dot b(\Theta)$. For means $\mu=\dot b(\theta)$ and $\mu'=\dot b(\theta')$ the Kullback–Leibler divergence is

$$d(\mu,\mu')=\mathrm{KL}(\nu_\theta,\nu_{\theta'})=b(\theta')-b(\theta)-\dot b(\theta)(\theta'-\theta).$$

Bernoulli laws and Gaussian laws with known variance are the standard examples.

A bandit model is identified with its vector of means $\boldsymbol\mu=(\mu_1,\dots,\mu_K)\in\dot b(\Theta)^K$. $\mathcal S$ is the set of models with a unique optimal arm $a^*(\boldsymbol\mu)$, and $\mathrm{Alt}(\boldsymbol\mu)=\{\boldsymbol\lambda\in\mathcal S:a^*(\boldsymbol\lambda)\ne a^*(\boldsymbol\mu)\}$ is the set of alternatives. $\Sigma_K$ is the probability simplex. The transportation cost of proportions $w\in\Sigma_K$ and the objects of the paper are

$$c_{\boldsymbol\mu}(w)=\inf_{\boldsymbol\lambda\in\mathrm{Alt}(\boldsymbol\mu)}\sum_{a=1}^Kw_a\,d(\mu_a,\lambda_a),\qquad T^*(\boldsymbol\mu)^{-1}=\sup_{w\in\Sigma_K}c_{\boldsymbol\mu}(w),\qquad w^*(\boldsymbol\mu)=\operatorname*{argmax}_{w\in\Sigma_K}c_{\boldsymbol\mu}(w).$$

The arms are sorted so that $\mu_1>\mu_2\ge\dots\ge\mu_K$. The parameterized Jensen–Shannon divergence is, for $\alpha\in[0,1]$,

$$I_\alpha(\mu_1,\mu_2)=\alpha\,d\big(\mu_1,\alpha\mu_1+(1-\alpha)\mu_2\big)+(1-\alpha)\,d\big(\mu_2,\alpha\mu_1+(1-\alpha)\mu_2\big).$$

For $a\in\{2,\dots,K\}$ let $g_a(x)=(1+x)I_{1/(1+x)}(\mu_1,\mu_a)$ for $x\ge0$, let $x_a=g_a^{-1}$, and let $x_1\equiv1$. Finally

$$F_{\boldsymbol\mu}(y)=\sum_{a=2}^K\frac{d\big(\mu_1,m_a(y)\big)}{d\big(\mu_a,m_a(y)\big)},\qquad m_a(y)=\frac{\mu_1+x_a(y)\mu_a}{1+x_a(y)}.$$

Formalization targets

Goal: Theorem 5 (p. 5)

With $D=d(\mu_1,\mu_2)$: $F_{\boldsymbol\mu}$ is continuous and strictly increasing on $[0,D[$, $F_{\boldsymbol\mu}(0)=0$, $F_{\boldsymbol\mu}(y)\to\infty$ as $y\to D$, the equation $F_{\boldsymbol\mu}(y)=1$ has a unique solution $y^*\in[0,D[$, and

$$w\in w^*(\boldsymbol\mu)\iff w_a=\frac{x_a(y^*)}{\sum_{i=1}^Kx_i(y^*)}\quad\text{for every arm }a.$$

The equivalence says at once that the argmax exists, that it is a single point, and that it is given by eq. (5).

Milestones

1. Lemma 3 (p. 5): for every $w\in\Sigma_K$,

$$c_{\boldsymbol\mu}(w)=\min_{a\ne1}(w_1+w_a)\,I_{\frac{w_1}{w_1+w_a}}(\mu_1,\mu_a).$$

2. Claim after eq. (4) (p. 5): $g_a$ is a strictly increasing one-to-one mapping from $[0,+\infty[$ onto $[0,d(\mu_1,\mu_a)[$.
3. Lemma 4 (p. 5): for every maximizer $w^*$ and all $a,b\in\{2,\dots,K\}$,

$$(w^*_1+w^*_a)I_{\frac{w^*_1}{w^*_1+w^*_a}}(\mu_1,\mu_a)=(w^*_1+w^*_b)I_{\frac{w^*_1}{w^*_1+w^*_b}}(\mu_1,\mu_b).$$

Significance

The result. Theorem 5 reduces a $(K-1)$-dimensional non-smooth max–min problem to finding the root of one continuous increasing function on a bounded interval, each evaluation of which requires $K-1$ scalar inversions. It gives existence and uniqueness of $w^*(\boldsymbol\mu)$, which the paper's lower bound only presupposes, and it is the computational core of Track-and-Stop: without an explicit, well-posed $w^*$ the tracking strategy is not defined. Lemma 3 alone gives the closed form of the inner infimum used again in the analysis of the stopping rule.

Formalizing it. The results are proved in the paper; nothing here is open. To the best of our knowledge none of them has a machine-checked proof: the platform's existing best-arm-identification rows concern Gaussian arms and state the characteristic time at the level of measures, without this characterization. The mission produces a checked reduction for general one-parameter exponential families, including the edge cases the text passes over (ties among suboptimal arms, zero weights, the behaviour of $x_a$ near the end of its domain).

Difficulty

The infimum in Lemma 3 ranges over $\mathrm{Alt}(\boldsymbol\mu)$, a set of models with a unique best arm, so it is an open condition: the minimizing configuration, in which $\lambda_1$ and $\lambda_a$ coincide, lies outside $\mathrm{Alt}(\boldsymbol\mu)$ and is only approached. Other arms may also compete for the best position. A statement in which the infimum is taken over the closed relaxation $\{\lambda_a\ge\lambda_1\}$ is a lemma of the proof, not Lemma 3.

For Theorem 5, the equalization in Lemma 4 needs an argument that holds for every maximizer, not only for one found by a first-order condition, because the objective is a minimum of functions and is not differentiable. The monotonicity of $F_{\boldsymbol\mu}$ needs the monotonicity of each $x_a$ and of each ratio in the moving point $m_a$, and the limit at $D$ rests on the second-best arm(s) only, which is where the ordering $\mu_1>\mu_2\ge\dots$ enters. Finally the analytic facts about $d$ (continuity, positivity off the diagonal, monotonicity in each argument) must be derived from the exponential family itself.

Formalization scope

Lean represents a model by μ : Fin K → ℝ with 2 ≤ K and every μ a in the mean space deriv F.b '' F.Θ. The paper's arm $1$ is index 0, arm $2$ is index 1. The exponential family is a structure ExpFamily whose parameter set is a nonempty open interval and whose b is twice continuously differentiable with $\ddot b>0$ on $\Theta$. These two conditions are added to the paper's "convex, twice differentiable" and are disclosed: strict convexity is what makes the mean parameterization unique, and openness is what lets alternatives approach the boundary of $\mathrm{Alt}(\boldsymbol\mu)$. The reference measure and normalization are part of the structure but unused here.

The transportation cost is an infimum in EReal, so it is the true infimum of the set of values rather than a default 0. $w^*(\boldsymbol\mu)$ is never defined by choice: "$w$ is optimal" is a predicate, and Theorem 5 characterizes the set of such $w$. The functions $x_a$ are the inverse of $g_a$ on $[0,+\infty[$ and are evaluated only on $[0,d(\mu_1,\mu_2)[$. "Increasing" in Theorem 5 is stated as strictly increasing, as proved in Appendix A.2. Lemmas 3 and 4 and the claim on $g_a$ assume only that arm $1$ is the unique best arm, which is weaker than the paper's standing ordering.

A formalization that replaces $\mathrm{Alt}(\boldsymbol\mu)$ by $\{\lambda_a\ge\lambda_1\}$, assumes the maximizer exists and is unique, or asserts only existence of some $y^*$ without the formula for $w^*$, does not state these results and is ruled out.

A complete development needs: basic calculus of exponential families (the Bregman form of $d$, its continuity and strict positivity off the diagonal, its monotonicity in the second argument), the inverse function of a continuous strictly monotone map on an interval, and compactness of the simplex. The divergence facts are reusable in every bandit mission built on exponential families. Proofs of the milestones, of auxiliary facts about $d$ and $I_\alpha$, and a sorry-free instance of ExpFamily (Bernoulli or unit-variance Gaussian) are welcome.

Selected references

• A. Garivier, E. Kaufmann, Optimal Best Arm Identification with Fixed Confidence, COLT 2016 (JMLR W&CP 49), arXiv:1602.04589v2. https://arxiv.org/abs/1602.04589
• E. Kaufmann, O. Cappé, A. Garivier, On the Complexity of Best-Arm Identification in Multi-Armed Bandit Models, JMLR 17, 2016. https://arxiv.org/abs/1407.4443
• N. K. Vaidhyan, R. Sundaresan, Learning to detect an oddball target, arXiv:1508.05572, 2015. https://arxiv.org/abs/1508.05572
• O. Cappé, A. Garivier, O.-A. Maillard, R. Munos, G. Stoltz, Kullback–Leibler upper confidence bounds for optimal sequential allocation, Annals of Statistics 41(3), 2013. https://arxiv.org/abs/1210.1136

Motivation

In the contextual bandit problem a learner repeatedly observes a context, picks one of $K$ actions, and sees the reward of that action only. Against a finite class $\Pi$ of policies, statistically optimal regret of order $\sqrt{KT\ln|\Pi|}$ has been known since EXP4 (Auer et al., 2002), but EXP4 maintains a weight per policy and costs $\Omega(|\Pi|)$ time per round. For the large policy classes used in practice (linear classifiers, trees), that is prohibitive.

The oracle-efficient line of work accesses $\Pi$ only through a cost-sensitive classification oracle (an arg max oracle, AMO). The RandomizedUCB algorithm of Dudík et al. (2011) obtains optimal regret with polynomially many oracle calls by solving a convex program in each round, but the number of calls is large. Agarwal, Hsu, Kale, Langford, Li and Schapire (2014) replace that solver by a coordinate descent method whose number of iterations, and hence of oracle calls, is bounded independently of $|\Pi|$. Their algorithm, ILOVETOCONBANDITS, and its practical variant are now standard references for oracle-based exploration.

This mission formalizes the optimization half of that paper: Algorithm 2 solves the per-epoch problem (OP) after at most $4\ln(1/(K\mu))/\mu$ coordinate steps.

Setting

Let $A=\{0,\dots,K-1\}$ be the actions, $X$ any set of contexts, and $\Pi\subseteq A^X$ a finite nonempty set of policies. A history $H_t$ is a sequence of $t\ge1$ records $(x_i,a_i,r_i(a_i),p_i(a_i))$ with $r_i(a_i)\in[0,1]$ the observed reward and $p_i(a_i)\in(0,1]$ the probability with which $a_i$ was chosen. Write $\widehat{\mathbb E}_{x\sim H_t}[f(x)]=\frac1t\sum_i f(x_i)$.

The inverse propensity scoring estimate (Eq. (1)) is

$$\widehat{\mathcal R}_t(\pi)=\frac1t\sum_{i=1}^t\frac{r_i(a_i)\,\mathbb 1\{\pi(x_i)=a_i\}}{p_i(a_i)},$$

the estimated regret is $\widehat{\mathrm{Reg}}_t(\pi)=\max_{\pi'\in\Pi}\widehat{\mathcal R}_t(\pi')-\widehat{\mathcal R}_t(\pi)$, and for a minimum probability $\mu$ one sets $b_\pi=\widehat{\mathrm{Reg}}_t(\pi)/(\psi\mu)$ with $\psi=100$.

Weights are vectors $Q\in\mathbb R^\Pi$; $\Delta^\Pi$ is the set of nonnegative $Q$ with $\sum_\pi Q(\pi)\le1$. The smoothed projection of $Q$ is

$$Q^\mu(a\mid x)=(1-K\mu)\sum_{\pi:\ \pi(x)=a}Q(\pi)+\mu .$$

The optimization problem (OP) asks for $Q\in\Delta^\Pi$ with

$$\sum_{\pi\in\Pi}Q(\pi)b_\pi\le2K\quad(2),\qquad \widehat{\mathbb E}_{x\sim H_t}\Bigl[\frac1{Q^\mu(\pi(x)\mid x)}\Bigr]\le2K+b_\pi\ \ \forall\pi\in\Pi\quad(3).$$

Algorithm 2 starts from $Q_{\mathrm{init}}$ and loops. With $V_\pi(Q)=\widehat{\mathbb E}[1/Q^\mu(\pi(x)\mid x)]$, $S_\pi(Q)=\widehat{\mathbb E}[1/Q^\mu(\pi(x)\mid x)^2]$ and $D_\pi(Q)=V_\pi(Q)-(2K+b_\pi)$: if $\sum_\pi Q(\pi)(2K+b_\pi)>2K$ it rescales $Q$ by $c=2K/\sum_\pi Q(\pi)(2K+b_\pi)$ (Eq. (4)); then, if some $\pi$ has $D_\pi(Q)>0$, it adds

$$\alpha_\pi(Q)=\frac{V_\pi(Q)+D_\pi(Q)}{2(1-K\mu)S_\pi(Q)}$$

to $Q(\pi)$ (Step 8) and repeats; otherwise it halts and outputs $Q$.

The analysis uses the potential (Eq. (6)), with $\tau=t$ and $\mathcal U_A$ uniform on $A$,

$$\Phi_m(Q)=\tau\mu\left(\frac{\widehat{\mathbb E}_x[\mathrm{RE}(\mathcal U_A\,\|\,Q^\mu(\cdot\mid x))]}{1-K\mu}+\frac{\sum_\pi Q(\pi)b_\pi}{2K}\right),\qquad \mathrm{RE}(p\|q)=\sum_a\bigl(p_a\ln\tfrac{p_a}{q_a}+q_a-p_a\bigr).$$

Formalization targets

Goal: Theorem 3 (p. 6)

For $0<\mu\le1/(2K)$, Algorithm 2 with $Q_{\mathrm{init}}=\mathbf 0$ satisfies: every run executes Step 8 at most

$$\frac{4\ln(1/(K\mu))}{\mu}$$

times, whatever policy each Step 8 chooses among those with $D_\pi>0$; and when it halts, its output solves (OP). The bound depends on $K\mu$ only, not on $|\Pi|$ or $t$.

Milestones

1. Lemma 5 (p. 10). If Algorithm 2 halts and outputs $Q$, then $Q$ satisfies (2), (3) and $\sum_\pi Q(\pi)\le1$.
2. Lemma 6 (p. 10). If $\sum_\pi Q(\pi)(2K+b_\pi)>2K$ and $c$ is as in Eq. (4), then $\Phi_m(cQ)\le\Phi_m(Q)$.
3. Lemma 7 (p. 10). If $D_\pi(Q)>0$ and $Q'$ adds $\alpha_\pi(Q)$ to $Q(\pi)$, then

$$\Phi_m(Q)-\Phi_m(Q')\ge\frac{\tau\mu^2}{4(1-K\mu)}.$$

Significance

The result. Theorem 3 is what makes ILOVETOCONBANDITS computationally efficient: each call of Algorithm 2 is implemented with one AMO call per iteration (Lemma 1 of the paper), so the oracle complexity of an epoch is $O(\ln(1/(K\mu))/\mu)$. Combined with the epoch schedule and warm start, this gives the paper's total of $\tilde O(\sqrt{KT/\ln(|\Pi|/\delta)})$ oracle calls over $T$ rounds. Theorem 3 also gives a constructive proof that (OP) is feasible for every history, which the regret analysis (a separate mission in this series) assumes.

Formalizing it. The result is proved in the paper, with complete proofs of Lemmas 5–7 in Appendix D. No machine-checked version is known. The formalization would give a checked termination bound for a coordinate descent method on a non-smooth feasibility problem, with a fully explicit constant, and a verified definition of the unnormalized relative entropy potential that is reusable for other smoothed-projection analyses (e.g. RandomizedUCB-type convex programs).

Difficulty

Termination cannot be read off the constraints. Step 8 raises one weight and can push the total weight above 1, after which Step 5 shrinks every coordinate, so no constraint and no single weight moves monotonically along a run. The number of policies that violate (3) can also go up after a step. Bounding the number of iterations therefore needs a global quantity that tracks progress through both kinds of step. The rescaling step is the harder of the two: it lowers every $Q^\mu(a\mid x)$ at once, which pushes the relative-entropy term the wrong way, and it must be offset by the drop in the regret term. Knowing that (OP) is feasible, or that some convex function has a minimizer, bounds nothing about how many steps a particular method takes; that is the obvious approach, and it gives no count.

Formalization scope

• Actions are Fin K with $K\ge1$; contexts form an arbitrary type (no measure is needed: Theorem 3 is deterministic). $\Pi$ is a nonempty Finset (X → Fin K); weights are real functions on its subtype.
• Histories are indexed by Fin t with $t\ge1$ (0-based indices). The paper allows $p_i(a_i)\in[0,1]$; the formalization requires $p_i(a_i)\in(0,1]$, since Eq. (1) divides by it.
• $\widehat{\mathrm{Reg}}_t(\pi)$ is written as $\max_{\pi'}\widehat{\mathcal R}_t(\pi')-\widehat{\mathcal R}_t(\pi)$, which equals $\widehat{\mathcal R}_t(\pi_t)-\widehat{\mathcal R}_t(\pi)$ for any maximizer $\pi_t$; $\psi=100$ is hard-wired in $b_\pi$.
• $Q^\mu$, $V_\pi$, $S_\pi$, (OP) and $\Phi_m$ all use the smoothed projection of the unnormalized weights; there is no default policy in this mission.
• $\mu$ ranges over $(0,1/(2K)]$, the range of $\mu_m$ in Algorithm 1 that the printed theorem refers to. $\tau$ in $\Phi_m$ is the history length $t$.
• Algorithm 2 is encoded relationally. A run of length $n$ from $Q_{\mathrm{init}}$ is a sequence $Q^{(0)}=Q_{\mathrm{init}},\dots,Q^{(n)}$ in which each $Q^{(k+1)}$ is Step 8, for some policy with $D_\pi>0$, applied to the rescaled $Q^{(k)}$. It halts at $Q^{(n)}$ when no policy has $D_\pi>0$ after rescaling, and it then outputs the rescaled $Q^{(n)}$. "Iterations" means executions of Step 8. The last pass, which halts at Step 10, is not counted: the paper's proof bounds "the number of times Step 8 is executed". The bound is compared in $\mathbb R$, without rounding.
• Lemmas 5–7 are stated for nonnegative weight vectors without a bound on their sum, because Algorithm 2 rescales vectors whose sum may exceed 1. Lemma 7's "$\alpha=\alpha_\pi(Q)>0$" is part of its conclusion.
• A trivializing formalization is ruled out: the goal quantifies over every run from $\mathbf 0$ and every choice in Step 8, not over some run, and the potential, $b_\pi$ and $D_\pi$ are computed from the history rather than taken as free parameters.
• The auxiliary facts $\Phi_m\ge0$ and $\Phi_m(\mathbf 0)\le\tau\mu\ln(1/(K\mu))/(1-K\mu)$ are inline claims in the paper and are not stated separately; contributions stating and proving them are welcome, as are general lemmas on the unnormalized relative entropy.
• Out of scope: the regret bound (Theorem 2) and the probabilistic model (mission I of this series), the AMO implementation (Lemma 1), warm start and epoch-level oracle counts (Lemmas 2, 3, 8), and the support lower bound (Theorem 4).

Selected references

• A. Agarwal, D. Hsu, S. Kale, J. Langford, L. Li, R. E. Schapire, Taming the Monster: A Fast and Simple Algorithm for Contextual Bandits, ICML 2014; arXiv:1402.0555v2. https://arxiv.org/abs/1402.0555
• M. Dudík, D. Hsu, S. Kale, N. Karampatziakis, J. Langford, L. Reyzin, T. Zhang, Efficient Optimal Learning for Contextual Bandits, UAI 2011. https://arxiv.org/abs/1106.2369
• P. Auer, N. Cesa-Bianchi, Y. Freund, R. E. Schapire, The Nonstochastic Multiarmed Bandit Problem, SIAM J. Comput. 32(1), 2002. https://doi.org/10.1137/S0097539701398375