Bandit Algorithms

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

Motivation

An agent that interacts repeatedly with an unknown Markov decision process must trade exploration against exploitation. The dominant design principle for provably efficient reinforcement learning has been optimism in the face of uncertainty: UCRL2 (Jaksch, Ortner & Auer, 2010) and REGAL (Bartlett & Tewari, 2009) build confidence sets around the unknown model and act according to the most favourable model in them. Computing that optimistic policy can be expensive, and confidence sets built separately for every state–action pair can be loose.

Posterior sampling for reinforcement learning (PSRL), proposed by Strens (2000), replaces optimism by randomization: at the start of each episode it samples one MDP from the posterior distribution and follows the optimal policy of that sample. It is the reinforcement-learning analogue of Thompson sampling for bandits. Osband, Russo & Van Roy (2013) gave the first regret guarantee for PSRL, and with it the first regret guarantee for an RL algorithm not based on optimism. Their argument transfers the Bayesian-regret analysis of Thompson sampling by Russo & Van Roy (2014) from bandits to MDPs.

Timeline:

• 2000: Strens proposes PSRL as a heuristic.
• 2010: Jaksch, Ortner and Auer prove $\tilde O(DS\sqrt{AT})$ regret for UCRL2 in non-episodic MDPs with diameter $D$.
• 2013: Osband, Russo and Van Roy prove the $O(\tau S\sqrt{AT\log(SAT)})$ Bayesian regret bound for PSRL in episodic MDPs, the result of this mission.

Setting

A finite-horizon MDP $M=(\mathcal S,\mathcal A,R^M,P^M,\tau,\rho)$ has $S$ states, $A$ actions and horizon $\tau$. Choosing action $a$ in state $s$ yields a reward drawn from a distribution $R^M_a(s)$ on $[0,1]$, with mean $\overline R^M_a(s)$, and moves the state to $s'$ with probability $P^M_a(s'\mid s)$. Every episode starts from a state drawn from the initial distribution $\rho$. A policy $\mu$ maps a state and a step $i\in\{1,\dots,\tau\}$ to an action, and its value is the expected total mean reward from step $i$ on,

$$V^M_{\mu,i}(s)=\mathbb E_{M,\mu}\Big[\sum_{j=i}^{\tau}\overline R^M_{a_j}(s_j)\,\Big|\,s_i=s\Big].$$

A policy is optimal for $M$ if it maximizes $V^M_{\mu,i}(s)$ for every $s$ and $i$; $\mu^M$ denotes a fixed choice of optimal policy for each $M$.

The true MDP $M^*$ is random with prior $f$. In episode $k$, PSRL samples $M_k$ from the posterior $f(\cdot\mid H_{t_k})$ given the history $H_{t_k}$ of all earlier states, actions and rewards, and follows $\mu_k=\mu^{M_k}$ for $\tau$ steps. With $\mu^*=\mu^{M^*}$, the regret of episode $k$ and the cumulative regret are

$$\Delta_k=\sum_{s}\rho(s)\big(V^{M^*}_{\mu^*,1}(s)-V^{M^*}_{\mu_k,1}(s)\big),\qquad \mathrm{Regret}(T,\pi^{\mathrm{PS}}_\tau)=\sum_{k=1}^{\lceil T/\tau\rceil}\Delta_k .$$

In Lean, MDPs are indexed by a parameter $\theta$ in a measurable space $\Theta$ (MDPFamily), the value is value F θ π j with 0-based steps, and the run is the structure PSRLRun.

Formalization targets

Goal: Theorem 1

There is an absolute constant $C>0$ such that, for all $S,A,\tau\ge1$, every prior $f$, every measurable optimal-policy selector, every PSRL run with $M^*\sim f$ and every $T$,

$$\mathbb E\big[\mathrm{Regret}(T,\pi^{\mathrm{PS}}_\tau)\big]\le C\,\tau S\sqrt{AT\log(SAT)} .$$

This is the paper's $O(\cdot)$ statement. It does not fix the constant, which the paper's appendix computes with errors.

Milestones, in the order of the proof

1. Lemma 1: given $H_{t_k}$, $M^*$ and $M_k$ have the same conditional law.
2. Theorem 2, (4): $\mathbb E[\sum_{k\le m}\Delta_k]=\mathbb E[\sum_{k\le m}\tilde\Delta_k]$, where $\tilde\Delta_k=\sum_s\rho(s)(V^{M_k}_{\mu_k,1}(s)-V^{M^*}_{\mu_k,1}(s))$.
3. Lemma 2, (5): the dynamic programming equation $V^M_{\mu,i}=\mathcal T^M_{\mu(\cdot,i)}V^M_{\mu,i+1}$.
4. (6): $\mathbb E[\tilde\Delta_k\mid M^*,M_k]$ equals the expected sum of one-step Bellman errors along the visited states.
5. (7): the pathwise split of $\sum_k\tilde\Delta_k$ on the event $\{M_k,M^*\in\mathcal M_k\}$.
6. $\mathbb P(M^*\notin\mathcal M_k)\le1/m$ for the paper's confidence sets (Lemma 17 of Jaksch et al.).
7. (8): $\mathbb E[\sum_k\tilde\Delta_k]\le(\tau+1)\,\mathbb E[\sum_k\sum_i\min\{\beta_k(s_{k,i},a_{k,i}),1\}]+2\tau$.
8. Appendix B: $\sum_k\sum_i\mathbf 1(N_{t_k}(s_{k,i},a_{k,i})\le\tau)\le2\tau SA$.
9. Appendix B: $\sum_k\sum_i\sqrt{\mathbf 1(N_{k,i}>\tau)/N_{k,i}}\le\sqrt{8SAm\tau}$.

Significance

Theorem 1 holds for every prior, with no assumption on the MDP class beyond finiteness and bounded rewards. It shows that a single posterior sample per episode, rather than an optimistic search over a confidence set, already achieves the $\sqrt T$ rate of the optimistic algorithms. The reduction it rests on (Lemma 1 and Theorem 2) applies to any problem in which the agent can sample from the posterior.

The theorem has a paper proof but, as far as is known, no machine-checked proof. A formalization adds three things. First, an exact model of the episodic Bayesian setting, with posterior sampling stated as a conditional law. Second, corrected versions of two steps: the factor in (8), which the page's argument does not justify as printed, and the square-root sum of Appendix B, which is false as printed. Third, reusable pieces: a path-defined finite-horizon value with its dynamic programming equation, a conditional-expectation form of the posterior-sampling identity, and deterministic counting lemmas for visit counts.

Difficulty

The proof combines three kinds of argument, each with its own obstacle in Lean.

• Conditioning. Lemma 1 and Theorem 2 identify conditional laws given the history. The history is a random element whose length grows with $k$, and the posterior-sampling assumption only speaks about indicators of $M_k$. Extending it to functions of $(M,H_{t_k})$ and applying the tower property needs care with sub-$\sigma$-algebras. The same issue appears in (8): the confidence event depends on $H_{t_k}$, so it is not measurable with respect to $\sigma(M^*,M_k)$, the $\sigma$-algebra on which (6) conditions. The working argument conditions on $(M^*,M_k,H_{t_k})$ instead.
• Concentration over adaptive counts. The bound $\mathbb P(M^*\notin\mathcal M_k)\le1/m$ needs an $L^1$ deviation inequality for empirical transition distributions (Weissman et al.) and Hoeffding's inequality for rewards. Both must hold uniformly over the random number of visits, which the agent's own behaviour determines. Applying the inequalities at a fixed number of samples is not valid, because the sample size is random.
• Counting. The appendix sums $N^{-1/2}$ along the visited pairs; the paper's chain loses a factor of $2$ at its integral comparison.

Formalization scope

• Model. States and actions are Fin S and Fin A. Steps and episodes are 0-based: Lean step j is the paper's step $j+1$, and Lean episode k is the paper's episode $k+1$, with $t_k=k\tau+1$. MDPs are a measurable family over a parameter space Θ: transition rows satisfy the published IsTransitionKernel, and reward laws are Markov kernels supported on $[0,1]$. The initial distribution $\rho$ is fixed. The value is defined from the state laws along the trajectory, not by the Bellman recursion.

• The run. PSRLRun consists of measurable random elements on a probability space. Posterior sampling, the reset from $\rho$, rewards and transitions are stated as conditional expectations of indicators. Three assumptions the paper leaves implicit are made explicit:

  • the state is reset from $\rho$ at every episode start;
  • the state reached after the last action of an episode is observed;
  • the sampling step uses fresh randomness.

  The optimal-policy selector is any measurable map that is optimal at every step.

• Constants and corrections. $O(\cdot)$ is one absolute constant, quantified before every other object; a constant that depends on $S$, $A$, $\tau$, the prior or $T$ would make the goal trivial, because the regret is at most $\lceil T/\tau\rceil\tau$. Milestone 7 uses the factor $\tau+1$, which the page's chain proves, where the page prints $\tau$, and milestone 9 uses $\sqrt{8SAm\tau}$ where the page prints the false bound $\sqrt{2SAT}$; both corrections are disclosed in the statements.

• Ruled out. The value is not defined by the recursion, which would make Lemma 2 definitional. Measurability is required, so the expectations are not junk zeros. The posterior-sampling clause concerns indicators of $M_k$ only, so it does not already contain Lemma 1.

• Needed infrastructure. Conditional expectations with respect to $\sigma$-algebras generated by random elements; finite-horizon Markov chain laws; Weissman's $L^1$ inequality and Hoeffding's inequality at random sample sizes; elementary bounds on $\sum_j j^{-1/2}$. The counting milestones (8, 9) and Lemma 2 are self-contained and a good place to start. Proofs of the conditioning steps (milestones 1, 2, 4) are reusable for any posterior-sampling analysis.

Selected references

• I. Osband, D. Russo, B. Van Roy, (More) Efficient Reinforcement Learning via Posterior Sampling, NIPS 2013; arXiv:1306.0940v5. https://arxiv.org/abs/1306.0940
• T. Jaksch, R. Ortner, P. Auer, Near-optimal Regret Bounds for Reinforcement Learning, JMLR 11, 2010. https://jmlr.org/papers/v11/jaksch10a.html
• D. Russo, B. Van Roy, Learning to Optimize via Posterior Sampling, Mathematics of Operations Research 39(4), 2014; arXiv:1301.2609. https://arxiv.org/abs/1301.2609
• M. Strens, A Bayesian Framework for Reinforcement Learning, Proceedings of the 17th International Conference on Machine Learning (ICML), 2000 (reference [16] of the paper).
• P. L. Bartlett, A. Tewari, REGAL: A Regularization Based Algorithm for Reinforcement Learning in Weakly Communicating MDPs, UAI 2009; arXiv:1205.2661. https://arxiv.org/abs/1205.2661
• T. Weissman, E. Ordentlich, G. Seroussi, S. Verdú, M. J. Weinberger, Inequalities for the L1 Deviation of the Empirical Distribution, HP Labs Technical Report HPL-2003-97, 2003.

Contextual bandits and the reduction to regression

A contextual bandit is a sequential decision problem: in each round a learner sees a context (a user's features, a patient's covariates), picks one of $K$ actions, and observes the reward of that action only. Applications include recommendation, dynamic pricing and adaptive clinical decisions. The difficulty is statistical and computational at once: the learner must explore to learn which action is best for which context, and the class of models it learns over is typically huge.

A long-standing question was whether contextual bandits can be solved optimally with nothing more than an offline regression oracle, a black-box supervised learning routine that fits a predictor of rewards to i.i.d. data. Earlier optimal algorithms either required a cost-sensitive classification oracle called many times per round (the "monster" of Agarwal et al., 2014) or an online regression oracle that must handle adversarially generated data (Foster and Rakhlin, 2020). Simchi-Levi and Xu (2022) answered the question with FALCON+, which calls an arbitrary offline regression oracle once per epoch, $O(\log T)$ or $O(\log\log T)$ times in total, and whose regret is governed by the oracle's estimation error.

Timeline:

• 2014: Agarwal, Hsu, Kale, Langford, Li and Schapire, Taming the Monster: optimal regret with $\tilde O(\sqrt{KT})$ calls to a classification oracle.
• 2020: Foster and Rakhlin, Beyond UCB: SquareCB, optimal regret with an online regression oracle, via inverse gap weighting.
• 2020 (arXiv) / 2022 (journal): Simchi-Levi and Xu, FALCON and FALCON+: optimal regret with an offline regression oracle.

Setting

There is a finite set $\mathcal A$ of $K$ actions and a set $\mathcal X$ of contexts. In round $t$ nature draws a context $x_t$ and a reward vector $r_t\in[0,1]^{\mathcal A}$ from a fixed unknown distribution $\mathcal D$; the learner sees $x_t$, picks $a_t$ and observes $r_t(a_t)$. The conditional mean reward is $f^*(x,a)=\mathbb E[r_t(a)\mid x_t=x]$, and $\pi_{f^*}(x)$ is an action maximizing $f^*(x,\cdot)$. The regret after $T$ rounds is

$$\sum_{t=1}^T\big(r_t(\pi_{f^*}(x_t))-r_t(a_t)\big).$$

An action selection kernel $p(a\mid x)$ gives a probability distribution over actions for each context. The offline regression oracle $\mathrm{OffReg}_{\mathcal F}$ takes $n$ samples $(x_i,a_i,r_i(a_i))$ and returns a predictor $\hat f:\mathcal X\times\mathcal A\to\mathbb R$. It satisfies Assumption 2 with error function $\mathcal E_{\mathcal F,\delta}(n)$ if, for every kernel $p$, when the samples are i.i.d. with $(x_i,r_i)\sim\mathcal D$ and $a_i\sim p(\cdot\mid x_i)$, then with probability at least $1-\delta$,

$$\mathbb E_{x\sim\mathcal D_{\mathcal X},\,a\sim p(\cdot\mid x)}\big[(\hat f(x,a)-f^*(x,a))^2\big]\le\mathcal E_{\mathcal F,\delta}(n).$$

FALCON+ runs in epochs given by a schedule $0=\tau_0<\tau_1<\tau_2<\cdots$. In epoch $m$ it sets $\gamma_1=1$ and $\gamma_m=\tfrac12\sqrt{K/\mathcal E_{\mathcal F,\delta/(2m^2)}(\tau_{m-1}-\tau_{m-2})}$ for $m\ge2$; it obtains $\hat f_m$ by feeding only the data of epoch $m-1$ to the oracle ($\hat f_1\equiv0$); and in every round $t$ of the epoch it plays

$$p_t(a)=\frac{1}{K+\gamma_m\big(\hat f_m(x_t,\hat a_t)-\hat f_m(x_t,a)\big)}\ \ (a\ne\hat a_t),\qquad p_t(\hat a_t)=1-\sum_{a\ne\hat a_t}p_t(a),$$

where $\hat a_t$ maximizes $\hat f_m(x_t,\cdot)$. The epoch of round $t$ is $m(t)=\min\{m\ge1:t\le\tau_m\}$.

Formalization targets

Goal: Theorem 2 in explicit form

If $\tau_m\ge2^m$ and $\gamma_1\le\cdots\le\gamma_{m(T)}$ for $m\le m(T)$, then for every $T\ge1$ and $\delta>0$, with probability at least $1-\delta$,

$$\sum_{t=1}^T\big(r_t(\pi_{f^*}(x_t))-r_t(a_t)\big)\le 14.3\sum_{m=2}^{m(T)}\sqrt{K\,\mathcal E_{\mathcal F,\delta/(2m^2)}(\tau_{m-1}-\tau_{m-2})}\,(\tau_m-\tau_{m-1})+\tau_1+\sqrt{8T\log(2/\delta)}.$$

The paper states Theorem 2 as an $O(\cdot)$ bound; this is the explicit inequality its proof establishes, with the additive terms kept. It holds for every oracle, error function and schedule satisfying the hypotheses, so it is the shape of the result rather than a rate for a particular class.

Milestones

In attack order: Lemma A.2 (each oracle call is accurate with probability $1-\delta/(2m^2)$; the good event $\Gamma_2$ has probability $1-\delta/2$); Lemma A.3 (the kernel $p_m$ is induced by a randomized policy $Q_m$ on $\Psi=\mathcal A^{\mathcal X}$); Lemma A.4 (the conditional expected regret of a round is the implicit regret of $Q_{m(t)}$); Lemmas A.5 and A.6 (low predicted regret and bounded divergence $V(p_m,\pi)\le K+\gamma_m\widehat{\mathrm{Reg}}(\pi)$); Lemma A.7 (prediction error of implicit rewards on $\Gamma_2$); Lemma A.8 (true and predicted implicit regret agree up to factor 2 and $5.15K/\gamma_m$); Lemma A.9 ($\sum_\pi Q_m(\pi)\mathrm{Reg}(\pi)\le7.15K/\gamma_m$); Lemma A.10 in expectation; the Azuma display (A.10); and Lemma A.10 with high probability.

Significance

Theorem 2 makes contextual bandits reducible to offline regression with no loss in rate: for any function class with an estimation-error bound, plugging that bound into the theorem gives the regret. With empirical entropy $O(\varepsilon^{-p})$ this yields $O(T^{(1+p)/(2+p)}\log T)$, matching the known lower bound, and for linear classes it improves the best known bound when $K\ll T$ (Examples 1–2 of the paper). The oracle is called once per epoch on i.i.d. data, so any off-the-shelf supervised learner can be used, with a guarantee transferred automatically.

Formalizing the result produces a machine-checked offline-to-online reduction, independent of the function class. The paper's result is proved, but it has no machine-checked proof; the platform has formal statements for the online-oracle algorithm SquareCB and for the classification-oracle algorithm of Agarwal et al., not for this reduction. The milestones isolate reusable facts about inverse-gap-weighted kernels (Lemmas A.3, A.5, A.6) and an epoch-wise induction pattern (Lemma A.8) that recur in later work on bandits and reinforcement learning with regression oracles.

Difficulty

The obvious argument fails at the regression step. A natural approach feeds all past data to the oracle, but those data are adaptively collected and not i.i.d., so an offline guarantee does not apply to them; FALCON+ uses only the previous epoch's data, which are i.i.d. given the past, and the analysis must make this conditional application of Assumption 2 rigorous on a product space (Lemma A.2). The second obstacle is that the oracle's error is measured under the kernel of the previous epoch, while regret is incurred under the current one. Transferring the error across epochs requires the divergence $V(p,\pi)$ and the two-sided comparison of true and predicted implicit regret in Lemma A.8, proved by induction on epochs with exact constants; a one-sided bound does not close the induction.

Formalization scope

Lean representation and conventions:

• Finite contexts. $\mathcal X$ is a Fintype with the discrete σ-algebra. The paper claims Theorem 2 for arbitrary $\mathcal X$, but its detailed proof (App. A.1–A.6) is "under the condition that $|\mathcal X|<\infty$"; the uncountable case (App. A.7) is not formalized. No bound depends on $|\mathcal X|$.
• Rewards in $[0,1]$, the model of §1.2 and the assumption of the proof of Theorem 2. Setup 2's heavy-tailed generality (Condition (5)) is not formalized.
• Nature's law is a context marginal $\mathcal D_{\mathcal X}$ with a Markov reward kernel; $f^*(x,a)$ is the kernel mean.
• The run lives on the canonical space $\mathbb N\to(\mathcal X\times\mathbb R^{\mathcal A})\times[0,1]$ with the i.i.d. product law of $\mathcal D\otimes\mathrm{Uniform}[0,1]$; actions are drawn by the inverse CDF from the uniform coordinate.
• Probabilities in failure form: "with probability at least $1-\delta$" is "the failure set has outer measure at most $\delta$".
• Added hypotheses (disclosed in every statement): $\mathcal E_{\mathcal F,\delta}(n)>0$ (Algorithm 2 divides by it); measurability of the oracle and of the tie-breaking rule for $\hat a_t$ (App. A.7, p. 1929, assumes such conditions directly); $\delta>0$; $T\ge1$.
• The tie-breaking rule for $\hat a_t$ and the maximizer $\pi_{f^*}$ are universally quantified.
• Quantities the paper indexes by a round $t$ are indexed by its epoch; $\Upsilon_{t-1}$ is replaced by the coordinate filtration, which contains it.

A trivializing formalization is ruled out: the goal is a bound on the realized regret of the run of Algorithm 2, whose oracle sees only $(x,a,r(a))$ samples of the previous epoch; it is not a bound for an algorithm that is handed $f^*$ or its population error, or that observes the full reward vector.

Infrastructure needed: conditional application of an i.i.d. guarantee inside a product measure (Fubini over Measure.infinitePi), Azuma–Hoeffding for bounded martingale differences (proved on the platform as bounded_diff_martingale_two_sided), and finite-sum algebra for inverse gap weighting. The kernel lemmas A.3, A.5 and A.6 are reusable beyond this mission. Proofs of any milestone are welcome, as are proofs of the goal from the milestones.

Selected references

• D. Simchi-Levi and Y. Xu, Bypassing the Monster: A Faster and Simpler Optimal Algorithm for Contextual Bandits Under Realizability, Mathematics of Operations Research 47(3):1904–1931, 2022. https://doi.org/10.1287/moor.2021.1193
• D. J. Foster and A. Rakhlin, Beyond UCB: Optimal and Efficient Contextual Bandits with Regression Oracles, ICML 2020. https://arxiv.org/abs/2002.04926
• A. Agarwal, D. Hsu, S. Kale, J. Langford, L. Li and R. E. Schapire, Taming the Monster: A Fast and Simple Algorithm for Contextual Bandits, ICML 2014. https://arxiv.org/abs/1402.0555

Motivation

In a structured bandit problem a learner repeatedly chooses a decision $\pi$ from a set $\Pi$ and observes a noisy reward whose mean $f^M(\pi)$ is an unknown function from a known class $\mathcal{F}_{\mathcal{M}}$. Classical analyses of such problems measure the complexity of $\mathcal{F}_{\mathcal{M}}$ by the eluder dimension (Russo and Van Roy, 2013; 2014) or the star number, and prove regret bounds for posterior sampling (Thompson sampling) or optimistic algorithms in terms of these quantities.

Foster, Kakade, Qian and Rakhlin (2021) introduced the Decision-Estimation Coefficient (DEC), a single complexity measure that yields both upper and lower bounds on the minimax regret of interactive decision making. Section 6.2 of that paper connects the DEC to the older parameters: it shows that the square-loss DEC is bounded by the disagreement coefficient of the class, a quantity introduced in Foster, Rakhlin, Simchi-Levi and Xu (2020) and itself bounded by the star number and the eluder dimension. The bound is certified by posterior sampling, so it also explains why posterior sampling works for these classes.

Setting

Let $\Pi$ be a set of decisions. A model $M$ assigns to each decision a reward distribution; here a model enters only through its mean-reward function $f^M : \Pi \to [0, 1]$ and an optimal decision $\pi_M \in \arg\max_\pi f^M(\pi)$. The class $\mathcal{F}_{\mathcal{M}} = \{f^M : M \in \mathcal{M}\}$ collects the mean-reward functions of a model class $\mathcal{M}$. A reference model $\overline{M}$, not necessarily in $\mathcal{M}$, has mean reward $f^{\overline{M}} : \Pi \to [0, 1]$.

A prior $\mu$ is a finitely supported distribution $\mu = \sum_i w_i \delta_{M_i}$ over $\mathcal{M}$. The posterior sampling strategy plays $\rho_\mu(\pi) := \mu(\{\pi_M = \pi\})$, the law of $\pi_M$ when $M \sim \mu$.

The prior-dependent square-loss DEC (display (70) of the paper) is

$$\underline{\mathrm{dec}}^{\mathrm{Sq}}_\gamma(\mu, \overline{M}) = \inf_{p \in \Delta(\Pi)} \mathbb{E}_{M\sim\mu}\, \mathbb{E}_{\pi\sim p}\Bigl[ f^M(\pi_M) - f^M(\pi) - \gamma \bigl(f^M(\pi) - f^{\overline{M}}(\pi)\bigr)^2 \Bigr],$$

the best trade-off between regret and squared estimation error that a decision distribution $p$ can achieve against a model drawn from the prior.

For a class $\mathcal{F}$ of functions $\Pi \to \mathbb{R}$ and a distribution $\rho$ on $\Pi$, the disagreement coefficient (Definition 6.3) is

$$\theta(\mathcal{F}, \Delta_0, \varepsilon_0; \rho) = \sup_{\Delta \ge \Delta_0,\ \varepsilon \ge \varepsilon_0} \left\{ \frac{\Delta^2}{\varepsilon^2}\, \mathbb{P}_{\pi\sim\rho}\bigl( \exists f \in \mathcal{F} : |f(\pi)| > \Delta,\ \mathbb{E}_{\pi'\sim\rho}[f^2(\pi')] \le \varepsilon^2 \bigr) \right\} \vee 1,$$

where $\pi' \sim \rho$ is drawn independently of $\pi$. It measures how much mass $\rho$ puts on decisions where some function of the class is large although it is small in $L_2(\rho)$. The shifted class $\mathcal{F}_{\mathcal{M}} - f^M$ consists of the differences $f - f^M$, $f \in \mathcal{F}_{\mathcal{M}}$.

Formalization targets

Goal: Theorem 6.2

For every $\gamma \ge e$, posterior sampling certifies

$$\underline{\mathrm{dec}}^{\mathrm{Sq}}_\gamma(\mu, \overline{M}) \le \inf_{\Delta > 0} \left\{ 2\Delta + 24\, \frac{\sup_{M\in\mathcal{M}} \theta(\mathcal{F}_{\mathcal{M}} - f^M, \Delta, \gamma^{-1}; \rho_\mu) \log^2(\gamma)}{\gamma} \right\}.$$

In the formal statement, the objective of (70) evaluated at $p = \rho_\mu$ is bounded by $2\Delta + 24\Theta \log^2(\gamma)/\gamma$ for every $\Delta > 0$ and every upper bound $\Theta$ of the disagreement coefficients of the shifted classes.

Milestones

1. The disagreement coefficient bounds the probability of disagreement at every pair of scales (proof of Lemma E.2, p. 105).
2. The unit-scale decoupling bound with free parameters $\Delta, \varepsilon \in (0, 1]$, $\eta > 0$ (proof of Lemma E.2, p. 105).
3. Lemma E.2, the decoupling lemma: for $\mathcal{F} \subseteq (\Pi \to [-R, R])$, $\{f_z\} \subseteq \mathcal{F}$, $\{\pi_z\} \subseteq \Pi$ indexed by $z \sim \mu$,

$$\mathbb{E}_{z\sim\mu}\bigl[|f_z(\pi_z)|\bigr] \le \inf_{\Delta > 0} \left\{ 2\Delta + 6\, \frac{\theta(\mathcal{F}, \Delta, \gamma^{-1}; \rho_\mu) \log^2(R\gamma \vee e)}{\gamma} \right\} + \gamma\, \mathbb{E}_{z, z'\sim\mu}\bigl[f_z^2(\pi_{z'})\bigr].$$

4. The factor-four comparison of the decoupled squared error against a second prior draw with the squared error against $\overline{M}$ (proof of Theorem 6.2, p. 106).
5. Lemma E.2 applied to the shifted class $\mathcal{F}_{\mathcal{M}} - f^{\widetilde{M}}$ at parameter $\gamma/4$, for a fixed $\widetilde{M}$ (proof of Theorem 6.2, p. 106).

Significance

Theorem 6.2 bounds the DEC of any structured bandit class by its disagreement coefficient. With the bounds of the disagreement coefficient by the star number and the eluder dimension (Lemma 6.1 of the paper, from Foster et al. 2020) and the minimax theorem, it yields Theorem 6.1, which recovers the $\widetilde{O}(\sqrt{\mathfrak{e} T})$ regret bound of Russo and Van Roy for posterior sampling as a special case, and gives a $\widetilde{O}(\sqrt{\mathfrak{s}^2 T})$ bound in terms of the star number. The decoupling lemma (Lemma E.2) is a general tool: it controls a coupled quantity $\mathbb{E}[|f_z(\pi_z)|]$ by a decoupled second moment, and applies wherever an algorithm's decision and the function evaluated there are drawn from the same distribution.

The results are proved in the paper. None of them has a machine-checked proof; this mission produces the first formal statement of the disagreement coefficient and of the decoupling lemma, on which formal versions of eluder-dimension and star-number bounds can build.

Difficulty

The obvious argument fails at the decoupling step. The quantity $\mathbb{E}_{z\sim\mu}[|f_z(\pi_z)|]$ evaluates each function at its own decision, while the estimation error controls only $\mathbb{E}_{z, z'}[f_z^2(\pi_{z'})]$, with independent indices. For a finite set of $A$ decisions, Cauchy–Schwarz bridges the two at the price of a factor $A$; for an infinite decision space this gives nothing. The disagreement coefficient replaces the cardinality, but it controls disagreement only at one pair of scales at a time (the size of $|f(\pi)|$ and the $L_2(\rho_\mu)$ norm of $f$), while the coupled quantity involves all scales at once; obtaining only a $\log^2(\gamma)$ loss from this is the technical core of Lemma E.2.

Formalization scope

• Decisions form an arbitrary type $\Pi$; no finiteness or measurability is assumed. Priors and decision distributions are finitely supported (the paper's footnote 5 equips the model class with the discrete topology), encoded as finite weighted families, so every expectation is a finite sum and $\rho_\mu$ is the family of atoms $\pi_{M_i}$ with weights $w_i$.
• Models enter only through their mean-reward function and their optimal decision, which is all the square-loss DEC depends on; $\pi_M$ is a datum with the hypothesis $f^M(\pi) \le f^M(\pi_M)$ for all $\pi$.
• The disagreement coefficient uses the real supremum. All statements assume $\Delta > 0$, $\gamma^{-1} > 0$ and a uniformly bounded class, under which the supremum is finite; the inner expectation of (71) is over an independent copy of the decision.
• Infima and suprema of the page are stated as universally quantified bounds ("for every $\Delta > 0$", "for every upper bound $\Theta$"), which are equivalent and immune to Lean's default values.
• Lemma E.2 assumes $R \ge 1$: the page states it for every $R$, but its proof treats $R = 1$ and extends to $R \ge 1$ by rescaling; Theorem 6.2 needs only $R = 1$.
• $\log$ is the natural logarithm; $e = \exp(1)$.

The goal is not trivialized by a junk value: the disagreement coefficient is a genuine supremum under the stated hypotheses (a sorry-free check accompanies the definitions), $\gamma \ge e$ rules out negative logarithms, the class $\mathcal{F}_{\mathcal{M}}$ is the whole class rather than the prior's support, and the reference model is not assumed to lie in the class.

Contributions welcome: proofs of the milestones in attack order; a general layer-cake lemma for finite sums; a formal disagreement coefficient bound by the star number or the eluder dimension (Lemma 6.1), which would lead to Theorem 6.1.

Selected references

• D. J. Foster, S. M. Kakade, J. Qian, A. Rakhlin, The Statistical Complexity of Interactive Decision Making, arXiv preprint, 2021 (v3, 2023). https://arxiv.org/abs/2112.13487
• D. J. Foster, A. Rakhlin, D. Simchi-Levi, Y. Xu, Instance-Dependent Complexity of Contextual Bandits and Reinforcement Learning: A Disagreement-Based Perspective, Conference on Learning Theory (cited in the paper as Foster et al. 2020b). https://arxiv.org/abs/2010.03104
• D. Russo, B. Van Roy, Eluder Dimension and the Sample Complexity of Optimistic Exploration, Advances in Neural Information Processing Systems 26, pp. 2256–2264, 2013. https://papers.nips.cc/paper_files/paper/2013
• D. Russo, B. Van Roy, Learning to Optimize via Posterior Sampling, Mathematics of Operations Research 39(4):1221–1243, 2014. https://doi.org/10.1287/moor.2014.0650 (arXiv: https://arxiv.org/abs/1301.2609)

Why a lower bound on the DEC for linear bandits

In a linear bandit a learner repeatedly chooses a decision $\pi$ from a set $\Pi \subseteq \mathbb{R}^d$ and observes a noisy reward whose mean is $\langle \theta^\star, \pi\rangle$ for an unknown parameter $\theta^\star$. It is the standard model for sequential decisions with many correlated actions, such as ad placement, routing and recommendation, and its minimax regret over $T$ rounds is known to scale as $d\sqrt{T}$ up to logarithmic factors (Dani, Hayes and Kakade, COLT 2008; see Lattimore and Szepesvári, 2020, Ch. 19–24).

Foster, Kakade, Qian and Rakhlin (2021) introduce the Decision-Estimation Coefficient (DEC), a single complexity measure that yields both upper and lower bounds on the regret of every interactive decision problem. A complexity measure of this kind is only useful if it is tight on the classical examples. Proposition 6.2 of that paper checks this for linear bandits on the Euclidean unit ball: the localized DEC is at least of order $d/\gamma$, which, through the paper's general lower bound (Theorem 3.2), gives the regret lower bound $\Omega(\sqrt{dT})$. Proposition 6.8 gives the analogous statement for linear bandits whose models have a fixed gap $\Delta$.

Setting

Let $\mathbb{B}^d = \{v \in \mathbb{R}^d : \|v\|_2 \le 1\}$ be the closed Euclidean unit ball. It is both the decision space $\Pi$ and the parameter set $\Theta$. A model with parameter $\theta \in \Theta$ returns, at decision $\pi$, an outcome in $\{-1, +1\}$ drawn from the Rademacher distribution $\mathrm{Rad}(\langle\theta,\pi\rangle)$, which puts mass $(1+\mu)/2$ on $+1$ and $(1-\mu)/2$ on $-1$ when its mean is $\mu$. The mean reward is $f^\theta(\pi) = \langle \theta, \pi\rangle$.

A maximizer selector $\theta \mapsto \pi_\theta$ picks a decision with $\langle\theta,\pi\rangle \le \langle\theta,\pi_\theta\rangle$ for all $\pi$. The regret of a decision is $g^\theta(\pi) = f^\theta(\pi_\theta) - f^\theta(\pi)$. Two outcome laws are compared by the squared Hellinger distance $D^2_{\mathrm{H}}(P,Q) = \sum_y (\sqrt{P(y)}-\sqrt{Q(y)})^2$.

Given a reference model $\overline{M}$, the $L_\infty$-localized class at radius $\varepsilon$ is

$$\mathcal{M}^\infty_\varepsilon(\overline{M}) = \{ M \in \mathcal{M} : |g^M(\pi) - g^{\overline{M}}(\pi)| \le \varepsilon \ \ \forall \pi \in \Pi \},$$

and the DEC at scale $\gamma > 0$ is

$$\mathsf{dec}_\gamma(\mathcal{M}', \overline{M}) = \inf_{p \in \Delta(\Pi)} \sup_{M \in \mathcal{M}'} \mathbb{E}_{\pi\sim p}\bigl[ g^M(\pi) - \gamma\, D^2_{\mathrm{H}}(M(\pi), \overline{M}(\pi)) \bigr],$$

the infimum running over all Borel probability measures $p$ on $\Pi$.

Formalization targets

Goal: Proposition 6.2

For all $d \ge 4$ and $\gamma \ge 2d/3$ there is $\overline{M} \in \mathcal{M}$ with

$$\mathsf{dec}_\gamma\bigl(\mathcal{M}^\infty_{\varepsilon_\gamma}(\overline{M}), \overline{M}\bigr) \ge \frac{d}{12\gamma}, \qquad \varepsilon_\gamma = \frac{2d}{3\gamma}.$$

The page prints $\varepsilon_\gamma = d/(3\gamma)$. The hard family of its proof has regret functions $\Delta(1-\pi_i)$, which reach $2\Delta$ at $\pi = -e_i$ while the reference regret is identically $0$, so the family lies in the class of radius $2\Delta$ and not in the class of radius $\Delta$. The goal is stated at the radius the proof supports.

Milestones

1. Lemma A.8: $D^2_{\mathrm{H}}(\mathrm{Rad}(\mu), \mathrm{Rad}(0)) \le \tfrac34\mu^2$ on $[-1,1]$, together with the two general bounds of the lemma.
2. Lemma 5.1: an $(\alpha,\beta,\delta)$-family forces $\mathsf{dec}_\gamma \ge \alpha/2 - \gamma(\beta/N + \delta)$, stated for a general measurable decision space.
3. The hard family $\theta_i = \Delta e_i$: regret $\Delta(1-\pi_i)$ and $D^2_{\mathrm{H}}(M_i(\pi), \mathrm{Rad}(0)) \le \tfrac34\Delta^2\pi_i^2$. With the coordinate bounds $\sum_i \pi_i \le \sqrt d \le d/2$ ($d \ge 4$) and $\sum_i \pi_i^2 \le 1$, stated as a separate item, this makes the family a $(\Delta, \tfrac34\Delta^2, 0)$-family.
4. Localization: the family lies in $\mathcal{M}^\infty_{2\Delta}(\mathrm{Rad}(0))$.

Companion: Proposition 6.8

For $\Delta \in (0, 1/4)$ and $d \ge 2$, an explicit class of linear bandit models on $\{e_1,\dots,e_d\}$, each with gap $\Delta$, satisfies $\mathsf{dec}_\gamma(\mathcal{M}^\infty_\Delta(\overline{M}),\overline{M}) \ge (\Delta/4)\,\mathbb{I}\{\gamma \le d/(12\Delta)\}$ for all $\gamma > 0$.

Significance

The bound shows that the DEC of linear bandits under Euclidean geometry is of order $d/\gamma$, which matches, up to constants, the upper bound $\mathsf{dec}^{\mathrm{Sq}}_\gamma \le d/(4\gamma)$ on the square-loss variant of the DEC certified by the strategy of Proposition 6.1. Through Theorem 3.2 it gives the regret lower bound $\Omega(\sqrt{dT})$ for every algorithm. Proposition 6.8 shows that the DEC gives meaningful lower bounds even for classes of models with a fixed gap.

All results are proved in the paper. None has a machine-checked proof. The mission produces a formal statement of the linear-bandit lower bound with its radius corrected, the hard-family lemma (Lemma 5.1) in a form that applies to infinite decision spaces and to range-free $u_i$, and the Rademacher Hellinger estimates that later DEC lower bounds reuse.

Difficulty

The arithmetic of the construction is short. The work is in the infrastructure.

• The infimum runs over all Borel probability measures on the ball, not over finitely supported ones. Lemma 5.1 must therefore be proved for Bochner integrals, with the integrability of the payoff established from its continuity on the compact ball.
• The bound $\sum_i \pi_i \le \sqrt d \le d/2$ is Cauchy–Schwarz on $\mathbb{R}^d$ and needs $d \ge 4$.
• The value $\langle\theta_i, \pi_{\theta_i}\rangle = \Delta$ must come from the selector hypothesis plus Cauchy–Schwarz, because the selector is not given explicitly.
• Lemma 5.1 cannot be applied in the form printed in Definition 5.1: there $u_i$ takes values in $[0,1]$, but the family's $u_i(\pi) = \pi_i$ can be negative. The lemma is needed without the range conditions.

Formalization scope

• Outcomes. They are finite: the $\pm1$ outcome is encoded on Bool, and models are the Rademacher laws $\mathrm{Rad}(\langle\theta,\pi\rangle)$, identified with their parameters $\theta \in \mathbb{B}^d$. The paper's class contains every reward law on $[-1,1]$ with linear mean. The Rademacher subclass has a smaller localized class, so a lower bound for it implies the paper's.
• Decisions. For the goal they range over the ball itself (an infinite space with its Borel $\sigma$-algebra), and decision distributions are arbitrary ProbabilityMeasures on it.
• The DEC is unfolded. For every $p$ some model of the localized class attains the bound. This is what the proof shows, and it implies the inf–sup inequality.
• Selectors. $\pi_M$ is a selector with a maximizer hypothesis, so statements hold for every choice of maximizer.
• Added hypotheses. Lemma 5.1 carries $\alpha, \beta \ge 0$ and integrability of its four functions. Proposition 6.8 carries $d \ge 2$.
• No trivializing reading. The integrals in the goal are genuine: the integrand is bounded and continuous, and a sanity file proves integrability, so the Bochner convention $\int f = 0$ for non-integrable $f$ never applies. The goal's quantifier over $p$ is not restricted. The radius $2d/(3\gamma)$ is the smallest the construction allows.
• Definitions and reuse. The mission defines the unit ball, $\mathrm{Rad}$, the linear model, the regret $g^\theta$, and the localized class over a measurable decision space. It references the published hellingerSq, fM and decGf. The general Lemma 5.1 and Lemma A.8 are reusable for every DEC lower bound in §§5–7.

Contributions welcome: proofs of the milestones, a version of the goal through an explicit inf–sup definition of the DEC over measures, and the general model class with arbitrary reward laws on $[-1,1]$.

Selected references

• D. J. Foster, S. M. Kakade, J. Qian, A. Rakhlin, The Statistical Complexity of Interactive Decision Making, arXiv preprint, v3, 2023. https://arxiv.org/abs/2112.13487
• T. Lattimore, Cs. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020 (linear bandits, Ch. 19–24). https://doi.org/10.1017/9781108571401
• D. J. Foster, C. Gentile, M. Mohri, J. Zimmert, Adapting to Misspecification in Contextual Bandits, NeurIPS 2020 (Proposition 6.1's strategy). https://arxiv.org/abs/2107.05745