Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

Bandit Algorithms

125 missions · 55 completed

Missions

Open70Completed55All125
🏆Completed
Machine LearningOperations Research·Captain: Shuze Chen

Bandit Algorithms III: Asymptotic and Minimax Optimality of UCBTextbook

The basic UCB regret bound of Mission II is logarithmic but not tight: its leading constant 16/Δi16/\Delta_i16/Δi​ is eight times the information-theoretic limit, and its worst-case rate carries a spurious log⁡n\sqrt{\log n}logn​. Chapters 8–9 of Lattimore–Szepesvári close both gaps. A refined confidence schedule f(t)=1+tlog⁡2tf(t) = 1 + t\log^2 tf(t)=1+tlog2t yields the asymptotically optimal lim sup⁡n→∞Rn/log⁡n≤∑i:Δi>02/Δi\limsup_{n\to\infty} R_n/\log n \le \sum_{i:\Delta_i>0} 2/\Delta_ilimsupn→∞​Rn​/logn≤∑i:Δi​>0​2/Δi​ — exactly matching the instance-dependent lower bound of Mission VII for Gaussian noise. The MOSS index μ^i+4Tilog⁡+ ⁣(nkTi)\hat\mu_i + \sqrt{\tfrac{4}{T_i}\log^+\!\big(\tfrac{n}{k T_i}\big)}μ^​i​+Ti​4​log+(kTi​n​)​ achieves minimax regret Rn≤39kn+∑iΔiR_n \le 39\sqrt{kn} + \sum_i \Delta_iRn​≤39kn​+∑i​Δi​, matching the Ω(kn)\Omega(\sqrt{kn})Ω(kn​) lower bound up to a constant. These two theorems are the gold standard for finite-armed stochastic bandits.

24 thms10 active usersReviewed
🏆Completed
Machine LearningOperations Research·Captain: Shuze Chen

Bandit Algorithms II: Stochastic Bandits and the UCB AlgorithmTextbook

A learner repeatedly chooses one of kkk slot machines, observes only the reward of the chosen arm, and wants to earn almost as much as the best arm in hindsight. This is the stochastic multi-armed bandit, the canonical model of the exploration–exploitation dilemma. This mission formalizes the model (environments, policies, regret, and the regret decomposition Rn=∑iΔi E[Ti(n)]R_n = \sum_i \Delta_i\,\mathbb{E}[T_i(n)]Rn​=∑i​Δi​E[Ti​(n)]) and the two classical algorithms of Chapters 6–7 of Lattimore–Szepesvári: Explore-Then-Commit and the Upper Confidence Bound algorithm built on the optimism principle. The goal theorem is the instance-dependent UCB regret bound Rn≤3∑iΔi+∑i:Δi>016log⁡(n)/ΔiR_n \le 3\sum_i \Delta_i + \sum_{i:\Delta_i>0} 16\log(n)/\Delta_iRn​≤3∑i​Δi​+∑i:Δi​>0​16log(n)/Δi​ — logarithmic regret with explicit constants, the single most cited result of bandit theory — together with its distribution-free companion Rn≤8nklog⁡n+3∑iΔiR_n \le 8\sqrt{nk\log n} + 3\sum_i \Delta_iRn​≤8nklogn​+3∑i​Δi​.

27 thms9 active usersReviewed
🏆Completed
Machine LearningOperations Research·Captain: Shuze Chen

Bandit Algorithms XIV: Bayesian Bandits, the Gittins Index and Thompson SamplingTextbook

The oldest bandit algorithm (Thompson, 1933) is also the most modern: sample a parameter from the posterior and act greedily. Chapters 34–36 of Lattimore–Szepesvári develop the Bayesian view in two crowning results. The Gittins index theorem: for infinite-horizon discounted Markov bandits, the seemingly intractable dynamic program is solved exactly by an index policy — each arm gets a retirement-value index computable arm-by-arm, and playing the largest index is Bayesian optimal. And the frequentist analysis of Thompson sampling — the goal theorem: with Gaussian posteriors, Thompson sampling on 1-subgaussian bandits achieves lim⁡n→∞Rn/log⁡n=∑i:Δi>02/Δi\lim_{n\to\infty} R_n/\log n = \sum_{i:\Delta_i>0} 2/\Delta_ilimn→∞​Rn​/logn=∑i:Δi​>0​2/Δi​, exactly asymptotically optimal, alongside the minimax-grade Rn≤Cknlog⁡nR_n \le C\sqrt{kn\log n}Rn​≤Cknlogn​. Together they explain why posterior sampling is both principled and practically dominant.

88 thms7 active usersReviewed
🏆Completed
Machine LearningOperations Research·Captain: Shuze Chen

Bandit Algorithms XI: Lower Bounds for Stochastic Linear BanditsTextbook

Is the dnd\sqrt{n}dn​ regret of LinUCB (Mission X) an artifact of the algorithm or a law of nature? Chapters 24–25 of Lattimore–Szepesvári prove it is essentially unimprovable. On the unit ball there is a parameter θ\thetaθ with ∥θ∥22=d2/(48n)\|\theta\|_2^2 = d^2/(48n)∥θ∥22​=d2/(48n) forcing Rn≥dn163R_n \ge \frac{d\sqrt{n}}{16\sqrt{3}}Rn​≥163​dn​​ — the goal theorem — and the hypercube gives the same Ω(dn)\Omega(d\sqrt{n})Ω(dn​) rate. The asymptotic chapter is more striking still: for fixed finite action sets, the instance-optimal constant c(A,θ)c(\mathcal{A},\theta)c(A,θ) is characterized by an allocation program, and optimism itself is provably suboptimal — LinUCB and Thompson sampling cannot achieve it, because exploration must sometimes deliberately play actions optimism would never touch. These lower bounds define the targets for the entire linear-bandit literature.

14 thms7 active usersReviewed
🏆Completed
Machine LearningOperations Research·Captain: Shuze Chen

Bandit Algorithms V: Adversarial Bandits and Exp3Textbook

What if the rewards are not random at all, but chosen by an adversary who knows your algorithm? Remarkably, a randomized learner can still compete with the best fixed arm in hindsight. Chapters 11–12 of Lattimore–Szepesvári develop the adversarial kkk-armed bandit: rewards xti∈[0,1]x_{ti} \in [0,1]xti​∈[0,1] are an arbitrary fixed matrix, the learner samples At∼PtA_t \sim P_tAt​∼Pt​, and regret is measured against max⁡i∑txti\max_i \sum_t x_{ti}maxi​∑t​xti​. The exponential-weights algorithm Exp3, fed by importance-weighted loss estimates X^ti=1−1{At=i}(1−Xt)/Pti\hat X_{ti} = 1 - \mathbb{1}\{A_t = i\}(1 - X_t)/P_{ti}X^ti​=1−1{At​=i}(1−Xt​)/Pti​, achieves Rn≤2nklog⁡kR_n \le \sqrt{2nk\log k}Rn​≤2nklogk​ — the goal theorem. The companion Exp3-IX, which deliberately biases its estimator, upgrades this to a bound holding with high probability rather than only in expectation. These results are the foundation of all adversarial online learning with partial feedback.

12 thms7 active usersReviewed
🏆Completed
Machine LearningOperations ResearchProbability·Captain: mikedeng1

Improved Algorithms for Linear Stochastic Bandits I: High-Probability Regret Bound for the OFUL AlgorithmResearch Paper

Motivation

In a linear stochastic bandit, a learner repeatedly chooses an action from a set of vectors and receives a noisy reward whose mean is linear in the action. The model underlies contextual recommendation, adaptive routing and dynamic pricing, where each option is described by features and the payoff of a feature vector must be learned while it is exploited. The quality of a strategy is measured by its regret: the reward lost, relative to always playing the best action, over the first nnn rounds.

The optimism-in-the-face-of-uncertainty principle (play as if the most favourable parameter consistent with the data were true) was introduced for linear bandits by Auer (2002), and developed by Dani, Hayes and Kakade (2008) (ConfidenceBall, regret O(dnlog⁡3/2n)O(d\sqrt n\log^{3/2} n)O(dn​log3/2n) with confidence sets from a union bound over time) and Rusmevichientong and Tsitsiklis (2010). Abbasi-Yadkori, Pál and Szepesvári (NIPS 2011) replaced the union bound by a self-normalized martingale inequality that holds uniformly in time. It gives smaller confidence ellipsoids and, through them, a high-probability regret bound for the resulting algorithm, OFUL, that improves the earlier ones by logarithmic factors. The inequality became the standard tool for linear and kernelized bandits and for linear reinforcement learning.

Setting

Fix a dimension d≥1d \ge 1d≥1 and an unknown parameter θ∗∈Rd\theta_* \in \mathbb R^dθ∗​∈Rd. In round t=1,2,…t = 1, 2, \dotst=1,2,… the learner is given a nonempty decision set Dt⊆RdD_t \subseteq \mathbb R^dDt​⊆Rd, chooses Xt∈DtX_t \in D_tXt​∈Dt​, and observes the reward

Yt=⟨Xt,θ∗⟩+ηt.Y_t = \langle X_t, \theta_* \rangle + \eta_t .Yt​=⟨Xt​,θ∗​⟩+ηt​.

There is a filtration {Ft}t≥0\{F_t\}_{t \ge 0}{Ft​}t≥0​ such that XtX_tXt​ is Ft−1F_{t-1}Ft−1​-measurable and ηt\eta_tηt​ is FtF_tFt​-measurable and conditionally RRR-sub-Gaussian: E[eληt∣Ft−1]≤exp⁡(λ2R2/2)\mathbf E[e^{\lambda\eta_t} \mid F_{t-1}] \le \exp(\lambda^2R^2/2)E[eληt​∣Ft−1​]≤exp(λ2R2/2) for all λ∈R\lambda \in \mathbb Rλ∈R, with R≥0R \ge 0R≥0 fixed.

For a regularization parameter λ>0\lambda > 0λ>0 let V‾t=λI+∑s=1tXsXs⊤\overline V_t = \lambda I + \sum_{s=1}^t X_sX_s^\topVt​=λI+∑s=1t​Xs​Xs⊤​ and let θ^t=V‾t−1∑s=1tYsXs\widehat\theta_t = \overline V_t^{-1}\sum_{s=1}^t Y_sX_sθt​=Vt−1​∑s=1t​Ys​Xs​ be the regularized least-squares estimate. With ∥v∥A=v⊤Av\|v\|_A = \sqrt{v^\top A v}∥v∥A​=v⊤Av​ and a known bound ∥θ∗∥2≤S\|\theta_*\|_2 \le S∥θ∗​∥2​≤S, the confidence ellipsoid is

Ct={θ:∥θ^t−θ∥V‾t≤R2log⁡(det⁡(V‾t)1/2det⁡(λI)−1/2/δ)+λ1/2S}.C_t = \Big\{\theta : \|\widehat\theta_t - \theta\|_{\overline V_t} \le R\sqrt{2\log\big(\det(\overline V_t)^{1/2}\det(\lambda I)^{-1/2}/\delta\big)} + \lambda^{1/2}S\Big\}.Ct​={θ:∥θt​−θ∥Vt​​≤R2log(det(Vt​)1/2det(λI)−1/2/δ)​+λ1/2S}.

The OFUL algorithm chooses, in round ttt, a pair (Xt,θ~t)(X_t, \widetilde\theta_t)(Xt​,θt​) maximizing ⟨x,θ⟩\langle x, \theta \rangle⟨x,θ⟩ over Dt×Ct−1D_t \times C_{t-1}Dt​×Ct−1​. The pseudo-regret is Rn=∑t=1n⟨xt∗−Xt,θ∗⟩R_n = \sum_{t=1}^n \langle x^*_t - X_t, \theta_* \rangleRn​=∑t=1n​⟨xt∗​−Xt​,θ∗​⟩, where ⟨xt∗,θ∗⟩=max⁡x∈Dt⟨x,θ∗⟩\langle x^*_t, \theta_*\rangle = \max_{x\in D_t}\langle x,\theta_*\rangle⟨xt∗​,θ∗​⟩=maxx∈Dt​​⟨x,θ∗​⟩.

Formalization targets

Goal: Theorem 3, the regret of OFUL

If ∥Xt∥2≤L\|X_t\|_2 \le L∥Xt​∥2​≤L, ⟨x,θ∗⟩∈[−1,1]\langle x, \theta_*\rangle \in [-1,1]⟨x,θ∗​⟩∈[−1,1] for all x∈Dtx \in D_tx∈Dt​, and λ≥max⁡(1,L2)\lambda \ge \max(1, L^2)λ≥max(1,L2), then for every δ>0\delta > 0δ>0, with probability at least 1−δ1 - \delta1−δ,

∀n≥0,Rn≤4ndlog⁡(λ+nL2/d)(λ1/2S+R2log⁡(1/δ)+dlog⁡(1+nL2/(λd))).\forall n \ge 0, \quad R_n \le 4\sqrt{nd\log(\lambda + nL^2/d)}\Big(\lambda^{1/2}S + R\sqrt{2\log(1/\delta) + d\log(1 + nL^2/(\lambda d))}\Big).∀n≥0,Rn​≤4ndlog(λ+nL2/d)​(λ1/2S+R2log(1/δ)+dlog(1+nL2/(λd))​).

Milestone: Theorem 1, the self-normalized bound

For any positive definite VVV, V‾t=V+∑s≤tXsXs⊤\overline V_t = V + \sum_{s\le t}X_sX_s^\topVt​=V+∑s≤t​Xs​Xs⊤​ and St=∑s≤tηsXsS_t = \sum_{s \le t}\eta_sX_sSt​=∑s≤t​ηs​Xs​: with probability at least 1−δ1-\delta1−δ, for all t≥0t \ge 0t≥0,

∥St∥V‾t−12≤2R2log⁡(det⁡(V‾t)1/2det⁡(V)−1/2/δ).\|S_t\|^2_{\overline V_t^{-1}} \le 2R^2\log\big(\det(\overline V_t)^{1/2}\det(V)^{-1/2}/\delta\big).∥St​∥Vt−1​2​≤2R2log(det(Vt​)1/2det(V)−1/2/δ).

Milestones: Theorem 2, the confidence ellipsoids

With probability at least 1−δ1 - \delta1−δ, θ∗∈Ct\theta_* \in C_tθ∗​∈Ct​ for all t≥0t \ge 0t≥0 (first claim). If ∥Xt∥2≤L\|X_t\|_2 \le L∥Xt​∥2​≤L, then with probability at least 1−δ1-\delta1−δ, for all ttt, ∥θ^t−θ∗∥V‾t≤Rdlog⁡((1+tL2/λ)/δ)+λ1/2S\|\widehat\theta_t - \theta_*\|_{\overline V_t} \le R\sqrt{d\log((1 + tL^2/\lambda)/\delta)} + \lambda^{1/2}S∥θt​−θ∗​∥Vt​​≤Rdlog((1+tL2/λ)/δ)​+λ1/2S (second claim, stated here for d≥2d \ge 2d≥2).

Significance

Theorem 3 bounds the regret of OFUL by O(dnlog⁡n)O(d\sqrt n\log n)O(dn​logn) with high probability, uniformly over the horizon, so it holds for an unknown horizon without restarting. The bound applies to arbitrary, even adversarially changing, decision sets. Theorem 1 is the ingredient that makes this possible: a deviation bound for a vector-valued martingale, normalized by its own random covariance, that holds for all times simultaneously and whose logarithmic term is a determinant rather than a union-bound count. The same inequality underlies regret analyses of generalized linear bandits, kernelized bandits, linear Markov decision processes and many confidence-sequence constructions.

All three results are proved in the paper's appendices (not included in the source file used here). None of them is formalized in the stated generality. Prove2Me holds the special cases V=λIV = \lambda IV=λI, R=1R = 1R=1, δ<1\delta < 1δ<1 of Theorems 1 and 2 (from the Bandit Algorithms textbook series), a pathwise LinUCB regret lemma that assumes the confidence event, and the elliptical potential lemma. A formal proof of Theorem 3 would be the first machine-checked high-probability regret bound for OFUL with the paper's confidence sets.

Difficulty

The actions are chosen adaptively, by an argmax over a data-dependent set, so the sequence XtX_tXt​ has no independence structure and the least-squares estimate is not a sum of independent terms. A fixed-design concentration bound followed by a union bound over time and over a covering of the sphere loses logarithmic factors and does not produce the determinant in the radius; that is the route of the earlier work that Theorem 1 improves. Theorem 1 must hold for all times at once for a quantity normalized by the random matrix V‾t\overline V_tVt​, which is itself built from the adaptively chosen actions; a bound for each fixed ttt does not give it.

Formalization scope

Vectors are Fin d → ℝ, matrices Matrix (Fin d) (Fin d) ℝ, and ∥x∥A\|x\|_A∥x∥A​ is Real.sqrt (x ⬝ᵥ A *ᵥ x). Rounds are indexed t+1t+1t+1 for t:Nt : ℕt:N, so sums over s≤ts \le ts≤t are sums over Finset.range t at index s + 1, and the time-0 objects are empty sums. The probability space is standard Borel, as Mathlib's conditional sub-Gaussianity (HasCondSubgaussianMGF, variance proxy R2R^2R2) requires; this is an added hypothesis. Every "with probability at least 1−δ1-\delta1−δ, for all ttt" is stated as an outer-measure bound ≤δ\le \delta≤δ on the failure event, with the time quantifier inside the event. det⁡(⋅)1/2\det(\cdot)^{1/2}det(⋅)1/2 is the real square root of the determinant; the matrices inverted are positive definite, so Lean's junk inverse never occurs.

OFUL is a predicate on the whole process: in every round the chosen pair maximizes ⟨x,θ⟩\langle x,\theta\rangle⟨x,θ⟩ over Dt×Ct−1D_t \times C_{t-1}Dt​×Ct−1​, with any tie-breaking. Runs exist whenever the decision sets are nonempty and compact. The measurability of the actions is assumed, as in Theorem 1. The optimal reward ⟨xt∗,θ∗⟩\langle x^*_t, \theta_*\rangle⟨xt∗​,θ∗​⟩ is the supremum over DtD_tDt​, finite because of the reward bound.

Two corrections to the printed Theorem 3 are made and disclosed. The printed nL/dnL/dnL/d is replaced by nL2/dnL^2/dnL2/d, which is what the determinant–trace bound det⁡V‾n≤(λ+nL2/d)d\det\overline V_n \le (\lambda + nL^2/d)^ddetVn​≤(λ+nL2/d)d gives; for L≤1L \le 1L≤1 the corrected bound implies the printed one. The hypothesis λ≥max⁡(1,L2)\lambda \ge \max(1, L^2)λ≥max(1,L2) is added: for λ<1\lambda < 1λ<1 the printed logarithm can be negative, and the printed bound would then assert Rn≤0R_n \le 0Rn​≤0. In the second claim of Theorem 2, d≥2d \ge 2d≥2 is added, because at d=1d = 1d=1 the claim does not follow from the first claim and the paper's proof is not available.

The goal is a probability bound over the noise, not the pathwise statement "if θ∗∈Ct−1\theta_* \in C_{t-1}θ∗​∈Ct−1​ for all ttt then Rn≤…R_n \le \dotsRn​≤…". The pathwise statement assumes the confidence event instead of proving it, and is already on the platform. The confidence sets inside the OFUL predicate use the same δ\deltaδ as the conclusion.

Needed infrastructure: maximal inequalities for nonnegative supermartingales, Gaussian integrals of quadratic forms on Rd\mathbb R^dRd, log-determinant bounds for sums of rank-one updates, and the determinant–trace inequality. The platform rows BanditAlgorithm.self_normalized_martingale_bound, BanditAlgorithm.least_squares_confidence_ellipsoid and BanditAlgorithm.elliptical_potential_lemma are referenced as tools. Proofs of the milestones, generalizations of the existing special cases to general VVV and RRR, and reusable determinant lemmas are all welcome.

Selected references

  • Y. Abbasi-Yadkori, D. Pál, Cs. Szepesvári, Improved Algorithms for Linear Stochastic Bandits, Advances in Neural Information Processing Systems 24 (NIPS), 2011. https://proceedings.neurips.cc/paper/2011
  • P. Auer, Using Confidence Bounds for Exploitation-Exploration Trade-offs, Journal of Machine Learning Research 3, 2002. https://www.jmlr.org/papers/v3/auer02a.html
  • V. Dani, T. P. Hayes, S. M. Kakade, Stochastic Linear Optimization under Bandit Feedback, COLT, 2008. http://colt2008.cs.helsinki.fi/papers/80-Dani.pdf
  • P. Rusmevichientong, J. N. Tsitsiklis, Linearly Parameterized Bandits, Mathematics of Operations Research 35(2), 2010. https://doi.org/10.1287/moor.1100.0446
  • T. Lattimore, Cs. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapters 19–20. https://doi.org/10.1017/9781108571401
12 thms6 active usersReviewed
🏆Completed
Machine LearningOperations Research·Captain: Shuze Chen

Bandit Algorithms XVI: Markov Decision Processes and UCRL2Textbook

The final step from bandits to reinforcement learning: actions now change the state of the world. Chapter 38 of Lattimore–Szepesvári studies online learning in an unknown Markov decision process with SSS states, AAA actions and rewards in [0,1][0,1][0,1]. The optimism principle of Mission II scales up: UCRL2 maintains confidence sets over transition kernels, solves an extended MDP by extended value iteration, and recomputes only when a state-action count doubles. The goal theorem: with probability 1−δ1-\delta1−δ, R^n<C D(M) SAnlog⁡(nSA/δ)\hat R_n < C\,D(M)\,S\sqrt{An\log(nSA/\delta)}R^n​<CD(M)SAnlog(nSA/δ)​, where D(M)D(M)D(M) is the diameter of the MDP — sublinear regret with no prior knowledge of the dynamics. The matching lower bound E[R^n]≥C′DSAn\mathbb{E}[\hat R_n] \ge C'\sqrt{DSAn}E[R^n​]≥C′DSAn​ brackets the true complexity of tabular reinforcement learning up to DS\sqrt{DS}DS​.

35 thms6 active users
🏆Completed
Machine LearningOperations Research·Captain: Shuze Chen

Bandit Algorithms VII: Lower Bounds for Finite-Armed BanditsTextbook

How well can any algorithm possibly do? Chapters 13–17 of Lattimore–Szepesvári answer with three matching impossibility results. The divergence decomposition identifies the information a policy collects: D(Pνπ,Pν′π)=∑iE[Ti(n)]D(Pi,Pi′)D(\mathbb{P}_{\nu\pi}, \mathbb{P}_{\nu'\pi}) = \sum_i \mathbb{E}[T_i(n)] D(P_i, P_i')D(Pνπ​,Pν′π​)=∑i​E[Ti​(n)]D(Pi​,Pi′​). Feeding it into the Bretagnolle–Huber inequality of Mission VI yields the goal theorem — the minimax lower bound Rn≥127(k−1)nR_n \ge \frac{1}{27}\sqrt{(k-1)n}Rn​≥271​(k−1)n​ over Gaussian bandits, showing MOSS (Mission III) is optimal up to a constant. The same machinery gives the instance-dependent bound of Lai–Robbins type: every consistent policy suffers lim inf⁡nRn/log⁡n≥∑i:Δi>0Δi/dinf⁡(Pi,μ∗,Mi)\liminf_n R_n/\log n \ge \sum_{i:\Delta_i>0} \Delta_i / d_{\inf}(P_i, \mu^*, \mathcal{M}_i)liminfn​Rn​/logn≥∑i:Δi​>0​Δi​/dinf​(Pi​,μ∗,Mi​), certifying the asymptotic optimality of the UCB of Mission III and KL-UCB of Mission IV, and a high-probability lower bound showing the Exp3-IX guarantees of Mission V cannot be improved.

13 thms6 active usersReviewed
🏆Completed
Machine LearningOperations ResearchProbability+1·Captain: mikedeng1

Optimal Best Arm Identification with Fixed Confidence IV: Asymptotic Optimality of the Track-and-Stop StrategyResearch Paper

Motivation

In best arm identification with fixed confidence, a learner samples KKK unknown distributions (arms) sequentially and must, as early as possible, name the arm with the largest mean, while being wrong with probability at most a prescribed risk δ\deltaδ. The problem models adaptive A/B/n testing, clinical and simulation-based selection among alternatives, and the "ranking and selection" problem of operations research and simulation optimization. The quantity of interest is the sample complexity Eμ[τδ]\mathbb E_{\boldsymbol\mu}[\tau_\delta]Eμ​[τδ​], the expected number of samples a strategy takes before stopping.

Timeline of the question this mission formalizes:

  • Chernoff (1959) introduced sequential tests based on generalized likelihood ratios for adaptive design of experiments, with a finite set of hypotheses (doi:10.1214/aoms/1177706205).
  • Kaufmann, Cappé and Garivier (2016, JMLR) proved a change-of-measure lower bound on the sample complexity of every δ\deltaδ-PAC strategy (arXiv:1407.4443).
  • Garivier and Kaufmann (COLT 2016) identified the exact constant T∗(μ)T^*(\boldsymbol\mu)T∗(μ) in that lower bound and gave the first strategy, Track-and-Stop, whose sample complexity matches it asymptotically as δ→0\delta\to0δ→0 (arXiv:1602.04589). This mission covers the upper-bound half of that paper.

Setting

A canonical one-parameter exponential family is a family of laws νθ\nu_\thetaνθ​, θ∈Θ\theta\in\Thetaθ∈Θ, on R\mathbb RR with density exp⁡(θx−b(θ))\exp(\theta x-b(\theta))exp(θx−b(θ)) with respect to a reference measure ξ\xiξ; bbb is twice differentiable and strictly convex, and νθ\nu_\thetaνθ​ has mean b˙(θ)\dot b(\theta)b˙(θ). Bernoulli, Poisson and Gaussian laws with known variance are examples. The divergence d(μ,μ′)d(\mu,\mu')d(μ,μ′) is the Kullback–Leibler divergence between the members with means μ\muμ and μ′\mu'μ′.

A bandit model μ=(μ1,…,μK)\boldsymbol\mu=(\mu_1,\dots,\mu_K)μ=(μ1​,…,μK​) assigns a member of the family to each arm. The class S\mathcal SS consists of models with a unique optimal arm a∗(μ)a^*(\boldsymbol\mu)a∗(μ). At each round t=1,2,…t=1,2,\dotst=1,2,… the learner picks an arm AtA_tAt​ as a function of past observations, observes a reward drawn from that arm's law, and at a stopping time τδ\tau_\deltaτδ​ recommends an arm. Na(t)N_a(t)Na​(t) is the number of draws of arm aaa in the first ttt rounds and μ^a(t)\hat\mu_a(t)μ^​a​(t) its empirical mean.

With Alt(μ)={λ∈S:a∗(λ)≠a∗(μ)}\mathrm{Alt}(\boldsymbol\mu)=\{\boldsymbol\lambda\in\mathcal S: a^*(\boldsymbol\lambda)\ne a^*(\boldsymbol\mu)\}Alt(μ)={λ∈S:a∗(λ)=a∗(μ)} and ΣK\Sigma_KΣK​ the probability simplex, the characteristic time is

T∗(μ)−1=sup⁡w∈ΣK inf⁡λ∈Alt(μ) ∑a=1Kwa d(μa,λa),T^*(\boldsymbol\mu)^{-1}=\sup_{w\in\Sigma_K}\ \inf_{\boldsymbol\lambda\in\mathrm{Alt}(\boldsymbol\mu)}\ \sum_{a=1}^K w_a\,d(\mu_a,\lambda_a),T∗(μ)−1=w∈ΣK​sup​ λ∈Alt(μ)inf​ a=1∑K​wa​d(μa​,λa​),

and the maximizer w∗(μ)w^*(\boldsymbol\mu)w∗(μ) are the optimal proportions of arm draws.

Track-and-Stop combines two ingredients:

  • a sampling rule that tracks the plug-in proportions w∗(μ^(t))w^*(\hat{\boldsymbol\mu}(t))w∗(μ^​(t)) while forcing each arm to be drawn about t\sqrt tt​ times: C-Tracking tracks the cumulated sum of projections of w∗(μ^(s))w^*(\hat{\boldsymbol\mu}(s))w∗(μ^​(s)) onto ΣKϵs={w∈ΣK:wa≥ϵs}\Sigma^{\epsilon_s}_K=\{w\in\Sigma_K: w_a\ge\epsilon_s\}ΣKϵs​​={w∈ΣK​:wa​≥ϵs​}, ϵs=(K2+s)−1/2/2\epsilon_s=(K^2+s)^{-1/2}/2ϵs​=(K2+s)−1/2/2; D-Tracking draws an under-sampled arm when some Na(t)<t−K/2N_a(t)<\sqrt t-K/2Na​(t)<t​−K/2, and otherwise the arm maximizing t wa∗(μ^(t))−Na(t)t\,w^*_a(\hat{\boldsymbol\mu}(t))-N_a(t)twa∗​(μ^​(t))−Na​(t);
  • Chernoff's stopping rule, which stops at the first ttt at which some arm aaa beats every other arm bbb in a generalized likelihood ratio test, Za,b(t)>β(t,δ)Z_{a,b}(t)>\beta(t,\delta)Za,b​(t)>β(t,δ), here with β(t,δ)=log⁡(r(t)/δ)\beta(t,\delta)=\log(r(t)/\delta)β(t,δ)=log(r(t)/δ).

Formalization targets

Goal: Theorem 14 (p. 13)

For α∈[1,e/2]\alpha\in[1,e/2]α∈[1,e/2] and r(t)=O(tα)r(t)=O(t^\alpha)r(t)=O(tα), Chernoff's stopping rule with β(t,δ)=log⁡(r(t)/δ)\beta(t,\delta)=\log(r(t)/\delta)β(t,δ)=log(r(t)/δ) combined with C-Tracking or D-Tracking satisfies

lim sup⁡δ→0Eμ[τδ]log⁡(1/δ)≤α T∗(μ)\limsup_{\delta\to0}\frac{\mathbb E_{\boldsymbol\mu}[\tau_\delta]}{\log(1/\delta)}\le\alpha\,T^*(\boldsymbol\mu)δ→0limsup​log(1/δ)Eμ​[τδ​]​≤αT∗(μ)

for every μ∈S\boldsymbol\mu\in\mathcal Sμ∈S.

Milestones

  • Lemma 15 (p. 20): greedy tracking of cumulated proportions P(k)P(k)P(k) keeps max⁡i∣Ni(n)−Pi(n)∣≤K−1\max_i|N_i(n)-P_i(n)|\le K-1maxi​∣Ni​(n)−Pi​(n)∣≤K−1.
  • Lemma 7 (p. 7): C-Tracking ensures Na(t)≥t+K2−2KN_a(t)\ge\sqrt{t+K^2}-2KNa​(t)≥t+K2​−2K and max⁡a∣Na(t)−∑s<twa∗(μ^(s))∣≤K(1+t)\max_a|N_a(t)-\sum_{s<t}w^*_a(\hat{\boldsymbol\mu}(s))|\le K(1+\sqrt t)maxa​∣Na​(t)−∑s<t​wa∗​(μ^​(s))∣≤K(1+t​).
  • Lemma 8 (p. 7): D-Tracking ensures Na(t)≥(t−K/2)+−1N_a(t)\ge(\sqrt t-K/2)_+-1Na​(t)≥(t​−K/2)+​−1, and proportions within 3(K−1)ϵ3(K-1)\epsilon3(K−1)ϵ of w∗(μ)w^*(\boldsymbol\mu)w∗(μ) after a time tϵt_\epsilontϵ​ that does not depend on the trajectory, once the plug-in targets are within ϵ\epsilonϵ.
  • Proposition 9 (p. 8): under either rule, Na(t)/t→wa∗(μ)N_a(t)/t\to w^*_a(\boldsymbol\mu)Na​(t)/t→wa∗​(μ) almost surely.
  • Lemma 18 (p. 27): an explicit xxx with c1x≥log⁡(c2xα)c_1x\ge\log(c_2x^\alpha)c1​x≥log(c2​xα) for α∈[1,e/2]\alpha\in[1,e/2]α∈[1,e/2].
  • Proposition 13 (p. 11): with any sampling rule whose proportions converge almost surely to w∗w^*w∗, τδ<∞\tau_\delta<\inftyτδ​<∞ almost surely and lim sup⁡δ→0τδ/log⁡(1/δ)≤αT∗(μ)\limsup_{\delta\to0}\tau_\delta/\log(1/\delta)\le\alpha T^*(\boldsymbol\mu)limsupδ→0​τδ​/log(1/δ)≤αT∗(μ) almost surely.

Significance

Theorem 1 of the same paper shows Eμ[τδ]≥T∗(μ) kl(δ,1−δ)\mathbb E_{\boldsymbol\mu}[\tau_\delta]\ge T^*(\boldsymbol\mu)\,\mathrm{kl}(\delta,1-\delta)Eμ​[τδ​]≥T∗(μ)kl(δ,1−δ) for every δ\deltaδ-PAC strategy, and kl(δ,1−δ)∼log⁡(1/δ)\mathrm{kl}(\delta,1-\delta)\sim\log(1/\delta)kl(δ,1−δ)∼log(1/δ). Theorem 14 with α=1\alpha=1α=1 therefore shows that the lower bound is attained: T∗(μ)T^*(\boldsymbol\mu)T∗(μ) is the exact asymptotic sample complexity of best arm identification in exponential family models, and Track-and-Stop is asymptotically optimal.

The result is proved in the paper. What is not available is a machine-checked proof for exponential families. The platform already holds a Lean development of the Gaussian case following Lattimore and Szepesvári, Bandit Algorithms, Ch. 33, stated for one existentially chosen policy with a different threshold. This mission asks for the universal statement: every run of either tracking rule, for every exponential family, with the paper's thresholds. The tracking lemmas (Lemmas 15, 7, 8) are deterministic combinatorics and reusable by any tracking-based algorithm.

Difficulty

The obvious argument plugs the almost-sure behaviour of Proposition 13 into an expectation. That step fails: almost-sure convergence of τδ/log⁡(1/δ)\tau_\delta/\log(1/\delta)τδ​/log(1/δ) does not control E[τδ]\mathbb E[\tau_\delta]E[τδ​], because on the rare events where the empirical means are far from μ\boldsymbol\muμ the stopping time may be very large. Theorem 14 needs a quantitative concentration of μ^(t)\hat{\boldsymbol\mu}(t)μ^​(t) on events whose complements have summable probability, which in turn relies on the forced exploration guaranteed by the t\sqrt tt​ lower bounds on Na(t)N_a(t)Na​(t) (the concentration step of App. D, Lemmas 19–20).

A second obstacle is the regularity of w∗w^*w∗: the tracking lemmas only transfer convergence of μ^(t)\hat{\boldsymbol\mu}(t)μ^​(t) to convergence of Na(t)/tN_a(t)/tNa​(t)/t through the continuity of μ↦w∗(μ)\boldsymbol\mu\mapsto w^*(\boldsymbol\mu)μ↦w∗(μ) on S\mathcal SS, proved from the characterization of w∗w^*w∗ in §2.2 (Proposition 6). The GLR statistic also needs its closed form (7) near μ\boldsymbol\muμ, which requires the empirical means to lie in the interior of the mean space.

Formalization scope

  • Model. The exponential family is a structure (ξ,Θ,b)(\xi,\Theta,b)(ξ,Θ,b) with Θ\ThetaΘ a nonempty open interval, each νθ\nu_\thetaνθ​ normalized, bbb twice continuously differentiable and b¨>0\ddot b>0b¨>0 on Θ\ThetaΘ. Openness and b¨>0\ddot b>0b¨>0 are added to the paper's "convex, twice differentiable"; strict convexity is what makes νμ\nu^\muνμ unique. Bandit models are parameter vectors θ∈ΘK\theta\in\Theta^Kθ∈ΘK with K≥2K\ge2K≥2; arms are indexed 0,…,K−10,\dots,K-10,…,K−1. S\mathcal SS is the set of parameter vectors with a unique arm of largest mean b˙(θa)\dot b(\theta_a)b˙(θa​).
  • Protocol. Policies, the trajectory law Pμ\mathbb P_{\boldsymbol\mu}Pμ​, pull counts, empirical means and T∗(μ)T^*(\boldsymbol\mu)T∗(μ) are the platform's published definitions (BanditPolicy, BanditTrajectory, TrackAndStop). T∗T^*T∗ uses Kullback–Leibler divergences of the arm laws over the class S\mathcal SS and takes values in [0,∞][0,\infty][0,∞]. Trajectory coordinate ttt is round t+1t+1t+1. An arm never drawn has empirical mean 000.
  • Target map. w∗(μ^(t))w^*(\hat{\boldsymbol\mu}(t))w∗(μ^​(t)) is undefined in the paper when μ^(t)∉S\hat{\boldsymbol\mu}(t)\notin\mathcal Sμ^​(t)∈/S (an unsampled arm, ties, a mean outside b˙(Θ)\dot b(\Theta)b˙(Θ)). Every tracking statement quantifies over every target map with values in ΣK\Sigma_KΣK​ that returns optimal proportions on S\mathcal SS, over every choice of L∞L^\inftyL∞ projections, and over every tie-breaking, including randomized ones.
  • Stopping rule. The two maxima in Za,b(t)Z_{a,b}(t)Za,b​(t) are suprema over Θ\ThetaΘ in the extended reals. Za,b(t)>βZ_{a,b}(t)>\betaZa,b​(t)>β is written without subtracting infinities. The stopping time is the first t≥1t\ge1t≥1 at which the test succeeds, +∞+\infty+∞ if none. "r(t)=O(tα)r(t)=O(t^\alpha)r(t)=O(tα)" is r(t)≤Dtαr(t)\le Dt^\alphar(t)≤Dtα for t≥1t\ge1t≥1; r>0r>0r>0 is added so that log⁡(r(t)/δ)\log(r(t)/\delta)log(r(t)/δ) is defined.
  • Values in [0,∞][0,\infty][0,∞]. Expectations of τδ\tau_\deltaτδ​, the ratios and T∗T^*T∗ live in [0,∞][0,\infty][0,∞]. No statement converts them to reals, so an infinite expected stopping time is never read as 000.
  • Corrections, disclosed. Proposition 9's printed Pw\mathbb P_wPw​ is Pμ\mathbb P_{\boldsymbol\mu}Pμ​. Lemma 18 adds c2/c1α>1c_2/c_1^\alpha>1c2​/c1α​>1 and x>0x>0x>0, without which its expressions are undefined.
  • Ruled out. Specializing to Gaussian arms, or asserting that some sampling policy achieves the bound, would restate existing platform results and is not this theorem: the goal is about every C-Tracking or D-Tracking run in every exponential family.
  • Welcome contributions. Exponential-family facts (b˙\dot bb˙ is the mean, the KL formula, concentration of empirical means); the continuity of w∗w^*w∗ (Proposition 6, App. A.3); Lemma 17 (App. B.2), from which Lemma 8 follows; the closed form (7) of the GLR statistic.

Selected references

  • A. Garivier, E. Kaufmann, Optimal Best Arm Identification with Fixed Confidence, COLT 2016, JMLR W&CP 49. arXiv:1602.04589v2
  • E. Kaufmann, O. Cappé, A. Garivier, On the Complexity of Best-Arm Identification in Multi-Armed Bandit Models, JMLR 17, 2016. arXiv:1407.4443
  • H. Chernoff, Sequential Design of Experiments, Ann. Math. Statist. 30(3), 1959. doi:10.1214/aoms/1177706205
  • T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Ch. 33. doi:10.1017/9781108571401
15 thms5 active usersReviewed
🏆Completed
Machine LearningOperations ResearchProbability+1·Captain: mikedeng1

Optimal Best Arm Identification with Fixed Confidence I: Non-Asymptotic Lower Bound on the Sample ComplexityResearch Paper

Motivation

Best arm identification with fixed confidence is the pure-exploration counterpart of the multi-armed bandit problem. A learner faces KKK unknown reward distributions ("arms"), samples them sequentially, and must stop and name the arm with the largest mean, being wrong with probability at most a prescribed δ\deltaδ. The question is how many samples this requires. It arises in adaptive A/B testing, in the selection of the best of several simulated systems (ranking and selection in simulation optimization), and in clinical trials that must declare the best treatment with a guaranteed error rate.

Lower bounds for this problem were first stated in terms of the gaps between means (Mannor and Tsitsiklis, 2004). Kaufmann, Cappé and Garivier (2016) replaced ad hoc changes of measure by a single "transportation" lemma relating expected sample counts, Kullback–Leibler divergences and the error probability. Garivier and Kaufmann (COLT 2016, arXiv:1602.04589v2) combine this lemma over all alternative models at once, in the spirit of Graves and Lai (1997), and obtain a lower bound whose constant T∗(μ)T^*(\boldsymbol\mu)T∗(μ) is exactly matched, as δ→0\delta \to 0δ→0, by their Track-and-Stop strategy. This mission formalizes that lower bound (Theorem 1 of the paper, p. 3).

Setting

A canonical one-parameter exponential family is given by a reference measure ξ\xiξ on R\mathbb RR, an open interval Θ⊂R\Theta \subset \mathbb RΘ⊂R and a function bbb, twice continuously differentiable on Θ\ThetaΘ with b¨>0\ddot b > 0b¨>0, such that the laws νθ\nu_\thetaνθ​ with density exp⁡(θx−b(θ))\exp(\theta x - b(\theta))exp(θx−b(θ)) with respect to ξ\xiξ are probability measures for θ∈Θ\theta \in \Thetaθ∈Θ. The mean of νθ\nu_\thetaνθ​ is b˙(θ)\dot b(\theta)b˙(θ). Bernoulli laws and Gaussian laws of known variance are examples.

A bandit model is a vector θ=(θ1,…,θK)∈ΘK\theta = (\theta_1, \dots, \theta_K) \in \Theta^Kθ=(θ1​,…,θK​)∈ΘK; arm aaa returns i.i.d. rewards with law νθa\nu_{\theta_a}νθa​​ and mean μa=b˙(θa)\mu_a = \dot b(\theta_a)μa​=b˙(θa​). Arm a∗(μ)a^*(\boldsymbol\mu)a∗(μ) is the unique optimal arm if μa∗>μa\mu_{a^*} > \mu_aμa∗​>μa​ for every a≠a∗a \ne a^*a=a∗. Let S\mathcal SS be any set of bandit models of the family each having a unique optimal arm, and put Alt(μ)={λ∈S:a∗(λ)≠a∗(μ)}\mathrm{Alt}(\boldsymbol\mu) = \{\boldsymbol\lambda \in \mathcal S : a^*(\boldsymbol\lambda) \ne a^*(\boldsymbol\mu)\}Alt(μ)={λ∈S:a∗(λ)=a∗(μ)}.

A strategy consists of a sampling rule π\piπ (the arm AtA_tAt​ drawn at round ttt depends, possibly with extra randomization, on the first t−1t - 1t−1 observations), a stopping time τ\tauτ of the natural filtration Ft=σ(A1,X1,…,At,Xt)\mathcal F_t = \sigma(A_1, X_1, \dots, A_t, X_t)Ft​=σ(A1​,X1​,…,At​,Xt​), and an Fτ\mathcal F_\tauFτ​-measurable decision a^τ\hat a_\taua^τ​. It is δ\deltaδ-PAC on S\mathcal SS if for every μ∈S\boldsymbol\mu \in \mathcal Sμ∈S, Pμ(τ<∞)=1\mathbb P_{\boldsymbol\mu}(\tau < \infty) = 1Pμ​(τ<∞)=1 and Pμ(a^τ≠a∗(μ))≤δ\mathbb P_{\boldsymbol\mu}(\hat a_\tau \ne a^*(\boldsymbol\mu)) \le \deltaPμ​(a^τ​=a∗(μ))≤δ. Na(t)N_a(t)Na​(t) is the number of draws of arm aaa among the first ttt rounds.

Write d(μa,λa)=KL(νθa,νλa)d(\mu_a, \lambda_a) = \mathrm{KL}(\nu_{\theta_a}, \nu_{\lambda_a})d(μa​,λa​)=KL(νθa​​,νλa​​) for the divergence between two arm laws, kl(x,y)=xlog⁡xy+(1−x)log⁡1−x1−y\mathrm{kl}(x, y) = x\log\frac{x}{y} + (1 - x)\log\frac{1 - x}{1 - y}kl(x,y)=xlogyx​+(1−x)log1−y1−x​, and ΣK\Sigma_KΣK​ for the probability simplex on the KKK arms. The characteristic time is defined by eq. (1):

T∗(μ)−1=sup⁡w∈ΣK inf⁡λ∈Alt(μ)∑a=1Kwa d(μa,λa).T^*(\boldsymbol\mu)^{-1} = \sup_{w \in \Sigma_K}\ \inf_{\boldsymbol\lambda \in \mathrm{Alt}(\boldsymbol\mu)} \sum_{a=1}^K w_a\, d(\mu_a, \lambda_a).T∗(μ)−1=w∈ΣK​sup​ λ∈Alt(μ)inf​a=1∑K​wa​d(μa​,λa​).

Formalization targets

Goal: Theorem 1 (p. 3)

For δ∈(0,1/2]\delta \in (0, 1/2]δ∈(0,1/2], every δ\deltaδ-PAC strategy on S\mathcal SS and every μ∈S\boldsymbol\mu \in \mathcal Sμ∈S,

Eμ[τ] ≥ T∗(μ) kl(δ,1−δ).\mathbb E_{\boldsymbol\mu}[\tau] \ \ge\ T^*(\boldsymbol\mu)\,\mathrm{kl}(\delta, 1 - \delta).Eμ​[τ] ≥ T∗(μ)kl(δ,1−δ).

The statement fixes no constant beyond those of the paper, and it holds for every δ\deltaδ, not only in the limit.

Milestone: eq. (2) (p. 4)

For every λ∈S\boldsymbol\lambda \in \mathcal Sλ∈S with a∗(λ)≠a∗(μ)a^*(\boldsymbol\lambda) \ne a^*(\boldsymbol\mu)a∗(λ)=a∗(μ),

∑a=1Kd(μa,λa) Eμ[Na(τ)] ≥ kl(δ,1−δ).\sum_{a=1}^K d(\mu_a, \lambda_a)\, \mathbb E_{\boldsymbol\mu}[N_a(\tau)] \ \ge\ \mathrm{kl}(\delta, 1 - \delta).a=1∑K​d(μa​,λa​)Eμ​[Na​(τ)] ≥ kl(δ,1−δ).

This is Lemma 1 of Kaufmann et al. (2016), which the paper quotes without proof; Theorem 1 follows from it for every alternative simultaneously.

Significance

Theorem 1 identifies T∗(μ)T^*(\boldsymbol\mu)T∗(μ) as the exact problem-dependent complexity of fixed-confidence best arm identification: since kl(δ,1−δ)∼log⁡(1/δ)\mathrm{kl}(\delta, 1 - \delta) \sim \log(1/\delta)kl(δ,1−δ)∼log(1/δ), it gives lim inf⁡δ→0Eμ[τδ]/log⁡(1/δ)≥T∗(μ)\liminf_{\delta \to 0} \mathbb E_{\boldsymbol\mu}[\tau_\delta]/\log(1/\delta) \ge T^*(\boldsymbol\mu)liminfδ→0​Eμ​[τδ​]/log(1/δ)≥T∗(μ), and the paper's Track-and-Stop strategy attains this rate (the subject of mission IV of this series). The bound also explains which proportions of draws an optimal strategy must use: the maximizer w∗(μ)w^*(\boldsymbol\mu)w∗(μ) of eq. (1) (mission II).

Both results are proved in the literature. Neither is formalized in the paper's generality. The platform holds the textbook form of Lattimore and Szepesvári (Theorem 33.5), which is stated for an arbitrary class with the weaker constant log⁡(1/(4δ))\log(1/(4\delta))log(1/(4δ)); for δ≤1/2\delta \le 1/2δ≤1/2, kl(δ,1−δ)≥log⁡(1/(2.4δ))>log⁡(1/(4δ))\mathrm{kl}(\delta, 1 - \delta) \ge \log(1/(2.4\delta)) > \log(1/(4\delta))kl(δ,1−δ)≥log(1/(2.4δ))>log(1/(4δ)), so Theorem 1 is strictly stronger. A formal proof here yields the transportation lemma for exponential families on the platform's infinite-horizon bandit model, which later missions (II–IV, and any lower bound by change of measure) can reuse.

Difficulty

The obvious proof applies the finite-horizon divergence decomposition KL(Pμn,Pλn)=∑aEμ[Na(n)] d(μa,λa)\mathrm{KL}(\mathbb P^n_{\boldsymbol\mu}, \mathbb P^n_{\boldsymbol\lambda}) = \sum_a \mathbb E_{\boldsymbol\mu}[N_a(n)]\,d(\mu_a, \lambda_a)KL(Pμn​,Pλn​)=∑a​Eμ​[Na​(n)]d(μa​,λa​) at a deterministic horizon nnn. That fails here: τ\tauτ is random and unbounded, the decision is Fτ\mathcal F_\tauFτ​-measurable, and the relevant divergence is between the laws of the stopped observations. The step from a fixed horizon to a stopping time, together with the data-processing inequality that turns the error guarantees under two models into kl(δ,1−δ)\mathrm{kl}(\delta, 1 - \delta)kl(δ,1−δ), is the central difficulty. A second, smaller difficulty is to identify the paper's divergence ddd and its means b˙(θ)\dot b(\theta)b˙(θ) with the measure-theoretic KL divergence and mean of the arm laws of the exponential family.

Formalization scope

Lean namespace OptimalBAI.LowerBound. The bandit protocol is the platform's (BanditAlgorithm.BanditPolicy, banditTrajMeasure, IsBanditStoppingTime, IsSoundBAI, baiComplexity); kl\mathrm{kl}kl is the platform's bernoulliRelativeEntropy and Na(t)N_a(t)Na​(t) is trajPullCount. Conventions:

  • arms are Fin K, 0-based (the paper's arm aaa is index a−1a - 1a−1); trajectory coordinate ttt is round t+1t + 1t+1;
  • Θ\ThetaΘ is a nonempty open interval and b¨>0\ddot b > 0b¨>0 on Θ\ThetaΘ (added: the paper says bbb is convex and twice differentiable; strict convexity is what makes "the unique distribution with mean μ\muμ" meaningful); the paper's ddd is written as the KL divergence of the arm laws (its first equality on p. 3), and the unique optimal arm is defined through the parameter means b˙(θa)\dot b(\theta_a)b˙(θa​);
  • S\mathcal SS is an arbitrary set of models with a unique optimal arm, not the specific set the paper fixes from p. 4 on;
  • δ\deltaδ-PAC keeps both halves of the paper's definition (almost-sure stopping and error at most δ\deltaδ);
  • T∗(μ)T^*(\boldsymbol\mu)T∗(μ), divergences and expectations of τ\tauτ take values in [0,∞][0, \infty][0,∞], never truncated to reals; T∗=0T^* = 0T∗=0 when Alt(μ)=∅\mathrm{Alt}(\boldsymbol\mu) = \emptysetAlt(μ)=∅ and T∗=∞T^* = \inftyT∗=∞ when the supremum in eq. (1) is 000;
  • δ≤1/2\delta \le 1/2δ≤1/2 is added. The paper states δ∈(0,1)\delta \in (0, 1)δ∈(0,1), but the theorem and eq. (2) are false for δ∈(1/2,1)\delta \in (1/2, 1)δ∈(1/2,1): with two unit-variance Gaussian arms, drawing arm 1 once and naming arm 1 exactly when the fractional part of the reward is below 1/21/21/2 is 0.90.90.9-PAC, while T∗(μ)→∞T^*(\boldsymbol\mu) \to \inftyT∗(μ)→∞ as the two means merge. At δ=1/2\delta = 1/2δ=1/2 the bound is 000.

A statement with log⁡(1/(4δ))\log(1/(4\delta))log(1/(4δ)) in place of kl(δ,1−δ)\mathrm{kl}(\delta, 1 - \delta)kl(δ,1−δ), or restricted to Gaussian arms, is the platform's existing textbook theorem and does not count as this mission's goal; nor does any version that drops the almost-sure stopping clause or truncates E[τ]\mathbb E[\tau]E[τ] or T∗T^*T∗ to real numbers.

Needed infrastructure: the transportation lemma at a stopping time (data processing for KL through an Fτ\mathcal F_\tauFτ​-measurable event, Wald-type identity for the stopped log-likelihood ratio), the identities "mean of νθ\nu_\thetaνθ​ =b˙(θ)= \dot b(\theta)=b˙(θ)" and "KL of two family members =b(θ′)−b(θ)−b˙(θ)(θ′−θ)= b(\theta') - b(\theta) - \dot b(\theta)(\theta' - \theta)=b(θ′)−b(θ)−b˙(θ)(θ′−θ)", and E[τ]=∑aE[Na(τ)]\mathbb E[\tau] = \sum_a \mathbb E[N_a(\tau)]E[τ]=∑a​E[Na​(τ)]. All are reusable beyond this mission. Contributions of any of these lemmas, of eq. (2) alone, or of the Gaussian and Bernoulli special cases as stepping stones are welcome.

Selected references

  • A. Garivier, E. Kaufmann, Optimal Best Arm Identification with Fixed Confidence, COLT 2016 (JMLR W&CP 49), arXiv:1602.04589v2. https://arxiv.org/abs/1602.04589
  • E. Kaufmann, O. Cappé, A. Garivier, On the Complexity of Best-Arm Identification in Multi-Armed Bandit Models, Journal of Machine Learning Research 17(1), 2016. https://arxiv.org/abs/1407.4443
  • T. L. Graves, T. L. Lai, Asymptotically Efficient Adaptive Choice of Control Laws in Controlled Markov Chains, SIAM Journal on Control and Optimization 35(3), 1997. https://doi.org/10.1137/S0363012994275440
  • S. Mannor, J. N. Tsitsiklis, The Sample Complexity of Exploration in the Multi-Armed Bandit Problem, Journal of Machine Learning Research 5, 2004. https://www.jmlr.org/papers/v5/mannor04b.html
  • T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapter 33. https://doi.org/10.1017/9781108571401
11 thms5 active usersReviewed
🏆Completed
Machine LearningOperations Research·Captain: mikedeng1

Improved Algorithms for Linear Stochastic Bandits II: Constant High-Probability Regret of UCB(δ)Research Paper

Motivation

The stochastic multi-armed bandit is the basic model of sequential decision making under uncertainty: a learner repeatedly chooses one of ddd actions, observes a noisy reward for the chosen action only, and must balance exploring poorly known actions against exploiting the one that currently looks best. It underlies adaptive clinical trials, online advertising, recommendation, dynamic pricing and many simulation-optimization procedures in operations research.

The standard algorithm is UCB (Auer, Cesa-Bianchi and Fischer, 2002, doi:10.1023/A:1013689704352), which plays the arm with the largest upper confidence bound on its mean. Its confidence widths grow with the current time ttt (or with a horizon nnn fixed in advance), and its guarantee is on the expected regret, which grows like log⁡n\log nlogn. Lai and Robbins (1985, doi:10.1016/0196-8858(85)90002-8) showed that logarithmic growth of the expected regret cannot be avoided by a consistent algorithm.

Abbasi-Yadkori, Pál and Szepesvári (NIPS 2011) proved a self-normalized concentration inequality for vector-valued martingales that holds uniformly over time. Section 6 of their paper applies it to the ddd-armed bandit. The resulting confidence intervals depend on neither the horizon nor the current time. The UCB variant built on them, UCB(δ\deltaδ), has pseudo-regret bounded by a constant, independent of the horizon, on a single event of probability at least 1−δ1-\delta1−δ. This mission formalizes that section.

Setting

There are d≥1d \ge 1d≥1 arms with unknown means μ1,…,μd∈R\mu_1, \dots, \mu_d \in \mathbb Rμ1​,…,μd​∈R. Write μ∗=max⁡1≤i≤dμi\mu_* = \max_{1 \le i \le d} \mu_iμ∗​=max1≤i≤d​μi​ for the best mean and Δi=μ∗−μi≥0\Delta_i = \mu_* - \mu_i \ge 0Δi​=μ∗​−μi​≥0 for the gap of arm iii.

Randomness lives on a probability space (Ω,F,P)(\Omega, \mathcal F, P)(Ω,F,P) with a filtration (Ft)t≥0(\mathcal F_t)_{t \ge 0}(Ft​)t≥0​. In round t=1,2,…t = 1, 2, \dotst=1,2,… the learner plays an arm ItI_tIt​ that is Ft−1\mathcal F_{t-1}Ft−1​-measurable and receives the reward μIt+ηt\mu_{I_t} + \eta_tμIt​​+ηt​. The noise ηt\eta_tηt​ is Ft\mathcal F_tFt​-measurable and conditionally 1-sub-Gaussian:

E[eληt∣Ft−1]≤eλ2/2for all λ∈R.\mathbf E\left[e^{\lambda\eta_t} \mid \mathcal F_{t-1}\right] \le e^{\lambda^2/2} \qquad \text{for all } \lambda \in \mathbb R .E[eληt​∣Ft−1​]≤eλ2/2for all λ∈R.

The noise need not be independent or identically distributed across rounds, and the rewards need not be bounded.

After ttt rounds, Ni,tN_{i,t}Ni,t​ is the number of plays of arm iii and X‾i,t\overline X_{i,t}Xi,t​ is the average reward received from it. For a confidence level δ>0\delta > 0δ>0 the confidence width is

ci,t=1+Ni,tNi,t2(1+2log⁡d (1+Ni,t)1/2δ)(3)c_{i,t} = \sqrt{\frac{1 + N_{i,t}}{N_{i,t}^2}\left(1 + 2\log\frac{d\,(1 + N_{i,t})^{1/2}}{\delta}\right)} \qquad (3)ci,t​=Ni,t2​1+Ni,t​​(1+2logδd(1+Ni,t​)1/2​)​(3)

with ci,t=+∞c_{i,t} = +\inftyci,t​=+∞ when Ni,t=0N_{i,t} = 0Ni,t​=0. UCB(δ\deltaδ) plays, in round ttt, an arm that maximizes X‾i,t−1+ci,t−1\overline X_{i,t-1} + c_{i,t-1}Xi,t−1​+ci,t−1​; in particular every arm is played once before any comparison is made. The pseudo-regret after nnn rounds is

Rn=∑t=1n(μ∗−μIt).R_n = \sum_{t=1}^n \left(\mu_* - \mu_{I_t}\right).Rn​=t=1∑n​(μ∗​−μIt​​).

This is the linear bandit of the paper with the standard basis of Rd\mathbb R^dRd as decision set and θ∗=μ\theta_* = \muθ∗​=μ.

Formalization targets

Goal: Theorem 7 (constant regret of UCB(δ\deltaδ))

For every δ>0\delta > 0δ>0, with probability at least 1−δ1-\delta1−δ, for all n≥0n \ge 0n≥0 simultaneously,

Rn≤∑i:Δi>0(3Δi+16Δilog⁡2dΔiδ).R_n \le \sum_{i : \Delta_i > 0}\left(3\Delta_i + \frac{16}{\Delta_i}\log\frac{2d}{\Delta_i\delta}\right).Rn​≤i:Δi​>0∑​(3Δi​+Δi​16​logΔi​δ2d​).

The right-hand side depends only on the gaps, ddd and δ\deltaδ.

Milestone: Lemma 6 (confidence intervals)

For any adapted choice of arms (not only UCB(δ\deltaδ)) and every δ>0\delta > 0δ>0, with probability at least 1−δ1-\delta1−δ,

∣X‾i,t−μi∣≤ci,tfor all arms i and all t≥0.|\overline X_{i,t} - \mu_i| \le c_{i,t} \qquad \text{for all arms } i \text{ and all } t \ge 0 .∣Xi,t​−μi​∣≤ci,t​for all arms i and all t≥0.

Significance

The result. Theorem 7 shows that, once a confidence level is fixed, a UCB-type algorithm can stop paying for exploration after finitely many rounds: with probability 1−δ1-\delta1−δ the total regret over an infinite horizon is bounded. The paper notes that this does not contradict the Lai–Robbins lower bound, which concerns expected regret; on the failure event of probability δ\deltaδ the regret may grow linearly. Lemma 6 is the practical content behind this: anytime-valid confidence intervals for adaptively sampled means under martingale noise, usable for stopping rules, best-arm identification and any sequential procedure that inspects its estimates at data-dependent times.

Formalizing it. Both results are proved in the paper's appendices (F and G). No machine-checked proof of either is known to exist. The platform already has the self-normalized martingale bound for V=λIV = \lambda IV=λI and unit sub-Gaussian noise (BanditAlgorithm.self_normalized_martingale_bound, listed here as a reference item), and UCB bounds with horizon-dependent widths and in-expectation or pathwise conclusions. Neither is Theorem 7. The mission produces a formal account of time-uniform confidence intervals for adaptively sampled arm means, and of a regret bound that is uniform in the horizon.

Difficulty

Two points separate this from textbook UCB analyses. First, the number of samples Ni,tN_{i,t}Ni,t​ of an arm is itself random and depends on past noise, so a fixed-sample concentration inequality with a union bound over times does not give widths that are free of ttt: a union bound over all ttt costs a factor that diverges. The time-uniform event must come from a maximal (self-normalized) inequality applied to the martingale ∑sηs1{Is=i}\sum_s \eta_s \mathbf 1\{I_s = i\}∑s​ηs​1{Is​=i}. Second, the regret statement is uniform in nnn with constants depending on the gaps; converting a condition of the form "c(N)≥Δi/2c(N) \ge \Delta_i/2c(N)≥Δi​/2" into an explicit bound on NNN requires solving an inequality in which NNN appears both polynomially and inside a logarithm, and the explicit constants 333 and 161616 must come out of that step.

Formalization scope

The Lean development lives in the namespace ImprovedLinBandits.UCBDelta.

  • Arms are Fin d with 0 < d in the goal; means are μ : Fin d → ℝ, μ∗\mu_*μ∗​ is ⨆ i, μ i (the maximum over a nonempty finite type).
  • Rounds are indexed t + 1 for t : ℕ: the arm I (t + 1) is ℱ t-measurable, the noise η (t + 1) is ℱ (t + 1)-measurable and satisfies Mathlib's HasCondSubgaussianMGF (ℱ t) … (η (t + 1)) 1 P. Values at index 000 are unused.
  • The sample space is assumed to be a standard Borel space, which Mathlib's conditional sub-Gaussianity requires; this hypothesis is not in the paper.
  • "With probability at least 1−δ1-\delta1−δ, for all …" is stated as: the outer probability of the failure event, with the quantifiers over arms and times inside it, is at most δ\deltaδ. For δ≥1\delta \ge 1δ≥1 the statements are trivially true, as in the paper.
  • The rule (4) is read with the statistics of rounds 1,…,t−11, \dots, t-11,…,t−1, because the printed X‾i,t\overline X_{i,t}Xi,t​, ci,tc_{i,t}ci,t​ already count round ttt. An unplayed arm, whose width is +∞+\infty+∞ in the paper, is played before the indices are compared. Every tie-breaking rule is allowed, and measurability of the chosen arm is assumed rather than derived.
  • The printed Theorem 7 has no quantifier on nnn; it is formalized in the uniform-in-nnn form, matching the section's claim of constant regret and the time-uniform event of Lemma 6.
  • Lean's division by zero makes X‾i,t\overline X_{i,t}Xi,t​ and ci,tc_{i,t}ci,t​ equal to 000 when Ni,t=0N_{i,t} = 0Ni,t​=0. Lemma 6 therefore excludes Ni,t=0N_{i,t} = 0Ni,t​=0 explicitly (where the paper's inequality is vacuous), and the run predicate handles unplayed arms separately. The regret bound sums over arms with Δi>0\Delta_i > 0Δi​>0, so its divisions are well defined.

A trivializing formalization is ruled out: the confidence event is not assumed as a hypothesis of Theorem 7, the i.i.d. bandit model is not substituted for the martingale noise model, and no bound on the means or rewards is imposed.

Useful infrastructure for solvers: the self-normalized bound of Theorem 1 in the scalar case (d=1d = 1d=1, λ=1\lambda = 1λ=1, As=1{Is=i}A_s = \mathbf 1\{I_s = i\}As​=1{Is​=i}, V‾t=1+Ni,t\overline V_t = 1 + N_{i,t}Vt​=1+Ni,t​), a union bound over arms, and elementary inequalities inverting N↦1+NN2(1+2log⁡(d1+N/δ))N \mapsto \frac{1+N}{N^2}(1 + 2\log(d\sqrt{1+N}/\delta))N↦N21+N​(1+2log(d1+N​/δ)). Lemmas about pull counts and empirical means under adaptive sampling are reusable beyond this mission and are welcome as contributions.

Selected references

  • Y. Abbasi-Yadkori, D. Pál, Cs. Szepesvári, Improved Algorithms for Linear Stochastic Bandits, Advances in Neural Information Processing Systems 24 (NIPS), 2011. https://papers.nips.cc/paper/2011/hash/e1d5be1c7f2f456670de3d53c7b54f4a-Abstract.html
  • 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
  • T. L. Lai, H. Robbins, Asymptotically Efficient Adaptive Allocation Rules, Advances in Applied Mathematics 6, 1985. https://doi.org/10.1016/0196-8858(85)90002-8
  • J.-Y. Audibert, R. Munos, Cs. Szepesvári, Exploration–exploitation tradeoff using variance estimates in multi-armed bandits, Theoretical Computer Science 410, 2009. https://doi.org/10.1016/j.tcs.2009.01.016
6 thms5 active usersReviewed
🏆Completed
Operations ResearchOptimizationProbability·Captain: naimengye

Multi-armed Bandit Allocation Indices III: Superprocesses, Condition D and the Index Theorem for a SFASTextbook

Motivation

The index theorem says that among several Markov reward processes, of which one may be advanced at each decision time, the right one to advance is the one of greatest Gittins index. Chapter 4 of Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., doi:10.1002/9780470980033), asks how far this extends when the constituents are not reward processes but decision processes, each with its own controls: a research project that can be run in several ways, a job that can be processed at different speeds, a sampling process that may be stopped and exploited. A family of such superprocesses requires two choices at every decision time, which superprocess to continue and with which control, and an index policy in the sense of Chapter 2 need not be optimal (Example 4.1). Whittle (1980) identified the condition under which it is: Condition D, that when a superprocess is played against a standard bandit process paying a constant rent, the control one should apply to it does not depend on the rent. Under that condition the index theorem survives (Theorem 4.3), the index is characterized (Note 4.2), stoppable bandit processes with improving stopping options satisfy the condition (Lemma 4.4), and the chapter adds two results about indices themselves: any index that works for all bandit processes is a strictly increasing function of the Gittins index (Theorem 4.8), and a policy that is within ε\varepsilonε of the index policy loses at most εγ−1(1−e−γ)−1\varepsilon\gamma^{-1}(1-e^{-\gamma})^{-1}εγ−1(1−e−γ)−1 (Theorem 4.18).

Setting

A decision process DDD on a countable state space SSS has in each state xxx a nonempty finite set Γ(x)\Gamma(x)Γ(x) of controls; applying uuu yields the reward r(x,u)r(x, u)r(x,u) and moves the state by P(⋅∣x,u)P(\cdot \mid x, u)P(⋅∣x,u). Adding the freeze control, which leaves the state unchanged and yields nothing, makes DDD a superprocess SSS. Operating DDD under a feasible deterministic stationary Markov policy ggg (that is, g(x)∈Γ(x)g(x) \in \Gamma(x)g(x)∈Γ(x)) gives an ordinary bandit process DgD_gDg​, and the superprocess index is

ν(S,x,u)=sup⁡g:g(x)=uν(Dg,x),ν(S,x)=max⁡u∈Γ(x)ν(S,x,u),(4.1)\nu(S, x, u) = \sup_{g : g(x) = u} \nu(D_g, x), \qquad \nu(S, x) = \max_{u \in \Gamma(x)} \nu(S, x, u), \tag{4.1}ν(S,x,u)=g:g(x)=usup​ν(Dg​,x),ν(S,x)=u∈Γ(x)max​ν(S,x,u),(4.1)

with ν(Dg,x)\nu(D_g, x)ν(Dg​,x) the Gittins index of the Bandit Algorithms model. A simple family of alternative superprocesses (SFAS) is nnn superprocesses on a common (S,U)(S, U)(S,U); at each decision time 0,1,2,…0, 1, 2, \dots0,1,2,… exactly one is continued, with a control from its control set, the others being frozen, and rewards are discounted by ata^tat. A policy is a Markov kernel per decision time from the history to the pair (superprocess, control); it is optimal if it is feasible and attains the supremum of the discounted payoff over feasible policies from every initial state-vector, and it is an index policy if it always continues a superprocess and control of maximal ν(Si,xi,u)\nu(S_i, x_i, u)ν(Si​,xi​,u).

Condition D. Let Λ\LambdaΛ be a standard bandit process with parameter λ\lambdaλ (one state, reward λ\lambdaλ). SSS satisfies Condition D if there is a function ggg such that, for every xxx and λ\lambdaλ for which it is optimal in the family {S,Λ}\{S, \Lambda\}{S,Λ} to select SSS in state xxx, it is optimal to apply the control g(x)g(x)g(x). A stoppable bandit process is a bandit process with a stop control that makes it behave as a standard bandit process with parameter μ(x)\mu(x)μ(x); its stopping option is improving if μ(x(t))\mu(x(t))μ(x(t)) is almost surely nondecreasing in process time.

Formalization targets

Goal: Theorem 4.3

For a decision process with bounded rewards and a Condition-D control ggg, every index policy with respect to ν(D,⋅,⋅)\nu(D, \cdot, \cdot)ν(D,⋅,⋅) that applies g(xi)g(x_i)g(xi​) to the superprocess iii it continues is optimal for the family of nnn superprocesses:

index policy π  ⟹  π feasible and Rπ(x)=sup⁡π′ feasibleRπ′(x)  for every x∈Sn.\text{index policy } \pi \implies \pi \text{ feasible and } R_\pi(x) = \sup_{\pi' \text{ feasible}} R_{\pi'}(x)\ \text{ for every } x \in S^n.index policy π⟹π feasible and Rπ​(x)=π′ feasiblesup​Rπ′​(x)  for every x∈Sn.

Milestones

Note 4.2 (under Condition D, SSS is selected in {S,Λ(λ)}\{S, \Lambda(\lambda)\}{S,Λ(λ)} iff ν(S,x)≥λ\nu(S, x) \ge \lambdaν(S,x)≥λ, and at λ=ν(S,x)\lambda = \nu(S, x)λ=ν(S,x) a control uuu is optimal iff ν(S,x,u)=ν(S,x)\nu(S, x, u) = \nu(S, x)ν(S,x,u)=ν(S,x); the printed equivalence fails for λ<ν(S,x)\lambda < \nu(S, x)λ<ν(S,x)); Lemma 4.4 (Condition D for stoppable bandit processes with improving stopping options); Theorem 4.8 (an index for the bandit processes with discount factor aaa is strictly increasing in ν\nuν); Theorem 4.18 (the ε\varepsilonε-index bound, ε/(1−a)2\varepsilon/(1-a)^2ε/(1−a)2 for the discrete-time index).

Significance

Theorem 4.3 is the widest form in which the index theorem holds without further structure, and Condition D is exactly the right hypothesis: it says the superprocess has a canonical control, and once it does the family reduces to a family of bandit processes and the prevailing-charge argument goes through. Lemma 4.4 gives the model where the condition is known to hold, a research project that may be exploited at any time; the buyer's problem of Bergman and Bather is the case where it fails. Theorem 4.8 explains why every index theorem in the book is about the Gittins index: any function that orders bandit processes optimally must order them as ν\nuν does. Theorem 4.18 is the quantitative version of the index theorem that heuristics and computations rely on.

Nothing here is machine-checked. The mission builds the first controlled multi-armed model on the platform, a run law for families of decision processes with an explicit feasibility constraint, and states Whittle's condition as a property of the two-member family, which is how the literature uses it. Theorems 4.8 and 4.18 are statements about the existing Bandit Algorithms model and are usable by any later work on that model.

Difficulty

The obvious attack on Theorem 4.3, "replace each superprocess by the bandit process DgD_{g}Dg​ for its Condition-D policy ggg and apply the index theorem", is the second half of the book's proof; the first half is to show that an optimal policy never gains by applying a control other than g(xi)g(x_i)g(xi​) to a superprocess it continues, and that uses the prevailing-stake accounting of §4.3 with the other superprocesses treated as one bandit process, plus the observation that the class of policies deviating at most kkk times is ε\varepsilonε-exhaustive. Both halves require the whole run law of the family to be related to the run laws of its constituents, which is where a formalization spends its effort. Note 4.2 is short on the page but needs the optimal-stopping characterization of Chapter 2 for the bandit process DgD_gDg​ under charge λ\lambdaλ. Theorem 4.8 is elementary given the value of {B,Λ}\{B, \Lambda\}{B,Λ} under a freezing rule, Rf(B)+λγ−1−λWf(B)R_f(B) + \lambda\gamma^{-1} - \lambda W_f(B)Rf​(B)+λγ−1−λWf​(B), but that identity is itself a computation on the run law. Theorem 4.18 has no proof in the book (Glazebrook 1982c); the natural route is the prevailing-charge upper bound with the charges perturbed by ε\varepsilonε.

Formalization scope

Decision processes carry their control sets as finsets with a nonemptiness proof and their kernels as Markov kernels; the state space is countable with measurable singletons (so stationary kernels and control-dependent maps are measurable without side conditions) and the control type is finite with measurable singletons. The family's run law is built decision time by decision time as the Bandit Algorithms model builds markovBanditMeasure, with the policy's kernel producing the pair (superprocess, control). Feasibility is an almost-sure condition on the policy kernel, and optimality is the book's: feasible, and the supremum from every initial state-vector. The superprocess index is a real supremum over feasible stationary policies with g(x)=ug(x) = ug(x)=u, bounded by the reward bound and nonempty for u∈Γ(x)u \in \Gamma(x)u∈Γ(x); for an unavailable uuu it is a default value that no index policy consults. Condition D is stated on the family {S,Λ}\{S, \Lambda\}{S,Λ} on S⊕UnitS \oplus \mathrm{Unit}S⊕Unit, where the standard state has every control available, all equivalent. A stoppable bandit process is the decision process with control type Bool. Theorem 4.8 quantifies over index functions defined on every measurable state space and takes as hypothesis only what its proof uses, optimality of μ\muμ-index policies for the families {B,Λ}\{B, \Lambda\}{B,Λ}. Theorem 4.18 is on the kkk-armed Bandit Algorithms model with ε≥0\varepsilon \ge 0ε≥0 and the bound ε/(1−a)2\varepsilon/(1-a)^2ε/(1−a)2: the book's εγ−1(1−e−γ)−1\varepsilon\gamma^{-1}(1 - e^{-\gamma})^{-1}εγ−1(1−e−γ)−1 is in continuous-time index units, γ/(1−a)\gamma/(1-a)γ/(1−a) times the discrete-time index used here, and read with the discrete index it is false for a<1/ea < 1/ea<1/e. Theorem 4.3's index policy applies the Condition-D control ggg to the superprocess it continues, as the book's proof does; an index policy that breaks ties among controls otherwise need not be optimal.

Trivializing readings are excluded: index policies must be feasible, optimality is required from every initial state, and Condition D is a statement about optimal policies of a genuine two-member family, not about a chosen policy. Welcome contributions: the relation between the family's run law and the constituents' chain laws, the freezing-rule value identity behind Theorem 4.8, and the prevailing-stake accounting of §4.3.

Selected references

  • J. Gittins, K. Glazebrook, R. Weber, Multi-armed Bandit Allocation Indices, 2nd ed., Wiley, 2011, Chapter 4. doi:10.1002/9780470980033
  • P. Whittle, Multi-armed bandits and the Gittins index, Journal of the Royal Statistical Society B 42(2), 1980. doi:10.1111/j.2517-6161.1980.tb01111.x
  • K. D. Glazebrook, Stoppable families of alternative bandit processes, Journal of Applied Probability 16(4), 1979. doi:10.2307/3213152
  • K. D. Glazebrook, On the evaluation of suboptimal strategies for families of alternative bandit processes, Journal of Applied Probability 19(3), 1982. doi:10.2307/3213524
  • T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapter 35. doi:10.1017/9781108571401
10 thms5 active usersReviewed
🏆Completed
Operations ResearchOptimizationProbability·Captain: naimengye

Multi-armed Bandit Allocation Indices II: Jobs, Parallel Machines, Search and Bandit-Dependent DiscountingTextbook

Motivation

Chapter 3 of Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., doi:10.1002/9780470980033), asks which of the assumptions behind the index theorem can be dropped and which cannot, using the simplest bandit processes there are: jobs, which pay a single reward when they complete. Along the way it settles three questions that matter on their own. When identical machines run in parallel, which schedule of deterministic jobs minimizes the total completion time (Baker's theorem), and what does the equal-ratio case look like (Theorem 3.3)? When an object is hidden in one of several boxes and each search costs money and may fail, in what order should the boxes be searched (Blackwell's search-index theorem, Theorem 3.6)? And when two bandit processes discount at different rates, is there still an index policy (Nash's Theorem 3.4)? The search theorem is the chapter's example of what the index machinery yields once undiscounted criteria are admitted through the limit γ↓0\gamma \downarrow 0γ↓0; the scheduling results are the source of the counterexamples that show a second machine breaks the index structure.

Setting

Jobs on parallel machines. There are nnn jobs with service times si>0s_i > 0si​>0 and weights cic_ici​, and mmm identical machines. A schedule assigns each job a machine and a position in that machine's processing order; each machine processes its jobs consecutively. The completion time CiC_iCi​ of a job is the total service time of the jobs on its machine up to and including it; the flow time is ∑iCi\sum_i C_i∑i​Ci​ and the weighted flow time ∑iciCi\sum_i c_i C_i∑i​ci​Ci​. The load of a machine is the total service time assigned to it, and δj\delta_jδj​ is its excess over the average S/mS/mS/m. The SPT list schedule sorts the jobs by increasing service time and deals them out cyclically to the machines. The level of a job is its position counted from the end of its machine's schedule.

The search problem (Problem 3). A stationary object is hidden in one of nnn boxes, in box iii with probability pip_ipi​. A search of box iii costs cic_ici​ and finds the object with probability qiq_iqi​ if it is there. A search policy is a sequence of boxes; after NiN_iNi​ unsuccessful searches of box iii the posterior probability that the object is there is proportional to pi(1−qi)Nip_i(1-q_i)^{N_i}pi​(1−qi​)Ni​, and the search index of the box is pi′qi/cip'_i q_i/c_ipi′​qi​/ci​, the current probability of finding the object per unit cost. The expected cost of a policy is ∑kcσkPr⁡[not found by the first k searches]\sum_k c_{\sigma_k}\Pr[\text{not found by the first } k \text{ searches}]∑k​cσk​​Pr[not found by the first k searches].

Two discount factors. Bandit process AAA (state space SAS_ASA​, kernel PAP_APA​, reward rAr_ArA​) discounts at rate aaa and BBB at rate bbb; a reward obtained at time ttt is worth ata^tat or btb^tbt times its face value according to which process produced it. The cross indices are νAB(x)=sup⁡τ>0E∑t<τatrA(x(t))/E[1−bτ]\nu_{AB}(x) = \sup_{\tau>0} \mathbb{E}\sum_{t<\tau} a^t r_A(x(t)) \big/ \mathbb{E}[1 - b^\tau]νAB​(x)=supτ>0​E∑t<τ​atrA​(x(t))/E[1−bτ] and νBA(y)\nu_{BA}(y)νBA​(y) with the roles exchanged: each is computed from one process's stopping times but with the other's discount factor in the denominator. The book prints the denominator as E∫0τbt dt\mathbb{E}\int_0^\tau b^t\,dtE∫0τ​btdt and compares νAB(x)\nu_{AB}(x)νAB​(x) with νBA(y)\nu_{BA}(y)νBA​(y) at every time; both are corrected here (see the Theorem 3.4 item), since the printed rule is not optimal. The family is the two-armed Markov bandit of the Bandit Algorithms model on the disjoint union SA⊕SBS_A \oplus S_BSA​⊕SB​.

Formalization targets

Goal: Theorem 3.6

For prior probabilities pi≥0p_i \ge 0pi​≥0 summing to one, detection probabilities 0<qi≤10 < q_i \le 10<qi​≤1 and costs ci>0c_i > 0ci​>0, a search policy is optimal if and only if at every step it searches a box of maximal current index pi′qi/cip'_i q_i / c_ipi′​qi​/ci​:

optimal(σ)  ⟺  ∀k, ∀i: pi(1−qi)Ni(k)qici≤pσk(1−qσk)Nσk(k)qσkcσk.\text{optimal}(\sigma) \iff \forall k,\ \forall i:\ \frac{p_i (1-q_i)^{N_i(k)} q_i}{c_i} \le \frac{p_{\sigma_k}(1-q_{\sigma_k})^{N_{\sigma_k}(k)} q_{\sigma_k}}{c_{\sigma_k}}.optimal(σ)⟺∀k, ∀i: ci​pi​(1−qi​)Ni​(k)qi​​≤cσk​​pσk​​(1−qσk​​)Nσk​​(k)qσk​​​.

Milestones

Theorem 3.3, as the identity ∑iciCi=κ2(∑isi2+S2/m+∑jδj2)\sum_i c_i C_i = \frac{\kappa}{2}\big(\sum_i s_i^2 + S^2/m + \sum_j \delta_j^2\big)∑i​ci​Ci​=2κ​(∑i​si2​+S2/m+∑j​δj2​) when ci=κsic_i = \kappa s_ici​=κsi​; Theorem 3.4 in discrete time and corrected, that a policy selecting, at time ttt, AAA when atνAB(x)>btνBA(y)a^t \nu_{AB}(x) > b^t \nu_{BA}(y)atνAB​(x)>btνBA​(y) and BBB when atνAB(x)<btνBA(y)a^t \nu_{AB}(x) < b^t \nu_{BA}(y)atνAB​(x)<btνBA​(y) attains the supremum of the bandit-dependently discounted payoff; Theorem 3.7, that SPT minimizes the flow time on mmm machines and that the optimal schedules are exactly those placing the rrr-th block of mmm longest jobs at level rrr from the end, for some order of the equal jobs.

Significance

Theorem 3.6 is the classical solution of the discrete search problem (Blackwell, reported by Matula 1964; Kadane 1969): the greedy rule in probability-per-cost is optimal, and every optimal policy is of that form. The book derives it from the index theorem through an auxiliary family of bandit processes (Problem 3A) and the undiscounted limit (Corollary 3.5), which is why it sits in this chapter; as a statement it is elementary and self-contained, and it is the template for the tax problems and Klimov's model of Chapter 4. Theorem 3.7 and Theorem 3.3 are the positive results about parallel machines that survive the loss of the index structure; Theorem 3.4 shows the index theorem's shape persisting under bandit-dependent discounting, with two twists: each index depends on the other process's discount factor, which is exactly why it does not extend to three processes, and the comparison at time ttt weighs the indices by ata^tat and btb^tbt, so the rule is not stationary in the states. The printed statement misses the second twist and misnormalizes the first; two one-state bandits paying 0.180.180.18 (a=0.9a = 0.9a=0.9) and 111 (b=0.5b = 0.5b=0.5) are best played B,B,BB, B, BB,B,B and then AAA forever, which no stationary rule does.

None of these is machine-checked. Formalizing them gives the platform an optimality theorem for an infinite-horizon search process with an explicit index characterization in both directions, the standard parallel-machine flow-time results with a precise uniqueness clause, and a first statement on the Bandit Algorithms two-armed model with unequal discounting.

Difficulty

For Theorem 3.6 the obvious route, comparing two adjacent searches, gives only that interchanging a pair in the wrong index order lowers the cost; turning that into optimality over all infinite sequences needs that an optimal policy exists (costs are bounded below by zero and the index policy has finite cost), that a policy neglecting a box of positive prior has infinite cost, and that any first deviation from the index rule can be improved by moving a later search forward, which requires tracking how the not-found probability changes along the whole tail. The converse direction is the same interchange run backwards, and the tie case must be handled so that the equivalence is exact. Theorem 3.7's first part follows from writing the flow time as ∑iℓisi\sum_i \ell_i s_i∑i​ℓi​si​ with ℓi\ell_iℓi​ the level and applying a rearrangement inequality over the multiset of levels, but the multiset of levels itself depends on how many jobs each machine gets, so balancing the machine counts is part of the argument; the uniqueness clause needs both that the multiset is forced and that the pairing of levels with service times is forced by strict monotonicity. Theorem 3.4 is the hardest: the book's proof changes the time scale of each process so that the two share a discount factor, which produces a semi-Markov family, and applies the index theorem there; in discrete time on the Markov model one needs either a discrete analogue of that argument or a direct prevailing-charge proof with two charge scales.

Formalization scope

Schedules are assignments of machines and positions with distinct positions on a machine, without idling; the flow-time quantities are finite sums over Fin n. The SPT schedule is defined by the ascending rank of a job (ties broken by index) and carries its own injectivity proof. The search cost is a series in [0,∞][0, \infty][0,∞] of nonnegative terms, so no summability hypothesis is needed and "infinite cost" is literal; the index is stated unnormalized, pi(1−qi)Niqi/cip_i(1-q_i)^{N_i} q_i/c_ipi​(1−qi​)Ni​qi​/ci​, which orders the boxes exactly as the posterior index does. The two-discount family uses the platform's MarkovBanditPolicy 2 (S_A ⊕ S_B) and markovBanditMeasure with the kernel that moves an AAA-state by PAP_APA​ and a BBB-state by PBP_BPB​; the payoff is the round-by-round series ∑t(atE[r1{At=A}]+btE[r1{At=B}])\sum_t (a^t \mathbb{E}[r\mathbf 1\{A_t = A\}] + b^t \mathbb{E}[r\mathbf 1\{A_t = B\}])∑t​(atE[r1{At​=A}]+btE[r1{At​=B}]), absolutely summable for bounded rewards, and the policy condition is imposed at histories whose current states have the right types (all reachable histories do). Hypotheses: m≥1m \ge 1m≥1, service times positive; pi≥0p_i \ge 0pi​≥0, ∑pi=1\sum p_i = 1∑pi​=1, 0<qi≤10 < q_i \le 10<qi​≤1, ci>0c_i > 0ci​>0; countable state spaces, bounded rewards, a,b∈(0,1)a, b \in (0,1)a,b∈(0,1).

Trivializing readings are excluded: the search "iff" is over all sequences, not a finite horizon; the uniqueness clause is stated in full, with ties resolved by any ranking of the equal jobs; the cross indices are suprema over positive stopping times (denominators at least one), and the two-discount rule weighs the indices by ata^tat, btb^tbt. Welcome contributions: the rearrangement and level-count lemmas for schedules, the interchange lemma for the search cost, and a discrete prevailing-charge argument for Theorem 3.4.

Selected references

  • J. Gittins, K. Glazebrook, R. Weber, Multi-armed Bandit Allocation Indices, 2nd ed., Wiley, 2011, Chapter 3. doi:10.1002/9780470980033
  • D. W. Matula, A periodic optimal search, American Mathematical Monthly 71(1), 1964. doi:10.2307/2311300
  • J. B. Kadane, Quiz show problems, Journal of Mathematical Analysis and Applications 27(3), 1969. doi:10.1016/0022-247X(69)90140-2
  • K. R. Baker, Introduction to Sequencing and Scheduling, Wiley, 1974.
  • P. Nash, A generalized bandit problem, Journal of the Royal Statistical Society B 42(2), 1980. doi:10.1111/j.2517-6161.1980.tb01119.x
8 thms5 active usersReviewed
🏆Completed
Machine LearningOperations Research·Captain: Shuze Chen

Bandit Algorithms XIII: Pure Exploration and Best-Arm IdentificationTextbook

Sometimes reward during learning is irrelevant — a pharmaceutical company running phase-II trials only cares about identifying the best treatment, as quickly and as reliably as possible. Chapter 33 of Lattimore–Szepesvári formalizes fixed-confidence best-arm identification: a policy together with a stopping time τ\tauτ and a recommendation must be sound (wrong with probability at most δ\deltaδ) while minimizing E[τ]\mathbb{E}[\tau]E[τ]. The information-theoretic complexity is c∗(ν)−1=sup⁡α∈Pk−1inf⁡ν′∈Ealt(ν)∑iαiD(νi,νi′)c^*(\nu)^{-1} = \sup_{\alpha\in\mathcal{P}_{k-1}} \inf_{\nu'\in\mathcal{E}_{alt}(\nu)} \sum_i \alpha_i D(\nu_i, \nu_i')c∗(ν)−1=supα∈Pk−1​​infν′∈Ealt​(ν)​∑i​αi​D(νi​,νi′​): every sound strategy needs E[τ]≥c∗(ν)log⁡14δ\mathbb{E}[\tau] \ge c^*(\nu)\log\frac{1}{4\delta}E[τ]≥c∗(ν)log4δ1​, and the Track-and-Stop algorithm — the goal theorem — achieves lim⁡δ→0E[τ]/log⁡(1/δ)=c∗(ν)\lim_{\delta\to 0} \mathbb{E}[\tau]/\log(1/\delta) = c^*(\nu)limδ→0​E[τ]/log(1/δ)=c∗(ν) exactly. The mission also covers the fixed-budget counterpart, sequential halving.

50 thms5 active usersReviewed
🏆Completed
Machine LearningOperations Research·Captain: Shuze Chen

Bandit Algorithms IV: Bernoulli Bandits and KL-UCBTextbook

When rewards are binary — a click or no click, a cure or no cure — the subgaussian machinery of Missions I–III is not tight: the variance of a Bernoulli arm degrades near the boundary of [0,1][0,1][0,1], and the correct exponential rate is governed by the binary relative entropy d(p,q)=plog⁡pq+(1−p)log⁡1−p1−qd(p,q) = p\log\frac{p}{q} + (1-p)\log\frac{1-p}{1-q}d(p,q)=plogqp​+(1−p)log1−q1−p​ rather than a squared distance. Chapter 10 of Lattimore–Szepesvári develops Chernoff's tail bound in its information-theoretic form and the KL-UCB algorithm, whose upper confidence bounds are level sets of ddd. The goal theorem shows KL-UCB attains

lim sup⁡n→∞Rn/log⁡n=∑i:Δi>0Δi/d(μi,μ∗)\limsup_{n\to\infty} R_n/\log n = \sum_{i:\Delta_i>0} \Delta_i/d(\mu_i, \mu^*)n→∞limsup​Rn​/logn=i:Δi​>0∑​Δi​/d(μi​,μ∗)

— asymptotic optimality with exactly the constant demanded by the lower bound of Mission VII, strictly improving subgaussian UCB on every Bernoulli instance.

25 thms5 active usersReviewed
🏆Completed
Machine LearningOperations Research·Captain: Shuze Chen

Bandit Algorithms VI: Information-Theoretic FoundationsTextbook

Every lower bound in bandit theory rests on one question: how hard is it to tell two probability measures apart from a sample? The answer is quantified by the relative entropy D(P,Q)D(P,Q)D(P,Q), and the sharpest elementary tool is the Bretagnolle–Huber inequality: for any event AAA, P(A)+Q(Ac)≥12exp⁡(−D(P,Q))P(A) + Q(A^c) \ge \frac{1}{2}\exp(-D(P,Q))P(A)+Q(Ac)≥21​exp(−D(P,Q)) — no test can distinguish PPP from QQQ with total error probability below 12e−D(P,Q)\frac{1}{2}e^{-D(P,Q)}21​e−D(P,Q). This mission formalizes Chapter 14 of Lattimore–Szepesvári: the Bretagnolle–Huber inequality (the goal theorem, proved via Le Cam's inequality ∫p∧q≥12(∫pq)2\int p \wedge q \ge \frac{1}{2}(\int\sqrt{pq})^2∫p∧q≥21​(∫pq​)2), Pinsker's inequality δ(P,Q)≤D(P,Q)/2\delta(P,Q) \le \sqrt{D(P,Q)/2}δ(P,Q)≤D(P,Q)/2​, and the closed-form divergences between Gaussians and Bernoullis. These half-page inequalities power every impossibility result in Missions VII, XI and beyond.

5 thms5 active usersReviewed
🏆Completed
Machine LearningProbabilityReinforcement Learning·Captain: mikedeng1

Provably Efficient Reinforcement Learning with Linear Function Approximation 1: LSVI-UCB Has Regret O(√(d³H³Tι²)) with Probability 1 − p on Linear MDPsResearch Paper

Motivation

Reinforcement learning with large or continuous state spaces is done in practice with function approximation: the agent represents value functions in a low-dimensional parametric family instead of a table indexed by states. For tabular Markov decision processes, regret bounds of order H2SAT\sqrt{H^2SAT}H2SAT​ have been known since the work on UCRL and UCBVI, but they scale with the number of states SSS and actions AAA and say nothing when SSS is infinite. Before 2019, provable guarantees for function approximation either needed a simulator, assumed deterministic transitions, or had regret exponential in the horizon.

Jin, Yang, Wang and Jordan, Provably Efficient Reinforcement Learning with Linear Function Approximation (arXiv:1907.05388, COLT 2020), identified a model, the linear MDP, in which an optimistic version of least-squares value iteration has regret polynomial in the feature dimension ddd and the horizon HHH and independent of SSS and AAA. The model and the algorithm, LSVI-UCB, became a standard reference point for the theory of RL with function approximation.

Timeline:

  • 2017–2018: Azar, Osband, Munos (arXiv:1703.05449) and Jin, Allen-Zhu, Bubeck, Jordan (arXiv:1807.03765) give near-optimal T\sqrt TT​ regret for tabular episodic MDPs.
  • 2019: Yang and Wang (arXiv:1902.04779) study linear transition models with a simulator; Jin, Yang, Wang, Jordan prove Theorem 3.1 below without a simulator.
  • 2020: Zanette, Lazaric, Kochenderfer, Brunskill (arXiv:2003.00153) improve the dependence on ddd under a low inherent Bellman error assumption.

Setting

An episodic MDP MDP(S,A,H,P,r)\mathrm{MDP}(\mathcal S,\mathcal A,H,\mathbb P,r)MDP(S,A,H,P,r) has a measurable state space S\mathcal SS, a finite action set A\mathcal AA, a horizon HHH, transition kernels Ph(⋅∣x,a)\mathbb P_h(\cdot\mid x,a)Ph​(⋅∣x,a) and deterministic rewards rh(x,a)∈[0,1]r_h(x,a)\in[0,1]rh​(x,a)∈[0,1] for steps h=1,…,Hh=1,\dots,Hh=1,…,H. A policy π(x,h)\pi(x,h)π(x,h) chooses an action at each state and step. Its value functions satisfy the Bellman equation Qhπ=rh+PhVh+1πQ^\pi_h=r_h+\mathbb P_hV^\pi_{h+1}Qhπ​=rh​+Ph​Vh+1π​, Vhπ(x)=Qhπ(x,π(x,h))V^\pi_h(x)=Q^\pi_h(x,\pi(x,h))Vhπ​(x)=Qhπ​(x,π(x,h)), VH+1π=0V^\pi_{H+1}=0VH+1π​=0, where PhV(x,a)=∫V dPh(⋅∣x,a)\mathbb P_hV(x,a)=\int V\,d\mathbb P_h(\cdot\mid x,a)Ph​V(x,a)=∫VdPh​(⋅∣x,a); the optimal values Vh⋆V^\star_hVh⋆​, Qh⋆Q^\star_hQh⋆​ satisfy the same recursion with a maximum over actions.

The MDP is linear (Assumption A) with feature map ϕ:S×A→Rd\phi:\mathcal S\times\mathcal A\to\mathbb R^dϕ:S×A→Rd if ∥ϕ∥≤1\|\phi\|\le1∥ϕ∥≤1 and for each step there are signed measures μh=(μh(1),…,μh(d))\boldsymbol\mu_h=(\mu_h^{(1)},\dots,\mu_h^{(d)})μh​=(μh(1)​,…,μh(d)​) and a vector θh\theta_hθh​ with

Ph(⋅∣x,a)=⟨ϕ(x,a),μh(⋅)⟩,rh(x,a)=⟨ϕ(x,a),θh⟩,\mathbb P_h(\cdot\mid x,a)=\langle\phi(x,a),\boldsymbol\mu_h(\cdot)\rangle,\qquad r_h(x,a)=\langle\phi(x,a),\theta_h\rangle,Ph​(⋅∣x,a)=⟨ϕ(x,a),μh​(⋅)⟩,rh​(x,a)=⟨ϕ(x,a),θh​⟩,

and ∥θh∥≤d\|\theta_h\|\le\sqrt d∥θh​∥≤d​, ∥(∣μh(1)∣(S),…,∣μh(d)∣(S))∥≤d\|(|\mu_h^{(1)}|(\mathcal S),\dots,|\mu_h^{(d)}|(\mathcal S))\|\le\sqrt d∥(∣μh(1)​∣(S),…,∣μh(d)​∣(S))∥≤d​.

In each episode k=1,…,Kk=1,\dots,Kk=1,…,K an adversary chooses the initial state x1kx^k_1x1k​; the agent then plays HHH steps, the next state xh+1kx^k_{h+1}xh+1k​ being drawn from Ph(⋅∣xhk,ahk)\mathbb P_h(\cdot\mid x^k_h,a^k_h)Ph​(⋅∣xhk​,ahk​). LSVI-UCB (Algorithm 1) computes, backwards over hhh, the Gram matrix Λhk=∑τ<kϕhτ(ϕhτ)⊤+λI\Lambda^k_h=\sum_{\tau<k}\phi^\tau_h(\phi^\tau_h)^\top+\lambda IΛhk​=∑τ<k​ϕhτ​(ϕhτ​)⊤+λI of the past features ϕhτ=ϕ(xhτ,ahτ)\phi^\tau_h=\phi(x^\tau_h,a^\tau_h)ϕhτ​=ϕ(xhτ​,ahτ​), the ridge-regression weight whkw^k_hwhk​ for the targets rh+max⁡aQh+1kr_h+\max_aQ^k_{h+1}rh​+maxa​Qh+1k​, and the optimistic estimate

Qhk(x,a)=min⁡{(whk)⊤ϕ(x,a)+βϕ(x,a)⊤(Λhk)−1ϕ(x,a), H},Q^k_h(x,a)=\min\Big\{(w^k_h)^\top\phi(x,a)+\beta\sqrt{\phi(x,a)^\top(\Lambda^k_h)^{-1}\phi(x,a)},\ H\Big\},Qhk​(x,a)=min{(whk​)⊤ϕ(x,a)+βϕ(x,a)⊤(Λhk​)−1ϕ(x,a)​, H},

and then plays greedily with respect to QhkQ^k_hQhk​. Its policy in episode kkk is πk\pi_kπk​, and the regret is

Regret(K)=∑k=1K[V1⋆(x1k)−V1πk(x1k)],T=KH.\mathrm{Regret}(K)=\sum_{k=1}^K\big[V^\star_1(x^k_1)-V^{\pi_k}_1(x^k_1)\big],\qquad T=KH.Regret(K)=k=1∑K​[V1⋆​(x1k​)−V1πk​​(x1k​)],T=KH.

Formalization targets

Goal: Theorem 3.1

There are absolute constants c,C>0c,C>0c,C>0 such that for every linear MDP, every p∈(0,1)p\in(0,1)p∈(0,1) and every run of LSVI-UCB with λ=1\lambda=1λ=1 and β=c⋅dHι\beta=c\cdot dH\sqrt\iotaβ=c⋅dHι​, ι=log⁡(2dT/p)\iota=\log(2dT/p)ι=log(2dT/p),

P(Regret(K)≤Cd3H3Tι2)≥1−p.\mathbb P\Big(\mathrm{Regret}(K)\le C\sqrt{d^3H^3T\iota^2}\Big)\ge1-p .P(Regret(K)≤Cd3H3Tι2​)≥1−p.

Milestones

The milestones follow Appendix B of the paper: linearity of QπQ^\piQπ (Proposition 2.3) and the weight bounds (Lemmas B.1, B.2, with Lemma D.1); the covering bound for the value class (Lemma D.6, with the Euclidean-ball covering of Lemma D.5); the uniform self-normalized concentration (Lemma D.4, with Theorem D.3) and the good event (Lemma B.3); the error propagation (Lemma B.4), optimism (Lemma B.5) and the recursion (Lemma B.6); and the bonus-sum bound (17)–(18), with Lemma D.2. Lemma D.2, Theorem D.3 and Lemma D.5 are already on the platform and are referenced.

A companion statement, not a milestone, formalizes Proposition 5.1 (§5): on a finite state space with non-degenerate features, if the Bellman operators Thπ\mathbb T^\pi_hThπ​ of (8) map linear action-value functions to linear ones for every policy, then Ph\mathbb P_hPh​ is linear in ϕ\phiϕ.

Significance

The theorem shows that exploration with function approximation can be sample-efficient without a simulator: the regret depends on the intrinsic dimension ddd of the features and polynomially on HHH, not on the size of the state space. Its analysis, a uniform concentration bound over a data-dependent class of value functions combined with optimism, is the template for a large later literature: misspecified and low-rank MDPs, kernel and neural function approximation, and reward-free exploration.

The result has a published proof, but no machine-checked one. A formalization supplies the measure-theoretic episodic MDP on a general state space, an interaction protocol with adaptive initial states, the LSVI-UCB algorithm, and a checked chain from self-normalized martingale bounds to the regret theorem. The formal statements also record two points where the printed paper is imprecise: the normalization of the measures μh\boldsymbol\mu_hμh​ (see Formalization scope) and the existential reading of the weights in Lemma B.1.

Difficulty

The regression targets rh+max⁡aQh+1k(xh+1τ,⋅)r_h+\max_aQ^k_{h+1}(x^\tau_{h+1},\cdot)rh​+maxa​Qh+1k​(xh+1τ​,⋅) depend on all past data through Qh+1kQ^k_{h+1}Qh+1k​. The self-normalized bound for vector-valued martingales (Theorem D.3) therefore cannot be applied to them directly: the natural first idea, conditioning on the past and treating Vh+1kV^k_{h+1}Vh+1k​ as fixed, fails because Vh+1kV^k_{h+1}Vh+1k​ is not measurable with respect to the past at the time xh+1τx^\tau_{h+1}xh+1τ​ is drawn. The concentration must hold uniformly over a function class, which requires a covering-number bound for a class parametrized by vectors and matrices (Lemma D.6) and a union bound in the right scale.

A second difficulty is formal: the probabilistic protocol mixes an adversary, a learning algorithm reading its own past outputs, and transition kernels on a general measurable space, and the martingale argument (Azuma–Hoeffding over the KHKHKH steps) needs every object to be measurable with respect to the right σ-algebra.

Formalization scope

  • Model. S\mathcal SS is any measurable space; A\mathcal AA is a finite nonempty type with its discrete σ-algebra and a linear order used only to break ties in the argmax. Steps and episodes are 1-based. VπV^\piVπ, QπQ^\piQπ, V⋆V^\starV⋆, Q⋆Q^\starQ⋆ are defined by the Bellman recursions (1) and (2), with value 000 outside 1≤h≤H1\le h\le H1≤h≤H; theorems about general policies assume them measurable.
  • Assumption A is stated with the total-variation normalization ∥(∣μh(i)∣(S))i∥≤d\|(|\mu_h^{(i)}|(\mathcal S))_i\|\le\sqrt d∥(∣μh(i)​∣(S))i​∥≤d​ instead of the printed ∥μh(S)∥≤d\|\boldsymbol\mu_h(\mathcal S)\|\le\sqrt d∥μh​(S)∥≤d​; under the printed condition Lemma B.1 is false. The feature map is assumed measurable.
  • Runs. A run is a process on a probability space with a filtration over the flattened time (k−1)(H+1)+(h−1)(k-1)(H+1)+(h-1)(k−1)(H+1)+(h−1): states are adapted, actions are those of Algorithm 1, and the conditional law of xh+1kx^k_{h+1}xh+1k​ given the past is Ph(⋅∣xhk,ahk)\mathbb P_h(\cdot\mid x^k_h,a^k_h)Ph​(⋅∣xhk​,ahk​). The initial states are otherwise unrestricted.
  • Constants. ccc and CCC are quantified before the spaces, ddd, HHH, KKK, ppp, the MDP and the run; d,H,K≥1d,H,K\ge1d,H,K≥1 and p∈(0,1)p\in(0,1)p∈(0,1). "With probability 1−p1-p1−p" is an upper bound on the outer measure of the failure event.
  • Ruling out trivializations. The goal does not assume the good event, optimism, or any milestone conclusion; β\betaβ is fixed by the existentially quantified ccc, not free; the regret uses the model value of the greedy policy, not a realized return. A sorry-free check exhibits a linear MDP and a run satisfying all hypotheses.
  • Known gap. Algorithm 1 clips QhkQ^k_hQhk​ only from above, so the bound ∣Vh+1k∣≤H|V^k_{h+1}|\le H∣Vh+1k​∣≤H that Lemma B.3's proof needs (and the target bound in Lemma B.2's proof, here an explicit hypothesis) is not automatic off the good event. Lemma B.3 is stated as printed, for every cβ>0c_\beta>0cβ​>0; a solver who finds it unprovable should report this in the discussion.
  • Infrastructure needed: covering numbers of norm balls, the self-normalized martingale bound, Azuma–Hoeffding (in Mathlib), integration against signed measures, and measurability of the algorithm's outputs. The MDP and run definitions are reusable for other episodic RL results; contributions of general lemmas about them are welcome.

Selected references

  • C. Jin, Z. Yang, Z. Wang, M. I. Jordan, Provably Efficient Reinforcement Learning with Linear Function Approximation, COLT 2020; arXiv:1907.05388v2, 2019. https://arxiv.org/abs/1907.05388
  • Y. Abbasi-Yadkori, D. Pál, Cs. Szepesvári, Improved Algorithms for Linear Stochastic Bandits, NeurIPS 2011. https://papers.nips.cc/paper/2011/hash/e1d5be1c7f2f456670de3d53c7b54f4a-Abstract.html
  • M. G. Azar, I. Osband, R. Munos, Minimax Regret Bounds for Reinforcement Learning, ICML 2017. https://arxiv.org/abs/1703.05449
  • C. Jin, Z. Allen-Zhu, S. Bubeck, M. I. Jordan, Is Q-learning Provably Efficient?, NeurIPS 2018. https://arxiv.org/abs/1807.03765
  • L. F. Yang, M. Wang, Sample-Optimal Parametric Q-Learning Using Linearly Additive Features, ICML 2019. https://arxiv.org/abs/1902.04779
  • A. Zanette, A. Lazaric, M. Kochenderfer, E. Brunskill, Learning Near Optimal Policies with Low Inherent Bellman Error, ICML 2020. https://arxiv.org/abs/2003.00153
19 thms4 active usersReviewed
🏆Completed
Machine LearningOperations ResearchProbability+1·Captain: mikedeng1

Optimal Best Arm Identification with Fixed Confidence III: δ-PAC Guarantee of Chernoff's Stopping Rule for Bernoulli BanditsResearch Paper

Motivation

In best arm identification with fixed confidence, a learner samples KKK unknown distributions ("arms") one at a time, and must eventually stop and name the arm with the largest mean, with an error probability at most a prescribed risk δ\deltaδ, while using as few samples as possible. The problem goes back to the sequential design of experiments (Chernoff, 1959; Even-Dar, Mannor and Mansour, 2006) and underlies adaptive A/B testing, clinical trial design and hyperparameter selection.

Any fixed-confidence strategy consists of three parts: a sampling rule, a stopping rule and a decision rule. Garivier and Kaufmann (arXiv:1602.04589, COLT 2016) proposed the Track-and-Stop strategy, the first shown to match the asymptotic lower bound on the expected sample complexity. Its stopping rule is a generalized likelihood ratio (GLR) test, Chernoff's stopping rule. Its correctness, the guarantee that the recommended arm is wrong with probability at most δ\deltaδ, must hold whatever the sampling rule, which is what allows the sampling rule to be tuned freely for efficiency. This mission formalizes that guarantee for Bernoulli arms, Theorem 10 of the paper, with its explicit threshold β(t,δ)=log⁡(2t(K−1)/δ)\beta(t,\delta) = \log(2t(K-1)/\delta)β(t,δ)=log(2t(K−1)/δ).

Setting

The arms are A={1,…,K}\mathcal A = \{1,\dots,K\}A={1,…,K}. A Bernoulli bandit model is a mean vector μ=(μ1,…,μK)∈[0,1]K\boldsymbol\mu = (\mu_1,\dots,\mu_K) \in [0,1]^Kμ=(μ1​,…,μK​)∈[0,1]K: pulling arm aaa returns reward 111 with probability μa\mu_aμa​ and 000 otherwise, independently of the past. The class S\mathcal SS contains the models with a unique optimal arm a∗(μ)a^*(\boldsymbol\mu)a∗(μ), i.e. μa∗>μi\mu_{a^*} > \mu_iμa∗​>μi​ for all i≠a∗i \ne a^*i=a∗.

At round ttt the learner chooses an arm AtA_tAt​ as a (possibly randomized) function of the past observations and observes a reward XtX_tXt​. Write Na(t)N_a(t)Na​(t) for the number of pulls of arm aaa among the first ttt rounds, sa(t)s_a(t)sa​(t) for the number of those pulls that returned 111, and μ^a(t)=Na(t)−1∑s≤tXs1{As=a}\hat\mu_a(t) = N_a(t)^{-1}\sum_{s \le t} X_s \mathbb 1\{A_s = a\}μ^​a​(t)=Na​(t)−1∑s≤t​Xs​1{As​=a} for the empirical mean. The likelihood of arm aaa's observations under mean uuu is pu(X‾Na(t)a)=usa(t)(1−u)Na(t)−sa(t)p_u(\underline X^a_{N_a(t)}) = u^{s_a(t)}(1-u)^{N_a(t)-s_a(t)}pu​(X​Na​(t)a​)=usa​(t)(1−u)Na​(t)−sa​(t).

The GLR statistic for "arm aaa is at least as good as arm bbb" is

Za,b(t)=log⁡max⁡μa′≥μb′pμa′(X‾Na(t)a) pμb′(X‾Nb(t)b)max⁡μa′≤μb′pμa′(X‾Na(t)a) pμb′(X‾Nb(t)b).Z_{a,b}(t) = \log \frac{\max_{\mu'_a \ge \mu'_b} p_{\mu'_a}(\underline X^a_{N_a(t)})\, p_{\mu'_b}(\underline X^b_{N_b(t)})}{\max_{\mu'_a \le \mu'_b} p_{\mu'_a}(\underline X^a_{N_a(t)})\, p_{\mu'_b}(\underline X^b_{N_b(t)})}.Za,b​(t)=logmaxμa′​≤μb′​​pμa′​​(X​Na​(t)a​)pμb′​​(X​Nb​(t)b​)maxμa′​≥μb′​​pμa′​​(X​Na​(t)a​)pμb′​​(X​Nb​(t)b​)​.

Chernoff's stopping rule with exploration rate β(t,δ)\beta(t,\delta)β(t,δ) is

τδ=inf⁡{t≥1:∃a∈A, ∀b≠a, Za,b(t)>β(t,δ)},\tau_\delta = \inf\{t \ge 1 : \exists a \in \mathcal A,\ \forall b \ne a,\ Z_{a,b}(t) > \beta(t,\delta)\},τδ​=inf{t≥1:∃a∈A, ∀b=a, Za,b​(t)>β(t,δ)},

and the decision rule recommends a^τδ∈argmax⁡aμ^a(τδ)\hat a_{\tau_\delta} \in \operatorname{argmax}_a \hat\mu_a(\tau_\delta)a^τδ​​∈argmaxa​μ^​a​(τδ​).

The Krichevsky–Trofimov (KT) distribution on binary sequences x∈{0,1}nx \in \{0,1\}^nx∈{0,1}n is kt(x)=∫01(πu(1−u))−1pu(x) du\mathrm{kt}(x) = \int_0^1 \big(\pi\sqrt{u(1-u)}\big)^{-1} p_u(x)\,\mathrm dukt(x)=∫01​(πu(1−u)​)−1pu​(x)du, the Bernoulli likelihood mixed over the Beta(1/2,1/2)(1/2,1/2)(1/2,1/2) prior.

Formalization targets

Goal: Theorem 10

For every δ∈(0,1)\delta \in (0,1)δ∈(0,1), every sampling strategy, and the threshold β(t,δ)=log⁡(2t(K−1)/δ)\beta(t,\delta) = \log\big(2t(K-1)/\delta\big)β(t,δ)=log(2t(K−1)/δ),

∀μ∈S,Pμ(τδ<∞, a^τδ≠a∗)≤δ.\forall \boldsymbol\mu \in \mathcal S,\qquad \mathbb P_{\boldsymbol\mu}\big(\tau_\delta < \infty,\ \hat a_{\tau_\delta} \ne a^*\big) \le \delta .∀μ∈S,Pμ​(τδ​<∞, a^τδ​​=a∗)≤δ.

Milestone: Lemma 11 (Willems, Shtarkov and Tjalkens, 1995)

kt\mathrm{kt}kt is a probability law on {0,1}n\{0,1\}^n{0,1}n, and for n≥1n \ge 1n≥1,

sup⁡x∈{0,1}n sup⁡u∈[0,1]pu(x)kt(x)≤2n.\sup_{x\in\{0,1\}^n}\ \sup_{u\in[0,1]} \frac{p_u(x)}{\mathrm{kt}(x)} \le 2\sqrt n .x∈{0,1}nsup​ u∈[0,1]sup​kt(x)pu​(x)​≤2n​.

Milestone: the pairwise crossing bound of Appendix C.1

With Ta,b=inf⁡{t:Za,b(t)>β(t,δ)}T_{a,b} = \inf\{t : Z_{a,b}(t) > \beta(t,\delta)\}Ta,b​=inf{t:Za,b​(t)>β(t,δ)}, for all arms with μa<μb\mu_a < \mu_bμa​<μb​,

Pμ(Ta,b<∞)≤δK−1.\mathbb P_{\boldsymbol\mu}(T_{a,b} < \infty) \le \frac{\delta}{K-1}.Pμ​(Ta,b​<∞)≤K−1δ​.

Significance

Theorem 10 decouples correctness from efficiency. Because the guarantee holds for every sampling strategy, any sampling rule, including the C-Tracking and D-Tracking rules of Track-and-Stop, the uniform rule, or a heuristic, inherits δ\deltaδ-correctness as soon as it is paired with Chernoff's stopping rule at this threshold. The asymptotic optimality result of the paper (Theorem 14) then only has to control the sample complexity. The threshold is explicit, with no unspecified constant, in contrast to the deviational threshold of Proposition 12.

The result is proved in the paper, in Appendix C.1, and rests on Lemma 11, which the paper quotes from the universal coding literature without proof. As far as the platform's catalog shows, none of these results is formalized. The platform holds a machine-checkable statement of the analogous result for Gaussian arms with the Lattimore–Szepesvári threshold (BanditAlgorithm.chernoff_stopping_rule_sound, Lemma 33.7 of Bandit Algorithms), which is a different model and a different threshold. Formalizing Theorem 10 adds a proof of Lemma 11 (the KT regret bound, reusable in information theory and universal prediction), the Bernoulli GLR statistic, and a change of measure from the true bandit law to a Bayesian mixture law on the trajectory space.

Difficulty

The obvious approach bounds, for each fixed ttt, the probability that Za,b(t)Z_{a,b}(t)Za,b​(t) exceeds β(t,δ)\beta(t,\delta)β(t,δ) by a concentration inequality and sums over ttt. This fails: the sampling strategy is arbitrary and adaptive, so Na(t)N_a(t)Na​(t) and Nb(t)N_b(t)Nb​(t) are random and depend on the past rewards, and a fixed-sample-size deviation bound does not apply; a union bound over the possible values of the counts loses more than the threshold allows. The maximum likelihood in the numerator of Za,bZ_{a,b}Za,b​ is also not a probability density, so the likelihood ratio cannot directly be read as a change of measure. The argument must control the whole trajectory law under an arbitrary randomized policy, and must handle empty samples (an arm never pulled contributes likelihood 111) and the boundary means 000 and 111.

Formalization scope

The formalization is in Lean 4 with Mathlib and reuses the platform's canonical bandit model: StochasticBandit, BanditPolicy (a Markov kernel per round from the observed history to the next arm, so randomized strategies are included), banditTrajMeasure (the law of the infinite trajectory, where coordinate sss is round s+1s+1s+1) and IsSoundBAI from BanditTrajectory; bernoulliBandit from bernoulliRelativeEntropy; and only the pull counts trajPullCount and empirical means trajEmpiricalMean from TrackAndStop. The Gaussian GLR and threshold of TrackAndStop are not used.

Conventions committed to:

  • Arms are Fin K. Bernoulli means range over [0,1][0,1][0,1], degenerate laws included; the paper's exponential-family mean space is (0,1)(0,1)(0,1), so the [0,1][0,1][0,1] statement implies the paper's.
  • Za,b(t)Z_{a,b}(t)Za,b​(t) is defined as the ratio of the two maxima over [0,1]2[0,1]^2[0,1]2, not by the closed form (7), which holds only when μ^a(t)≥μ^b(t)\hat\mu_a(t) \ge \hat\mu_b(t)μ^​a​(t)≥μ^​b​(t). Both maxima are attained and positive.
  • The stopping rule ranges over t≥1t \ge 1t≥1; at t=0t = 0t=0 there is no observation and the paper's β(0,δ)=log⁡0\beta(0,\delta) = \log 0β(0,δ)=log0 is undefined. τδ=∞\tau_\delta = \inftyτδ​=∞ when the rule never fires.
  • The decision rule is quantified: the goal holds for every recommendation that maximizes the empirical mean at τδ\tau_\deltaτδ​, whatever the tie-breaking.
  • Probabilities of events are outer measures under the trajectory law; no measurability is assumed.
  • K≥1K \ge 1K≥1 only. For K=1K = 1K=1 the statement is trivially true (no suboptimal arm).

Disclosed deviations from the page: Lemma 11's ratio bound is stated for n≥1n \ge 1n≥1, since at n=0n = 0n=0 the printed bound reads 1≤01 \le 01≤0; the use of the lemma in Appendix C.1 is unaffected. Appendix C.1 calls the result "Proposition 10" (a slip for Theorem 10) and prints the KT density as 1/πu(1−u)1/\sqrt{\pi u(1-u)}1/πu(1−u)​ (a slip for 1/(πu(1−u))1/(\pi\sqrt{u(1-u)})1/(πu(1−u)​) of Lemma 11, which is the normalized one); the formalization follows Lemma 11.

A trivializing formalization is ruled out: stating the result for Gaussian arms or with the Lattimore–Szepesvári threshold is the platform's existing Lemma 33.7 and is not Theorem 10, and a free decision rule without the argmax hypothesis would make the claim false rather than faithful.

Contributions welcome: a proof of Lemma 11; a change-of-measure lemma for banditTrajMeasure under a mixture of environments; and the union-bound reduction from the goal to the pairwise claim.

Selected references

  • A. Garivier, E. Kaufmann, Optimal Best Arm Identification with Fixed Confidence, COLT 2016 (JMLR W&CP 49), arXiv:1602.04589v2, 2016. https://arxiv.org/abs/1602.04589
  • F. M. J. Willems, Y. M. Shtarkov, T. J. Tjalkens, The context-tree weighting method: basic properties, IEEE Transactions on Information Theory 41(3), 1995. https://doi.org/10.1109/18.382012
  • R. Krichevsky, V. Trofimov, The performance of universal encoding, IEEE Transactions on Information Theory 27(2), 1981. https://doi.org/10.1109/TIT.1981.1056331
  • H. Chernoff, Sequential design of experiments, Annals of Mathematical Statistics 30(3), 1959. https://doi.org/10.1214/aoms/1177706205
  • T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapter 33. https://doi.org/10.1017/9781108571401
10 thms4 active usersReviewed
🏆Completed
Machine LearningOperations ResearchProbability·Captain: mikedeng1

Stochastic Linear Optimization under Bandit Feedback 1: The Regret Bound of ConfidenceBallResearch Paper

Motivation

In stochastic linear optimization under bandit feedback a learner repeatedly chooses a decision xtx_txt​ from a fixed set D⊆RnD\subseteq\mathbb R^nD⊆Rn and observes only the noisy cost of that one decision, whose expectation is a fixed but unknown linear function μ⊤xt\mu^\top x_tμ⊤xt​. The model covers online routing, ad and product selection with feature vectors, and any sequential decision problem whose decision set is too large to enumerate but whose expected cost is linear in a known representation. The multi-armed bandit is the special case where DDD is the set of standard basis vectors.

Dani, Hayes and Kakade (COLT 2008) analysed the algorithm ConfidenceBall₂, a generalization of Auer's LinRel (JMLR 2002), and proved that its regret is O∗(nT)O^*(n\sqrt T)O∗(nT​) with high probability for an arbitrary compact decision set, and that this is optimal up to logarithmic factors. Their confidence-ellipsoid construction became the template for later linear bandit algorithms (OFUL, LinUCB), and the ellipsoid-plus-potential analysis is the standard argument of the field (Lattimore and Szepesvári, Bandit Algorithms, Chapters 19–20).

Timeline: Auer (2002) introduced LinRel for finite decision sets; Dani, Hayes and Kakade (2008) extended it to arbitrary compact sets with the O∗(nT)O^*(n\sqrt T)O∗(nT​) bound and a matching Ω(nT)\Omega(n\sqrt T)Ω(nT​) lower bound; Rusmevichientong and Tsitsiklis (Math. Oper. Res. 2010) studied linearly parameterized bandits with dimension-dependent regret bounds; Abbasi-Yadkori, Pál and Szepesvári (NeurIPS 2011) sharpened the confidence ellipsoids with self-normalized martingale bounds.

Setting

Fix n≥1n\ge1n≥1 and a compact decision set D⊆RnD\subseteq\mathbb R^nD⊆Rn whose standard basis e1,…,ene_1,\dots,e_ne1​,…,en​ is a barycentric spanner: each ei∈De_i\in Dei​∈D and every x∈Dx\in Dx∈D lies in the cube [−1,1]n[-1,1]^n[−1,1]n. The paper's Section 5 adopts these coordinates without loss of generality. An unknown vector μ∈Rn\mu\in\mathbb R^nμ∈Rn satisfies ∣μ⊤x∣≤1|\mu^\top x|\le1∣μ⊤x∣≤1 for x∈Dx\in Dx∈D, and x∗∈Dx^*\in Dx∗∈D minimises μ⊤x\mu^\top xμ⊤x.

On round t=1,2,…t=1,2,\dotst=1,2,… the learner plays xt∈Dx_t\in Dxt​∈D, measurable with respect to the information Ft\mathcal F_tFt​ before round ttt, and observes a loss ℓt∈[−1,1]\ell_t\in[-1,1]ℓt​∈[−1,1] with E[ℓt∣Ft]=μ⊤xt\mathbb E[\ell_t\mid\mathcal F_t]=\mu^\top x_tE[ℓt​∣Ft​]=μ⊤xt​. The regret after TTT rounds is

RT=∑t=1T(μ⊤xt−μ⊤x∗).R_T=\sum_{t=1}^T\big(\mu^\top x_t-\mu^\top x^*\big).RT​=t=1∑T​(μ⊤xt​−μ⊤x∗).

ConfidenceBall₂(D,δ)(D,\delta)(D,δ) maintains the design matrix At=I+∑τ<txτxτ⊤A_t=I+\sum_{\tau<t}x_\tau x_\tau^\topAt​=I+∑τ<t​xτ​xτ⊤​, the least-squares estimate μ^t=At−1∑τ<tℓτxτ\hat\mu_t=A_t^{-1}\sum_{\tau<t}\ell_\tau x_\tauμ^​t​=At−1​∑τ<t​ℓτ​xτ​, the radius

βt=max⁡(128 nln⁡tln⁡(t2/δ), (83ln⁡(t2/δ))2),\beta_t=\max\Big(128\,n\ln t\ln(t^2/\delta),\ \big(\tfrac83\ln(t^2/\delta)\big)^2\Big),βt​=max(128nlntln(t2/δ), (38​ln(t2/δ))2),

and the confidence ellipsoid Bt2={ν:(ν−μ^t)⊤At(ν−μ^t)≤βt}B^2_t=\{\nu:(\nu-\hat\mu_t)^\top A_t(\nu-\hat\mu_t)\le\beta_t\}Bt2​={ν:(ν−μ^​t​)⊤At​(ν−μ^​t​)≤βt​}. It plays the optimistic decision xt∈argmin⁡x∈Dmin⁡ν∈Bt2ν⊤xx_t\in\operatorname{argmin}_{x\in D}\min_{\nu\in B^2_t}\nu^\top xxt​∈argminx∈D​minν∈Bt2​​ν⊤x. The analysis uses the width wt=xt⊤At−1xtw_t=\sqrt{x_t^\top A_t^{-1}x_t}wt​=xt⊤​At−1​xt​​, the error Zt=(μ^t−μ)⊤At(μ^t−μ)Z_t=(\hat\mu_t-\mu)^\top A_t(\hat\mu_t-\mu)Zt​=(μ^​t​−μ)⊤At​(μ^​t​−μ), and the noise ηt=ℓt−μ⊤xt\eta_t=\ell_t-\mu^\top x_tηt​=ℓt​−μ⊤xt​.

Formalization targets

Goal: Theorem 2, ConfidenceBall₂ bullet (corrected)

For 0<δ<10<\delta<10<δ<1 with n≤β1n\le\beta_1n≤β1​ and noise ∣ηt∣≤1|\eta_t|\le1∣ηt​∣≤1,

Pr⁡(∀T≥1, RT≤8nTβTln⁡(T+1))≥1−δ.\Pr\Big(\forall T\ge1,\ R_T\le\sqrt{8nT\beta_T\ln(T+1)}\Big)\ge1-\delta.Pr(∀T≥1, RT​≤8nTβT​ln(T+1)​)≥1−δ.

A single event covers every horizon, so the bound is anytime.

Milestones

  • Lemma 8. If μ∈Bt2\mu\in B^2_tμ∈Bt2​ then rt≤2min⁡(βtwt,1)r_t\le2\min(\sqrt{\beta_t}w_t,1)rt​≤2min(βt​​wt​,1).
  • Lemma 10. det⁡At+1=∏τ=1t(1+wτ2)\det A_{t+1}=\prod_{\tau=1}^t(1+w_\tau^2)detAt+1​=∏τ=1t​(1+wτ2​).
  • Lemma 9 (corrected). ∑τ=1tmin⁡(wτ2,1)≤2nln⁡(t+1)\sum_{\tau=1}^t\min(w_\tau^2,1)\le2n\ln(t+1)∑τ=1t​min(wτ2​,1)≤2nln(t+1).
  • Theorem 6 (corrected). If μ∈Bt2\mu\in B^2_tμ∈Bt2​ for all t≤Tt\le Tt≤T, then ∑t≤Trt2≤8nβTln⁡(T+1)\sum_{t\le T}r_t^2\le8n\beta_T\ln(T+1)∑t≤T​rt2​≤8nβT​ln(T+1).
  • Theorem 4 (Freedman). Pr⁡(∑Xi≥a, V≤v)≤exp⁡(−a2/(2v+2ab/3))\Pr(\sum X_i\ge a,\ V\le v)\le\exp(-a^2/(2v+2ab/3))Pr(∑Xi​≥a, V≤v)≤exp(−a2/(2v+2ab/3)) for martingale differences bounded above by bbb.
  • Lemma 12. Zt≤n+2∑τ<tητxτ⊤(μ^τ−μ)1+wτ2+∑τ<tητ2wτ21+wτ2Z_t\le n+2\sum_{\tau<t}\eta_\tau\frac{x_\tau^\top(\hat\mu_\tau-\mu)}{1+w_\tau^2}+\sum_{\tau<t}\eta_\tau^2\frac{w_\tau^2}{1+w_\tau^2}Zt​≤n+2∑τ<t​ητ​1+wτ2​xτ⊤​(μ^​τ​−μ)​+∑τ<t​ητ2​1+wτ2​wτ2​​.
  • Lemma 14. Pr⁡(∀t, ∑τ<tMτ≤βt/2)≥1−δ\Pr(\forall t,\ \sum_{\tau<t}M_\tau\le\beta_t/2)\ge1-\deltaPr(∀t, ∑τ<t​Mτ​≤βt​/2)≥1−δ.
  • Theorem 5 (Confidence). Pr⁡(∀t, μ∈Bt2)≥1−δ\Pr(\forall t,\ \mu\in B^2_t)\ge1-\deltaPr(∀t, μ∈Bt2​)≥1−δ.

Significance

The result gives a regret bound for linear bandits over an arbitrary compact decision set that depends on the dimension nnn rather than on ∣D∣|D|∣D∣, holds uniformly over horizons, and requires no gap between the best and second-best decision. With the paper's lower bound it shows that the price of bandit feedback, compared with full information, is a factor Θ∗(n)\Theta^*(\sqrt n)Θ∗(n​). The two components, a confidence theorem for a least-squares ellipsoid under martingale noise and a deterministic potential argument on log⁡det⁡At\log\det A_tlogdetAt​, are reused in the analysis of most optimistic linear and generalized-linear bandit algorithms.

The theorem has a published proof but, to our knowledge, no machine-checked one. The platform already has the elliptical potential lemma (BanditAlgorithm.elliptical_potential_lemma, Lattimore–Szepesvári Lemma 19.4), the matrix determinant lemma and the Woodbury identity, which cover the linear-algebra layer; the LinUCB regret theorem there (BanditAlgorithm.linear_bandit_linucb_regret_bound) is pathwise given confidence, for a different algorithm, so the probabilistic half is new. Formalization also settles the printed constants, three of which need correction (below).

Difficulty

The deterministic half is linear algebra. The difficulty is the confidence theorem. Hoeffding–Azuma applied to ∑τMτ\sum_\tau M_\tau∑τ​Mτ​ would need a deterministic step bound, and the natural one gives only a T3/4T^{3/4}T3/4 regret. The step sizes of MtM_tMt​ are bounded in terms of the random widths wtw_twt​, so the argument must control the conditional variances pathwise and apply Freedman's inequality, whose event {V≤v}\{V\le v\}{V≤v} is random. The escape indicator EtE_tEt​, which switches the martingale off after the first failure of confidence, is what makes the variance bound hold on every path, and the induction that turns Lemma 14 into Theorem 5 must be carried out on a single event for all ttt simultaneously. Freedman's inequality itself is not in Mathlib.

Formalization scope

Vectors are Fin n → ℝ, matrices Matrix (Fin n) (Fin n) ℝ, rounds are indexed t=1,2,…t=1,2,\dotst=1,2,… in ℕ. The spanner is the standard basis, as in Section 5 of the paper (the algorithm is equivariant under the linear change of coordinates). The probability model is a probability space with a general filtration (Ft)(\mathcal F_t)(Ft​); xtx_txt​ is Ft\mathcal F_tFt​-measurable and ℓt\ell_tℓt​ is Ft+1\mathcal F_{t+1}Ft+1​-measurable. The argmin is encoded as a joint minimiser over D×Bt2D\times B^2_tD×Bt2​, which admits every tie-break and is required on every outcome; measurability of xtx_txt​ is a hypothesis, not derived from the selection. The optimum x∗x^*x∗ is a hypothesis (x∗∈Dx^*\in Dx∗∈D, minimising), not an sInf.

Corrections of the printed statements, each labelled in the item's Formalization Note:

  1. ln⁡(T+1)\ln(T+1)ln(T+1) for ln⁡T\ln TlnT in Lemma 9, Theorem 6 and Theorem 2. The printed bounds are false at T=1T=1T=1 (with n=1n=1n=1, D=[−1,1]D=[-1,1]D=[−1,1], μ>0\mu>0μ>0, the tie-break x1=1x_1=1x1​=1 gives R1=2μ>0R_1=2\mu>0R1​=2μ>0 against a bound of 000); the proof of Lemma 9 gives 2ln⁡det⁡At+1≤2nln⁡(t+1)2\ln\det A_{t+1}\le2n\ln(t+1)2lndetAt+1​≤2nln(t+1).
  2. n≤β1=(83ln⁡(1/δ))2n\le\beta_1=(\tfrac83\ln(1/\delta))^2n≤β1​=(38​ln(1/δ))2 is added to Theorems 5 and 2: the proof of Theorem 5 claims Z1≤n<β1Z_1\le n<\beta_1Z1​≤n<β1​, which fails for δ\deltaδ near 111. Theorem 6 takes the proof's "1<β11<\beta_11<β1​" as the hypothesis β1≥1\beta_1\ge1β1​≥1.
  3. ∣ℓt−μ⊤xt∣≤1|\ell_t-\mu^\top x_t|\le1∣ℓt​−μ⊤xt​∣≤1 is added to Lemma 14, Theorems 5 and 2: Section 5.2 uses ∣ηt∣≤1|\eta_t|\le1∣ηt​∣≤1, while the model gives only ∣ηt∣≤2|\eta_t|\le2∣ηt​∣≤2. It holds when costs lie in [0,1][0,1][0,1].
  4. Theorem 5's "δ>0\delta>0δ>0" is stated with 0<δ<10<\delta<10<δ<1; Lemma 10's index typo (wtw_twt​ for wτw_\tauwτ​) and Theorem 4's ∑i=1n\sum_{i=1}^n∑i=1n​ (for TTT) are corrected.

A regret bound for an arbitrary decision sequence under the assumption μ∈Bt2\mu\in B^2_tμ∈Bt2​ for all ttt is Theorem 6, not the goal; the goal carries the ConfidenceBall₂ selection rule, the conditional-mean and measurability hypotheses, and δ\deltaδ as the algorithm's own parameter. The hypotheses are jointly satisfiable, for example by a finite DDD with a fixed tie-break and i.i.d. costs in [0,1][0,1][0,1].

Needed infrastructure: Freedman's inequality for a filtration (reusable across all of bandit theory), the potential lemma (available), and measurability of the algorithm's statistics. Contributions of alternative proofs of Theorem 5, for example via self-normalized bounds, are welcome.

Selected references

  • V. Dani, T. P. Hayes, S. M. Kakade, Stochastic Linear Optimization under Bandit Feedback, COLT 2008. http://colt2008.cs.helsinki.fi/papers/80-Dani.pdf
  • P. Auer, Using Confidence Bounds for Exploitation-Exploration Trade-offs, JMLR 3, 2002. https://www.jmlr.org/papers/v3/auer02a.html
  • D. A. Freedman, On Tail Probabilities for Martingales, Annals of Probability 3(1), 1975. https://doi.org/10.1214/aop/1176996452
  • B. Awerbuch, R. Kleinberg, Adaptive Routing with End-to-End Feedback, STOC 2004. https://doi.org/10.1145/1007352.1007367
  • P. Rusmevichientong, J. N. Tsitsiklis, Linearly Parameterized Bandits, Mathematics of Operations Research 35(2), 2010. https://doi.org/10.1287/moor.1100.0446
  • Y. Abbasi-Yadkori, D. Pál, Cs. Szepesvári, Improved Algorithms for Linear Stochastic Bandits, NeurIPS 2011. https://arxiv.org/abs/1102.2670
  • T. Lattimore, Cs. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020. https://doi.org/10.1017/9781108571401
12 thms4 active usersReviewed
🏆Completed
Operations ResearchOptimizationProbability·Captain: naimengye

Multi-armed Bandit Allocation Indices I: The Gittins Index, Optimal Stopping and MonotonicityTextbook

Motivation

A decision-maker has nnn projects, each a Markov reward process, and at every decision time may advance exactly one of them; the others stay frozen. Which project to advance so as to maximize the expected total discounted reward? Posed as a dynamic program the problem has a state space that is the product of the nnn state spaces, and the size of that product defeats every general method. The index theorem of Gittins and Jones (1974) says the dynamic program is solved exactly by an index policy: there is a real number ν(B,x)\nu(B, x)ν(B,x), computable for each bandit process BBB from its own data and its own current state xxx, such that always advancing a process of greatest index is optimal. Chapter 2 of Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., doi:10.1002/9780470980033), introduces the index, proves the theorem three times, and works out the properties of the index that the rest of the book, from jobs and superprocesses to restless bandits, is built on: which stopping time attains it, how it is computed, how it moves with the discount factor, and when it collapses to the myopic rule.

The index theorem itself is already on the platform, proved, as BanditAlgorithm.gittins_index_theorem in the Bandit Algorithms series (Lattimore and Szepesvári, Theorem 35.9). This mission cites it and formalizes what Chapter 2 establishes around it.

Setting

A bandit process BBB (§2.3–2.4) is a Markov reward process on a countable state space EEE: transition probabilities P(y∣x)P(y \mid x)P(y∣x), a bounded reward r(x)r(x)r(x) received each time the continuation control is applied in state xxx, and a discount factor a∈(0,1)a \in (0, 1)a∈(0,1); the freeze control leaves the state unchanged and yields nothing. The law of the process started at xxx is Px\mathbb{P}_xPx​ and x(t)x(t)x(t) is its state at process time t=0,1,2,…t = 0, 1, 2, \dotst=0,1,2,…. A stopping time τ\tauτ is a past-measurable rule for switching from continuation to freezing, taking values in {1,2,… }∪{∞}\{1, 2, \dots\} \cup \{\infty\}{1,2,…}∪{∞}. For such τ\tauτ, Rτ(B,x)=Ex[∑t<τatr(x(t))]R_\tau(B, x) = \mathbb{E}_x[\sum_{t < \tau} a^t r(x(t))]Rτ​(B,x)=Ex​[∑t<τ​atr(x(t))] is the expected discounted reward and Wτ(B,x)=Ex[∑t<τat]W_\tau(B, x) = \mathbb{E}_x[\sum_{t < \tau} a^t]Wτ​(B,x)=Ex​[∑t<τ​at] the expected discounted time; their ratio ντ(B,x)\nu_\tau(B, x)ντ​(B,x) (2.7) is the equivalent constant reward rate of that portion of BBB. The Gittins index is

ν(B,x)=sup⁡τ>0Rτ(B,x)Wτ(B,x)(2.6)\nu(B, x) = \sup_{\tau > 0} \frac{R_\tau(B, x)}{W_\tau(B, x)} \tag{2.6}ν(B,x)=τ>0sup​Wτ​(B,x)Rτ​(B,x)​(2.6)

and, equivalently, the fair charge (2.5): the greatest rent λ\lambdaλ per period for which continuing BBB for one or more periods, paying λ\lambdaλ each period, can be done without expected loss. A simple family of alternative bandit processes (SFABP) is nnn such processes with a common discount factor, one of which is continued at each decision time; an index policy continues a process of greatest index. In the Lean development the single-arm model is the platform's (GittinsIndex): the chain law is built by the Ionescu–Tulcea construction, stopping times are adapted N∪{∞}\mathbb{N}\cup\{\infty\}N∪{∞}-valued maps on trajectories, and gittinsIndex P r a x is (2.6).

Formalization targets

Goal: Lemma 2.2, the optimal stopping set

The supremum in (2.6) is attained. For the initial state ξ\xiξ, the attaining stopping rule may be taken to be "stop at the first time t≥1t \ge 1t≥1 at which the state lies in Σ0\Sigma_0Σ0​" for any set Σ0\Sigma_0Σ0​ with

{x:ν(B,x)<ν(B,ξ)}⊆Σ0⊆{x:ν(B,x)≤ν(B,ξ)},\{x : \nu(B, x) < \nu(B, \xi)\} \subseteq \Sigma_0 \subseteq \{x : \nu(B, x) \le \nu(B, \xi)\},{x:ν(B,x)<ν(B,ξ)}⊆Σ0​⊆{x:ν(B,x)≤ν(B,ξ)},

and every such rule has ντ(B,ξ)=ν(B,ξ)\nu_\tau(B, \xi) = \nu(B, \xi)ντ​(B,ξ)=ν(B,ξ).

Milestones

Theorem 2.1 as a reference to the proved platform theorem; Eq. (2.5), the fair-charge characterization of the index; the restart-in-state formulation of §2.6.4 as the convergence of the Katehakis–Veinott value iteration; Theorem 2.3, monotonicity in the discount factor; Lemma 2.4, the interchange of two bandit portions; Propositions 2.5–2.8, the monotone-index cases in which the index is the immediate reward, or is attained only after the first step, or only at τ=∞\tau = \inftyτ=∞.

Significance

Lemma 2.2 is the working form of the index: it turns the supremum over all stopping times into a specific rule, the first time the index falls below its starting value, and it is what the interchange proof of §2.7, the modified-forwards-induction policies of §2.6.6, the monotone-index propositions of §2.11 and the treatment of jobs in Chapter 3 all use. The fair-charge form (2.5) is the prevailing-charge proof of the theorem (Weber 1992) and the interpretation that carries over to superprocesses and restless bandits. The restart formulation is how indices are computed in practice (Katehakis and Veinott 1987), and Theorem 2.3 is the first of the comparative statics used throughout Chapters 7 and 8. Lemma 2.4 is the elementary inequality behind the original proof of Gittins and Jones.

Of these, only the index theorem has a machine-checked proof today. Formalizing the rest gives the platform the index as a usable object: a characterization of the optimal stopping rule, a convergent algorithm for it, and the monotonicity facts, all stated against the existing model so that every later mission of this series and every future use of the L&S model can build on them.

Difficulty

The obvious first move for Lemma 2.2, "take the stopping time that achieves the supremum", is what has to be proved: the supremum is over an uncountable family, and attainment comes from the optimal stopping problem with charge λ=ν(B,ξ)\lambda = \nu(B, \xi)λ=ν(B,ξ), whose value function satisfies φ(x)=max⁡{0,r(x)−λ+aE[φ(x(1))∣x(0)=x]}\varphi(x) = \max\{0, r(x) - \lambda + a\mathbb{E}[\varphi(x(1)) \mid x(0) = x]\}φ(x)=max{0,r(x)−λ+aE[φ(x(1))∣x(0)=x]}, together with the fact that its optimal stopping set is characterized by the strict and non-strict inequalities λ>ν(B,x)\lambda > \nu(B, x)λ>ν(B,x) and λ≥ν(B,x)\lambda \ge \nu(B, x)λ≥ν(B,x). That last step is the content: it identifies the local decision "stop or continue" with a comparison of indices, which is why any set between the two level sets works. On the platform's model this requires the dynamic-programming theory of discounted optimal stopping on a countable space (Theorem 2.10 of the book), the identification of fairChargeProfit with that value function, and the strong Markov property of markovChainMeasure at a trajectory stopping time. Theorem 2.3 needs randomized stopping times (a geometric kill) and the fact that they do not enlarge the supremum. The restart iteration is monotone and bounded but its operator is not a contraction in the restart value, so its limit has to be identified with the restart problem's value directly; that value is max⁡(0,ν/(1−a))\max(0, \nu/(1-a))max(0,ν/(1−a)), not ν/(1−a)\nu/(1-a)ν/(1−a), because restarting forever is free.

Formalization scope

The state space is a countable type with measurable singletons, so every subset is measurable; rewards are bounded; a∈(0,1)a \in (0, 1)a∈(0,1). The chain law, stopping times, the discounted stopped sums and the index are the platform's, unchanged. Expectations are Bochner integrals; with bounded rewards they are finite and no total-function default value enters. IsPositiveStoppingTime fixes τ≥1\tau \ge 1τ≥1 everywhere, so Wτ≥1W_\tau \ge 1Wτ​≥1 and the ratio (2.7) is a genuine quotient. The stopping rule of Lemma 2.2 is the hitting time from time 111 of a set, with ∞\infty∞ when the set is never hit. The fair-charge profit is a real supremum over the nonempty bounded family of positive stopping times, and (2.5) is stated with the outer supremum over {λ:profit(λ)≥0}\{\lambda : \text{profit}(\lambda) \ge 0\}{λ:profit(λ)≥0}, a nonempty set bounded above. The restart iteration is stated as a limit, with the value max⁡(0,ν(B,ξ)/(1−a))\max(0, \nu(B, \xi)/(1-a))max(0,ν(B,ξ)/(1−a)): for a nonnegative index this is the book's ν/(1−a)\nu/(1-a)ν/(1−a), and the maximum is forced by a one-state example with negative reward. The propositions' hypotheses are almost-sure events under Px\mathbb{P}_xPx​, written as events of measure one.

Two trivializing readings are excluded: the index is never taken over all N∪{∞}\mathbb{N}\cup\{\infty\}N∪{∞}-valued maps but over adapted stopping times, and the stopping set of the goal is not restricted to the two extreme level sets. Contributions welcome: the optimal-stopping dynamic program on markovChainMeasure (value iteration, the strong Markov property at a stopping time), the equivalence of randomized and non-randomized stopping times for the supremum, and the monotone convergence of the restart iteration.

Selected references

  • J. Gittins, K. Glazebrook, R. Weber, Multi-armed Bandit Allocation Indices, 2nd ed., Wiley, 2011, Chapter 2. doi:10.1002/9780470980033
  • J. C. Gittins, D. M. Jones, A dynamic allocation index for the sequential design of experiments, in Progress in Statistics (Gani, ed.), North-Holland, 1974.
  • R. Weber, On the Gittins index for multiarmed bandits, Annals of Applied Probability 2(4), 1992. doi:10.1214/aoap/1177005588
  • M. N. Katehakis, A. F. Veinott, The multi-armed bandit problem: decomposition and computation, Mathematics of Operations Research 12(2), 1987. doi:10.1287/moor.12.2.262
  • T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapter 35. doi:10.1017/9781108571401
12 thms4 active usersReviewed
🏆Completed
Machine LearningOperations Research·Captain: Shuze Chen

Bandit Algorithms XV: Partial MonitoringTextbook

Bandit feedback is only one point on a spectrum: a learner might see more than its own loss (full information) or less (a spam filter never learns what happened to mail it deleted). Chapter 37 of Lattimore–Szepesvári studies finite adversarial games G=(L,Φ)G = (\mathcal{L}, \Phi)G=(L,Φ) where the loss matrix and the feedback matrix are decoupled. The goal theorem is the celebrated classification theorem: every finite partial-monitoring game has minimax regret exactly 000, Θ(n)\Theta(\sqrt{n})Θ(n​), Θ(n2/3)\Theta(n^{2/3})Θ(n2/3) or Ω(n)\Omega(n)Ω(n) — determined by two purely combinatorial conditions, global and local observability, on the game's neighbourhood structure. A single geometric dichotomy thus governs the price of information in every online decision problem with finite actions and feedback.

16 thms4 active users
🏆Completed
Machine LearningOperations Research·Captain: Shuze Chen

Bandit Algorithms X: Stochastic Linear Bandits and LinUCBTextbook

When actions are feature vectors and the mean reward is linear — Xt=⟨θ∗,At⟩+ηtX_t = \langle \theta_*, A_t\rangle + \eta_tXt​=⟨θ∗​,At​⟩+ηt​ — a bandit can generalize across arms: pulling one arm reveals information about all of them. Chapter 19 of Lattimore–Szepesvári carries the optimism principle into this setting: LinUCB (a.k.a. OFUL) plays the action maximizing max⁡θ∈Ct⟨θ,a⟩\max_{\theta\in\mathcal{C}_t}\langle\theta, a\ranglemaxθ∈Ct​​⟨θ,a⟩ over the confidence ellipsoid Ct\mathcal{C}_tCt​ of Mission IX. The goal theorem: with probability 1−δ1-\delta1−δ, R^n≤8nβnlog⁡det⁡Vndet⁡V0≤8dnβnlog⁡dλ+nL2dλ\hat R_n \le \sqrt{8n\beta_n \log\frac{\det V_n}{\det V_0}} \le \sqrt{8dn\beta_n\log\frac{d\lambda + nL^2}{d\lambda}}R^n​≤8nβn​logdetV0​detVn​​​≤8dnβn​logdλdλ+nL2​​ — regret O~(dn)\tilde O(d\sqrt{n})O~(dn​) independent of the number of actions. The combinatorial engine is the elliptical potential lemma, bounding how many times adaptively chosen directions can be surprising. Chapter 22's phased elimination with G-optimal design (Mission IX) sharpens this to O~(dnlog⁡k)\tilde O(\sqrt{dn\log k})O~(dnlogk​) for finite action sets.

7 thms4 active usersReviewed
🏆Completed
Machine LearningOperations Research·Captain: Shuze Chen

Bandit Algorithms IX: Self-Normalized Concentration and Optimal DesignTextbook

Least-squares estimation from adaptively collected data is the statistical heart of linear bandits: the actions AtA_tAt​ depend on past noise, so classical fixed-design theory does not apply. Chapter 20 of Lattimore–Szepesvári resolves this with the method of mixtures: the process Mt(x)=exp⁡(⟨x,St⟩−12∥x∥Vt(λ)2)M_t(x) = \exp(\langle x, S_t\rangle - \frac{1}{2}\|x\|^2_{V_t(\lambda)})Mt​(x)=exp(⟨x,St​⟩−21​∥x∥Vt​(λ)2​) is a supermartingale, and integrating over a Gaussian mixture yields the self-normalized bound — the goal theorem — P(∃t:∥St∥Vt(λ)−12≥2log⁡1δ+log⁡det⁡Vt(λ)λd)≤δ\mathbb{P}\big(\exists t : \|S_t\|^2_{V_t(\lambda)^{-1}} \ge 2\log\frac{1}{\delta} + \log\frac{\det V_t(\lambda)}{\lambda^d}\big) \le \deltaP(∃t:∥St​∥Vt​(λ)−12​≥2logδ1​+logλddetVt​(λ)​)≤δ, valid uniformly over all times. The resulting confidence ellipsoids for the regularized least-squares estimator (Abbasi-Yadkori et al.) calibrate every algorithm of Mission X. The mission also formalizes the Kiefer–Wolfowitz theorem of Chapter 21: G-optimal and D-optimal experimental designs coincide, with optimal value exactly ddd — the classical equivalence theorem of optimal design theory.

9 thms4 active usersReviewed
🏆Completed
Dynamic ProgrammingOperations ResearchProbability·Captain: mikedeng1

A Short Proof of the Gittins Index Theorem: For Finite-State Semi-Markov Bandits, Every Priority Policy Ordering States by the Index Algorithm's Indices Is OptimalResearch Paper

Motivation

The multi-armed bandit problem with discounted rewards asks how to allocate effort among nnn independent projects, only one of which can be worked on at a time, when the project worked on evolves randomly and the others stay frozen. It models job scheduling, research planning, search, and sequential clinical experimentation. Gittins and Jones showed in 1974 that the problem has an index solution: each state of each project has a number, computed from that project alone, and it is optimal always to work on the project whose current state has the largest number. The result turns an nnn-dimensional dynamic program into nnn one-dimensional computations.

Several proofs followed, each with its own model and its own definition of the index:

  • Gittins and Jones (1974) and Gittins (1979): the original interchange proofs, with the index as a supremum over stopping times of a reward-to-time ratio.
  • Whittle (1980): a proof through the retirement option and the dynamic-programming equation of the multi-armed problem.
  • Varaiya, Walrand and Buyukkoc (1985): the largest-remaining-index algorithm for finite-state Markov bandits, which computes the indices by removing states one at a time.
  • Weber (1992): the "prevailing charge" proof.
  • Tsitsiklis (1994): the short proof formalized here, for semi-Markov bandits with finite state spaces, by induction on the total number of states, with the indices produced by an index algorithm of the largest-remaining-index type.

Setting

There are n≥1n\ge1n≥1 bandit processes. Bandit iii has a finite nonempty state space Xi\mathcal X_iXi​, and X=X1∪⋯∪Xn\mathcal X=\mathcal X_1\cup\cdots\cup\mathcal X_nX=X1​∪⋯∪Xn​ is their disjoint union. When bandit iii at state x∈Xix\in\mathcal X_ix∈Xi​ is played, a random reward R(x)R(x)R(x) is received, the bandit is busy for a random time T(x)≥0T(x)\ge0T(x)≥0, and it then moves to a random state Y(x)∈XiY(x)\in\mathcal X_iY(x)∈Xi​; the other bandits do not move. The joint law of (T(x),R(x),Y(x))(T(x),R(x),Y(x))(T(x),R(x),Y(x)) depends only on xxx, and different plays are independent.

A policy is a map π:X1×⋯×Xn→{1,…,n}\pi:\mathcal X_1\times\cdots\times\mathcal X_n\to\{1,\dots,n\}π:X1​×⋯×Xn​→{1,…,n}: at time zero and at every play completion time it chooses the bandit to play from the current states. With tit_iti​ the start time and RiR_iRi​ the reward of the iii-th play and a discount rate β>0\beta>0β>0, the expected discounted reward from the initial joint state zzz is

Jπ(z)=E[∑i=1∞Rie−βti].J_\pi(z)=\mathbb E\Big[\sum_{i=1}^{\infty}R_i e^{-\beta t_i}\Big].Jπ​(z)=E[i=1∑∞​Ri​e−βti​].

A policy is optimal if it maximizes Jπ(z)J_\pi(z)Jπ​(z) for every initial state zzz. A priority rule is a policy for which some ordering of X\mathcal XX makes it always play the bandit whose current state is ordered highest.

The reward rate of a state is

r(x)=E[R(x)]E[∫0T(x)e−βt dt].(2.1)r(x)=\frac{\mathbb E[R(x)]}{\mathbb E\big[\int_0^{T(x)}e^{-\beta t}\,dt\big]}. \tag{2.1}r(x)=E[∫0T(x)​e−βtdt]E[R(x)]​.(2.1)

Reducing bandit i∗i^*i∗ by removing a state s∗s^*s∗ merges every play that ends in s∗s^*s∗ with the following run of plays at s∗s^*s∗ into one composite play, whose reward rate is r^(x)\hat r(x)r^(x) of (2.3). The index algorithm repeatedly picks a state s∗s^*s∗ of maximal current rate, sets its index γ(s∗)\gamma(s^*)γ(s∗) to that rate, and reduces its bandit by removing s∗s^*s∗ (or removes the bandit if s∗s^*s∗ was its last state).

Formalization targets

Goal: Theorem 2.2

Let γ\gammaγ be the indices of a run of the index algorithm. Then every priority rule whose ordering satisfies

γ(y)<γ(x) ⟹ y is ordered below x\gamma(y)<\gamma(x)\ \Longrightarrow\ y \text{ is ordered below } xγ(y)<γ(x) ⟹ y is ordered below x

is optimal. Ties in γ\gammaγ may be ordered either way, and the run may break ties in its own choices arbitrarily.

Milestones, in the order the proof uses them

  1. (2.2), the interchange inequality E[(1−e−βτ)∫0T(s∗)r(s∗)e−βtdt]≥E[(1−e−βT(s∗))∫0τrˉ(t)e−βtdt]\mathbb E\big[(1-e^{-\beta\tau})\int_0^{T(s^*)}r(s^*)e^{-\beta t}dt\big]\ge\mathbb E\big[(1-e^{-\beta T(s^*)})\int_0^{\tau}\bar r(t)e^{-\beta t}dt\big]E[(1−e−βτ)∫0T(s∗)​r(s∗)e−βtdt]≥E[(1−e−βT(s∗))∫0τ​rˉ(t)e−βtdt] when rˉ≤r(s∗)\bar r\le r(s^*)rˉ≤r(s∗).
  2. Lemma 2.1: if r(s∗)=max⁡xr(x)r(s^*)=\max_{x}r(x)r(s∗)=maxx​r(x), some optimal policy always plays bandit i∗i^*i∗ when it is at s∗s^*s∗.
  3. Reduction step: optimizing within the policies giving s∗s^*s∗ top priority is a bandit problem with one state fewer, the reduced bandit with rates (2.3).
  4. Theorem 2.1: some priority rule is optimal.
  5. Pick-order optimality: a priority rule that orders the states as a run of the index algorithm picks them is optimal.
  6. Index monotonicity: along a run, γ(s∗)≥γ(q∗)\gamma(s^*)\ge\gamma(q^*)γ(s∗)≥γ(q∗) for consecutive picks s∗,q∗s^*,q^*s∗,q∗.
  7. Picked-before characterization: xxx can be picked before yyy (in a run with the same indices) if and only if γ(x)≥γ(y)\gamma(x)\ge\gamma(y)γ(x)≥γ(y).

Significance

The theorem shows that the optimal priority order is determined by numbers that, by the reduction formulas, depend only on the statistics of each bandit separately. It is the basis of index policies in scheduling (the cμc\mucμ rule and its semi-Markov generalizations), of Klimov's problem and of branching bandits, which the paper's Section 3 obtains by modifying the same argument.

The result has been proved many times, but not in this generality on Prove2Me. The platform has a discrete-time Gittins index theorem for arms sharing one transition kernel and one reward function, with the index defined as a stopping-time supremum. This mission adds semi-Markov dynamics with random play durations and continuous discounting, heterogeneous finite bandits, priority rules, and the index algorithm as the definition of the index. A complete development would also give a machine-checked proof of correctness of a state-elimination algorithm for computing Gittins indices.

Difficulty

Lemma 2.1 compares an optimal stationary policy with a modified policy that is not stationary, and closes the gap by the optimality of stationary policies, which itself requires the dynamic-programming theory of discounted semi-Markov decision problems with finite state spaces. The reduction step requires an exact identification of the values of all top-priority policies with values in a different problem whose plays are composite and may never end. Theorem 2.1 is an induction over a family of problems with shrinking state spaces that are no longer raw semi-Markov bandits. Theorem 2.2 adds ties: a priority order compatible with the indices need not be the order of the given run, and one needs another run with the same indices.

Formalization scope

  • Bandits are indexed by Fin n (0,…,n−10,\dots,n-10,…,n−1), with n≥1n\ge1n≥1 and each state type finite and nonempty. X\mathcal XX is the sigma type Σ i, X i, disjoint by construction.
  • The law of (T(x),R(x),Y(x))(T(x),R(x),Y(x))(T(x),R(x),Y(x)) is a probability measure on R×R×Xi\mathbb R\times\mathbb R\times\mathcal X_iR×R×Xi​ with T≥0T\ge0T≥0 almost surely and RRR integrable. The model also assumes P(T(x)>0)>0\mathbb P(T(x)>0)>0P(T(x)>0)>0, which the page leaves implicit: it makes the denominator of (2.1) nonzero.
  • JπJ_\piJπ​ is computed from the moments E[R(x)]\mathbb E[R(x)]E[R(x)] and D(x,y)=E[e−βT(x);Y(x)=y]D(x,y)=\mathbb E[e^{-\beta T(x)};Y(x)=y]D(x,y)=E[e−βT(x);Y(x)=y]: it is the limit of the expected discounted reward of the first kkk plays, given by the first-step recursion. No path space is constructed. The row sums of DDD are below 111, so the limit exists; it never mentions rates, indices or reductions.
  • Policies are the paper's stationary deterministic maps of the current joint state, and optimality is within that class, for every initial state. An ordering of X\mathcal XX is an injective ranking into N\mathbb NN.
  • The reduced bandit is given by explicit formulas for its expected discounted reward, discounted duration and discounted transition data. These make the page's "transition probabilities are suitably modified" concrete, and the reduced rate is (2.3). Removing a bandit is the reduction of its last state.
  • The index is that of any run of the index algorithm, with arbitrary tie choices.

A formalization in which the value of a policy is defined through rates or indices, or in which γ\gammaγ is any function compatible with some order rather than the output of the algorithm, would make the goal trivial or empty; both are excluded by the definitions above.

Needed infrastructure: the convergence of the kkk-play values and the first-step (Bellman) equation for JπJ_\piJπ​; existence of an optimal stationary policy for finite discounted semi-Markov problems; the value identity for composite plays. The last two are reusable for any finite semi-Markov decision problem. Proofs of individual milestones, alternative arguments (Weber's prevailing charge, the retirement formulation), and the separability statement of p. 198 ("the index algorithm can be carried out separately for each different bandit") are welcome.

Selected references

  • J. N. Tsitsiklis, A Short Proof of the Gittins Index Theorem, Annals of Applied Probability 4(1) (1994), 194–199.
  • J. C. Gittins and D. M. Jones, A dynamic allocation index for the sequential design of experiments, in Progress in Statistics (J. Gani et al., eds.), North-Holland, 1974, 241–266.
  • J. C. Gittins, Bandit processes and dynamic allocation indices, J. Roy. Statist. Soc. Ser. B 41 (1979), 148–177. https://doi.org/10.1111/j.2517-6161.1979.tb01068.x
  • P. Whittle, Multi-armed bandits and the Gittins index, J. Roy. Statist. Soc. Ser. B 42 (1980), 143–149. https://doi.org/10.1111/j.2517-6161.1980.tb01111.x
  • P. P. Varaiya, J. C. Walrand and C. Buyukkoc, Extensions of the multiarmed bandit problem: the discounted case, IEEE Trans. Automat. Control 30 (1985), 426–439. https://doi.org/10.1109/TAC.1985.1103989
  • R. Weber, On the Gittins index for multiarmed bandits, Annals of Applied Probability 2(4) (1992), 1024–1033. https://doi.org/10.1214/aoap/1177005588
11 thms3 active usersReviewed
🏆Completed
Operations ResearchProbabilityStatistics·Captain: mikedeng1

Dynamic Pricing Without Knowing the Demand Function: Risk Bounds and Near-Optimal Algorithms I: The Nonparametric Learn-then-Price Policy Has Regret at Most C(log n)^{1/2}/n^{1/4}Research Paper

Why price without knowing demand

A seller with a fixed stock of a single product and a finite selling season has to set prices without knowing how demand responds to them. This is the standard situation in revenue management: airline seats, hotel rooms, fashion goods and event tickets. The classical theory of dynamic pricing (Gallego and van Ryzin, 1994) assumes that the demand function λ(p)\lambda(p)λ(p), the rate of purchase requests at price ppp, is known. In practice it has to be learned from sales, while the season runs and the stock is consumed.

Besbes and Zeevi (2009) asked how much revenue is lost for not knowing λ\lambdaλ. They answered it with explicit policies and matching-order bounds. Their setting differs from the multi-armed bandit literature it borrows from in three ways:

  • the problem is constrained by an initial inventory;
  • the set of prices is a continuum;
  • the set of possible demand functions is a nonparametric class.

This mission formalizes their first main result, Proposition 1: a simple learn-then-price policy has worst-case relative regret of order (log⁡n)1/2n−1/4(\log n)^{1/2}n^{-1/4}(logn)1/2n−1/4 in a market of size nnn.

Setting

Prices. Fix 0<p‾<p‾<∞0<\underline p<\overline p<\infty0<p​<p​<∞ and an off price p∞>0p_\infty>0p∞​>0 outside [p‾,p‾][\underline p,\overline p][p​,p​]. The seller may charge any price in [p‾,p‾]∪{p∞}[\underline p,\overline p]\cup\{p_\infty\}[p​,p​]∪{p∞​}; charging p∞p_\inftyp∞​ stops demand.

Demand. Requests arrive as a Poisson process whose intensity at time ttt is λ(p(t))\lambda(p(t))λ(p(t)). Let NNN be a unit-rate Poisson process. By the time change (1), the cumulative requests up to time ttt under a price path p(⋅)p(\cdot)p(⋅) are N(∫0tλ(p(s)) ds)N\big(\int_0^t\lambda(p(s))\,ds\big)N(∫0t​λ(p(s))ds). The seller starts with inventory xxx and sells until either the horizon TTT ends or the stock runs out. The expected revenue of a policy π\piπ is Jπ(x,T;λ)J^\pi(x,T;\lambda)Jπ(x,T;λ).

Demand class. L=L(M,K‾,K‾,m)\mathcal L=\mathcal L(M,\underline K,\overline K,m)L=L(M,K​,K,m) is the set of regular demand functions satisfying Assumption 1. Regular means:

  • λ≥0\lambda\ge0λ≥0 and λ(p∞)=0\lambda(p_\infty)=0λ(p∞​)=0;
  • λ\lambdaλ is non-increasing on [p‾,p‾][\underline p,\overline p][p​,p​], with inverse γ\gammaγ;
  • the revenue rate r(l)=lγ(l)r(l)=l\gamma(l)r(l)=lγ(l) is concave.

Assumption 1 requires:

  • (i) λ≤M\lambda\le Mλ≤M on [p‾,p‾][\underline p,\overline p][p​,p​];
  • (ii) λ\lambdaλ is K‾\overline KK-Lipschitz and γ\gammaγ is K‾−1\underline K^{-1}K​−1-Lipschitz;
  • (iii) max⁡ppλ(p)≥m\max_p p\lambda(p)\ge mmaxp​pλ(p)≥m.

Benchmark. The deterministic relaxation (5) replaces the random demand by its mean:

JD(x,T∣λ)=sup⁡{∫0Tp(s)λ(p(s)) ds:∫0Tλ(p(s)) ds≤x}.J^D(x,T\mid\lambda)=\sup\Big\{\int_0^T p(s)\lambda(p(s))\,ds:\int_0^T\lambda(p(s))\,ds\le x\Big\}.JD(x,T∣λ)=sup{∫0T​p(s)λ(p(s))ds:∫0T​λ(p(s))ds≤x}.

The regret of a policy is Rπ=1−Jπ/JD\mathcal R^\pi=1-J^\pi/J^DRπ=1−Jπ/JD.

Scaling. In a market of size nnn the inventory is nxnxnx and the demand function is nλn\lambdanλ, as in (11). The corresponding quantities are JnπJ^\pi_nJnπ​, JnD=nJDJ^D_n=nJ^DJnD​=nJD and Rnπ\mathcal R^\pi_nRnπ​.

Algorithm 1, π(τ,κ)\pi(\tau,\kappa)π(τ,κ). The policy has three phases.

  1. Learning. On [0,τ][0,\tau][0,τ] it tests κ\kappaκ equally spaced prices pi=p‾+(i−1)(p‾−p‾)/κp_i=\underline p+(i-1)(\overline p-\underline p)/\kappapi​=p​+(i−1)(p​−p​)/κ, each for Δ=τ/κ\Delta=\tau/\kappaΔ=τ/κ time units. It estimates λ(pi)\lambda(p_i)λ(pi​) by the normalized request counts λ^(pi)\hat\lambda(p_i)λ^(pi​).
  2. Optimization. It chooses p^u=arg⁡max⁡ipiλ^(pi)\hat p^u=\arg\max_i p_i\hat\lambda(p_i)p^​u=argmaxi​pi​λ^(pi​) and p^c=arg⁡min⁡i∣λ^(pi)−x/T∣\hat p^c=\arg\min_i|\hat\lambda(p_i)-x/T|p^​c=argmini​∣λ^(pi​)−x/T∣, and sets p^=max⁡{p^u,p^c}\hat p=\max\{\hat p^u,\hat p^c\}p^​=max{p^​u,p^​c}.
  3. Pricing. It charges p^\hat pp^​ on (τ,T](\tau,T](τ,T] until the stock runs out.

Formalization targets

Goal: Proposition 1

Let τn≍n−1/4\tau_n\asymp n^{-1/4}τn​≍n−1/4 and κn≍n1/4\kappa_n\asymp n^{1/4}κn​≍n1/4, and let πn=π(τn,κn)\pi_n=\pi(\tau_n,\kappa_n)πn​=π(τn​,κn​). Then there is a finite constant CCC, independent of λ\lambdaλ and nnn, such that

sup⁡λ∈LRnπ(x,T;λ)≤C(log⁡n)1/2n1/4(n≥2).\sup_{\lambda\in\mathcal L}\mathcal R^{\pi}_n(x,T;\lambda)\le\frac{C(\log n)^{1/2}}{n^{1/4}}\qquad(n\ge2).λ∈Lsup​Rnπ​(x,T;λ)≤n1/4C(logn)1/2​(n≥2).

The constant is left unspecified, as in the paper. Its dependence on the class parameters, xxx and TTT is "somewhat complex" (p. 12), and the order (log⁡n)1/2n−1/4(\log n)^{1/2}n^{-1/4}(logn)1/2n−1/4 is the content of the result.

Milestones

The milestones follow the proof in the appendix, in order:

  • the scaling JnD=nJDJ^D_n=nJ^DJnD​=nJD (p. 12);
  • Fact 1, JD≥mmin⁡{T,x/M}J^D\ge m\min\{T,x/M\}JD≥mmin{T,x/M} on L\mathcal LL;
  • Lemma 1, the solution of (5): charge pD=max⁡{pu,pc}p^D=\max\{p^u,p^c\}pD=max{pu,pc} until the stock runs out;
  • Lemma 2, a Poisson deviation bound;
  • the revenue lower bound (A-2);
  • Lemma 3, the learned price is near pDp^DpD with high probability;
  • Lemma 4 and the Case 1 bound (A-11), for λ(p‾)≤x/T\lambda(\overline p)\le x/Tλ(p​)≤x/T;
  • Lemma 5 and the Case 2 bound (A-15), for λ(p‾)>x/T\lambda(\overline p)>x/Tλ(p​)>x/T;
  • the Step 4 bound Rnπ≤C12(un+τn)\mathcal R^\pi_n\le C_{12}(u_n+\tau_n)Rnπ​≤C12​(un​+τn​), where un=(log⁡n)1/2max⁡{1/κn,(nΔn)−1/2}u_n=(\log n)^{1/2}\max\{1/\kappa_n,(n\Delta_n)^{-1/2}\}un​=(logn)1/2max{1/κn​,(nΔn​)−1/2}.

Significance

Proposition 1 shows that a seller who knows only a nonparametric class of demand functions can approach the full-information revenue uniformly over the class. Learning costs a vanishing fraction of revenue, and the policy needs no parametric model. Together with the paper's lower bound of order n−1/2n^{-1/2}n−1/2 for every admissible policy (Proposition 2, not in this mission), it brackets the minimax regret of nonparametric pricing under an inventory constraint. The result is a reference point for the learning-and-earning literature in operations management that followed it.

The result is proved in the paper; to our knowledge, it has no machine-checked proof. Formalizing it requires:

  • a working theory of policies driven by a time-changed Poisson process, with sales capped by an inventory;
  • the deterministic relaxation of Gallego and van Ryzin for a continuum of prices with an off price;
  • uniform (over the class) Poisson concentration bounds.

The mission produces Lean statements of all of these. A proof would also check every constant chain of the appendix, where the argument uses some displays in a form slightly different from their printed statement (see the scope section).

Difficulty

The obvious argument controls the estimation error at the tested prices and concludes that p^\hat pp^​ is close to the optimal price. It breaks in two places.

First, pDp^DpD is the larger of two prices, the revenue maximizer and the price that sells the inventory exactly. Near the boundary between these regimes, the revenue rate at p^\hat pp^​ is not controlled by the error in p^\hat pp^​ alone: it needs the concavity of the revenue rate and the inverse Lipschitz bound on γ\gammaγ.

Second, when demand at the highest price exceeds the inventory rate (λ(p‾)>x/T\lambda(\overline p)>x/Tλ(p​)>x/T), the revenue is limited by stock-outs rather than by the price. The bound must then show that nearly all of the inventory is sold during the pricing phase, uniformly over the class.

Throughout, every constant must be independent of the demand function, so the estimates have to hold uniformly over an infinite-dimensional class.

Formalization scope

  • Poisson process. The demand is driven by IsPoissonProcess N 1 on a probability space (Ω,P)(\Omega,\mathbb P)(Ω,P), a published platform definition: ℕ-valued, N(0)=0N(0)=0N(0)=0, monotone paths, independent Poisson increments. The time change (1) is rendered by evaluating NNN at cumulative intensities.
  • Inventory. The inventory of the market of size nnn is ⌊nx⌋\lfloor nx\rfloor⌊nx⌋ units, and sales are min⁡{N(⋅),⌊nx⌋}\min\{N(\cdot),\lfloor nx\rfloor\}min{N(⋅),⌊nx⌋}. The cap is never dropped.
  • Revenue. JnπJ^\pi_nJnπ​ is the Bochner expectation of a bounded, finitely-valued revenue, so it is a genuine integral.
  • Demand functions. A demand function is a map R→R\mathbb R\to\mathbb RR→R, nonnegative, with λ(p∞)=0\lambda(p_\infty)=0λ(p∞​)=0. Regularity and Assumption 1 are imposed on [p‾,p‾][\underline p,\overline p][p​,p​], and the inverse γ\gammaγ is Function.invFunOn.
  • Benchmark. JDJ^DJD is a supremum over measurable price paths with integrable demand rate. The supremum is genuine: the set of path revenues is nonempty and bounded.
  • Algorithm. The grid excludes p‾\overline pp​, as in the paper. Ties in the grid argmax and argmin go to the smallest index. The estimates compare λ^(pi)\hat\lambda(p_i)λ^(pi​) with x/Tx/Tx/T.
  • Tuning. τn≍n−1/4\tau_n\asymp n^{-1/4}τn​≍n−1/4 and κn≍n1/4\kappa_n\asymp n^{1/4}κn​≍n1/4 are encoded with explicit constants 0<c≤c′0<c\le c'0<c≤c′, with τn∈(0,T]\tau_n\in(0,T]τn​∈(0,T] and κn≥1\kappa_n\ge1κn​≥1. Constants may depend on c,c′c,c'c,c′, the class parameters, the prices, xxx and TTT, but never on λ\lambdaλ or nnn.
  • Range of nnn. Bounds whose right side vanishes at n=1n=1n=1 because log⁡1=0\log1=0log1=0 are stated for n≥2n\ge2n≥2: the goal and (A-15).
  • Typo correction. Lemma 5's event uses nx−C9nunnx-C_9nu_nnx−C9​nun​, as in its proof, not the printed nx−C9unnx-C_9u_nnx−C9​un​.
  • Ruled out. A specific demand curve, a fixed nnn, deterministic demand, a finite price set, a known λ\lambdaλ, constants depending on λ\lambdaλ, or dropping the inventory cap would each make the statement a different and easier theorem. None is used.
  • Not included. The lower bound of Proposition 2 and the second assertion of Lemma 1 (Jπ≤JDJ^\pi\le J^DJπ≤JD for all admissible policies) are not included.

Contributions are welcome at any level: proofs of the milestones (Fact 1, Lemma 1 and Lemma 2 are self-contained), measurability and integrability lemmas for the revenue functional, and a reusable Poisson concentration library built on Mathlib's poissonMeasure.

Selected references

  • O. Besbes and A. Zeevi, Dynamic Pricing Without Knowing the Demand Function: Risk Bounds and Near-Optimal Algorithms, Operations Research 57(6):1407–1420, 2009. https://doi.org/10.1287/opre.1080.0640
  • G. Gallego and G. van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons, Management Science 40(8):999–1020, 1994. https://doi.org/10.1287/mnsc.40.8.999
  • K. Talluri and G. van Ryzin, The Theory and Practice of Revenue Management, Springer, 2005. https://doi.org/10.1007/b139000
15 thms3 active usersReviewed
PreviousPage 1 of 3Next

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me