Bandit Algorithms

Motivation

Many demand, traffic and click-through series are seasonal: their mean repeats after a fixed number of periods (a week of days, a year of months), while the length of that cycle is not known in advance. A retailer choosing among $K$ promotions, or a platform choosing among $K$ recommendations, then faces a multi-armed bandit whose arms have time-varying but periodic mean rewards. Standard stochastic bandit algorithms assume stationary means and fail here, and fully adversarial or arbitrarily drifting models give up the structure that periodicity offers.

N. Chen, C. Wang and L. Wang (arXiv:2005.08088, Operations Research, 2025) propose a two-stage policy for this problem: a spectral first stage that estimates every arm's period from a short exploration phase, and a confidence-bound second stage that learns and exploits the resulting "effective arms". Their main upper bound, Theorem 1, shows that the policy's regret grows like $\sqrt{T\sum_k T_k}$ up to logarithmic factors. This mission formalizes that theorem and the chain of lemmas behind it. The matching lower bound (Theorem 3 of the paper) is the subject of a separate mission of this series.

Setting

At each epoch $t=1,\dots,T$ a decision maker pulls one of $K$ arms. Pulling arm $k$ at epoch $t$ yields the reward $Y_{k,t}=\mu_{k,t}+\epsilon_t$. The mean $\mu_{k,t}$ has a minimum period $T_k\ge1$: $\mu_{k,t+T_k}=\mu_{k,t}$ for all $t\ge1$, and no smaller positive shift has this property. The standing assumptions are:

• Assumption 1: $\mu_{k,t}\in[0,1]$.
• Assumption 2: the noises $\epsilon_t$ are independent and sub-Gaussian with parameter $\sigma$, i.e. $\mathbb E[e^{\lambda\epsilon_t}]\le e^{\sigma^2\lambda^2/2}$ for all real $\lambda$ and $\mathbb P(|\epsilon_t|>x)\le2e^{-x^2/(2\sigma^2)}$.

The pseudo-regret of an arm sequence $\pi$ is $R^\pi_T=\sum_{t=1}^T(\max_k\mu_{k,t}-\mu_{\pi_t,t})$, and the number of effective arms is $d=\sum_{k=1}^KT_k$: arm $k$ at phase $t \bmod T_k$ is one effective arm.

Stage one (Algorithm 1). Each arm is pulled $n$ times in a row. From its $n$ rewards the policy computes the periodogram $|\tilde y_k(v)|$, the modulus of the discrete Fourier transform $\tilde y_k(v)=\frac1n\sum_sY_{k,s}e^{-2\pi ivs}$, on $v\in[0,1/2]$. A data-driven threshold $\tau_k$ is computed from the constants $U_1,U_2$ (sums of sinc-type maxima), $\bar\epsilon_v=\frac{2\sigma H}{1-\pi/24}\sqrt{\log(n)/n}$ and $\sup_v|\tilde y_k(v)|$. The algorithm repeatedly takes the highest peak above $\tau_k$ in $[g/n,1/2]$, snaps it to the nearest fraction $j_1/j_2$ with $j_2<n/(2g)$, and removes a $2g/n$-neighbourhood. The period estimate $\hat T_k$ is the least common multiple of the selected reciprocals.

Stage two (Algorithm 2). At every later epoch an $S$-round screening tournament, $S=\lfloor\log_2T\rfloor$, compares the arms at their current phases modulo $\hat T_k$. It uses estimated means $m^{(s)}_{k,t}$ and widths $w^{(s)}_{k,t}$ pooled from the stage-one samples and from round-specific index sets $\Psi^{(s)}(t)$. The weak oracle runs the same policy with the true periods in place of $\hat T_k$.

The parameters are fixed by (7): $n=\lfloor\sqrt{T/K}\rfloor$, $g=\lceil\sqrt n\rceil$, $H=\sqrt{1+\log n}$. Assumption 3 asks $T>4K$, $g\ge\max\{2,\sqrt n\}$ and $T_k<n/(2g)$. Assumption 4 asks the smallest present Fourier coefficient $b_k$ of each arm to dominate a combination of $\bar\epsilon_v$ and the largest coefficient $B_k$.

Formalization targets

Goal: Theorem 1

Under Assumptions 1–4 and (7), the two-stage policy satisfies

$$\mathbb E\big[R^\pi_T\big]\le C\sqrt{T\,d\,\log^2(T)\,\log(T/d)} ,$$

with $C$ depending only on $\sigma$ and $K$, and with Algorithm 2 run at $\delta=8/T$.

Stage one: correct period identification

• Lemma 1: uniform noise bound for the periodogram, $48n\exp(-(n\delta^2/4\sigma^2)(1-\pi/24)^2)$.
• Lemmas 2–3: leakage bounds $\pi B_kU_1$, $\pi B_kU_2$, and $B_k\le(\sup|\tilde\epsilon_k|+\sup|\tilde y_k|)/(1-\pi U_2)$.
• Lemmas 4–5: the threshold separates the neighbourhoods of the present frequencies from the rest, with probability $1-48/n^{H^2-1}$.
• Lemmas 6–7: the sharper noise bound near possible present frequencies, and the location of the peaks within $1/n$ of them.
• Theorem 2: $\mathbb P(\Lambda)\ge1-48K/n^{H^2-1}-200K/n^{0.867H^2-1}-200K/n^{0.6934H^2-1}$.

Stage two: the oracle's regret

• Lemma 15: an anytime sub-Gaussian deviation bound.
• Lemma 9: the confidence event $\mathcal E$ has probability at least $1-\delta S$.
• Lemma 10: on $\mathcal E$ the optimal arm survives screening, and each epoch's gap is at most $1$, $8\sigma/2^s$ or $2\sigma/\sqrt T$.
• Lemma 16: the summed widths of a round are at most $4\sigma\sqrt{|\Psi^{(s)}(T)|\,d\log(8T/\delta)\log(T/d)}$.
• Lemma 11: the oracle's expected regret is at most $C\sqrt{Td\log^2(T)\log(T/d)}$ with $C$ depending only on $\sigma$.

Significance

The theorem shows that unknown seasonality costs only the factor $\sqrt{d}=\sqrt{\sum_kT_k}$ that would be paid if every phase of every arm were a separate stationary arm. Up to logarithmic factors this matches the $\sqrt{TK}$ rate of the classical stationary bandit with $d$ arms in place of $K$. Together with the paper's lower bound $\Omega(\sqrt{T\max_kT_k})$ it locates the minimax regret of periodic bandits within a factor $\sqrt K$. Stage one is a non-asymptotic, finite-sample period-identification guarantee for a thresholded periodogram, which is of independent use in spectral estimation.

The paper proves these results; none of them is machine-checked. A complete development yields a verified finite-sample periodogram theory (noise bounds for random trigonometric polynomials, Dirichlet-kernel leakage estimates), a verified anytime sub-Gaussian inequality, and a verified analysis of a nested elimination algorithm with data reuse. The formalization also pins down several points the printed text leaves open: the constant $0.233$ of Lemma 6 and the exponent $0.694$ of Lemma 7 and Theorem 2 are slightly stronger than what the proofs give, and the printed claim that Theorem 1's constant is independent of $K$ is not established by the printed argument.

Difficulty

Two steps resist the obvious approach. In stage one, the periodogram has to be controlled at uncountably many frequencies at once. A union bound over $v$ is unavailable, and the leakage of each present frequency spreads over the whole spectrum, so both the noise and the signal must be bounded uniformly in $v$ with explicit constants. In stage two, the samples used to estimate an effective arm are selected with the estimated periods, which were computed from the same stage-one data, so the usual independence behind confidence bounds fails. Lemmas 9–11 are therefore stated for the weak oracle, whose sample selection does not depend on the data; on the event $\Lambda$ the definitions make the oracle's run and the policy's run the same function of the noise path.

Formalization scope

Epochs are natural numbers $t\ge1$; arms are Fin K (the paper's arm $k$ is index $k-1$), and $K\ge1$. The noise is a sequence $\epsilon:\mathbb N\to\Omega\to\mathbb R$ on a probability space, independent, with Mathlib's HasSubgaussianMGF at variance proxy $\sigma^2$, plus the printed tail clause. Both algorithms are defined in full, as deterministic functions of the noise path, with canonical tie-breaking: smallest maximizer, smallest closest candidate, smallest arm index. Algorithm 1's loop runs at most $n$ passes, and $\mathrm{LCM}(\hat v_i^{-1})$ is the least common multiple of the reduced denominators of the selected frequencies. Algorithm 2 takes its period vector as an argument; the two-stage policy and the oracle are its two instances. Expected regret is an outer expectation: an integrable majorant of the regret whose integral obeys the bound. Probability bounds bound the outer measure of the bad event. Every DFT uses the absolute stage-one epochs, as in Step 8 of Algorithm 1.

Disclosed deviations: Theorem 1's constant depends on $\sigma$ and $K$ (the printed proof does not give uniformity in $K$), and $\delta=8/T$ is fixed as in the proof of Lemma 11. Lemma 6 uses $0.2328$ for the printed $0.233$; Lemma 7 and Theorem 2 use $0.6934$ for the printed $0.694$. Lemma 7 covers the nonzero present frequencies. Lemma 11 states the standing Assumption 3 and the parameters (7) as hypotheses, as its proof uses them.

The algorithm is the object of the theorem. Replacing Algorithm 1 by "any estimator that is correct with high probability", or Algorithm 2 by "any policy with the oracle's regret", would make the goal a different and much weaker statement. So would placing the constant after the horizon or the instance, since the regret is at most $T$, or using a bare Lebesgue integral of a possibly non-measurable regret.

A complete development needs discrete Fourier analysis of finite sequences, Bernstein's inequality for complex polynomials on the unit disc (Lemma 14 of the paper, from Nagy and Totik), sinc-function estimates, anytime concentration for sub-Gaussian sums, and a bookkeeping layer for the nested index sets of Algorithm 2. The concentration and polynomial-inequality parts are reusable beyond this mission. Proofs of individual lemmas, helper lemmas such as the closed form (6) of the frequency components, and alternative arguments are welcome.

Selected references

• N. Chen, C. Wang, L. Wang, Learning and Optimization with Seasonal Patterns, arXiv:2005.08088v4, 2021; Operations Research, 2025. https://arxiv.org/abs/2005.08088
• P. Auer, Using Confidence Bounds for Exploitation-Exploration Trade-offs, Journal of Machine Learning Research 3, 397–422, 2002. https://www.jmlr.org/papers/v3/auer02a.html
• L. Li, Y. Lu, D. Zhou, Provably Optimal Algorithms for Generalized Linear Contextual Bandits, ICML 2017. https://arxiv.org/abs/1703.00048
• B. Nagy, V. Totik, Bernstein's Inequality for Algebraic Polynomials on Circular Arcs, Constructive Approximation 37, 223–232, 2013.

Motivation

Personalized decisions — which drug to prescribe, which product to recommend, which price to quote — are made one user at a time, from user features observed on arrival, and the effect of each decision is learned only from the users it was applied to. This is the contextual (covariate) bandit. In electronic records and online platforms the feature vector is high-dimensional, often with more coordinates than there will ever be users, while the outcome is binary or count-valued, so a linear reward model is a poor fit. Wang, Wei and Yao (arXiv:1812.02962, published in Management Science, 2025) combine three ingredients: a generalized linear model (GLM) for rewards, sparsity of the parameter vectors, and the minimax concave penalty (MCP) of Zhang (2010) for estimation.

Timeline. Goldenshluger and Zeevi (2013) obtained $O(\log T)$ regret for a two-armed linear bandit with low-dimensional covariates, under a margin condition, and showed it is the right order. Bastani and Bayati (2020) extended the setting to high-dimensional sparse linear rewards with the LASSO, obtaining $O(s_0^2\log^2 T)$ regret. Wang, Wei and Yao (2018 preprint) treat GLM rewards with the MCP and claim $O(|\mathcal K|s^2(s+\log d)\log T)$, recovering the $\log T$ order in the high-dimensional setting.

Setting

At each time $t=1,2,\dots$ a user with covariate vector $x_t\in\mathcal X\subseteq\mathbb R^d$ arrives; the $x_t$ are i.i.d. with an unknown law $\mathcal P_x$. The decision-maker chooses a decision $\pi_t\in\mathcal K=\{1,\dots,K\}$, $K\ge2$, and observes only the reward of that decision.

The reward of decision $k$ at covariate $x$ has law $g(r\mid x^\top\beta_k)\,\nu(dr)$, where $\nu$ is a known base measure on $[-R_{\max},R_{\max}]$, $g(\cdot\mid\eta)$ a known density, and $\beta_k\in\mathbb R^d$ an unknown sparse parameter: its support $\mathcal S_k$ has at most $s$ elements. Write $f(r\mid\eta)=-\log g(r\mid\eta)$ and $\mu(\eta)=\int r\,g(r\mid\eta)\,d\nu(r)$, so the expected reward is $\mu(x^\top\beta_k)$. The Bernoulli–logistic model is $\nu=\delta_0+\delta_1$, $\mu(\eta)=1/(1+e^{-\eta})$.

The cumulative regret compares the decisions with the oracle that knows every $\beta_k$:

$$R^C(T)=\sum_{t=1}^T\mathbb E\Big[\max_k\mu(x_t^\top\beta_k)-\mu(x_t^\top\beta_{\pi_t})\Big].$$

The G-MCP-Bandit algorithm has inputs $t_0,h,\lambda_{1,0},\lambda_{2,0},a$. At time $t$, with probability $\min\{1,t_0/t\}$ it explores: it plays a uniformly random decision (ε-decay random sampling). Otherwise it forms a shortlist $\Pi_t$ of the decisions whose estimated mean reward, under the random-sample estimates $\beta^{random}_k$ (trained on exploration data only), is within $h/2$ of the best; it then plays the decision of $\Pi_t$ with the largest estimated mean under the whole-sample estimates $\beta^{whole}_k$ (trained on all data of $k$). Both estimates are computed by the 2-step weighted Lasso (2sWL): an $\ell_1$-penalized maximum likelihood fit with weights $\lambda$, then a refit whose weights $w_j=\max(0,\lambda-|\beta_{1,j}|/a)$ are the MCP derivatives at the first fit, both over the ball $\|\beta\|_1\le b$, with the anytime schedules $\lambda_1(t)=\lambda_{1,0}\sqrt{1+\log d/\log(t+1)}$ and $\lambda_2(t)=\lambda_{2,0}\sqrt{(\log(t+1)+\log d)/(t+1)}$.

The paper assumes A.1 (bounded covariates, rewards and parameters; $\beta_{\min}$ lower-bounds the nonzero coefficients), A.2 (margin: $\mathbb P(0<|\mu(x^\top\beta_i)-\mu(x^\top\beta_j)|\le\gamma)\le CR_{\max}\gamma$), A.3 (every decision is either $h$-suboptimal everywhere or $h$-optimal on a region $U_k$ of probability at least $p^*$), A.4 (a restricted eigenvalue condition with constant $\kappa$ for samples in $U_k$) and A.5 (smoothness and convexity of $f$ with derivative bounds $\sigma,\sigma_2,\sigma_3$).

Formalization targets

Goal: Theorem 1 (p. 15)

For every $a\ge2304s/(\kappa p^*)$ there are constants $C_0\ge10$ and $C_4,C_5,T_0,C_\beta>0$, independent of $T$, such that with $t_0=2C_0|\mathcal K|$, $\lambda_{1,0}=C_5$, $\lambda_{2,0}=C_4$, for every $T\ge T_0$,

$$R^C(T)\le R_{\max}(T_0+|\mathcal K|)+\Big(6R_{\max}|\mathcal K|C_0+41R_{\max}|\mathcal K|+2e^{4\sigma_2x_{\max}b}CR_{\max}^3|\mathcal K|x_{\max}^2C_\beta s^3\Big)\log(T+1).$$

The goal keeps every explicit coefficient of the page and leaves the constants the paper calls "independent of $T$" existential.

Milestones

In the order the proof of Theorem 1 (pp. ec5–ec8) uses them:

1. Proposition 2 (p. 13): the exploration count $n_k$ is between $C_0(1+\log(T+1)-\log(t_0+1))$ and $3C_0(1+\log T-\log t_0)$ with probability $\ge1-2/(T+1)$.
2. Lemma EC.8, statements 2 and 3 (p. ec16): enough exploration samples of an optimal decision fall in its region $U_k$.
3. Proposition 4 (p. 18): $\|\beta^{random}_k(T)-\beta_k\|_1\le\min\{1/(\sigma_2x_{\max}),h/(4e\sigma_2R_{\max}x_{\max})\}$ with probability $\ge1-15/(T+1)$.
4. Lemma EC.10 (p. ec20): a Lipschitz bound for $\mu$, and the $h/2$ separation it implies on $U_i$.
5. Proposition 6 (p. 19): $\|\beta^{whole}_k(T)-\beta_k\|_2\le\sqrt{C_\beta s^2/(T+1)}$ with probability $\ge1-13/(T+1)$.

Significance

Theorem 1 says that, under the stated assumptions, learning with high-dimensional GLM rewards costs regret logarithmic in the horizon, the order known to be unavoidable already for low-dimensional linear bandits. It improves the $\log^2T$ of the LASSO bandit and shows how a non-convex penalty, computed by two convex weighted-Lasso solves, can be analysed under the non-i.i.d. sampling that a bandit induces. Propositions 4 and 6 are estimation results of independent interest: tail bounds for an MCP estimator trained on random and on adaptively collected samples.

The result is proved on paper; it is not formalized anywhere. The mission produces a machine-checked statement of the full algorithm and its regret, and the milestones isolate reusable facts: an exploration-count bound for ε-decay sampling, a Lipschitz bound for GLM means, and the estimator tail bounds. Alternative arguments and sharper constants are welcome as separate theorems.

Difficulty

The whole-sample data are not i.i.d.: which samples decision $k$ receives depends on the past estimates. Standard high-dimensional estimation results (restricted eigenvalue arguments for the Lasso or MCP) assume i.i.d. designs, and so does the analysis of the oracle estimator. The obvious argument — apply the i.i.d. result to $\beta^{whole}$ — fails at this step. The paper instead extracts an i.i.d. subsample, the exploration samples in $U_k$, and controls the rest through a martingale count. A second difficulty is that the MCP objective is non-convex; the 2sWL estimate must be shown to coincide with the oracle estimator, which requires a minimum signal strength $\beta_{\min}$ and a sufficiently large $a$.

Formalization scope

Covariates are Fin d → ℝ with $d\ge1$, decisions are Fin K with $K\ge2$ (the paper's decision $k$ is k.val + 1), times are $t\ge1$. Norms are explicit sums. Pinned readings, all disclosed in the items:

• The reward family is a base measure $\nu$ concentrated on $[-R_{\max},R_{\max}]$ with a jointly measurable, positive, normalized density $g$; $\mathbb E[R_k\mid x,\beta]=\mu(x^\top\beta)$.
• A.5's derivatives are in the linear predictor $\eta$, bounded for $|\eta|\le bx_{\max}$; smoothness is ContDiff ℝ ∞.
• Both weighted-Lasso steps minimize over $B_b=\{\|\beta\|_1\le b\}$ (A.1's "all feasible β").
• A.3's "every $x$" means every $x\in\mathcal X$; A.4 is required for $k\in\mathcal K_o$ only.
• Exploration is driven by exogenous coins $V_t\sim\mathrm{Unif}[0,1]$ and uniform draws $A_t$, independent of the covariates and rewards. The rewards of different decisions at the same time may be dependent.
• The algorithm uses the box's anytime $\lambda_1(t),\lambda_2(t)$, with $\lambda_{1,0}=C_5$, $\lambda_{2,0}=C_4$.
• Propositions 4 and 6 are stated for $k\in\mathcal K_o$, with the algorithm parameters and the threshold on $T$ that Lemma EC.9 supplies. Lemma EC.10 adds the bound $|f'|\le\sigma_2$ its proof uses.

Trivializing formalizations are ruled out: the estimates are minimizers of the stated objective over $B_b$ (not arbitrary functions), the selection and tie-breaking rules are measurable (otherwise every expectation would be the junk value $0$), and every existential constant comes before the probability space, the rules and $T$, so that $C_\beta$ and $T_0$ cannot depend on the horizon. The trailing $O(|\mathcal K|s^2(s+\log d)\log T)$ and the explicit lower bound on $T_0$ are not formalized.

A complete development needs a measurable argmin selection over a compact ball, Chernoff bounds for sums of independent non-identical Bernoulli variables, differentiation under the integral for GLM means, a restricted-eigenvalue oracle inequality for the weighted Lasso with GLM loss, and a martingale concentration bound. The first three are reusable beyond this mission. Contributions on any milestone are welcome.

Selected references

• X. Wang, M. M. Wei and T. Yao, Online Learning and Decision-Making under Generalized Linear Model with High-Dimensional Data, arXiv preprint, 2018 (Management Science, 2025). https://arxiv.org/abs/1812.02962
• H. Bastani and M. Bayati, Online Decision Making with High-Dimensional Covariates, Operations Research 68(1), 2020. https://doi.org/10.1287/opre.2019.1902
• A. Goldenshluger and A. Zeevi, A Linear Response Bandit Problem, Stochastic Systems 3(1), 2013. https://doi.org/10.1287/11-SSY032
• C.-H. Zhang, Nearly Unbiased Variable Selection under Minimax Concave Penalty, Annals of Statistics 38(2), 2010. https://doi.org/10.1214/09-AOS729

Motivation

Thompson sampling (TS) is the most widely used heuristic for Bayesian multi-armed bandits: at each step it samples a parameter from the current posterior and plays the arm that is best for the sample. Its Bayesian regret has been analysed extensively (Russo and Van Roy, 2014; Bubeck and Liu, 2013). Min, Maglaras and Moallemi (arXiv:1902.04251) place TS inside a larger family of information relaxation sampling (IRS) policies, obtained from the information-relaxation duality of Brown, Smith and Sun (2010). Each choice of penalty function yields a performance bound $W^z$ and a randomized policy $\pi^z$; TS is the member with the trivial penalty. Their Theorem 3 gives explicit, finite-$T$ bounds on the suboptimality gap $W^z(T,y)-V(\pi^z,T,y)$ of three members of the family when the rewards come from a natural exponential family with conjugate priors. This mission formalizes Theorem 3 and the lemmas of its proof (Appendix §D.4).

Setting

There are $K\ge1$ arms $\mathcal A=\{1,\dots,K\}$ and a horizon $T$. Arm $a$ has an unknown parameter $\theta_a\in\mathbb R$; given $\theta_a$, its rewards $R_{a,1},R_{a,2},\dots$ (indexed by the number of the pull, not by time) are i.i.d. with the natural exponential family law $h_a(dr)\exp(\theta_a r-A_a(\theta_a))$, where $h_a$ is a reference measure and $A_a$ the log-partition function, $e^{A_a(\theta)}=\int e^{\theta r}h_a(dr)$. The prior of $\theta_a$ is the conjugate law proportional to $\exp(\xi_a\theta-\nu_a A_a(\theta))\,d\theta$, indexed by a belief $y_a=(\xi_a,\nu_a)$; observing a reward $r$ updates it to $(\xi_a+r,\nu_a+1)$. Arms are independent.

The conditional mean reward is $\mu_a(\theta_a)=\mathbb E[R_{a,n}\mid\theta_a]$, the predictive mean is $\bar\mu_a(y_a)=\mathbb E_{y_a}[\mu_a(\theta_a)]$, and the posterior predictive mean after $n$ rewards is $\hat\mu_{a,n}=\mathbb E_{y_a}[\mu_a(\theta_a)\mid R_{a,1},\dots,R_{a,n}]$. The outcome $\omega=(\theta,(R_{a,n}))$ has law $\mathcal I(y)$.

The three performance bounds are

$$W^{\rm TS}(T,y)=\mathbb E_y\Big[T\max_a\mu_a(\theta_a)\Big],\qquad W^{\rm IRS.FH}(T,y)=\mathbb E_y\Big[T\max_a\hat\mu_{a,T-1}\Big],$$ $$W^{\rm IRS.V\text{-}Zero}(T,y)=\mathbb E_y\Big[\max_{n\in\mathcal N_T}\sum_a\sum_{i=0}^{n_a-1}\hat\mu_{a,i}\Big],\qquad\mathcal N_T=\Big\{n\in\mathbb N_0^K:\sum_a n_a=T\Big\}.$$

With remaining horizon $T$ and current belief $y$, TS samples $\tilde\theta$ from the prior $\mathcal P(y)$ and plays $\arg\max_a\mu_a(\tilde\theta_a)$. IRS.FH samples an outcome $\tilde\omega\sim\mathcal I(y)$ and plays $\arg\max_a\hat\mu_{a,T-1}(\tilde\omega)$. IRS.V-Zero samples $\tilde\omega$, finds an allocation $\tilde n^*\in\mathcal N_T$ maximizing the bracket above, and plays $\arg\max_a\tilde n^*_a$. Each policy repeats this at every step with the updated belief. $V(\pi,T,y)$ is the expected total reward of $\pi$.

Formalization targets

Goal: Theorem 3

If every $A_a$ is $L$-smooth ($A_a''\le L$ on $\mathbb R$) and $\nu_a=\nu$ for all $a$, then for every $T\ge2$

$$W^{\rm TS}-V(\pi^{\rm TS})\le2\sqrt L\Big[\tfrac1{\sqrt\nu}+\sqrt{2\log T}\big(\tfrac K{\sqrt\nu}+2\sqrt{KT}\big)\Big],$$ $$W^{\rm IRS.FH}-V(\pi^{\rm IRS.FH})\le2\sqrt L\Big[\tfrac1{\sqrt\nu}+\sqrt{2\log T}\big(\tfrac K{\sqrt\nu}+2\sqrt{KT}-\tfrac13\sqrt{T/K}\big)\Big],$$ $$W^{\rm IRS.V\text{-}Zero}-V(\pi^{\rm IRS.V\text{-}Zero})\le\sqrt L\Big[\tfrac1{\sqrt\nu}+\sqrt{2\log T}\big(\tfrac K{\sqrt\nu}+2\sqrt{KT}-\tfrac13\sqrt{T/K}\big)\Big].$$

The TS bound (60) is also posed alone as a companion statement.

Milestones

1. Lemma 3: the loss of a first action $a$ in the penalized inner problem is $\mu_{a^*}-\mu_a$ (TS), $\hat\mu_{a^*,T-1}-\hat\mu_{a,T-1}$ (IRS.FH), and at most $\max_{n<T}\hat\mu_{a^*,n}-\hat\mu_{a,0}$ (IRS.V-Zero).
2. Lemma 4 and Corollary 3: a Gaussian tail, in particular sub-Gaussianity, gives $\mathbb E[(X-\mathbb EX-z\sigma)^+]\le(\sigma/z)e^{-z^2/2}$.
3. Lemma 5: $\bar\mu_a=\xi_a/\nu$, $\mu_a$ is $\sqrt{L/\nu}$-sub-Gaussian and $\hat\mu_{a,n}$ is $\sqrt{Ln/(\nu(\nu+n))}$-sub-Gaussian.
4. Lemma 6: the maximal version of Lemma 4 for $\max_{i\le n}\hat\mu_{a,i}$.
5. (259)–(261) and (269)–(275): deterministic summation bounds over the pull counts of an action sequence.

Significance

Theorem 3 shows that the IRS policies, although built from tighter performance bounds than TS, keep the $O(\sqrt{KT\log T})$ behaviour of TS, and that they improve the leading coefficient (IRS.V-Zero) or subtract a $\sqrt{T/K}$ term (IRS.FH, IRS.V-Zero). Because $W^{\rm TS}-V(\pi^{\rm TS})$ is the Bayesian regret of TS, (60) is also an explicit Bayesian regret bound for TS that applies to unbounded rewards such as Gaussian ones. The bounds apply to the Bernoulli family (with $L=1/4$) and to Gaussian rewards with known variance.

None of these results has a machine-checked proof. A formal development produces a reusable Lean model of a conjugate-prior Bayesian bandit with natural-exponential-family rewards, the sub-Gaussianity of its posterior mean process, and a Lean account of TS as a belief-Markov randomized policy. The paper's proofs are in its Appendix D.4.

Difficulty

The obvious route to (60) is the standard Bayesian-regret decomposition with upper confidence bounds. For unbounded natural-exponential-family rewards the required concentration does not come from boundedness. It has to come from the conjugate structure: the prior of $\mu_a(\theta_a)=A_a'(\theta_a)$ is sub-Gaussian because $A_a$ is $L$-smooth, which uses the whole real line as parameter space. For the IRS policies there is a further step: the policy must match nature's randomness in the same way TS does, with the penalized inner problem in place of the true best arm. The printed arguments for (61) and (62) pass through a time-$t$ version of Lemma 3 whose IRS.FH and IRS.V-Zero cases do not hold in full generality as printed, so those two bounds need new or repaired arguments.

Formalization scope

Arms are Fin K and reward indices are 0-based. The parameter space of every arm is $\mathbb R$, and a belief is a pair $(\xi,\nu)\in\mathbb R^2$. $\mu_a$, $\bar\mu_a$ and $\hat\mu_{a,n}$ are defined as integrals, with $\hat\mu_{a,n}$ the predictive mean at the conjugate posterior belief (13), so the closed forms (14) are consequences, not assumptions. Products of probability measures are Measure.infinitePi. $W^{\rm IRS.FH}$ is defined by its closed form (33). $V(\pi,T,y)$ is the recursion of the outer loop: draw the action from the policy's law at the current belief, earn the predictive mean, observe a reward from the predictive law, and update the belief. Every policy is a map from (remaining horizon, current belief) to a law on arms, so no policy can see the true outcome; a formalization in which TS used the true parameter would make (60) trivial and is excluded by construction. Ties are broken by arbitrary measurable selectors, and the goal quantifies over all of them.

Standing hypotheses carried by the goal:

• normalization $\int e^{\theta r}h_a(dr)=e^{A_a(\theta)}$;
• $A_a\in C^2$ with $A_a''\le L$;
• $\nu>0$ and a proper prior at the initial belief;
• integrability (3) of the rewards at the initial belief;
• $K\ge1$.

Properness is not assumed at every belief, since for Bernoulli rewards it fails outside $0<\xi<\nu$. Lemma 3 (3) carries the added hypothesis that $a$ is strictly suboptimal; without it the printed statement fails at ties. Sub-Gaussianity uses Mathlib's HasSubgaussianMGF with variance proxy $\sigma^2$.

Useful infrastructure: conjugate updating for exponential families, the moment generating function of a natural exponential family, Doob's maximal inequality for the submartingale $e^{\lambda\hat\mu_{a,n}}$, and a probability-matching lemma for TS in the belief-recursion model. Contributions are welcome on any milestone, and on a proof that the Beta–Bernoulli instance satisfies the hypotheses.

Selected references

• S. Min, C. Maglaras, C. C. Moallemi, Thompson Sampling with Information Relaxation Penalties, Management Science, 2025; preprint arXiv:1902.04251v2, 2021. https://arxiv.org/abs/1902.04251
• D. B. Brown, J. E. Smith, P. Sun, Information Relaxations and Duality in Stochastic Dynamic Programs, Operations Research 58(4), 2010. https://doi.org/10.1287/opre.1090.0796
• D. Russo, B. Van Roy, Learning to Optimize via Posterior Sampling, Mathematics of Operations Research 39(4), 2014. https://doi.org/10.1287/moor.2014.0650
• S. Bubeck, C.-Y. Liu, Prior-free and prior-dependent regret bounds for Thompson Sampling, NeurIPS 2013. https://arxiv.org/abs/1304.5758

Why action elimination is the question

In stochastic multi-armed bandits, a robust way to explore is action elimination: keep confidence intervals for every arm, discard an arm once its upper confidence bound falls below another arm's lower confidence bound, and sample uniformly among the arms that survive. Uniform sampling is what makes the first corruption-robust bandit algorithm work (Lykouris, Mirrokni & Paes Leme, STOC 2018): an adversary that corrupts a few rounds cannot steer a learner whose choice among surviving arms is random.

Lykouris, Simchowitz, Slivkins and Sun (arXiv:1911.08689v4, Mathematics of Operations Research) extend corruption-robust exploration to episodic reinforcement learning. Their algorithm also maintains active sets of actions, but it does not play uniformly among them; it follows an optimistic (UCB) policy restricted to the active sets. Section 7 of the paper explains why: Theorem 7.1 shows that the bandit recipe, transplanted verbatim to episodic MDPs, suffers linear regret for exponentially many episodes, even when every confidence statement it makes is correct. This mission formalizes that lower bound.

Setting

An episodic environment $\mathscr E=(\mathcal X,\mathcal A,H)$ has a finite state set $\mathcal X$, a finite action set $\mathcal A$ with $|\mathcal A|=A$, and a horizon $H$. A stochastic problem instance $\mathcal M=(p_0,p,\mathcal D_{\mathrm{rew}})$ on it fixes an initial state law $p_0$, a transition kernel $p(\cdot\mid x,a)$ (the same at every stage), and reward laws $\mathcal D_{\mathrm{rew}}(x,a)$ on $[0,1]$ with means $r^\star(x,a)$. The optimal Q-function and value are defined backwards from $V^\star_{H+1}\equiv0$ by $Q^\star_h(x,a)=r^\star(x,a)+\sum_{x'}p(x'\mid x,a)V^\star_{h+1}(x')$ and $V^\star_h(x)=\max_aQ^\star_h(x,a)$; the optimal actions are $\pi^\star_h(x)=\{a:Q^\star_h(x,a)=V^\star_h(x)\}$, and $V^\star=\sum_xp_0(x)V^\star_1(x)$.

A Q-supervisor $\mathcal T=(\bar Q,\underline Q,\mathscr A,\pi^{\mathrm{ucb}})$ holds estimates $\bar Q_h(x,a),\underline Q_h(x,a)\in[0,H]$, active sets $\mathscr A_h(x)\subseteq\mathcal A$, and a policy $\pi^{\mathrm{ucb}}$ greedy for $\bar Q$. It is confidence-admissible for $\mathcal M$ (Definition 4.1) if $\pi^\star_h(x)\subseteq\mathscr A_h(x)$ and $\underline Q_h\le Q^\star_h\le\bar Q_h$ everywhere. Its plausible sets are

$$\mathscr A^{\mathrm{plaus}}_h(x)=\{a\in\mathscr A_h(x):\ \bar Q_h(x,a)\ge\underline Q_h(x,a')\ \ \forall a'\in\mathscr A_h(x)\}.$$

An algorithm is uniformly action-eliminating if before each episode $k$ it outputs a Q-supervisor $\mathcal T_k$, possibly at random and depending on everything observed so far, and at each stage $h$ plays $a_{k;h}$ uniformly at random from $\mathscr A^{\mathrm{plaus}}_{k;h}(x_{k;h})$, independently across stages. It is uniformly admissible for $\mathscr E$ if for every instance on $\mathscr E$ its Q-supervisors are confidence-admissible with probability at least $\tfrac12$. The regret over $K$ episodes is $\mathrm{Regret}^{\mathcal M}_K=\sum_{k=1}^K\bigl(V^\star-V^{\mathcal M,\pi_k}\bigr)$, with $\pi_k$ the uniformly-at-random policy of episode $k$.

Formalization targets

Goal: Theorem 7.1

For every $H\ge1$ and $A\ge2$ there is an instance $\mathcal M$ on an environment with $|\mathcal X|=H+1$ and $|\mathcal A|=A$ such that every uniformly action-eliminating, uniformly admissible algorithm satisfies

$$K\le\frac{A^H}{4}\quad\Longrightarrow\quad\mathbb E^{\mathcal M}\bigl[\mathrm{Regret}^{\mathcal M}_K\bigr]\ge\frac K8 .$$

Milestones (Appendix A)

The witness is the combination lock $\mathcal M$: states $x^{(0)},\dots,x^{(H)}$, action $1$ advances $x^{(h)}\to x^{(h+1)}$, any other action falls into the sink $x^{(0)}$, and the only reward is $1$ for action $1$ at $x^{(H)}$. Its twin $\mathcal M_0$ has the same transitions and zero rewards. The milestones are the steps of the paper's proof:

1. (A.1) $\mathcal M$ and $\mathcal M_0$ induce the same law on histories in which $(1,\dots,1)$ was never played.
2. (A.2) If no action is eliminated, the combination is played with probability $A^{-H}$.
3. Observation 2 If no action is eliminated, $V^\star-V^{\mathcal M,\pi_k}=1-A^{-H}$.
4. Observation 3 Admissibility for $\mathcal M_0$ forces no elimination.
5. Union bound $\mathbb P^{\mathcal M_0}[\bigcap_k(\mathcal E^{\mathrm{combi}}_k)^c\cap\bigcap_k\mathcal E^{\mathrm{adm}}_k]\ge\mathbb P^{\mathcal M_0}[\bigcap_k\mathcal E^{\mathrm{adm}}_k]-\sum_k\mathbb P^{\mathcal M_0}[\mathcal E^{\mathrm{combi}}_k\cap\mathcal E^{\mathrm{adm}}_k]$.
6. Chain (i)–(iii) $\mathbb E^{\mathcal M}[\mathrm{Regret}^{\mathcal M}_K]\ge(1-A^{-H})K\,\mathbb P^{\mathcal M_0}[\bigcap_k(\mathcal E^{\mathrm{combi}}_k)^c\cap\bigcap_k\mathcal E^{\mathrm{adm}}_k]$.

Significance

The theorem separates two exploration principles that coincide in bandits. For $K$ episodes of uniform elimination the regret is $\Omega(K)$ until $K$ is of order $A^H$, while optimistic exploration over the same confidence sets attains regret polynomial in $H$, $|\mathcal X|$, $|\mathcal A|$ and $\sqrt K$ (Azar, Osband & Munos, ICML 2017). It is the reason the paper's SuperVIsed.C algorithm combines active sets with a UCB policy rather than sampling uniformly, and it applies to any uniformly admissible construction of the confidence bounds, so better estimators do not escape it.

The result is proved in the paper (Appendix A); it is not formalized anywhere. A machine-checked version adds a precise account of what "algorithm" means here (a learner that may use all past observations and internal randomness), of the probability space of a whole run, and of the change-of-instance argument (A.1), which is the template for many reinforcement-learning lower bounds.

Difficulty

The arithmetic of the final step is elementary. The work is in the probability space: the run of an adaptive learner over $K$ episodes is a sequential composition of the learner's choice of supervisor, the episode's states, actions and rewards, and the learner's update. Equation (A.1) needs a likelihood argument on this composed law: on histories that never play $(1,\dots,1)$, every factor of the two run laws agrees, because the two instances differ only at a state–action pair such histories never visit. Equation (A.2) needs that, conditionally on the supervisor of episode $k$, the episode's actions are independent and uniform. Neither can be read off the per-episode description; both require induction over episodes on the run law.

A tempting shortcut is to apply admissibility one episode at a time. It does not suffice: the proof needs the joint event $\bigcap_{k\le K}\mathcal E^{\mathrm{adm}}_k$ to have probability at least $\tfrac12$ (see the scope section).

Formalization scope

• Representation. States are Fin (H+1), actions Fin A; the paper's action $1$ is 0, the sink is state 0. Stages and episodes are 0-based. Transitions, initial laws, rewards, supervisor laws and action laws are PMFs. The value $V^\star$ is the backward recursion on p. 8, written on the number of remaining stages since the kernel is stage-independent.
• The algorithm. A learner is a map from the observed history (past Q-supervisors and episodes with their states, actions and rewards, oldest first) to a discrete law of the next Q-supervisor. It sees nothing of the instance beyond these observations. If a plausible set is empty, the action is drawn uniformly from $\mathcal A$; this only enlarges the class of algorithms.
• Uniform admissibility (pinned). §7 says each Q-supervisor is admissible "with probability at least 1/2"; the proof uses $\mathbb P[\bigcap_{k=1}^K\mathcal E^{\mathrm{adm}}_k]\ge\tfrac12$ ("By assumption", p. 39). The formalization uses the joint event, for every instance on the environment, over the same $K$ episodes as the regret.
• Unstated parts of the construction (pinned). Both instances start at $x^{(1)}$; actions at $x^{(H)}$ lead to the sink. The page states neither. The start is what makes the combination have probability $A^{-H}$; the second choice is never used because $x^{(H)}$ is reached only at the last stage.
• Reward laws of the instances quantified in the hypothesis are discrete; this weakens the hypothesis and strengthens the theorem.
• Not trivial. The hypothesis is satisfiable: the learner that always outputs $\bar Q\equiv H$, $\underline Q\equiv0$, $\mathscr A\equiv\mathcal A$ is uniformly admissible for every $K$. A statement in which the instance is fixed in the admissibility hypothesis, or in which admissibility is relative to $\mathcal M$ rather than to every instance, would be a different theorem.
• Not posed. The paper's headline upper bounds (Theorems 2.1, 2.2) are stated with $\lesssim$ and belong to a separate mission of this series.

Welcome contributions: lemmas on the run law of an adaptive learner (marginals of the $k$-th supervisor, conditional independence of episode $k$ given its supervisor), which are reusable for other episodic lower bounds.

Selected references

• T. Lykouris, M. Simchowitz, A. Slivkins, W. Sun, Corruption-robust exploration in episodic reinforcement learning, Mathematics of Operations Research; arXiv:1911.08689v4, 2023. https://arxiv.org/abs/1911.08689
• T. Lykouris, V. Mirrokni, R. Paes Leme, Stochastic bandits robust to adversarial corruptions, STOC 2018. https://arxiv.org/abs/1803.09353
• M. G. Azar, I. Osband, R. Munos, Minimax regret bounds for reinforcement learning, ICML 2017. https://arxiv.org/abs/1703.05449

Motivation

Reinforcement-learning algorithms with regret guarantees, such as UCBVI (Azar, Osband & Munos 2017), assume that every episode is generated by the same Markov decision process. In practice a fraction of episodes can be generated by something else: fraudulent users of a recommender, sensor faults, a strategic participant. Corruption-robust learning asks for regret that degrades gracefully with the number $C$ of corrupted episodes, without knowing $C$ in advance.

Timeline. For stochastic multi-armed bandits, Lykouris, Mirrokni & Paes Leme (STOC 2018) introduced the corruption model and a multi-layer active arm elimination algorithm whose regret grows linearly in $C$; Gupta, Koren & Talwar (COLT 2019) improved the dependence to additive. For episodic reinforcement learning, Lykouris, Simchowitz, Slivkins & Sun (abstract at COLT 2021; Mathematics of Operations Research 2025) gave SuperVIsed.C, the first algorithm with sublinear regret under any deviation from i.i.d. episodes in this setting: in tabular MDPs with $T$ steps its regret is of order $C\,H^3\sqrt{SAT}$ up to logarithmic factors and lower-order terms (their Theorem 2.1), with an analogous bound for linear MDPs, without knowing $C$. Their analysis isolates a deterministic regret guarantee, Theorem 4.1, from which the headline bounds follow by concentration.

Setting

An episodic tabular MDP has a finite state set $\mathcal X$, a finite nonempty action set $\mathcal A$ and a horizon $H\ge1$. The nominal MDP consists of an initial distribution $p^\star_0$, stage-independent transition probabilities $p^\star(x'\mid x,a)$ and mean rewards $r^\star(x,a)\in[0,1]$. With $V^\star_{H+1}\equiv0$, the optimal values are $Q^\star_h(x,a)=r^\star(x,a)+p^\star(x,a)^\top V^\star_{h+1}$ and $V^\star_h(x)=\max_aQ^\star_h(x,a)$, and $V^\star=E_{x_1\sim p^\star_0}[V^\star_1(x_1)]$. A randomized Markovian policy $\pi$ is a probability distribution over finitely many deterministic Markov policies, and $V^\pi$ is its expected total reward.

A Q-supervisor $\mathcal T=(\bar Q,\underline Q,\mathcal A,\pi^{\mathrm{ucb}})$ holds upper and lower estimates of $Q^\star$, active sets $\mathcal A_h(x)$ of actions, and a UCB policy maximizing $\bar Q$ over the active set. It is confidence-admissible if $\underline Q\le Q^\star\le\bar Q$ and every optimal action is active. A policy is Q-supervised if it plays only plausible actions, those $a\in\mathcal A_h(x)$ with $\bar Q_h(x,a)\ge\underline Q_h(x,a')$ for all active $a'$. The Bellman errors are $\overline{\mathbf{Bell}}_h=\bar Q_h-(r^\star+p^{\star\top}\bar V_{h+1})$ and $\underline{\mathbf{Bell}}_h=\underline Q_h-(r^\star+p^{\star\top}\underline V_{h+1})$. A policy has UCB visitation ratio at most $\rho$ if switching to $\pi^{\mathrm{ucb}}$ at any stage $h$ multiplies the probability of any later state-action pair by at most $\rho$. A model-estimate $(\hat r,\hat p,b)$ is valid if the bonus $b$ bounds $|\hat r-r^\star+(\hat p-p^\star)^\top V^\star_{h+1}|$.

SuperVIsed.C runs $\ell_{\max}$ base learners. Learner $\ell$ runs a two-estimate value iteration, UCBVI-BASE, with a global model-estimate (all data, bonus inflated by $2^\ell$) and a subsampled one, inside the active sets handed down by learner $\ell+1$; it returns its base policy $\pi^{\mathrm{base}}_\ell$ and the active sets for learner $\ell-1$. In each episode a nondecreasing random layer schedule $(\ell_1,\dots,\ell_H)$ decides whose base policy is played at each stage; the master policy $\pi^{\mathrm{master}}$ is the resulting mixture, and $\pi^{\mathrm{master}}_\ell$, $\pi^{\mathrm{master}}_{\le\ell}$ are its conditionings on the final layer, with probabilities $q_\ell$, $q_{\le\ell}$.

Formalization targets

Goal: Theorem 4.1

With $\ell_\star=\min\{\ell\ge1:2^\ell\ge C\}$ and expected bonus sums $\Delta_{k,\ell}$ (subsampled, along $\pi^{\mathrm{master}}_{k,\ell}$) and $\Delta_{k,\le\ell_\star}$ (global, along $\pi^{\mathrm{master}}_{k,\le\ell_\star}$): if the global and subsampled model-estimates of every learner $\ell\ge\ell_\star$ are valid in every episode, then

$$CH+\sum_{k=1}^K\big(V^\star-V^{\pi^{\mathrm{master}}_k}\big)\le CH+8eH^2\sum_{\ell>\ell_\star}\ell\,q_\ell\sum_k\Delta_{k,\ell}+8eCH^2\log_2(2C)\,q_{\le\ell_\star}\sum_k\Delta_{k,\le\ell_\star}.$$

The left side is the paper's upper bound (2.2) on the regret. The statement leaves the estimates arbitrary apart from their ranges and validity, so it holds for every data realization.

Milestones

The milestones follow the proof: the value decomposition over final layers (Lemma 4.4), admissibility from validity (Lemma 4.6), supervision of the master policies (Lemma 4.5), the Bellman-error decompositions (Lemma D.1, Propositions 4.1 and 4.2), the bonus bound on Bellman errors (Lemma 4.7), and the schedule estimates (Claims 4.8, 4.9 and Lemma 4.10).

Significance

Theorem 4.1 is the explicit core of the paper's results: Theorems 2.1 and 2.2, stated only up to constant and logarithmic factors, follow from it by bounding the bonus sums. Its proof architecture, which supervises less robust learners with more robust ones and bounds their mismatch through the visitation ratio, is independent of the tabular setting; the paper applies it to linear MDPs as well.

The result is proved in the paper; no machine-checked proof exists. Formalizing it requires a fully explicit account of the master policy as a mixture over schedules, of concatenated policies, and of the step of Proposition 4.2 from fictitious trajectories to real ones. Several printed constants and statements need correction, which the formal statements record (see the scope section).

Difficulty

The obvious argument, optimism plus the Bellman-error decomposition of UCBVI, fails because the master policy does not play the UCB policy of any single learner. The regret of a supervised but non-greedy policy is controlled only along fictitious trajectories that switch to the UCB policy (Proposition 4.1), and turning those back into the policy's own trajectories needs a bound on the visitation ratio that holds for every schedule prefix of a mixture, not only for marginal layer probabilities. A second difficulty is bookkeeping: nested active sets, two estimates per learner, and conditioning the schedule on its final layer.

Formalization scope

• Representation. Finite types X, A with [Nonempty A]; stages 0-based (the paper's stage $h$ is Lean's h - 1, terminal values at index H); policies ℕ → X → A; randomized policies as finite weighted families of deterministic ones; trajectory laws as finite products, values and occupancies as finite sums; schedules Fin H → Fin ℓmax. Rewards enter through their mean $r^\star$; the regret is the bound (2.2). Logarithms are base 2.
• Pinned departures from the page, each disclosed in the item's note. (1) $8eH^2$ in place of the printed $4eH^2$, the constant the printed proof produces. (2) Positive parts in Proposition 4.2 and in the summands of $\Delta$: Proposition 4.2 is false as printed when Bellman errors are negative. (3) Lemma 4.5 assumes admissibility of the supervising learner, without which it is false. (4) The UCB policy maximizes over the active set (Algorithm 2), for every argmax selector; an empty filtered active set is replaced by the learner's own, which never happens for admissible learners. (5) Estimated transitions are probability vectors, as in the tabular setting.
• No trivialization. The schedule weights, $q_\ell$ and the master mixtures are computed from the schedule (3.3), never free inputs; validity is satisfiable (exact estimates with zero bonus are valid); the visitation ratio is cross-multiplied with $\rho\ge1$.
• Not posed. Theorems 2.1, 2.2 and 5.1 (bounds up to $\lesssim$), the concentration lemmas of §5–6, and the adversarial regret (2.1).
• Reusable infrastructure. Finite-horizon tabular MDPs with mixtures of deterministic policies, concatenation and occupancy measures; Q-supervisors and Bellman errors. Contributions of proofs of any milestone are welcome, and the schedule lemmas (Claims 4.8, 4.9, Lemma 4.10) are independent of the rest.

Selected references

• T. Lykouris, M. Simchowitz, A. Slivkins, W. Sun, Corruption-robust exploration in episodic reinforcement learning, Mathematics of Operations Research, 2025; arXiv:1911.08689v4. https://arxiv.org/abs/1911.08689
• M. G. Azar, I. Osband, R. Munos, Minimax regret bounds for reinforcement learning, ICML 2017. https://arxiv.org/abs/1703.05449
• T. Lykouris, V. Mirrokni, R. Paes Leme, Stochastic bandits robust to adversarial corruptions, STOC 2018. https://arxiv.org/abs/1803.09353
• A. Gupta, T. Koren, K. Talwar, Better algorithms for stochastic bandits with adversarial corruptions, COLT 2019. https://arxiv.org/abs/1902.08647

Motivation

Many service systems must match jobs to servers whose quality is not known in advance: crowdsourcing platforms routing tasks to worker types, wireless schedulers assigning users to channels, and switches in data networks. The scheduler learns server quality only by trying servers, and every poor assignment lets work pile up. The natural performance measure is therefore not the cumulative reward loss of classical bandits but the queue-regret: the expected excess backlog compared with a genie that knows the best assignment.

Krishnasamy, Sen, Johari and Shakkottai, Learning Unknown Service Rates in Queues: A Multiarmed Bandit Approach (Operations Research, 2021; arXiv:1604.06377), show that queue-regret has two regimes. In an early stage it grows like the regret of a bandit. In a late stage, once the queue regularly empties, past mistakes are forgotten at every empty instant and the queue-regret decays. This mission formalizes their upper bound for the late stage: a UCB scheduler with forced exploration, Q-UCB, has queue-regret of order $\log^3 t/t$.

Setting

A discrete-time switch has $U$ queues and $K\ge U$ servers. In every slot $t\ge1$, queue $u$ receives an arrival $A_u(t)\sim\mathrm{Bernoulli}(\lambda_u)$ and link $(u,k)$ offers a potential service $R_{uk}(t)\sim\mathrm{Bernoulli}(\mu_{uk})$, all independent and i.i.d. over slots. The scheduler picks a matching $\kappa(t)$, an injective assignment of a server $\kappa_u(t)$ to every queue, and queue $u$ evolves as

$$Q_u(t)=\big(Q_u(t-1)+A_u(t)-S_u(t)\big)^+,\qquad S_u(t)=R_{u\kappa_u(t)}(t).$$

The scheduler observes only past schedules and the services offered on scheduled links.

Write $\mu^*_u=\max_k\mu_{uk}$, $k^*_u$ for its maximizer, $\epsilon_u=\mu^*_u-\lambda_u$, and $\Delta=\min_{u,\,k\ne k^*_u}(\mu^*_u-\mu_{uk})$. Assumption 1: each queue has a unique best server and the best servers are distinct, so $k^*$ is the unique optimal matching. Assumption 2: $\epsilon_u>0$ for all $u$. The genie queue $Q^*_u$ always uses $k^*_u$. Assumption 3: the system starts from the stationary law of $Q^*$. The queue-regret is

$$\Psi_u(t)=\mathbb E\big[Q_u(t)-Q^*_u(t)\big].$$

Q-UCB (Algorithm 1) explores in slot $t$ with probability $\min\{1,3K\log^2t/t\}$, scheduling a uniformly random member of a fixed family $\mathcal X$ of $K$ matchings that together cover all $UK$ links. Otherwise it exploits: for each queue it picks the server with the largest index $\hat\mu_{uk}(t)+\sqrt{\log^2t/(2N_{uk}(t))}$, with $\hat\mu_{uk}$ the empirical mean and $N_{uk}$ the number of past assignments of link $(u,k)$, and schedules a matching closest in Hamming distance to these choices. Fix $\beta>1$ and set

$$w(t)=t^{1-1/\beta},\qquad v'_u(t)=\frac{6K}{\epsilon_u}w(t),\qquad v_u(t)=\frac{24}{\epsilon_u^2}\log t+\frac{60K}{\epsilon_u}\frac{v'_u(t)\log^2t}{t}.$$

Formalization targets

Goal: Theorem 5 for Q-UCB (p. 16)

For every $t\ge5800$ with $t\ge\exp\big(4/(\Delta^2(1-1/\beta)^3)\big)$, $w(t)/\log t\ge2/\epsilon_u$ and $v_u(t)+v'_u(t)\le t/2$,

$$\Psi_u(t)\le 6K\frac{v_u(t)\log^2t}{t}+\frac{24.004+UK}{6t^2}.$$

The constants are the paper's, stated exactly.

Milestones (§8.2, pp. 24–34)

• Lemma 10: the number of forced-exploration slots in a window exceeds $5\max(\log t,K(\log^3t_2-\log^3t_1))$ with probability at most $t^{-4}$. Over $[1,t]$ it exceeds $Kw(t)$ with probability at most $t^{-2K}$.
• Lemma 11: with probability at least $1-UK/(6t^3)$, no exploit slot in $(w(t),t]$ schedules a sub-optimal link (event $\mathcal E_1$).
• Lemma 12: pathwise, $Q_u(t)-Q^*_u(t)$ is at most the number of sub-optimal schedules since queue $u$ was last empty, at time $t-B_u(t)$.
• Lemmas 13–17: on $\mathcal E_1\cap\mathcal E_2$, a coarse queue bound $2Kw(t)$ (13), a first bound on the regenerative cycle (14), a maximal inequality for the arrival-minus-service walk (15), a refined polylogarithmic queue bound (16), and the refined cycle bound $B_u(t)\le v_u(t)$ (17), each failing with probability $O(t^{-3})$.

Significance

The theorem shows that a simple learning scheduler loses only $O(K\log^3t/(\epsilon_u^2t))$ in expected backlog in the late stage. Together with the paper's $\Omega(1/t)$ lower bound for consistent policies (Theorem 3), this places the optimal late-stage queue-regret within a polylogarithmic factor. The analysis method has two parts: a high-probability statement that the learner has locked onto the optimal matching, and a regenerative argument that converts it into a bound on queue length. It applies to other learning-in-queues problems in the same way.

All results are proved in the paper (§8.2). None of them has a machine-checked proof. The mission produces a formal model of the learning switch, including the algorithm with arbitrary tie-breaking, the coupled genie and the stationary start, and checks the explicit constants. These constants rely on numerical facts stated in the proofs, for example a positivity check for $x\ge\log5800$ in Lemma 10(b) and the absorption of lower-order terms into $24.004$, which a formal proof must verify.

Difficulty

The obvious argument says that UCB eventually identifies the best server, so the queue behaves like the genie's. This fails for two reasons. First, the regret is an expectation of a queue length, and a queue remembers every early mistake until it next empties. So one must bound the current regenerative cycle, and that bound itself depends on the queue length, which forces the recursion of Lemmas 13, 14, 16 and 17. Second, UCB's standard logarithmic-regret analysis bounds the expected number of sub-optimal pulls. It says nothing about whether a sub-optimal pull happens in a specific late window. Forced exploration at rate $\log^2t/t$ is what makes all indices concentrate at once, and Lemma 11 requires a union bound over every link, slot and sample count with explicit exponents.

Formalization scope

• Probability space. One canonical space: the initial queue vector together with an i.i.d. sequence of slot seeds, namely uniforms for arrivals, links and the explore coin, and a uniform explore index.
  • Arrivals and services are threshold events of the uniforms.
  • $Q(0)$ has the product geometric law $\mathbb P(Q_u(0)=n)=(1-\rho_u)\rho_u^n$ with $\rho_u=\lambda_u(1-\mu^*_u)/((1-\lambda_u)\mu^*_u)$, the stationary law of the genie chain under the printed recursion.
• Indexing and coupling. Queues and servers are Fin U and Fin K, and slots are $t\ge1$. The genie shares arrivals, services and $Q(0)$ with the system. This coupling is implicit in the paper's proofs and does not change $\Psi_u$.
• Algorithm. Q-UCB is formalized for every covering family $\mathcal X$ and every tie-breaking rule, deterministic in the slot and history, for the UCB argmax and the Hamming projection.
  • $N_{uk}(t)$ counts slots $1,\dots,t-1$.
  • An unsampled link has index $+\infty$.
  • $B_u(t)=t$ when queue $u$ never emptied on $[0,t]$.
• Disclosed additions.
  • $K\ge2$ in every statement; $K=1$ is trivial, and the constants fail there.
  • $t,t_1\ge1$ in Lemma 10(a).
  • $\log w(t)\ge(2\log t)^{2/3}$ in Lemma 10(b); the printed statement is false without it, and its proof uses it.
  • Lemmas 14 and 16 take the "arbitrary function" $v_u$ natural-valued.
• Excluded trivializations. Theorem 5 also asserts that $Q_u(t)-Q^*_u(t)$ is integrable, so $\Psi_u(t)$ cannot be a default value of a non-integrable integral. Every probability bound concerns the actual events, and every hypothesis set is satisfiable. For example, with $U=1$, $K=2$, $\lambda=0.5$, $\mu=(0.9,0.1)$, $\beta=2$, the range of Theorem 5 contains $t=\lceil e^{50}\rceil$.
• Out of scope. Theorem 5 and Lemma 11 for Q-ThS (Algorithm 2) are not formalized, and neither is Corollary 6.
• Infrastructure needed and welcome. Chernoff bounds for sums of independent non-identically distributed Bernoulli variables (Lemma 10), Hoeffding's inequality and a maximal suffix-sum bound (Lemmas 14, 15), measurability of the algorithm's trajectory in the seeds, and regenerative-cycle arguments for the reflected random walk. The Chernoff and stationary-queue lemmas are reusable well beyond this mission.

The source is the arXiv v4 preprint; the paper's proofs are in its §8 and §9.

Selected references

• S. Krishnasamy, R. Sen, R. Johari, S. Shakkottai, Learning Unknown Service Rates in Queues: A Multiarmed Bandit Approach, Operations Research 69(1), 2021. Preprint arXiv:1604.06377v4. https://arxiv.org/abs/1604.06377 ; https://doi.org/10.1287/opre.2020.1995
• P. Auer, N. Cesa-Bianchi, P. Fischer, Finite-time Analysis of the Multiarmed Bandit Problem, Machine Learning 47, 2002. https://doi.org/10.1023/A:1013689704352
• M. J. Neely, Stochastic Network Optimization with Application to Communication and Queueing Systems, Morgan & Claypool, 2010. https://doi.org/10.2200/S00271ED1V01Y201006CNT007