Graded monad prototype - #10
Closed
paulorauber wants to merge 37 commits into
Closed
paulorauber wants to merge 37 commits into
paulorauber wants to merge 37 commits into
Conversation
Brings the trace semantics for rdo programs (`rdo_trace`, `rdo_peel`, `record`), `transfer`, `extend_space` and `alg_env_trace`. The tactic files moved to `RandomDo/Tactic/IsMarkov/` on this side, so the imports of the incoming files are updated to the new paths. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
`lake update LeanMachineLearning` moves LML to dde3322, and Mathlib to 217ba06 with it. LML's rounds now have an observation before the action: `Algorithm 𝓞 𝓐 𝓨`, `Environment 𝓞 𝓐 𝓨`, `IsAlgEnvSeq O A Y alg env P`, with histories `Hist 𝓞 𝓐 𝓨 n = Fin n → Round 𝓞 𝓐 𝓨` and the action at step `n` drawn given the history and the observation `O n`. `AlgTrace` and `alg_env_trace` are ported to it. The first action is now the policy at the empty history, so the separate `K0`/`out0` fields of `AlgTrace` and the step-zero lemmas go: `hasCondDistrib_trace` and `action_ae_eq` hold uniformly in `n`, and the tactic introduces `Ω P O A Y T hseq htr hT hA`. The toy bandit of `Test/AlgTrace.lean` is an `Algorithm Unit (Fin K) ℝ`. Mathlib's `Measure.map` along a non-measurable function is now a Dirac mass, so `IsProbabilityMeasure (μ.map f)` is an instance (`isProbabilityMeasure_map` is gone) and `Measure.bind_smul` asks for measurability; `measurable_pi_lambda` is now `Measurable.of_eval`. An `extend_space` error test relied on `P.map Y` not being known to be a probability measure, and now uses `μ + μ`. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
ε-greedy's policy is an rdo program drawing a coin of bias ε and a uniform arm. With `rdo_trace` and `alg_env_trace`, its draws give that every arm is pulled with probability at least ε / K at every round (`le_map_action`), hence a linear lower bound on the regret (`le_integral_regret`). The bandit programs gain a randomized step, `banditStepRand` and `banditRunRand`, where the arm is itself a program, and `banditRunRand_eq_map` extends the law of the program to it, so that the lower bound holds for the program that runs (`le_integral_regret_banditRunRand`). The greedy arm pulls the arms never pulled first, so that it never compares undefined means. `lake exe bandits` runs ε-greedy with ε = 0.1, and `scripts/bandit_plot.py` replays it with numpy and draws its regret against the lower bound. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
`lake exe mk_all --check` wants the root files of `MetropolisHastings` and `Bandits` to be the import lists it generates. They carried a docstring, and the executables `MetropolisHastings/Main.lean` and `Bandits/Main.lean`, being in the library directories, were picked up as modules of the libraries. The executables move to the top level, as `RunMetropolisHastings.lean` and `RunBandits.lean`, like the other executables of the repository; the root files are regenerated by `mk_all`, and their overview moves to the docstrings of `MetropolisHastings.Defs` and `Bandits.Defs`. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
`MetropolisHastings` and `Bandits` become default targets, so that `lake build` and `lake lint`, and hence CI, build and lint them along with `RandomDo`. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ib/ForLML pseudoRegret takes the reward kernel, as LML's regret does, and the ETC, UCB and ε-greedy bounds are stated with LML's gap, replacing gapOf. General lemmas move out of Bandits.Theory into files mirroring their upstream homes, generalized where the statement allows: RandomDo/ForMathlib (map_compProd_eq_bind, bind_map, Measurable.finSnoc, hasSubgaussianMGF_gaussianReal) and RandomDo/ForLML (pullCount'_snoc, sumRewards'_snoc, IT.hist_succ_eq_snoc, IT.map_hist_succ). The Vector measurability lemmas join RandomDo.Measurable. Duplicates are removed: RDo.map_compProd and RDo.bind_map of Trace.lean are now the ForMathlib lemmas, and LML's Measure.dirac_compProd replaces dirac_compProd_eq_map. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Collaborator
Author
|
I am now quite convinced that this is not a promising approach - I will explain in our next meeting. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.