Contextual bandits

Everything about the contextual bandit in this repository is on this page: the idea, the index of files, the commands, the interface, what Z3 proves, the Haskell port, and the note for the video. The Z3 code itself stays in z3-scala/. Writing standard: ASD-STE100. Portuguese edition: README.pt-BR.md.

Contents

1. The idea
2. Files
3. Run
4. The interface
5. What Z3 proves
6. The Haskell port
7. Caveats
8. Note for the video
   • Scene map
   • Block 1. CMAB
   • Block 2. A/B test
   • Block 3. RSI
9. Sources

1. The idea

A system selects one option (an arm) for each request. It knows some data about the request (the context). It gets a reward for the selected arm only. The policy is the rule from context to arm. Regret is the reward of the best arm minus the reward of the selected arm, added for all rounds.

The bandit is a decision rule on top of a probabilistic model. The model turns history into beliefs. The decision rule turns beliefs into an action.

           context c
               │
               ▼
 history ─► RewardModel ──estimate(b, c, a) = (mean, width)──► DecisionRule ──► action a
   ▲        (belief b)    sample(b, c, a)  ~ posterior          greedy / ε-greedy /      │
   │                                                            UCB / Thompson           ▼
   └────────────── update(b, (c, a, r)) ◄────────────── reward r ◄──────────────── environment

The decision rule sees only the per-arm estimates, never the history or the context. Thus any model that gives a mean and an uncertainty works with any rule. policy_factors proves this boundary.

Figure 1. The model layer, the decision layer and the Z3 spec (archify; click for the interactive diagram).

2. Files

3. Run

just z3                                  # every Z3 statement (nix develop .#scala); each line OK
cd haskell && cabal run examples         # spec check, then 4 simulations; or: runghc -isrc app/Main.hs
cd haskell && cabal run video            # the video's experiments; writes the script's results.md
just liquid                              # LiquidHaskell; SAFE for each module
just agda                                # the Agda proofs for every K (nix develop .#agda)
just paper contextual-bandits            # the preprint (inside nix develop)
just script                              # the video script, pt-BR

The first block of cabal run examples is the spec check against Examples.scala and Video.scala. Each line must say OK.

4. The interface

5. What Z3 proves

Each statement is checked by refutation (unsat) for K = 1 to 5 arms and all real estimates.

ucb_gap says what the model owes the decision layer: calibrated uncertainty. A LinUCB regret bound needs ucb_gap in each round (done), calibration with probability ≥ 1 − δ for all rounds (a martingale bound, outside what Z3 decides), and Σ widths = O(√(d T log T)) (the elliptical potential lemma). The last two are open.

Agda proves the decision-layer rows of this table (greedy_valid to policy_factors) for every K, by induction, over exact rationals: agda/README.md. Z3 stays the specification; the Agda names are the Z3 names with - for _.

6. The Haskell port

The port uses only base and containers, and mirrors the Z3 names. Argmax keeps the first maximum, as in Z3. To connect a model, give four functions, or wrap a model with fromPredictor:

fromPredictor
  :: Int                                   -- number of arms
  -> s                                     -- model state (weights, handle, ...)
  -> (s -> Obs c -> s)                     -- online update; `const` if frozen
  -> (s -> c -> Arm -> (Double, Double))   -- predictive (mean, std)
  -> RewardModel c s

• Closed form (Beta-Bernoulli, Gaussian, Bayesian linear regression): update is the posterior update, estimate the posterior mean and std (betaBernoulli, bayesLinear in Models.hs).
• Trained offline (logistic regression, gradient boosting, an ensemble): freeze it with const and retrain in batches outside the loop.
• Any rule: act m greedy, act m (epsGreedy 0.1), act m (ucb 2), thompsonArm m.

The width must be an honest uncertainty. An over-confident model breaks the calibrated premise, and UCB and Thompson become greedy.

Output of cabal run examples (expected cumulative regret, one small simulation each, not a benchmark):

== 0. Spec check against Examples.scala and Video.scala ==   all OK
== 1. Beta-Bernoulli, 2 contexts x 3 arms, T=5000 (avg 20 runs)
greedy 41.1   eps-greedy 0.1 43.3   UCB beta=2 25.3   Thompson 32.8
== 2. Bayesian linear, d=3, 4 arms, T=2000 (avg 10 runs)
greedy 322.9  eps-greedy 0.1 62.0   LinUCB 25.3       LinTS 31.5

LiquidHaskell checks refinement types on ContextualBandit.hs and Models.hs: argmax returns an index in range, each rule returns probabilities in [0, 1], and Beta-Bernoulli keeps its counts at 1 or more. LIQUIDHASKELL.md lists what it trusts and what it does not cover.

7. Caveats

• Z3 proves over the reals and exact rationals. Haskell uses Double, so the proofs do not cover floating-point rounding. The spec check shows that the two agree on the shared example.
• Z3 has no induction: each theorem is checked for K = 1 to 5, not for all K.
• Thompson sampling is "greedy on a posterior sample". Its randomness and its regret are not formalised.
• The tabular example uses width 1/(n+1), a rational stand-in for 1/√n, so that the examples stay exact.

8. Note for the video

The video has three blocks of 10 minutes: CMAB, A/B test and RSI. Each heading gives its scene in the script. The numbers come from results.md, which cabal run video writes. The final style of the video is the script's (Manim, dark background, blue for the belief, yellow for the selection, red for the regret); the archify figures give the structure.

Scene map

Figures are in docs/diagrams/img/en/<name>.png and, interactive, in docs/diagrams/en/<name>.html. Desmos files are in script/desmos/. Every scene has a Manim take in script/animation/; just takes renders them.

Block 1. CMAB

Time in the video: 0:00 to 10:00.

1.1 Hook. The agent has a belief: option 0 is good in 67 % of the rounds, option 1 in 50 %. Then 4 positive signals for option 1 and 2 negative signals for option 0 come in. The new belief is 0.57 and 0.62, and the selection changes to option 1. The agent changes because of evidence.

Figure 2. One round: decide, act, learn. Scenes 1.1, 2.5 and 3.4.

1.2 Timeline. The script calls it steal like an artist, after the 2012 book by Austin Kleon.

The script checked the sources for 1952, 2012, globo.com and 2026 (REFERENCES.md). This note did not open them again. The friend of 2018 is not in the figure: the script still marks the name and month [a confirmar].

Figure 3. The timeline of scene 1.2. Dates are correct to the year or the month; archify shows day 1.

1.3 π and you. You are the reward. With one arm (the Leibniz series), the agent either shows π(N) again (exploit) or calculates one more term (explore). You grade the distance to π from 0 to 1. In 20 rounds with ε = 0.2, the agent exploited 9 times (mean grade 0.14), explored 11 times (mean grade 0.76) and stopped at π(12). With three arms, Gauss-Legendre doubles the digits at each step (3, 8, 19, 41) and Ramanujan gets 7 digits with 1 term and 48 with 6. The agent pulled Ramanujan 16 times, Gauss-Legendre 3 and Leibniz 1. Both have grade 1.00; greedy keeps the first maximum. The π example has no context, so it is a MAB, not a CMAB.

Figure 4. The π loop. Scenes 1.3 and 1.4.

1.4 The name. B for bandit (a slot machine is a "one-armed bandit"); M and A for multi-armed (many levers, each with an unknown mean prize); C for contextual (before the pull, the agent sees one data item, for example morning or night). With context, the best lever changes in each round and the policy learns a function from context to lever: linear in LinUCB [6], a table of two rows in the ice-cream shop.

1.5 and 1.6. See the idea: the two layers, policy_factors, and the rules table. The video's model is tabular: mean = sum / count, width = 1/(n+1). With β = 0, UCB is greedy (ucb_zero).

1.7 Netflix. Netflix selects the image that it shows for each title and member, as the Netflix Tech Blog post of December 2017 by Chandrashekar, Amat, Basilico and Jebara describes [1, 2]. In a 2018 keynote, Jebara gave these data [3]: the context is the viewing history and the country; the arm is the image; the reward is a play; the system uses online learning and contextual bandits; it gets about 20 million image requests per second at peak; the team uses replay to evaluate a new policy offline. At this scale the model must generalize, as bayesLinear does (mean = context · arm weights). The primary sources are from 2017 and 2018. This note found no primary source for the status in 2026: do not state that Netflix uses bandits today.

Block 2. A/B test

Time in the video: 10:00 to 20:00.

2.1 and 2.2. An A/B/n test sends each user to one of K variants at random, then commits to the best ("explore-then-commit"). It is simple to set up, read and defend. In bandit terms:

1. The test period is ε-greedy with ε = 1 (epsGreedy_one_is_ab_test).
2. The decision phase is ε-greedy with ε = 0, greedy (epsGreedy_zero).
3. The full test is an ε that changes from 1 to 0 on a fixed day (R3: etc_before, etc_after).

The question "A/B or bandit?" becomes: how must ε decrease over time?

Figure 5. The A/B test and the bandit loop. Scenes 2.1, 2.2 and 2.4.

2.3 and 2.4. The cost of the wait. An ice-cream shop: three flavours, two contexts (morning and night), 5,000 customers, the mean of 20 seeds. The A/B test uses half of the customers to split.

The bandit sends more traffic to the arms that look better during the test. Jebara calls "collect data for months, train, then test" "a massive amount of regret" [3]. One A/B test for each user segment is a special case of a contextual bandit.

2.5 What the A/B test does better. A fixed random allocation gives an unbiased estimate of the effect. A bandit changes the allocation, so a simple mean of its logs is biased. Record the probability of each selection (policy gives the full distribution) and use replay or inverse propensity weighting (IPW). Netflix used an A/B test to approve the artwork system before the rollout [3]: the bandit replaced the slow loop inside the A/B test, not the test.

2.6 Summary. An A/B test is one policy: no context, fixed uniform allocation, one decision at the end. A contextual bandit removes these three limits. In production, from the sources:

• Netflix homepage billboard: a 2018 talk by Jaya Kawale and Elliot Chow describes a bandit framework with ε-greedy, offline replay and online A/B tests, because batch models adapt too slowly to the catalog [4, 5].
• globo.com: the service selects a photo and the position of an advertisement [9].

Rule of thumb: an A/B test for one decision that you must defend; a bandit for a decision that occurs thousands of times each day at a low cost per error; the two together when you can.

Block 3. RSI

Time in the video: 20:00 to 30:00.

3.1 Three words.

Anthropic defines RSI as a system that "could fully autonomously design and develop its successor" [11].

3.2 The smallest recursive loop. The inner agent is the ice-cream shop's ε-greedy. The outer agent is a second bandit whose arms are values of ε. In each of 200 episodes it selects an ε, the inner agent serves 500 customers, and the mean gain is the outer reward.

The same epsGreedy works at the two levels (R4: rsi_valid, outer_explores). ε = 0.5 wins because the horizon is short and the model starts from zero.

Figure 6. The outer loop selects the ε of the inner loop. Scenes 3.1 to 3.3.

3.3 Real RSI. The SIA paper (2026) describes a "Feedback-Agent" that selects between edits to the scaffold, prompts and tools, and updates to the weights, with a deterministic evaluator as the reward [12]: a bandit. The script read SIA through a review, not the PDF. Anthropic reports a training-code speed-up from about 3 times (May 2025) to about 52 times (April 2026), and an automatic code review that would have found about one third of the errors behind past incidents [11].

3.4 Current belief against new belief. Beta-Bernoulli keeps two counts per option, successes and failures; each signal adds 1 to one count. The new belief adds the new signals to the old ones (0.67 and 0.50 become 0.57 and 0.62, scene 1.1), and the width decreases for both arms.

3.5 What is not a bandit. When the selection of today changes the state of tomorrow, the problem is full reinforcement learning. If it is easy to deceive the reward, the loop learns to deceive it: ucb_gap needs the premise calibrated. The script cites no specific work on reward hacking.

9. Sources

1. Netflix Tech Blog, "Artwork Personalization at Netflix", 2017-12. https://netflixtechblog.com/artwork-personalization-c589f074ad76 (this note read a summary, not the full text)
2. Dezeen, "Netflix targets different film artworks to suit users' viewing habits", 2017-12-20. https://www.dezeen.com/2017/12/20/netflix-targets-film-artwork-depending-users-viewing-habits-design-technology/
3. Tony Jebara, "Artwork Personalization at Netflix", keynote, 2018. https://www.aicouncil.com/talks/artwork-personalization-at-netflix
4. Jaya Kawale and Elliot Chow, "A Multi-Armed Bandit Framework for Recommendations at Netflix", 2018. https://aicouncil.com/a-multi-armed-bandit-framework-for-recommendations-at-netflix
5. Slides of [4]. https://www.slideshare.net/slideshow/a-multiarmed-bandit-framework-for-recommendations-at-netflix/102629078
6. Li, Chu, Langford, Schapire, "A Contextual-Bandit Approach to Personalized News Article Recommendation" (LinUCB), 2010. https://arxiv.org/abs/1003.0146
7. Lattimore and Szepesvári, Bandit Algorithms, Cambridge University Press, 2020.
8. The video script and the record of its sources: script/, refs.bib, REFERENCES.md.
9. Tiago Motta, post about the bandit service of globo.com, 2024-09-28. Key motta2024bandit in [8].
10. Renan Moreira de Oliveira, "Machine Learning na globo.com", slides, 2018. Key oliveira2018globo in [8].
11. Anthropic, "When AI builds itself", 2026. Key anthropic2026builds in [8].
12. A review of the SIA paper (arXiv 2605.27276), 2026. Key bhavsar2026sia in [8]; status partial.