BanditRLlib
Lean gate passed before this site build; local proof declarations are shown as compiled.Lean-verified build · exact declarations linked.

BanditRLwiki setting

Finite-horizon tabular reinforcement learning

Episodic tabular MDP regret, Hoeffding and Bernstein bonuses, and full-range minimax behavior.

← All settings

Comparison signature

  • Problem class. Unknown episodic tabular MDP
  • Feedback. Generated state, action, reward, and next-state trajectories
  • Objective. High-probability cumulative episode pseudo-regret
  • Parameters. S states, A actions, horizon H, episodes K, total steps T=HK
Matching rule. A rate is called matched only when the upper and lower theorem contracts agree on the fields above; every remaining mismatch is named in the case.

1 cases

tabular-finite-horizon-rl-ucbvi Tabular finite-horizon RL: UCBVI and minimax leading ratesUCBVI-BF has the near-minimax variance-aware leading rate; BanditRLlib currently compiles the known-reward Hoeffding UCBVI-CH terminal. Near minimaxPartial local route
Open stable case page →Faithful restatement
UCBVIUCBVI-CHUCBVI-BFtabular MDPBernsteinminimax RL
MDP
Unknown episodic tabular transitions with S states, A actions, horizon H
Episodes
K episodes and total steps T=H K
Regret
High-probability cumulative episode pseudo-regret
Target scale
square root(H S A T), plus lower-order terms

Comparison judgment

Near minimax

The literature and local status must be read separately: UCBVI-CH compiles locally, while the variance-aware source-leading theorem does not.

Known gap. UCBVI-BF gives a high-probability upper bound whose leading large-T polynomial rate matches the expected-regret minimax lower scale up to logs and lower-order terms; these probability modes are not identical theorem contracts. A later modified MVP route addresses the full parameter range. The compiled local theorem is Hoeffding, not Bernstein/minimax.

Local Lean boundary

Partial local route

The canonical recurrent known-reward Hoeffding UCBVI-CH 20/250 high-probability terminal and failure-aware expected consumer compile. Bernstein/Freedman, stochastic rewards, and a minimax lower pair do not.

Upper bound

UCBVI high-probability regret upper bounds

Minimax Regret Bounds for Reinforcement Learning

Mohammad Azar, Ian Osband, and Rémi Munos · 2017 · Theorems 1–2

Upper bound guarantee. The Hoeffding version has the explicit 20 and 250 bound; the Bernstein-Freedman version improves the leading horizon dependence to the near-minimax scale.

Use the paper's confidence logarithm L, reward model, and horizon conditions.

Open primary source

Upper bound

Modified MVP full-range minimax regret bound

Settling the sample complexity of online reinforcement learning

Zihan Zhang and collaborators · 2024 · Modified MVP full-range result

Upper bound guarantee. A modified MVP analysis supplies the closest full-range upper guarantee across all episode counts.

This is a separate algorithmic route and must not be relabeled as UCBVI.

Open primary source

Lower bound

Tabular episodic minimax lower-bound comparison

Minimax Regret Bounds for Reinforcement Learning

Mohammad Azar, Ian Osband, and Rémi Munos · 2017 · Minimax lower-bound comparison

Lower bound guarantee. Some tabular finite-horizon MDP forces expected regret at the square-root H S A T scale in the source regime.

Use the source's state, action, horizon, and total-time range.

Open primary source

Not yet proved here

Missing steps

  • Build the conditional variance and Freedman/Bernstein bonus layer.
  • Compile the law-of-total-variance and recurrent value/Q recursion needed by UCBVI-BF.
  • Treat stochastic rewards, realized sampled-return regret, and the MVP full-range route as distinct extensions.

formalization frontier

Can the recurrent generated UCBVI source be upgraded from Hoeffding bonuses to the exact Bernstein/Freedman source theorem?

The source-shaped UCBVI-CH endpoint compiles with the exact 20/250 surface; the minimax-leading UCBVI-BF route is absent.

  • Conditional variance
  • Freedman concentration
  • variance bonus summation
  • source-leading terminal
  • Named formalization leaf: UCBVI-BF-CONDITIONAL-VARIANCE
  • Named formalization leaf: UCBVI-BF-TOTAL-VARIANCE
  • Named formalization leaf: UCBVI-BF-TERMINAL