LMLExplore

How it is built

• Humans write the roadmaps in LMLRoadmaps. Five are active: bandit algorithms and their regret, bandit identification, Markov decision processes and reinforcement learning, online learning through convex optimization, and the restatement of merged material in the generality of the literature.

• AI agents, run with the Tau Ceti worker, pick targets on the roadmaps, write the Lean code and open pull requests.

• AI reviewers judge every pull request against ten rubrics: correctness, reuse, scope, attribution, API design, generality, placement, naming, documentation and proof quality. A pull request is merged when every rubric approves it and CI passes.

• CI rejects sorry, axioms other than the three standard ones (so no native_decide), and any warning of the Mathlib linters.

How it relates to LML

• LMLExplore imports LML: 49 of its files import LML directly, mostly its sequential learning framework and its bandit definitions, and 29 import Tau Ceti.

• LMLExplore never proposes material to the libraries it imports. The maintainers of LML pick, by hand, what to curate into LML.

• When Mathlib, Tau Ceti or LML later provides something that LMLExplore already has, the copy in LMLExplore is deleted and its uses move to the upstream version.

• The three dependencies are updated together, at Lean releases.

Theorems by area

Bandits

• Regret bounds for MOSS, E[R_n] ≤ 39 √(σ² k n) + ∑ Δ_a, and a gap-free bound for the UCB algorithm of LML.

• Lower bounds: every algorithm has regret at least √(σ² (k - 1) n) / 16 on some bandit (the minimax lower bound), and every consistent algorithm has regret at least c log n asymptotically, for an explicit constant c that depends on the bandit (the Lai–Robbins lower bound), with a finite-time version of the latter.

• Asymptotically optimal UCB, KL-UCB and Gaussian Thompson sampling, which match the Lai–Robbins lower bound. On Gaussian bandits, the regret of asymptotically optimal UCB and of Gaussian Thompson sampling is c log n + o(log n) with c = ∑ 2 σ² / Δ_a, and KL-UCB does the same on Bernoulli bandits, with c = ∑ Δ_a / d(μ_a, μ*).

• KL-UCB for exponential families, with a family for each arm, of which KL-UCB for rewards in [0, 1] and asymptotically optimal UCB are the Bernoulli and Gaussian instances. It has a finite-time regret bound for arms dominated, in moment generating function, by members of their families. On bandits whose arms belong to exponential families with a common set of means, its regret is c log n + o(log n) with c = ∑ Δ_a / d_a(μ_a, μ*), which matches the Lai–Robbins lower bound for these bandits. For Gaussian arms with known variances, which may differ between arms, c = ∑ 2 σ_a² / Δ_a.

• Stochastic linear bandits and OFUL, also called LinUCB: with probability at least 1 - δ, the regret of OFUL is at most √(8 n R² d log (1 + n L² / (λ d))), for confidence ellipsoids of radius R in dimension d and features of norm at most L. The minimax lower bound on the hypercube [-1, 1]^d: with Gaussian noise of variance σ², every algorithm has regret at least e⁻² d √(σ² n) / 4 on some instance.

• Adversarial bandits: adversarial regret, regret against expert advice, the pseudo-regret and the random regret against any environment, such as an adaptive adversary, and importance-weighted estimators. Mirror descent and follow-the-regularized-leader with bandit feedback, also against an adaptive adversary. On the unit ball in dimension d, follow-the-regularized-leader with bandit feedback has expected regret at most 2 √(3 n d log n) against an adaptive adversary.

• Exp4-IX, whose learning rates and implicit exploration may change with the rounds, with Exp4, Exp3-IX and Exp3 as its instances, all analyzed against an adaptive adversary for rewards in [0, 1]. Exp3 has pseudo-regret at most √(2 n k log k) and Exp4 at most √(2 n k log M) against the best of M experts, with learning rates tuned to the horizon n, and 2 √(n k log k) and 2 √(n k log M) with learning rates that do not depend on n. The high-probability bounds of Neu: with probability at least 1 - δ, the regret of Exp3-IX is at most 4 √(n k log k) + (√(n k / log k) + 1) log (2 / δ), and that of Exp4-IX against the best of M experts is at most 2 √(2 n k log M) + (√(n k / (2 log M)) + 1) log (2 / δ).

• Follow-the-perturbed-leader policies, among them Gaussian Thompson sampling, with the generic bound on their numbers of pulls of Lattimore and Szepesvári.

• Gaussian and Bernoulli bandits, index policies and randomized policies, as reusable building blocks.

Identification

• Identification tasks with general models and possibly several correct answers, including best arm, top-m, additive and multiplicative ε-best arm, thresholding, any low arm and half-space identification, in the fixed-confidence and fixed-budget settings. Gaussian arms with known or unknown variances, and the model of all bandits with real observations, so that the guarantees of the elimination, LUCB, KL-LUCB and fixed-budget algorithms below hold on every bandit of a class, such as the bandits with σ²-sub-Gaussian arms or with arms in [0, 1].

• The change of measure at a stopping time, and the lower bound E[τ] ≥ T*(θ) kl(δ, 1 - δ) on the expected number of samples of a δ-correct algorithm, and its explicit forms for top-m and ε-best arm identification, such as E[τ] ≥ K / (48 ε²) log (1 / (2.4 δ)) for Bernoulli arms. Lower bounds on the probability of error in the fixed-budget setting.

• The stopping rules of LUCB and KL-LUCB for top-m identification with tolerance ε, which are δ-correct whatever the sampling rule.

• Successive rejects and sequential halving, fixed-budget algorithms for best arm identification whose probability of error decays exponentially with the budget T. For σ²-sub-Gaussian arms, successive rejects errs with probability at most K (K - 1) / 2 · exp(-(T - K) / (4 σ² L_K H₂)), for a complexity H₂ of the bandit and L_K = 1/2 + ∑_{i=2}^K 1/i.

• Elimination algorithms: successive elimination is δ-correct, with a high-probability bound on its number of samples, and median elimination is (ε, δ)-PAC.

• Generalized likelihood ratio stopping rules, which are δ-PAC with any sampling rule that stops almost surely, when their thresholds come from a time-uniform concentration bound. The thresholds may depend on the history, for instance through the numbers of pulls. On every task whose models are vectors of means, for arms dominated, in moment generating function, by members of an exponential family (among them Gaussian arms), the thresholds K log (2 n (n + 1)) + x_δ with x_δ = log (1 / δ) + 2 K (1 + log (1 + log (1 / δ))) make the stopping rule δ-PAC, following Garivier and Kaufmann.

• Stopping rules that cover the alternatives by several pieces, each with its own statistic and threshold. For best arm and top-m identification with arms dominated by exponential families, pairwise stopping rules, which compare two arms at a time, are δ-PAC with thresholds that grow as 4 log n instead of 2 K log n.

• The pure exploration game: transportation costs, the characteristic time T*, the minimax form of the game, and the continuity of its value through Berge's maximum theorem. Oracle answers and oracle allocations for tasks with several correct answers.

• Closed forms of the game for best arm identification in exponential families, for thresholding and any low arm tasks, and for half-space and sphere identification with Gaussian arms. For best arm identification, the optimal allocation is unique and gives a positive proportion to every arm, and for Gaussian arms T* is within a factor 2 of the classical complexity H(μ) = ∑ 2 σ² / Δ_a².

• Product models, in which each arm has its own parameter, and the divergences K⁻ and K⁺ of Agrawal, Juneja and Glynn, from the law of an arm to the laws of mean below or above a level. They bound below the costs of the alternatives of best arm, top-m and thresholding identification, with equality for best arm identification under a continuity condition. Their explicit forms for exponential families, for Gaussian arms of unknown variance, where K⁻((μ, σ²), u) = log (1 + (μ - u)² / σ²) / 2 for u ≤ μ, and for laws on [0, 1], where they are at least the Bernoulli relative entropy.

• Top Two sampling: the β-optimal allocations of best arm identification are unique, and T*_{1/2} ≤ 2 T*.

• Track-and-Stop, defined for any task and any estimator of the model, with D-tracking or C-tracking. For vectors of means estimated by the empirical means, its expected number of samples is at most c log (1 / δ) for small δ, for every c > T*(μ). For Gaussian arms it is moreover δ-PAC, hence asymptotically optimal: E[τ_δ] / log (1 / δ) → T*(μ) as δ → 0. These results hold on tasks with one correct answer per model, under continuity conditions on the transportation costs, and with C-tracking even where the optimal allocations are not unique.

• The guarantees of D-tracking, C-tracking and cumulative tracking, the sampling rules that follow target allocations.

Markov decision processes and reinforcement learning

• Markov decision processes on general measurable spaces, as environments of the sequential learning framework of LML, so that every algorithm of that framework is a policy. Markov policies, discounted values, action values and advantages.

• The Bellman operators are contractions on bounded measurable functions. The optimality equation has a unique solution, the optimal value, and a deterministic stationary policy attains it. With finitely many actions, a stationary policy is optimal if and only if it plays, almost surely, actions with Q*(s, a) = v*(s).

• Value iteration, policy iteration and modified policy iteration, with their geometric convergence. Policy iteration terminates on finite state spaces. Bounds on the optimal value, the span stopping rule of value iteration, and the action elimination tests of Puterman, which detect suboptimal actions from these bounds. The Bellman optimality operator contracts the span at rate γ δ, where δ is the Dobrushin coefficient of the transitions, on general state spaces. Abstract dynamic programming, also when suprema are not attained.

• Discounted occupancy measures and the flow equation, the performance difference lemma, and the simulation lemma, also with an error on the rewards and in total variation.

• The variance of the discounted return: the total-variance identity of Sobel for Markov chains, and, for a stationary policy with rewards bounded by C, the variance Bellman equation and the total-variance lemma of Agarwal, Jiang, Kakade and Sun, (1 - γ P^π)⁻¹ √(Var_P(v^π)) ≤ C √(2 / (1 - γ)³).

• Episodic MDPs: occupancy measures and the policy-mixture lemma, optimal values by backward induction, an optimal greedy policy, the extended value-difference identity, the pessimistic decomposition of suboptimality, and bounds on the suboptimality of the policies that are greedy for approximate action values.

• Planning with a generative model: for S states and A actions, rewards bounded by C and N samples of each state-action pair, the empirical MDP, which keeps the rewards of the true MDP, has, with probability at least 1 - δ, optimal action values within γ C Δ / (1 - γ)² of those of the true MDP, where Δ = √(2 log (2 S A / δ) / N) (the crude bounds of Agarwal, Jiang, Kakade and Sun). The variance-aware analysis of Azar, Munos and Kappen improves this to 2 γ C √(L / ((1 - γ)³ N)) + 17 γ C L / ((1 - γ)³ N), with L = log (3 S A / δ). The absorbing modifications of Agarwal, Kakade and Yang, which make a state absorbing without changing its value.

• First steps in reinforcement learning: the learning-rate weights of optimistic Q-learning.

Online learning and probability tools

• The follow-the-regularized-leader lemma, and mirror descent with its regret bounds, also with nonincreasing learning rates. Projected online subgradient descent for online convex optimization. With the negative entropy on the simplex, follow-the-regularized-leader is exponential weights, with regret at most √(2 n log k). A local-norm regret bound for exponential weights, also with nonincreasing learning rates, and AdaHedge, whose learning rate tunes itself from the observed losses. The weights of the Tsallis-INF algorithm of Zimmert and Seldin, as the unique minimizers of the ½-Tsallis objective on the simplex.

• Concentration inequalities: Bennett's inequality and Bernstein's inequality in high-probability form, and Freedman's inequality for martingales, whose bounds scale with the conditional variances rather than the range. The empirical Bernstein inequality of Audibert, Munos and Szepesvári, in which the sample variance replaces the unknown variance. Exponential supermartingales for increments with conditionally bounded moment generating functions, which give time-uniform Chernoff bounds for the observations of each arm under any sampling rule. The self-normalized inequality of Garivier and Cappé for the mean of variables selected by a predictable rule, with the Cramér rate function as exponent, and the deviation bound of Lattimore and Szepesvári for all the arms at once, extended from Gaussian arms to any integrable rewards.

• Ville's inequality, the self-normalized bound for vector-valued martingales, confidence ellipsoids for ridge regression, and the elliptical potential lemma: the tools of linear bandits. Least squares with the Moore–Penrose inverse, for designs that need not span the space, with its fixed-design confidence bound. The Kiefer–Wolfowitz theorem: a nonempty compact set that spans a space of dimension d carries a finitely supported design w with ⟪a, V(w)⁻¹ a⟫ ≤ d for every point a of the set, the smallest possible bound.

• Exponential families on any measurable space, among them the Gaussian, Bernoulli, Poisson and exponential laws, and the gamma laws of known shape. Their divergences, extended to every real level, and the upper confidence levels that serve as the indices of KL-UCB, with the two concentration lemmas of its analysis. Cramér–Chernoff bounds with the Cramér rate function as exponent, the lower bound of Cramér's theorem, the ℓ¹ deviation of empirical laws, the Bretagnolle–Huber inequality, the inequality kl(E_P[X], E_Q[X]) ≤ KL(P, Q) of Garivier, Ménard and Stoltz for laws on [0, 1], and Wald's identities for sequential algorithms.

• The Dobrushin coefficient of a Markov kernel and uniform ergodicity: a Markov kernel κ such that the coefficient δ(κ^m) of some power is less than 1 has a unique invariant probability measure, and its n-step laws converge to it geometrically in total variation. On finite spaces, a chain with a primitive transition matrix is uniformly ergodic. Mixing times, with t_mix(ε) ≤ ⌈log₂ (1/ε)⌉ t_mix(1/4), and the resolvent ∑ₙ γⁿ κⁿ as the inverse of 1 - γ κ.

• Von Neumann's minimax theorem on the simplex, Berge's maximum theorem, and the hemicontinuity of correspondences.