Reinforcement Learning

Completed

Machine Learning Statistics·Captain: mikedeng1

The Statistical Complexity of Interactive Decision Making IV: Log-Loss Regret Controls Hellinger Estimation Error, Est_H ≤ Reg_KL + 2 log(1/δ) with Probability 1−δResearch Paper

Motivation

Interactive decision methods often need an estimate of an unknown outcome law after each round. A learner can be good at decisions only if its model of the observations is accurate where future decisions will sample. Foster, Kakade, Qian and Rakhlin measure this accuracy by a cumulative squared Hellinger distance and use it in their regret bounds for decision making with structured observations. They connect that estimation quantity to online log-loss regret, a standard objective for sequential probability prediction. The connection lets a regret guarantee for a density predictor supply the estimation guarantee needed by a decision method. Foster et al., Appendix A.3 and §4.1.1.

This mission isolates the online estimation result, Lemma A.14, from the rest of the paper. It addresses a learner that predicts a conditional outcome distribution before the next covariate and outcome are revealed. The covariates may respond to the entire preceding history. This matters in interactive decision making, where the learner's earlier choices change what it observes next. Foster et al., pp. 75–76.

Setting

There are $T$ rounds. At round $t$ , the learner has a history $H_{<t}=((x_s,y_s))_{s<t}$ of past covariates and outcomes. It predicts a probability distribution $\widehat g_t(\cdot\mid x;H_{<t})$ for every possible next covariate $x$ . Nature draws $x_t$ from a history-dependent distribution $c_t(\cdot\mid H_{<t})$ , then draws $y_t$ from the conditional law of a distinguished true expert $i^\star$ . An expert class indexed by $I$ supplies laws $g_{i,t}(\cdot\mid x;H_{<t})$ ; realizability means $g_{i^\star,t}$ is the actual outcome law at every round. The prediction $\widehat g_t$ is selected from the past history, before $x_t$ is observed. Foster et al., Assumption A.1, p. 76.

For a predicted distribution $q$ , the log loss on observation $y$ is $-\log q(y)$ . The learner's log-loss regret $\mathrm{Reg}_{\mathrm{KL}}$ is its cumulative log loss minus the smallest cumulative loss of an expert in $I$ . This is a realized quantity: both sums use the covariates and outcomes that actually occurred. The squared Hellinger distance is

D_{\mathrm H}^2(P,Q)=\sum_y\bigl(\sqrt{P(y)}-\sqrt{Q(y)}\bigr)^2.

The Hellinger estimation error $\mathrm{Est}_{\mathrm H}$ is different from a sum evaluated only at realized covariates. At each round it averages $D_{\mathrm H}^2(\widehat g_t(\cdot\mid x),g_{i^\star,t}(\cdot\mid x))$ over the conditional law of the next covariate $x$ , given $H_{<t}$ , then sums these conditional errors. Thus the error measures prediction quality in the distribution the learner is about to face. Foster et al., (99)–(100), pp. 75–76.

Formalization targets

Main high-probability bound

The main target is Lemma A.14 (102): for every $\delta\in(0,1)$ ,

\Pr\!\left\{\mathrm{Est}_{\mathrm H} \le \mathrm{Reg}_{\mathrm{KL}}+2\log(1/\delta)\right\}\ge 1-\delta.

The coefficient $2$ and the absence of a factor $1/2$ in $D_{\mathrm H}^2$ are part of the claim. The probability is under the complete history law generated by the adaptive covariate process and the true expert. Foster et al., Lemma A.14, p. 76.

Supporting results

The first milestone is Lemma A.4, an anytime conditional exponential-moment bound. It controls one event on which an adapted inequality fails at any horizon through $T$ , without replacing it by a single fixed-horizon claim. The second milestone is the affinity identity used in the proof of Lemma A.14:

\sum_y\sqrt{P(y)Q(y)}=1-\tfrac12D_{\mathrm H}^2(P,Q).

The proposal also states the expectation clause $\mathbb E[\mathrm{Est}_{\mathrm H}]\le\mathbb E[\mathrm{Reg}_{\mathrm{KL}}]$ from (101) and the predictable-mask clause (103), which bounds error accumulated only on rounds selected from the past. Foster et al., pp. 70, 76, 79.

Significance

The high-probability bound lets an online density estimator serve as an estimation oracle for the paper's interactive decision bounds. A user can choose a predictor because it has a log-loss regret guarantee, then obtain control of Hellinger estimation error under adaptive observations. The expectation clause supplies the corresponding average guarantee. The masked clause handles applications that evaluate accuracy only on rounds selected before the current observation. Foster et al., Proposition 4.1 and Lemma A.14.

The result is already proved in the source paper. This mission asks for machine-checked proofs of the finite-alphabet statements and a reusable interface for sequential probability kernels, conditional error and log-loss regret. The published FoundationsRL Hellinger definition supplies the same normalization used by the paper; the mission does not propose a new distance. These items have no machine-checked proof in this proposal yet. The source also gives Vovk's aggregation guarantee for finite expert classes, but that algorithmic bound is outside the current item list. Foster et al., Lemma A.15, p. 76.

Difficulty

The quantity to be bounded is conditional on the past. A pathwise distance at the observed $x_t$ is a different random quantity and does not give (102). Adaptive covariates add another dependence on history, while the learner must choose its prediction before seeing $x_t$ . A fixed covariate law would therefore omit a central feature of the theorem. The anytime milestone likewise concerns all prefixes of one process at once; separate claims at each fixed horizon do not preserve its statement. Foster et al., pp. 70, 75–79.

The log-loss formula also has a boundary. A zero predicted probability gives infinite loss in the paper, whereas Lean's real logarithm returns a finite default at zero. The formal statements must keep that default from affecting a positive-probability observation. Squared Hellinger distance has its own normalization convention, so the affinity identity checks the factor needed in the high-probability constant.

Formalization scope

The paper uses measurable covariate and outcome spaces and regular conditional densities. This mission specializes to finite covariates $X$ , finite outcomes $Y$ , and a finite nonempty expert class $I$ . Each kernel is represented by a nonnegative vector summing to one. Complete histories are finite sequences, and the probability of a history is the product of its covariate and true-expert outcome probabilities. Expectations and event probabilities are finite sums. Time is indexed from zero; round $t$ in Lean corresponds to round $t+1$ in the paper.

The learner, experts and covariate kernel may all depend on preceding history. The learner and experts predict a law for every possible covariate while seeing only that history. A Boolean mask for (103) has the same information restriction. The Hellinger error sums conditional averages over the next covariate, and the probability guarantee is expressed as a bound on the total mass of histories where the displayed inequality fails.

The real-valued log loss requires one additional condition: on every complete history of positive probability, the learner and every expert give the observed outcome positive probability at every round. The condition is imposed only where the history law has support. It excludes Lean's default value for $\log 0$ ; it is a scope restriction from the paper's extended-valued formulation. A normalized history law and a distinguished true expert are explicit, so the probability statement cannot be discharged by an empty event space or an unnormalized zero law. The sequential-kernel definitions can be reused in other finite online learning results, and the probability, affinity, expectation and masked bounds are separate proof targets.

Selected references

Dylan J. Foster, Sham M. Kakade, Jian Qian, Alexander Rakhlin, The Statistical Complexity of Interactive Decision Making, arXiv preprint arXiv:2112.13487v3, 2023. arXiv.

8 thms2 active usersReviewed

Bandit Algorithms Machine Learning·Captain: mikedeng1

The Statistical Complexity of Interactive Decision Making V: The Multi-Armed Bandit Has Localized DEC at Least 2⁻⁶·A/γ, via Hard Families of ModelsResearch Paper

Motivation

The Decision-Estimation Coefficient (DEC) of Foster, Kakade, Qian and Rakhlin (arXiv:2112.13487) is a single complexity measure that bounds the minimax regret of interactive decision making (bandits, reinforcement learning, and their structured variants) from above and from below. Its lower bound (Theorem 3.2 of the paper) states that every algorithm suffers expected regret at least a constant times $\mathsf{dec}_\gamma(\mathcal{M}^\infty_{\varepsilon_\gamma}(\overline{M}), \overline{M}) \cdot T$ , so concrete lower bounds on regret follow from concrete lower bounds on the DEC of localized model classes.

The multi-armed bandit is the first test of this program. Its minimax regret $\Theta(\sqrt{AT})$ is classical (Auer et al., 2002; Audibert and Bubeck, 2010). Section 5.1 of the paper recovers it through the DEC: posterior sampling (Proposition 5.1) and inverse gap weighting (Proposition 5.2) bound the DEC by $A/\gamma$ from above, and Proposition 5.3 bounds it by $2^{-6} A/\gamma$ from below. The lower bound is proved through a hard family of models (Definition 5.1, Lemma 5.1), the device that the paper reuses for linear, ReLU and gap-dependent lower bounds in §§6–7.

Setting

A decision space $\Pi$ is a finite set; here $\Pi = [A] = \{1, \dots, A\}$ , the arms. A model $M$ assigns to every arm $\pi$ a distribution $M(\pi)$ over rewards in $\mathcal{R} = [0,1]$ (observations are trivial). Its mean reward is $f^M(\pi) = \mathbb{E}_{r \sim M(\pi)}[r]$ , and $\pi_M \in \arg\max_\pi f^M(\pi)$ is an optimal arm. The squared Hellinger distance between distributions $P, Q$ on a finite set is $D^2_{\mathrm{H}}(P, Q) = \sum_y (\sqrt{P(y)} - \sqrt{Q(y)})^2$ (no factor $\tfrac12$ , the paper's (5)).

For a class $\mathcal{M}$ of models, a reference model $\overline{M}$ and $\gamma > 0$ , the DEC (2) is

\mathsf{dec}_\gamma(\mathcal{M}, \overline{M}) = \inf_{p \in \Delta(\Pi)} \sup_{M \in \mathcal{M}} \mathbb{E}_{\pi \sim p}\Bigl[ f^M(\pi_M) - f^M(\pi) - \gamma \cdot D^2_{\mathrm{H}}\bigl(M(\pi), \overline{M}(\pi)\bigr) \Bigr].

With $g^M(\pi) = f^M(\pi_M) - f^M(\pi)$ , the $L_\infty$ -localized class (12) is $\mathcal{M}^\infty_\varepsilon(\overline{M}) = \{ M \in \mathcal{M} : |g^M(\pi) - g^{\overline{M}}(\pi)| \le \varepsilon\ \forall \pi \}$ .

A reference model $\overline{M} \in \mathcal M$ and models $M_1, \dots, M_N \in \mathcal M$ , $N \ge 2$ , form an $(\alpha, \beta, \delta)$ -family (Definition 5.1) if there are $u_i, v_i : \Pi \to [0,1]$ with $\sum_i u_i(\pi) \le N/2$ , $\sum_i v_i(\pi) \le 1$ , $f^{M_i}(\pi_{M_i}) - f^{M_i}(\pi) \ge \alpha(1 - u_i(\pi))$ and $D^2_{\mathrm{H}}(M_i(\pi), \overline{M}(\pi)) \le \beta v_i(\pi) + \delta$ . $\mathrm{Ber}(q)$ is the Bernoulli distribution with mean $q$ .

Formalization targets

Goal: Proposition 5.3

For $A \ge 2$ arms, $\overline{M}(\pi) = \mathrm{Ber}(\tfrac12)$ and every $\gamma \ge A/3$ , with $\varepsilon_\gamma = \frac{A}{12\gamma}$ ,

\mathsf{dec}_\gamma\bigl(\mathcal{M}^\infty_{\varepsilon_\gamma}(\overline{M}), \overline{M}\bigr) \ge 2^{-6} \cdot \frac{A}{\gamma}.

Milestones

Lemma A.7: $D^2_{\mathrm{H}}(\mathrm{Ber}(p), \mathrm{Ber}(q)) \le (p-q)^2\bigl(\frac{1}{p+q} + \frac{1}{2-p-q}\bigr)$ , and in particular $D^2_{\mathrm{H}}(\mathrm{Ber}(\tfrac12 + \Delta), \mathrm{Ber}(\tfrac12)) \le 3\Delta^2$ for $\Delta \in (0, \tfrac12)$ .
Lemma 5.1: an $(\alpha, \beta, \delta)$ -family $\mathcal{M}'$ with $\beta \ge 0$ satisfies $\mathsf{dec}_\gamma(\mathcal{M}', \overline{M}) \ge \frac{\alpha}{2} - \gamma(\frac{\beta}{N} + \delta)$ for all $\gamma > 0$ .
The hard family of the proof: $M_i(\pi) = \mathrm{Ber}(\tfrac12 + \Delta\,\mathbb{I}\{\pi = i\})$ is a $(\Delta, 3\Delta^2, 0)$ -family around $\mathrm{Ber}(\tfrac12)$ .
Localization: this family lies in $\mathcal{M}^\infty_\Delta(\overline{M})$ .

Companions

The mission also states monotonicity of the DEC in the class (the step from the family to the localized class), Proposition 5.1 (posterior sampling bounds the dual square-loss DEC by $A/\gamma$ ), and Proposition 6.7, the gap-dependent variant: for bandits with gap exactly $\Delta \in (0, \tfrac18)$ , some $\overline{M}$ in the class has $\mathsf{dec}_\gamma(\mathcal{M}^\infty_\Delta(\overline{M}), \overline{M}) \ge \frac{\Delta}{4}\mathbb{I}\{\gamma \le \frac{A}{48\Delta}\}$ . Proposition 5.2 (inverse gap weighting) and the decoupling step of Proposition 5.1 are already proved on the platform and are included as references.

Significance

Proposition 5.3 is the DEC half of the $\Omega(\sqrt{AT})$ minimax lower bound for multi-armed bandits: combined with Theorem 3.2 and $\gamma \asymp \sqrt{AT}$ , it shows that the general DEC theory loses nothing in rate on the most basic interactive problem, and that the $A/\gamma$ upper bounds of Propositions 5.1 and 5.2 are tight up to constants. Lemma 5.1 is reusable: any lower bound on the DEC of a class can be obtained by exhibiting a hard family, and the paper uses it for linear bandits (Proposition 6.2), ReLU bandits (Proposition 6.6) and gap-dependent bounds (Propositions 6.7, 6.8).

The results are proved in the paper. As far as is known, none of them is machine-checked. A formal development provides a verified Bernoulli Hellinger bound, a reusable hard-family lemma for the DEC as published on the platform, and the first verified DEC lower bound for a concrete class.

Difficulty

The DEC is an inf-sup, so a lower bound must hold against every exploration distribution $p$ . A natural first attempt picks a single alternative model and compares; this fails because $p$ can concentrate on the arm where that alternative differs and then the Hellinger penalty cancels the regret. The family must be spread so that no single $p$ is good for all of its members at once, and the constants must balance the regret term against the information term at the chosen $\Delta$ . In Lean, an additional difficulty is that the DEC is written with real sInf/sSup, which are $0$ on empty or unbounded sets: every lower bound requires showing that the relevant sets are nonempty and bounded, and passing from the family to the localized class needs monotonicity of the DEC, which the paper uses without comment.

Formalization scope

Finite alphabets. The paper works over measurable spaces; this mission formalizes the finite-alphabet case, as the published FoundationsRL layer does. A model is m : S → Y → ℝ with every m π a probability vector; expectations are finite sums. The DEC is the published FoundationsRL.GeneralDM.decGf, the Hellinger distance hellingerSq, the mean reward fM.
Bernoulli subclass. The bandit class is the Bernoulli bandits (Y = Bool, reward $1$ on true), a subclass of the paper's all-distributions-on- $[0,1]$ class. The DEC is monotone in the class and the localized class shrinks with the class, so the Bernoulli lower bounds imply the paper's.
Optimal-arm selector. $\pi_M$ is a parameter piStar with the hypothesis that it picks a maximizer of $f^M$ ; every statement holds for every such selector, so for whichever maximizer the paper meant (the reference $\mathrm{Ber}(\tfrac12)$ has every arm optimal).
Added or dropped hypotheses. Lemma 5.1 makes the page's nonempty decision space explicit; its optimal-arm selector also implies nonemptiness. It adds $\beta \ge 0$ , necessary for the printed averaging argument: without it, even identical models can contradict (52). The family definition includes membership of the reference and family models in a probability-model class. The localization claim inherits $A \ge 2$ from Proposition 5.3. Proposition 6.7 states $A \ge 2$ , implicit on the page since a gap needs two arms. Proposition 5.1 represents models by their mean vectors and priors as finitely supported (footnote 5).
Constants. All constants are the page's: $2^{-6}$ , $A/(12\gamma)$ , $\gamma \ge A/3$ , $3\Delta^2$ , $5\Delta^2$ , $\Delta/4$ , $A/(48\Delta)$ . The page's proof of Proposition 6.7 names a $(\Delta, 5\Delta^2, 0)$ -family but computes with $12\Delta^2$ ; the stated proposition is the one its arithmetic supports.
No trivialization. A formalization in which the localized class could be empty, or the payoffs unbounded, would make decGf evaluate to the junk value $0$ ; the goal is stated over a class containing $\overline{M}$ with bounded rewards, so the inequality is the genuine one, and its right side $2^{-6} A/\gamma$ is strictly positive.

Contributions welcome: proofs of the milestones in attack order, sorry-free lemmas on nonemptiness and boundedness of the DEC's inner sets (reusable for every DEC lower bound in this series), and a proof of the gap-dependent companion.

Selected references

D. J. Foster, S. M. Kakade, J. Qian, A. Rakhlin, The Statistical Complexity of Interactive Decision Making, arXiv preprint, 2021 (v3, 2023). https://arxiv.org/abs/2112.13487
D. J. Foster, A. Rakhlin, Foundations of Reinforcement Learning and Interactive Decision Making, lecture notes, 2023. https://arxiv.org/abs/2312.16730
P. Auer, N. Cesa-Bianchi, Y. Freund, R. E. Schapire, The Nonstochastic Multiarmed Bandit Problem, SIAM Journal on Computing 32(1), 2002. https://doi.org/10.1137/S0097539701398375
J.-Y. Audibert, S. Bubeck, Regret Bounds and Minimax Policies under Partial Monitoring, Journal of Machine Learning Research 11, 2010. https://www.jmlr.org/papers/v11/audibert10a.html
D. J. Foster, A. Rakhlin, Beyond UCB: Optimal and Efficient Contextual Bandits with Regression Oracles, ICML, 2020. https://arxiv.org/abs/2002.04926

13 thms2 active usersReviewed

Dynamic Programming Machine Learning·Captain: mikedeng1

On the Sample Complexity of Reinforcement Learning III: Non-Stationary Approximate Policy Iteration Is Within 2T Times the Regression Error Averaged over Any Competitor's State-Time DistributionTextbook

Motivation

Approximate dynamic programming replaces the exact value functions of a Markov decision process by approximations, typically produced by a regression algorithm. The classical guarantees for the resulting policies are stated in the max norm: if every state-action value is estimated to within $\varepsilon$ uniformly over the state space, the greedy policy loses at most a multiple of $\varepsilon$ (Williams and Baird 1993; Bertsekas and Tsitsiklis 1996). Regression algorithms, however, control an average error under the distribution on which they are trained, not a worst-case error, so these guarantees rarely apply to the approximations actually computed.

Chapter 5 of S. M. Kakade's PhD thesis (On the Sample Complexity of Reinforcement Learning, UCL 2003, pp. 57–66) identifies the distribution under which the error of an approximate policy iteration algorithm should be measured. For the finite-horizon, non-stationary approximate policy iteration algorithm (NAPI), the loss relative to any competitor policy is bounded by twice the horizon times the regression error averaged under the future state-time distribution of that competitor. Taking the competitor optimal, the relevant "test" distribution is the one visited by an optimal policy, generally not the distribution on which the regressor was trained; the thesis calls this the "mismeasure" of reinforcement learning. The key tool, the performance difference lemma, was proved for the discounted case by Kakade and Langford (ICML 2002) and is used throughout the conservative policy iteration and policy search literature.

Setting

A $T$ -epoch MDP has a finite state set $S$ , a finite nonempty action set $A$ , decision epochs $t\in\{0,\dots,T-1\}$ , a transition kernel $P(s'\mid s,a)$ and a deterministic reward $r(s,a)\in[0,1]$ . A policy $\pi$ is a sequence of decision rules $\pi(\cdot\mid s,t)$ , distributions on $A$ ; it may be stochastic and non-stationary. A deterministic policy $h$ chooses the action $h(s,t)$ .

Values are normalized. The $t$ -value is $V_{\pi,t}(s)=\frac1T\mathbb E\big[\sum_{\tau=t}^{T-1}r(s_\tau,a_\tau)\mid s_t=s\big]$ , so $V_{\pi,t}=0$ for $t\ge T$ and

V_{\pi,t}(s)=\sum_a\pi(a\mid s,t)\Big(\tfrac1T r(s,a)+\sum_{s'}P(s'\mid s,a)V_{\pi,t+1}(s')\Big),\qquad V_\pi=V_{\pi,0}.

The state-action value is $Q_{\pi,t}(s,a)=\frac1T r(s,a)+\mathbb E_{s'\sim P(\cdot\mid s,a)}V_{\pi,t+1}(s')$ , the advantage is $A_{\pi,t}=Q_{\pi,t}-V_{\pi,t}$ , and the optimal value is $V^*(s)=\sup_\pi V_\pi(s)$ . The future state-time distribution of $\pi$ from $s_0$ is

d_{\pi,s_0}(s,t)=\tfrac1T\Pr(s_t=s\mid\pi,s_0)\quad\text{on } S\times\{0,\dots,T-1\}.

NAPI (Algorithm 6) starts from an arbitrary deterministic policy and updates its decision rules backwards, $t=T-1,\dots,0$ : at update $t$ a PolicyChooser receives the current policy $\pi$ and returns a decision rule $h_t$ , which replaces the rule at time $t$ . The output is $(h_0,\dots,h_{T-1})$ . With RegressionPolicyChooser (Algorithm 7), a regressor returns an approximation $\tilde Q_{\pi,t}$ of $Q_{\pi,t}$ and $h_t$ is greedy for it. The per state error and per state regression error at update $t$ are

\varepsilon_t(s)=\max_aQ_{\pi,t}(s,a)-Q_{\pi,t}(s,h_t(s)),\qquad \tilde\varepsilon_t(s)=\max_a|Q_{\pi,t}(s,a)-\tilde Q_{\pi,t}(s,a)|,

both measured against the input policy $\pi$ of update $t$ .

The discounted companions use the normalized discounted value $V_{\pi,\gamma}=(1-\gamma)\mathbb E[\sum_t\gamma^tr(s_t,a_t)]$ , its advantage $A_{\pi,\gamma}$ , and the Bellman error $B_J=\sup_{s,a}|Q_J(s,a)-J(s)|$ of a state vector $J$ , where $Q_J(s,a)=(1-\gamma)r(s,a)+\gamma\mathbb E_{s'}J(s')$ .

Formalization targets

Goal: Theorem 5.3.2 (p. 64)

For the policy $\pi$ returned by NAPI with RegressionPolicyChooser, every policy $\pi'$ and every state $s_0$ ,

V_\pi(s_0)\ \ge\ V_{\pi'}(s_0)-2T\,\mathbb E_{(s,t)\sim d_{\pi',s_0}}\big[\tilde\varepsilon_t(s)\big].

The regression outputs are arbitrary; the statement holds for every regressor and every tie-breaking rule.

Milestones

Lemma 5.2.1, undiscounted (p. 59): $V_{\pi'}(s_0)-V_\pi(s_0)=T\,\mathbb E_{(s,t)\sim d_{\pi',s_0}}\mathbb E_{a\sim\pi'(\cdot\mid s,t)}[A_{\pi,t}(s,a)]$ .
Lemma 5.3.1 (p. 63): for NAPI's output $\tilde\pi$ and the input policy $\pi$ of update $t$ , $Q_{\tilde\pi,t}=Q_{\pi,t}$ and $A_{\tilde\pi,t}(s,a)\le\varepsilon_t(s)$ .
Display in the proof of Theorem 5.3.2 (p. 64): $\varepsilon_t(s)\le2\tilde\varepsilon_t(s)$ when $h_t$ is greedy for $\tilde Q_{\pi,t}$ .
Corollary 5.2.2 (p. 61): $V_\pi(s_0)\ge V^*(s_0)-T\|A_{\pi,t}\|_\infty$ and $V_{\pi,\gamma}(s_0)\ge V^*_\gamma(s_0)-\frac{1}{1-\gamma}\|A_{\pi,\gamma}\|_\infty$ .
Theorem 5.1.3 (Williams–Baird, p. 59): a policy greedy for $Q_J$ satisfies $V_{\pi,\gamma}(s)\ge V^*_\gamma(s)-\frac{2B_J}{1-\gamma}$ .

The discounted half of Lemma 5.2.1 is already on the platform as ApproxOptRL.CPI.performance_difference and is referenced, not restated.

Significance

The goal replaces a max-norm hypothesis by an average one, under an explicit distribution. Its consequences: the approximation error only matters on the state-time pairs an optimal (or any good) policy visits; a regressor trained under a distribution $\mu$ over state-times performs well when $\mu$ resembles the state-time distribution of a good policy; and only one factor of the horizon $T$ appears, against two factors of $1/(1-\gamma)$ in the max-norm bounds for discounted approximate value and policy iteration (Chapter 3 of the thesis). The same chain, Lemma 5.2.1 and Lemma 5.3.1, underlies the μ-policy search analysis of Chapter 6 and, in the discounted case, conservative policy iteration.

All statements are proved in the thesis; none of the finite-horizon ones is formalized on the platform. A related performance difference identity, FoundationsRL.RLBasics.performance_difference, is proved on the platform for episodic MDPs with layer-dependent kernels and unnormalized values, with roll-in by one policy; it is the same mathematics up to the $1/T$ normalization but a different object, and is not reused. The mission produces a reusable normalized $T$ -epoch layer (values, advantages, state-time distributions) and machine-checked proofs of the chapter's results.

Difficulty

The obvious approach to Theorem 5.3.2 compares $V_\pi$ with $V_{\pi'}$ through max-norm contraction arguments, as in the discounted analysis of Chapter 3; that route only yields a bound in terms of $\max_{s,t}\tilde\varepsilon_t(s)$ and loses the averaging under $d_{\pi',s_0}$ . The averaged bound needs an exact identity between value differences and advantages along the competitor's trajectory distribution, which for non-stationary stochastic competitors requires a careful telescoping over epochs of the state distribution recursion. The second difficulty is bookkeeping in the algorithm: the regression error at update $t$ is measured against the input policy of that update, whose decision rules at later times have already been replaced, while the bound concerns the returned policy; relating the two requires showing that later updates do not change $Q_{\cdot,t}$ .

Formalization scope

Model. S, A are Fintypes with decidable equality, A nonempty; P s a s' is $P(s'\mid s,a)$ with IsTransitionKernel P; rewards satisfy 0 ≤ r s a ≤ 1 in every statement (the thesis's standing assumption, p. 22). The thesis also allows infinite state spaces; here S is finite.
Epochs and normalization. Epochs are 0-based, $t\in\{0,\dots,T-1\}$ , with 0 < T. All values carry the factor $1/T$ (discounted: $1-\gamma$ ), and $d_{\pi,s_0}$ carries $1/T$ ; the constants $T$ and $2T$ are right only in this normalization.
Policies. A policy is ℕ → S → A → ℝ, valid when every rule at a time $t<T$ is a distribution. Deterministic policies ℕ → S → A enter through their indicator policies. $V^*$ is the supremum over the subtype of valid policies. Discounted statements use the published ApproxOptRL.Shared.Model; $V^*_\gamma$ is the value of an optimal stationary policy.
The NAPI run is an explicit recursion (napiPolicy): the policy after updates $T-1,\dots,t$ , so the input of update $t$ is the policy at stage $t+1$ and the output is the policy at stage $0$ . The printed loop "For $t=T-1,\dots,1$ " omits the update at $t=0$ , which would leave the time-0 rule random and make the theorem false; the loop here runs to $t=0$ , as in the proof and in Algorithms 8–9.
Ruled out. A "run" whose returned policy is unconstrained, or regression errors measured against the returned policy instead of the input policy of each update, would trivialize or alter the goal; both are excluded by the explicit recursion. That the two measurements agree is Lemma 5.3.1, a milestone, not a definition.
Maxima. Maxima over actions are Finset.sup'; $\|\cdot\|_\infty$ on state-action functions is Mathlib's sup norm on S → A → ℝ. $B_J$ is a single number, as printed in Definition 5.1.2.

Welcome contributions: proofs of the milestones, general lemmas about the $T$ -epoch layer (values in $[0,1]$ , normalization of $d_{\pi,s_0}$ , the path-expectation form of $V_{\pi,t}$ ), and links to the platform's discounted performance difference results.

Selected references

S. M. Kakade, On the Sample Complexity of Reinforcement Learning, PhD thesis, Gatsby Computational Neuroscience Unit, University College London, 2003. https://discovery.ucl.ac.uk/id/eprint/10100726/
S. Kakade and J. Langford, Approximately Optimal Approximate Reinforcement Learning, ICML 2002. https://dl.acm.org/doi/10.5555/645531.656005
R. J. Williams and L. C. Baird, Tight Performance Bounds on Greedy Policies Based on Imperfect Value Functions, Technical Report NU-CCS-93-14, Northeastern University, 1993.
D. P. Bertsekas and J. N. Tsitsiklis, Neuro-Dynamic Programming, Athena Scientific, 1996.
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

16 thms2 active usersReviewed

Dynamic Programming Machine Learning Optimization·Captain: mikedeng1

On the Sample Complexity of Reinforcement Learning V: Exact Conservative Policy Iteration Improves at Every Update and Halts within 8H²/ε² Updates with Future Advantages at Most ε/HTextbook

Motivation

Policy iteration replaces the current policy by the greedy policy with respect to its state-action values. With exact values this improves the policy at every state. When the improvement step is only approximate, or is restricted to a class of policies, a greedy replacement can make the policy worse, and the resulting error bounds are stated in max norm over all states, a quantity that sampling cannot control in large state spaces.

Conservative policy iteration (CPI), introduced by Kakade and Langford (ICML 2002) and developed in Chapter 7 of Kakade's PhD thesis (UCL, 2003), takes a different route. Instead of switching to a new policy, it mixes the current policy with a small amount of a better one, and it measures progress by an average over states visited under the current policy rather than by a maximum over all states. The thesis proves that the exact form of the algorithm improves its objective at every step, halts after a number of updates polynomial in the horizon and the accuracy, and returns a policy whose average advantages against an entire policy class are small. The approach underlies later trust-region and conservative update methods in reinforcement learning.

Setting

A finite Markov decision process has a finite state set $S$ , a finite action set $A$ , transition probabilities $P(s'\mid s,a)$ and a deterministic reward $r(s,a)\in[0,1]$ . A stationary policy $\pi$ chooses action $a$ in state $s$ with probability $\pi(a\mid s)$ . For a discount factor $0\le\gamma<1$ the normalized value of $\pi$ is

V_\pi(s)=(1-\gamma)\,\mathbb E\Big[\sum_{t\ge0}\gamma^t r(s_t,a_t)\,\Big|\,\pi,\ s_0=s\Big],

which lies in $[0,1]$ . The state-action value is $Q_\pi(s,a)=(1-\gamma)r(s,a)+\gamma\,\mathbb E_{s'\sim P(\cdot\mid s,a)}V_\pi(s')$ and the advantage is $A_\pi(s,a)=Q_\pi(s,a)-V_\pi(s)$ . The horizon time is $H=1/(1-\gamma)$ .

Fix a reset distribution $\mu$ on $S$ . The value of $\mu$ is $V_\pi(\mu)=\mathbb E_{s\sim\mu}V_\pi(s)$ . The discounted future state distribution is

d_{\pi,\mu}(s)=(1-\gamma)\sum_{t\ge0}\gamma^t\Pr(s_t=s\mid\pi,\ s_0\sim\mu),

and $d_{\pi,s_0}$ is the case where $\mu$ is the point mass at $s_0$ . For another policy $h$ :

the advantage under a distribution $\nu$ is $A_\pi(\nu,h)=\mathbb E_{s\sim\nu}\mathbb E_{a\sim h(\cdot\mid s)}A_\pi(s,a)$ ;
the future state-action value is $\mathbb Q_\pi(\mu,h)=\mathbb E_{s\sim d_{\pi,\mu}}\mathbb E_{a\sim h(\cdot\mid s)}Q_\pi(s,a)$ ;
the future advantage is $\mathbb A_\pi(\mu,h)=\mathbb E_{s\sim d_{\pi,\mu}}\mathbb E_{a\sim h(\cdot\mid s)}A_\pi(s,a)$ .

The conservative update with mixing weight $\alpha\in[0,1]$ is $\pi_{\rm new}=(1-\alpha)\pi+\alpha\pi'$ .

Exact CPI (Algorithm 11) works with a class $\Pi$ of stationary policies and an accuracy $\varepsilon>0$ . Starting from any stationary policy, it repeats three steps:

The ExactPolicyChooser returns $\pi'\in\arg\max_{h\in\Pi}\mathbb Q_\pi(\mu,h)$ .
If $\mathbb A_\pi(\mu,\pi')>\varepsilon/H$ , the algorithm sets $\alpha=\mathbb A_\pi(\mu,\pi')/(4H)$ and replaces $\pi$ by $(1-\alpha)\pi+\alpha\pi'$ .
Otherwise it halts and returns $\pi$ .

Formalization targets

Goal: Theorem 7.3.2, explicit-constant form

Every run $\pi_0,\pi_1,\dots$ of Exact CPI has a halting round $K$ with

K<\frac{8H^2}{\varepsilon^2},\qquad V_{\pi_{k+1}}(\mu)-V_{\pi_k}(\mu)>\frac{\varepsilon^2}{8H^2}\ \ (k<K),\qquad \mathbb A_{\pi_K}(\mu,h)\le\frac{\varepsilon}{H}\ \ (h\in\Pi).

The returned $\pi_K$ is a stationary policy. The thesis states the halting bound as $O(H^2/\varepsilon^2)$ calls to the chooser. The constant $8$ is the one the thesis's own Corollary 7.2.3 supplies, and the mission states it explicitly.

Milestones

Lemma 7.2.2. For every $\alpha\in[0,1]$ , with $\epsilon_\infty=\max_s|\mathbb E_{a\sim\pi'(\cdot\mid s)}A_\pi(s,a)|$ ,

V_{\pi_{\rm new}}(\mu)-V_\pi(\mu)\ge\frac{\alpha}{1-\gamma}\Big(\mathbb A_\pi(\mu,\pi')-\frac{2\gamma\alpha}{1-\gamma(1-\alpha)}\epsilon_\infty\Big).

Corollary 7.2.3. If $\mathbb A_\pi(\mu,\pi')\ge0$ , the step $\alpha=\frac{1-\gamma}{4}\mathbb A_\pi(\mu,\pi')$ gives $V_{\pi_{\rm new}}(\mu)-V_\pi(\mu)\ge\mathbb A_\pi(\mu,\pi')^2/8$ .
Domination of the start distribution (p. 88): $d_{\pi,\mu}\ge\mu/H$ .
Lemma 5.2.1, discounted half: $V_{\pi'}(s_0)-V_\pi(s_0)=\frac1{1-\gamma}\mathbb E_{s\sim d_{\pi',s_0}}\mathbb E_{a\sim\pi'(\cdot\mid s)}A_\pi(s,a)$ .
Theorem 7.3.1. If $A_\pi(\nu,h)\le\varepsilon/H$ for all $h\in\Pi$ , then for every $\pi'\in\Pi$ and every state $s_0$ ,

V_\pi(s_0)\ge V_{\pi'}(s_0)-\varepsilon-H\|d_{\pi',s_0}-\nu\|_1.

Example 7.4.1. A two-state MDP on which the bound of Lemma 7.2.2 holds with equality for all $\alpha$ and $\gamma$ .

Milestones 1, 2 and 4 are already stated on the platform from Kakade–Langford (2002), in the same normalized model. They are included here as references and are not posed again.

Significance

The result. Theorem 7.3.2 is the exact-oracle core of CPI's sample-complexity analysis: the sample-based version later in the chapter replaces the exact chooser and the exact future advantage by estimates. The guarantee is stated through future advantages, so it does not depend on a max-norm accuracy over all states. Through Theorem 7.3.1 it translates into a value guarantee against every policy of the class whose future state distribution is close to the measure the algorithm was trained on. The output need not lie in $\Pi$ : even for a deterministic class the returned policy is in general stochastic.

Formalizing it. All results here are proved in the thesis, and the three referenced statements are proved on the platform. None of the new statements has a machine-checked proof. The mission adds a fully specified Exact CPI run as a Lean object, an explicit constant in place of the $O(\cdot)$ , and checked versions of the μ-optimality bound and of the tightness example. Its layer is shared with the Kakade–Langford missions, so later work on sample-based CPI can build on it directly.

Difficulty

The halting bound needs two ingredients that are easy to separate and easy to get wrong. The improvement guarantee of Corollary 7.2.3 holds only for a policy and a mixture weight in $[0,1]$ , so every iterate of the run must be shown to remain a policy and every step size to stay in range. The count of updates then rests on the normalized values being bounded in $[0,1]$ , a property of the model rather than of the algorithm. The output condition is stated for every $h\in\Pi$ , while the algorithm only tests the one policy the chooser returned, and the chooser maximizes future state-action values rather than future advantages.

A tempting shortcut is the thesis's remark on p. 88 that $\mathbb A_\pi(\mu,h)\le\varepsilon/H$ implies $A_\pi(\mu,h)\le\varepsilon$ . This is false in general: it would need $\mathbb E_{a\sim h}A_\pi(s,a)\ge0$ at every state. The mission formalizes only the true ingredient, $d_{\pi,\mu}\ge\mu/H$ .

Formalization scope

The layer is the published normalized model ApproxOptRL.Shared.Model: value, qValue, advantage, futureStateDist, and eta for $V_\pi(\mu)$ . The future advantage is ApproxOptRL.CPI.policyAdvantage and the conservative update is ApproxOptRL.CPI.mixPolicy. The model makes these commitments:

$S$ and $A$ are finite nonempty types.
Policies are maps $\pi:S\to A\to\mathbb R$ with IsPolicy, and deterministic policies are indicator policies.
Values carry the factor $1-\gamma$ , so all constants are the thesis's normalized ones. The thesis's statements for infinite state spaces are taken for finite $S$ , where $\|\cdot\|_1$ is a finite sum.
In Lean the policy class is called Pi because Π is reserved.

The run is the explicit predicate IsExactCPIRun: up to the round where the algorithm halts, the chooser output lies in $\Pi$ and maximizes $\mathbb Q_{\pi_k}(\mu,\cdot)$ over $\Pi$ , and the update uses exactly $\alpha_k=\mathbb A/(4H)$ . The halting round is part of the conclusion, never a hypothesis. A formalization in which the halting test or the step size is a free variable, or in which $\Pi$ is empty, would make "halts" an assumption or the run hypothesis unsatisfiable; the goal fixes both and requires $\Pi$ nonempty. The chooser's argmax is assumed to be attained, as in the thesis.

Contributions that would help: bounds $0\le V_\pi\le1$ and $|A_\pi|\le1$ for the normalized model, summability facts for futureStateDist, and a proof that a mixture of policies is a policy. These are reusable across every mission built on the same model.

Selected references

S. M. Kakade, On the Sample Complexity of Reinforcement Learning, PhD thesis, Gatsby Computational Neuroscience Unit, University College London, 2003, Chapter 7. https://discovery.ucl.ac.uk/id/eprint/10100726/
S. Kakade and J. Langford, Approximately Optimal Approximate Reinforcement Learning, Proceedings of the 19th International Conference on Machine Learning (ICML), 2002, pp. 267–274. https://dl.acm.org/doi/10.5555/645531.656005

12 thms2 active usersReviewed

Machine Learning Markov Chain Probability·Captain: mikedeng1

An Analysis of Temporal-Difference Learning with Function Approximation 2: For Every Sampling Distribution q and 5/6 < α < 1, Off-Line q-Sampled TD(0) Can Diverge in ExpectationResearch Paper

Motivation

Temporal-difference learning estimates the future cost of a system from observed transitions. In a Markov model, a state has a distribution of possible successors and each transition carries a cost. An agent may approximate the future cost with a small number of basis functions rather than store one number per state. This is useful when the state set is large or countably infinite, but the sampling rule then matters: the states used to update the approximation need not arrive in the same proportions as visits to the underlying Markov chain.

Tsitsiklis and Van Roy distinguish sampling along the chain from drawing current states independently from a chosen distribution $q$ . Their 1996 LIDS report, §9 constructs an example where the latter version of TD(0) has a mean parameter vector whose norm grows without bound. The example applies to every sampling distribution $q$ on a countable state space with at least two states and every discount factor $\alpha$ strictly between $5/6$ and $1$ . The mission formalizes that quantified counterexample, rather than selecting a particular two-state distribution.

Setting

Let $S$ be a finite or countably infinite set of states. A transition matrix $P$ assigns a probability distribution $p_{ij}$ over next states $j$ to each current state $i$ . A transition cost $g(i,j)$ is incurred when the chain moves from $i$ to $j$ , and $0<\alpha<1$ discounts later costs. The cost-to-go $J^*(i)$ is the expected sum of discounted costs along a chain started at $i$ . An invariant distribution $\pi$ satisfies $\pi^{\mathsf T}P=\pi^{\mathsf T}$ .

A feature vector $\phi(i)\in\mathbb R^K$ represents an approximate cost $\phi(i)^{\mathsf T}r$ , where $r\in\mathbb R^K$ is learned. The weighted norm $\|J\|_D$ uses the weights $\pi(i)$ , and $\Pi$ projects onto the span of the features in that norm. The one-step operator $T^{(0)}$ sends $J$ to the expected immediate cost plus $\alpha$ times the next-state value. These are the objects of §§2–4 of the report.

In $q$ -sampled TD(0), each current state $I_t$ is drawn independently from a probability distribution $q$ ; a successor $J_t$ is then drawn from row $P(I_t,\cdot)$ . Each new pair is independent of the earlier pairs. The parameter changes by

r_{t+1}=r_t+\gamma_t\phi(I_t)\left[g(I_t,J_t)+\alpha\phi(J_t)^{\mathsf T}r_t-\phi(I_t)^{\mathsf T}r_t\right].

The step sizes $\gamma_t$ satisfy the report's Assumption 4: they are chosen in advance, nonnegative and nonincreasing, their sum diverges, and the sum of their squares converges. Assumption 1 asks for a unique positive invariant law, finite stationary second moment of the transition costs, and finite cost-to-go from each state. Assumption 2 asks for linearly independent features with finite stationary second moments.

Formalization targets

Divergence of the mean

For every $q$ and $5/6<\alpha<1$ , Theorem 3 asserts the existence of $P$ , $g$ , and a feature map satisfying Assumptions 1 and 2, together with a unique projected fixed-point parameter $r^*$ , such that for every $r_0\ne r^*$ ,

\Pi T^{(0)}(\phi^{\mathsf T}r)=\phi^{\mathsf T}r\iff r=r^*, \qquad \lim_{t\to\infty}\bigl\|\mathbb E[r_t\mid r_0]\bigr\|=\infty.

The expectation is over the independent state–successor samples. The target is the norm of the mean vector; it does not assert divergence of individual sample paths. The formal goal quantifies over every probability space carrying samples with the stated joint law, so a choice of representation for the random process does not change the theorem.

Supporting statements

The milestones follow the claims in the proof of Theorem 3, pp. 24–25: existence of a full-support transition distribution; the one-feature construction and its assumptions; the general and specialized recurrences for $\mathbb E[r_t]$ ; a positive lower bound for their coefficient $\Delta$ ; and unbounded growth from that lower bound. The numerical inequality retains the report's threshold $5/(6\alpha)$ and its explicit positive factor $6\alpha p(s_2)-5$ .

Significance

The theorem identifies a limit of using TD(0) with linear approximation when the current states are sampled according to a distribution unrelated to the chain's invariant law. The constructed Markov chain itself has a well-defined zero cost-to-go, and the approximation uses only one nonzero feature direction. Nevertheless, the mean of the parameter sequence diverges for every nonfixed initialization. Thus the issue is present even without noisy costs or a complicated feature space. The report contrasts this with its convergence result for the on-line algorithm under additional assumptions; the counterexample says that those conclusions cannot be transferred to arbitrary independent state sampling by changing only the sample source. Tsitsiklis and Van Roy, §9.

The report proves Theorem 3 on paper. This mission asks for a machine-checked proof of its full quantifier structure, including countably infinite state spaces and arbitrary $q$ . A completed development would supply reusable Lean interfaces for countable Markov kernels, path laws, weighted projections, independent state–successor samples, and expected stochastic recurrences. The proposal currently contains the statements and definitions; the theorem proofs are open.

Difficulty

The apparent simplicity of the one-dimensional example hides two issues. First, the statement is uniform over $q$ , including distributions that put zero mass on nearly every state. A proof must choose the two feature states in response to $q$ while preserving the strict positivity needed for growth. Second, the recurrence concerns $\mathbb E[r_t]$ , where $r_t$ depends on all earlier random pairs. The step at time $t$ uses a fresh pair, and the factorization of its mean requires that temporal independence, plus justified integrability. Writing a positive scalar coefficient alone does not establish divergence of the expected parameter sequence for the sampled process.

Formalization scope

The Lean state space is a countable discrete measurable type with at least two elements. $P$ is a Markov kernel, its path law comes from the Ionescu–Tulcea construction, and the cost-to-go is the expectation of the discounted path sum. Weighted $L_2(S,D)$ membership is expressed by summability of $\pi(i)J(i)^2$ . The projection uses the inverse of the weighted Gram matrix under the independence and positive-mass assumptions that make it invertible. Only $T^{(0)}$ is needed here. The number $K$ of basis functions is existential, like the report's matrix $\Phi$ , but must be at least one: an empty parameter space would leave the universal divergence clause with no nonfixed initializations. The report's own example has $K=1$ .

Assumption 1 includes uniqueness of $\pi$ , positive mass at each state, the stationary squared-cost moment, and absolute integrability of the cost-to-go. Assumption 2 includes linear independence and integrability of squared features. Assumption 4 retains square-summability even though the displayed growth argument uses the divergent first-power sum. The general mean recurrence assumes bounded costs and features so its integrals and countable sums are meaningful; the constructed example satisfies those bounds. The goal additionally states finite-time integrability of the parameter vector. The source indexes states by 1 and 2; the formalization uses two distinct states $s_1,s_2$ and records the proof's ordering $0<q(s_1)$ and $q(s_2)\le q(s_1)$ in the growth milestone. The goal's quantification over probability spaces is restricted to Lean's Type universe.

The general mean recurrence is written with the immediate cost outside the matrix factor multiplying $\mathbb E[r_t]$ . This follows the algorithm displayed on p. 24 and corrects two slips in the printed recurrence on p. 25: its next-state subscript and the placement of the mean-cost term. Contributions to the path-law facts, independent-sampling calculations, countable weighted sums, and scalar growth theorem all support the same fixed goal.

Selected references

J. N. Tsitsiklis and B. Van Roy, An Analysis of Temporal-Difference Learning with Function Approximation, MIT Laboratory for Information and Decision Systems report LIDS-P-2322, 1996; published in IEEE Transactions on Automatic Control 42(5), 1997. MIT record.

9 thms2 active usersReviewed

Completed

Machine Learning Optimization·Captain: mikedeng1

On the Theory of Policy Gradient Methods: Optimality, Approximation, and Distribution Shift 3: Softmax Policy Gradient Ascent with Step Size η ≤ (1−γ)³/8 Converges to the Optimal ValuesResearch Paper

Motivation

Policy gradient methods optimize a parameterized policy of a Markov decision process by gradient ascent on its expected discounted return. They underlie much of modern reinforcement learning (REINFORCE, actor–critic methods, TRPO, PPO), yet the objective $\theta \mapsto V^{\pi_\theta}(\mu)$ is non-concave in the parameters, and until recently even the most basic question was open: does exact gradient ascent, run on a finite MDP with the standard softmax parameterization, reach the optimal values at all?

Agarwal, Kakade, Lee and Mahajan (arXiv:1908.00261v5, JMLR 22(98), 2021) answer this in the affirmative. Their Theorem 5.1 shows that unregularized softmax policy gradient with a small constant step size converges to the optimal value at every state, provided the start distribution used for the gradient puts positive mass on every state. The result is asymptotic: no rate is given. Later work (Mei, Xiao, Szepesvári and Schuurmans, ICML 2020, arXiv:2005.06392) obtained an $O(1/t)$ rate with constants that can be exponentially large, and the same paper by Agarwal et al. gives polynomial rates once a log-barrier regularizer is added (its Corollary 5.1) or once the natural gradient is used (its Theorem 5.3). Theorem 5.1 is the unregularized baseline for all of these.

Setting

A finite MDP consists of finite sets $\mathcal S$ of states and $\mathcal A$ of actions ( $\mathcal A$ nonempty), a transition kernel $P(s'\mid s,a)$ , rewards $r(s,a)\in[0,1]$ and a discount factor $\gamma\in[0,1)$ . A policy $\pi$ assigns to each state a probability vector $\pi(\cdot\mid s)$ on $\mathcal A$ . Its value $V^\pi(s)$ is the expected discounted sum of rewards $\mathbb E[\sum_{t\ge0}\gamma^t r(s_t,a_t)\mid s_0=s]$ when actions are drawn from $\pi$ ; its state–action value is $Q^\pi(s,a)=r(s,a)+\gamma\sum_{s'}P(s'\mid s,a)V^\pi(s')$ and its advantage is $A^\pi(s,a)=Q^\pi(s,a)-V^\pi(s)$ . For a distribution $\mu$ on states, $V^\pi(\mu)=\sum_s\mu(s)V^\pi(s)$ , and the discounted state visitation distribution is $d^\pi_\mu(s)=(1-\gamma)\sum_{t\ge0}\gamma^t\Pr^\pi(s_t=s\mid s_0\sim\mu)$ . A policy $\pi^\star$ is optimal if $V^{\pi}(s)\le V^{\pi^\star}(s)$ for every policy $\pi$ and every state $s$ ; $V^\star=V^{\pi^\star}$ .

The softmax policy with parameters $\theta\in\mathbb R^{|\mathcal S||\mathcal A|}$ is

\pi_\theta(a\mid s)=\frac{\exp(\theta_{s,a})}{\sum_{a'\in\mathcal A}\exp(\theta_{s,a'})}.

Softmax policy gradient ascent with step size $\eta$ produces, from an arbitrary $\theta^{(0)}$ , the iterates

\theta^{(t+1)}=\theta^{(t)}+\eta\,\nabla_\theta V^{(t)}(\mu),\qquad V^{(t)}=V^{\pi_{\theta^{(t)}}} .

The Lean development names these softmaxPolicy, softmaxValue P r γ µ θ $=V^{\pi_\theta}(\mu)$ , and IsSoftmaxPGRun P r γ µ η θ for the update rule; PolicyValue, QFunction and IsOptimalPolicy are the published FoundationsML definitions, and valueAt, advantage and visitation are the series' shared layer.

Formalization targets

Goal: Theorem 5.1

If $\mu(s)>0$ for every state and $0<\eta\le(1-\gamma)^3/8$ , then for every state $s$

V^{(t)}(s)\longrightarrow V^\star(s)\qquad(t\to\infty).

Milestones (Appendices C.1 and D)

Lemma C.1, the gradient formula $\partial V^{\pi_\theta}(\mu)/\partial\theta_{s,a}=\frac1{1-\gamma}d^{\pi_\theta}_\mu(s)\pi_\theta(a\mid s)A^{\pi_\theta}(s,a)$ .
Lemma D.1, smoothness $5\|c\|_\infty$ of $\theta_s\mapsto\sum_a\pi_\theta(a\mid s)c_a$ .
Lemma D.4 at $\lambda=0$ , smoothness $8/(1-\gamma)^3$ of $\theta\mapsto V^{\pi_\theta}(\mu)$ .
Lemma C.2, pointwise monotone improvement of $V^{(t)}(s)$ and $Q^{(t)}(s,a)$ for $\eta\le(1-\gamma)^2/5$ .
Lemma C.3, existence of the limits $V^{(\infty)}$ , $Q^{(\infty)}$ and the bound (40).
Lemma C.4, eventual sign separation (41) of the advantages on $I^s_+=\{a:Q^{(\infty)}(s,a)>V^{(\infty)}(s)\}$ and $I^s_-=\{a:Q^{(\infty)}(s,a)<V^{(\infty)}(s)\}$ .
Lemma C.5, vanishing gradients, $\pi^{(t)}(a\mid s)\to0$ off $I^s_0=\{a:Q^{(\infty)}(s,a)=V^{(\infty)}(s)\}$ , and $\sum_{a\in I^s_0}\pi^{(t)}(a\mid s)\to1$ .
Lemma C.6, eventual strict monotonicity of $\theta^{(t)}_{s,a}$ on $I^s_\pm$ .
Lemma C.7, divergence of $\max_{a\in I^s_0}\theta^{(t)}_{s,a}$ and $\min_a\theta^{(t)}_{s,a}$ when $I^s_+\neq\emptyset$ .
Lemma C.11, lower boundedness of $\theta^{(t)}_{s,a}$ on $I^s_+$ and $\theta^{(t)}_{s,a}\to-\infty$ on $I^s_-$ .

The goal states only convergence to the optimal values, with the paper's constants in the step-size bound; no rate is claimed.

Significance

The theorem establishes that the non-concavity of the softmax objective does not trap exact gradient ascent: from any initialization, the values of the iterates converge to $V^\star$ at every state, not only on average under $\mu$ . It is the reference point for the rate results of the same paper (log-barrier regularization, natural policy gradient) and for the subsequent literature on softmax policy gradient rates and lower bounds. It also isolates the role of exploration in the start distribution: Remark 5.1 of the paper leaves open whether $\mu>0$ can be dropped.

The result is proved in the paper; to the knowledge of the mission authors none of it is formalized in Lean or any other proof assistant. A complete development would provide a machine-checked gradient formula for the softmax class, smoothness bounds for discounted values, and a monotone-improvement argument for policy gradient, each reusable for other parameterizations and other policy optimization methods.

Difficulty

The obvious route fails. The gradient domination property of the direct parameterization (Lemma 4.1 of the paper) would conclude from $\nabla_\pi V^\pi(\mu)\to0$ , but under softmax $\partial V/\partial\theta_{s,a}=\pi_\theta(a\mid s)\,\partial V/\partial\pi_\theta(a\mid s)$ , so a vanishing $\theta$ -gradient says nothing once some action probabilities vanish, and the iterates do drive probabilities to zero while parameters diverge. A smoothness-based argument therefore gives only stationarity in the limit. The asymptotic analysis must instead track which actions keep positive limiting advantage, how the individual parameters $\theta^{(t)}_{s,a}$ move once the advantage signs are frozen, and why an action with strictly positive limiting advantage cannot coexist with the behaviour of the remaining parameters. Lemmas C.7–C.12 carry that bookkeeping; the limiting sets $I^s_0, I^s_\pm$ and the existence of the limits are themselves consequences of the pointwise monotone improvement of Lemma C.2, which needs its own smoothness bound.

Formalization scope

Standing setting of §3: finite types S, A with decidable equality, A nonempty; IsFiniteMDP P r γ (a transition kernel, rewards in $[0,1]$ , $0\le\gamma<1$ ); IsDist µ. Parameters live in EuclideanSpace ℝ (S × A), so norms are $\ell_2$ and Mathlib's gradient is $\nabla_\theta$ ; the coordinate $(s,a)$ of the gradient is $\partial/\partial\theta_{s,a}$ . Logarithms do not appear. Conventions committed to:

$V^\star(s)$ is PolicyValue πstar P r γ s for a policy πstar with IsOptimalPolicy πstar P r γ, optimal simultaneously at every state; it is not a real supremum over all functions.
The step size satisfies $0<\eta$ , which "gradient ascent" presupposes and the page does not write; at $\eta=0$ the theorem is false.
$\mu(s)>0$ for every $s$ is a hypothesis of the goal and of Lemmas C.5–C.11; Lemmas C.1–C.4 are stated without it, and Lemma C.1 for an arbitrary real weighting $\mu$ .
In Lemmas C.4–C.11 the limits $V^{(\infty)}$ , $Q^{(\infty)}$ are parameters with the hypotheses that they are the limits of $V^{(t)}$ , $Q^{(t)}$ . The paper's $\Delta=\min_{A^{(\infty)}(s,a)\neq0}|A^{(\infty)}(s,a)|$ is replaced by any $\Delta>0$ bounded by every nonzero $|A^{(\infty)}(s,a)|$ , which avoids an undefined minimum over an empty set.
" $\to\pm\infty$ " is Tendsto … atTop atTop / atBot; "strictly increasing for $t\ge T_1$ " is StrictMonoOn on Set.Ici T1, with $T_1$ existentially quantified.

The goal theorem does not assume the existence of limits, monotonicity of the iterates, or anything about the sets $I^s_0, I^s_\pm$ ; a formalization that did would assume the substance of the proof. Lemmas C.7 and C.11 (first part) carry the hypothesis $I^s_+\neq\emptyset$ of the paper's proof by contradiction, which no actual run satisfies once Theorem 5.1 is proved; they are steps of that argument.

A full development needs: differentiability of $\theta\mapsto V^{\pi_\theta}$ and the policy gradient theorem in the occupancy-measure form, the performance difference lemma, the descent lemma for $L$ -smooth functions, and Hessian bounds for the softmax map. Contributions to any of these, to the optional Lemmas C.8–C.10 and C.12 of the paper, or to the final contradiction argument are welcome.

Selected references

A. Agarwal, S. M. Kakade, J. D. Lee, G. Mahajan, On the Theory of Policy Gradient Methods: Optimality, Approximation, and Distribution Shift, JMLR 22(98), 2021; arXiv:1908.00261v5. https://arxiv.org/abs/1908.00261
J. Mei, C. Xiao, C. Szepesvári, D. Schuurmans, On the Global Convergence Rates of Softmax Policy Gradient Methods, ICML 2020. https://arxiv.org/abs/2005.06392
S. Kakade, J. Langford, Approximately Optimal Approximate Reinforcement Learning, ICML 2002. https://dl.acm.org/doi/10.5555/645531.656005
R. S. Sutton, D. McAllester, S. Singh, Y. Mansour, Policy Gradient Methods for Reinforcement Learning with Function Approximation, NeurIPS 1999. https://papers.nips.cc/paper/1713-policy-gradient-methods-for-reinforcement-learning-with-function-approximation

21 thms2 active usersReviewed

Completed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

Learning in Structured MDPs with Convex Cost Functions: Improved Regret Bounds for Inventory Management: Base-Stock Values from Any Two Starting States Differ by at Most 36 max(h,p)LxResearch Paper

Motivation

The lost-sales inventory problem with lead times is a basic model of operations management. A retailer reviews one product's stock each period and places an order that arrives $L$ periods later. Demand that cannot be met from stock on hand is lost, and the retailer pays a holding cost $h$ per unit left on the shelf and a penalty $p$ per unit of lost demand. The optimal policy depends on the whole pipeline of outstanding orders, so the state space grows with $L$ , and the problem is computationally hard for long lead times. Simple base-stock (order-up-to) policies are therefore the standard heuristic, and Huh, Janakiraman, Muckstadt and Rusmevichientong (Management Science 2009) showed they are asymptotically optimal as the lost-sales penalty grows.

Agrawal and Jia (arXiv:1905.04337) study the learning version, in which the demand distribution is unknown and only sales, not demands, are observed. They give an algorithm whose regret against the best base-stock policy is $\tilde O(L\sqrt T)$ , improving the earlier bound of Zhang, Chao and Shi, which grows exponentially in $L$ . The improvement rests on one structural fact: started from two different states, the base-stock system accumulates expected costs that differ by an amount linear in $L$ and independent of the horizon. That fact, Lemma 2.5 of the paper, is the goal of this mission.

Setting

Fix a lead time $L\ge 0$ and a base-stock level $x$ . A state is a vector $\mathbf s=(s(0),s(1),\dots,s(L))$ of real numbers. Its entry $s(0)$ is the on-hand inventory after the current period's arrival, and $s(1),\dots,s(L)$ are the outstanding orders, $s(L)$ the most recent. Under a base-stock policy with level $x$ the states lie in

\mathcal S^x=\Big\{\mathbf s : s(i)\ge 0\ \text{for all } i,\ \sum_{i=0}^{L}s(i)=x\Big\}.

In each period $t$ a demand $d_t\ge 0$ is drawn, independently across periods, from a distribution $F$ on $[0,\infty)$ . The sales are $y_t=\min\{s_t(0),d_t\}$ and the on-hand inventory is $I_t=s_t(0)$ . The policy reorders exactly what was sold, so for $L\ge 1$ the next state is

\mathbf s_{t+1}=\big(s_t(0)-y_t+s_t(1),\ s_t(2),\ \dots,\ s_t(L),\ y_t\big),

and for $L=0$ the state $(x)$ never changes. The pseudo-cost of period $t$ is $C^x_t=h(s_t(0)-y_t)-p\,y_t$ , and the value over horizon $T$ from the start state $\mathbf s$ is

V^x_T(\mathbf s)=\mathbb E\Big[\sum_{t=1}^{T}C^x_t\ \Big|\ \mathbf s_1=\mathbf s\Big].

Along a demand path, $n^x_T(\mathbf s)=\sum_{t=1}^T y_t$ is the total sales and $m^x_T(\mathbf s)=\sum_{t=1}^T I_t$ the total on-hand inventory.

States are compared by the order of Definition B.1: $\mathbf s'\succeq\mathbf s$ if $\mathbf s'-\mathbf s=\delta$ with $\sum_i\delta_i=0$ and some $0\le k\le L-1$ such that $\delta_i\ge 0$ for $i\le k$ and $\delta_i\le 0$ for $i>k$ . Thus $\mathbf s'$ holds the same total, shifted toward the shelf. The state $\hat{\mathbf s}=(x,0,\dots,0)$ dominates every state of $\mathcal S^x$ .

Formalization targets

Goal: Lemma 2.5 (p. 8)

For every $x$ , every horizon $T$ , all costs $h,p\ge 0$ , every demand law $F$ and all $\mathbf s,\mathbf s'\in\mathcal S^x$ ,

V^x_T(\mathbf s)-V^x_T(\mathbf s')\le 36\max(h,p)\,L\,x .

The constant is the paper's printed one. The proof's last display gives $18(h+p)Lx$ , a stronger bound, which is deliberately not the goal.

Milestones (Appendix B and the proof of Lemma 2.5)

All of the following hold for $L\ge 1$ , along any single demand path that drives both chains:

Lemma B.2 (p. 20). If $\mathbf s'_1\succeq\mathbf s_1$ then for $t\le L+1$ the cumulative sales satisfy $Y'_t-Y_t\le\max_{0\le k\le t-1}(\delta_0+\dots+\delta_k)$ .
Lemma B.3 (p. 20). If moreover $I'_t\ge I_t$ for $t=1,\dots,L+1$ , then $n_T(\mathbf s'_{L+1})=n_T(\mathbf s_{L+1})$ for every $T$ .
Lemma B.5 (p. 21). At the successive first crossing times $\sigma_i,\tau_i$ of Definition B.4, the state order alternates: $\mathbf s'_{\sigma_i}\succeq\mathbf s_{\sigma_i}$ and $\mathbf s'_{\tau_i}\preceq\mathbf s_{\tau_i}$ whenever these times exist.
Lemma B.6 (p. 21). If $\mathbf s'\succeq\mathbf s$ in $\mathcal S^x$ then $|n^x_T(\mathbf s')-n^x_T(\mathbf s)|\le 3x$ .
Lemma B.7 (p. 23). If $\mathbf s'\succeq\mathbf s$ in $\mathcal S^x$ then $|m^x_T(\mathbf s)-m^x_T(\mathbf s')|\le 6Lx$ .
Proof of Lemma 2.5 (p. 9). $\hat{\mathbf s}\succeq\mathbf s$ for every $\mathbf s\in\mathcal S^x$ .
Proof of Lemma 2.5 (p. 9). $|V^x_T(\mathbf s)-V^x_T(\hat{\mathbf s})|\le 9(h+p)Lx$ .

Significance

Lemma 2.5 bounds the dependence of the base-stock chain's finite-horizon cost on its starting state, uniformly in the horizon. In the paper it yields three consequences: the long-run average cost (the loss) of a base-stock policy does not depend on the initial state (Lemma 2.6), the bias of the chain is bounded by $36\max(h,p)Lx$ (Lemma 2.8), and finite-horizon average costs concentrate around the loss (Lemma 2.10). These feed the regret bound of Theorem 1.3. The lemma is also a statement about the base-stock lost-sales system alone, without any learning, so it is of independent interest for coupling arguments on lost-sales chains.

The paper's proof is complete on paper, but nothing in it has a machine-checked proof. Neither the lost-sales base-stock chain with lead times started from an arbitrary pipeline state nor any of the coupling lemmas of Appendix B is formalized elsewhere. This mission produces a checked proof of the goal and of the pathwise comparison lemmas. Theorem 1.3 is not posed: its supporting lemmas rely on limits whose existence the paper settles only by an informal discretization (Remark 4).

Difficulty

The obvious argument couples the two chains on a common demand path and waits until they coalesce. Coalescence is guaranteed only after $L$ consecutive periods of zero demand, an event of probability exponentially small in $L$ , so this argument gives a bound exponential in $L$ . That is the bound of earlier work.

The linear bound needs a finer pathwise accounting. The two coupled chains do not stay ordered: the one that starts with more inventory on the shelf sells more at first, then runs short and sells less. The order $\succeq$ between the two states alternates along a sequence of times, and the sales gained in one phase must be shown to be lost again in the next, so that the cumulative difference stays bounded by a constant multiple of $x$ for every horizon. Turning this alternation into a bound requires tracking how the pipeline vectors evolve between alternation times, including the boundary cases in which the chains coalesce or the horizon ends inside a phase.

Formalization scope

All declarations live in the namespace LostSalesLearning.ValueGap. A state is a function Fin (L + 1) → ℝ, a demand path is a function ℕ → ℝ≥0, and time is 0-based: traj s d 0 is the paper's $\mathbf s_1$ , traj s d t is $\mathbf s_{t+1}$ , and $\sum_{t=1}^T$ is a sum over Finset.range T. The demand law $F$ is a probability measure on ℝ≥0, and the demand path has the product law Measure.infinitePi (fun _ => F). The value is the expectation of the summed pseudo-costs, which equals Definition 2.4 by the tower property and is the form used in the paper's proof.

Committed conventions:

The costs satisfy $h\ge 0$ and $p\ge 0$ , the reading of "per unit holding cost and per unit lost sales penalty".
No assumption is placed on $F$ . The paper's assumptions $F(0)>0$ and bounded demand belong to other results.
The goal holds for every $L\ge 0$ ; the Appendix B milestones carry $L\ge 1$ , as Appendix B does.
The order $\succeq$ is Definition B.1 verbatim, with the equal-sum clause and the split index $k\le L-1$ .
The pathwise milestones quantify over every demand path and drive both chains with the same path.
The first crossing times of Definition B.4 are represented by alternationTimes; an absent next crossing is none.

Two trivializing formalizations are ruled out. A comparison of the two values on different or fixed demand paths would be a different statement: the goal compares two expectations under the same law, and each pathwise milestone uses one common path. A Bochner integral of a non-integrable function would be $0$ . The integrand here is measurable and bounded by $T(h+p)x$ on $\mathcal S^x$ , so the values are genuine expectations.

A complete development needs the elementary dynamics of the chain, including invariance of $\mathcal S^x$ and the shift of trajectories, which is reusable for other lost-sales models. It also needs the alternation times of Definition B.4, and measurability of the trajectory in the demand path. Proofs of individual milestones, alternative proofs of the goal, and sharper constants as separate statements are all welcome.

Selected references

S. Agrawal and R. Jia, Learning in Structured MDPs with Convex Cost Functions: Improved Regret Bounds for Inventory Management, arXiv:1905.04337v1, 2019. https://arxiv.org/abs/1905.04337
W. T. Huh, G. Janakiraman, J. A. Muckstadt and P. Rusmevichientong, Asymptotic Optimality of Order-Up-To Policies in Lost Sales Inventory Systems, Management Science 55(3), 2009. https://doi.org/10.1287/mnsc.1080.0945
H. Zhang, X. Chao and C. Shi, Closing the Gap: A Learning Algorithm for Lost-Sales Inventory Systems with Lead Times, Management Science 66(5), 2020. https://doi.org/10.1287/mnsc.2019.3288
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

9 thms2 active usersReviewed

Markov Chain Probability·Captain: mikedeng1

Linear Least-Squares Algorithms for Temporal Difference Learning II: Probability-One Convergence of LS TD on Ergodic Markov ChainsResearch Paper

Motivation

Temporal-difference (TD) learning estimates the value function of a Markov chain — the expected discounted sum of future rewards from each state — from a single stream of observed transitions, without knowing the transition probabilities. With a linear function approximator the value of state $x$ is represented as $\phi_x'\theta$ for a feature vector $\phi_x$ and a parameter $\theta$ . Classical TD( $\lambda$ ) updates $\theta$ by stochastic approximation, and its behaviour depends on a step-size schedule that must be tuned.

Bradtke and Barto (Machine Learning 22, 1996) replaced the stochastic-approximation update by a least-squares solve: LS TD (Eq. (11)) recomputes $\theta_t$ at every step as the instrumental-variable least-squares solution of the empirical consistency condition. The method, later generalized as LSTD( $\lambda$ ) by Boyan (Machine Learning 49, 2002), is the basis of least-squares policy iteration and of the "LSTD" methods in standard reinforcement-learning texts (Sutton and Barto, Reinforcement Learning, 2nd ed., 2018, §9.8). Its appeal is that it has no step size; the question this mission formalizes is whether it nonetheless converges, with probability one, to the true parameter.

Timeline. Sutton (1988) introduced TD( $\lambda$ ). Watkins and Dayan (1992) and Tsitsiklis (1994) proved probability-one convergence of tabular TD(0) and Q-learning. Bradtke and Barto (1996) proved probability-one convergence of LS TD on absorbing chains (Theorem 1) and on ergodic chains (Theorem 2). Tsitsiklis and Van Roy (IEEE TAC 42, 1997) proved convergence of linear TD( $\lambda$ ) with general features on ergodic chains.

Setting

A finite Markov chain on a finite nonempty set $X$ is a matrix $P$ with $P(x,y)\ge0$ and $\sum_yP(x,y)=1$ . A transition $x\to y$ earns reward $R(x,y)$ ; the expected reward out of $x$ is $\bar r_x=\sum_yP(x,y)R(x,y)$ . For a discount factor $\gamma$ the value function is

V(x)=E\Big\{\sum_{k=0}^\infty\gamma^kr_k\ \Big|\ x_0=x\Big\}=\sum_{k=0}^\infty\gamma^k(P^k\bar r)(x).

The chain is ergodic (Kemeny and Snell) if every state can be reached from every state: for all $x,y$ there is $n$ with $P^n(x,y)>0$ . An invariant distribution is a probability vector $\pi$ with $\pi P=\pi$ ; write $\Pi=\operatorname{diag}(\pi)$ .

Each state has a feature vector $\phi_x\in\mathbb R^m$ ; $\Phi$ is the matrix with rows $\phi_x$ . The true parameter $\theta^*$ is a vector with $V(x)=\phi_x'\theta^*$ for all $x$ .

The algorithm (Figure 3) starts at an arbitrary state $x_0$ , lets the chain move $x_0\to x_1\to\cdots$ , and after $t$ transitions computes

\theta_t=\Big[\frac1t\sum_{k}\phi_{x_k}(\phi_{x_k}-\gamma\phi_{x_{k+1}})'\Big]^{-1}\Big[\frac1t\sum_k\phi_{x_k}R(x_k,x_{k+1})\Big],\tag{11}

the sums running over the $t$ transitions observed so far.

Formalization targets

Goal: Theorem 2 (p. 44)

If $P$ is ergodic, (1) $\{\phi_x\}$ is linearly independent, (2) each $\phi_x$ has dimension $|X|$ , and (3) $0<\gamma<1$ , then $\theta^*$ is finite and, from any initial law,

\theta_t\longrightarrow\theta^*\qquad\text{with probability }1 .

The goal leaves the chain, the rewards, the features and the initial law arbitrary.

Milestones, in the order of the proof

Visit frequencies (Proof of Theorem 2, p. 45): an ergodic chain visits every state infinitely often and $\#\{k<t:x_k=x\}/t\to\pi_x$ almost surely.
Invertibility (Proof of Theorem 2, p. 45): $\pi_x>0$ for all $x$ , and $\Phi'\Pi(I-\gamma P)\Phi$ is invertible.
The pathwise limit (Proof of Lemma 5, pp. 54–55): along any path whose transition frequencies converge to $\pi_xP(x,y)$ , $\theta_t\to[\Phi'\Pi(I-\gamma P)\Phi]^{-1}[\Phi'\Pi\bar r]$ .
Lemma 5 (p. 43): for any chain, if almost surely every state is visited infinitely often and in proportion $\pi$ , and $\Phi'\Pi(I-\gamma P)\Phi$ is invertible, then $\theta_t\to[\Phi'\Pi(I-\gamma P)\Phi]^{-1}[\Phi'\Pi\bar r]$ almost surely.
Eq. (12) (p. 44): the value series converges and $\bar r=(I-\gamma P)\Phi\theta^*$ .

Significance

The result. Theorem 2 shows that an LS TD learner running on one long trajectory recovers the exact value function whenever the features can represent every function on the states, with no step-size schedule. It is the step-size-free counterpart of the tabular TD(0) convergence theorems and the starting point for the later analysis of LSTD with fewer features than states, where the limit is the TD fixed point $[\Phi'\Pi(I-\gamma P)\Phi]^{-1}\Phi'\Pi\bar r$ rather than $\theta^*$ . Lemma 5 is the general identification of that fixed point as the almost-sure limit of LSTD.

Formalizing it. The result is proved in the paper; it has not been machine-checked. A formalization adds three things the paper delegates: the strong law of large numbers for occupation times of a finite irreducible Markov chain, which the paper cites to Kemeny and Snell and which is not in Mathlib; the per-state transition frequencies used in the first sentence of the proof of Lemma 5; and the linear algebra of the limit. The first is reusable well beyond reinforcement learning.

Difficulty

The algebra is short once the empirical averages in (11) are known to converge. The difficulty is probabilistic: the averages are over a dependent sequence, so the ordinary strong law of large numbers does not apply. Two facts are needed: that the fraction of time in each state converges to $\pi_x$ almost surely for any starting law, including periodic chains, where $P^n$ itself does not converge; and that, among the visits to $x$ , the fraction followed by a move to $y$ converges to $P(x,y)$ , which needs the strong Markov property at successive visit times. Neither follows from convergence of the chain's distribution, and neither holds for a chain started at a fixed state without an argument that every state is reached.

Formalization scope

The model is a finite state type X with Fintype, DecidableEq, Nonempty, a row-stochastic matrix P : Matrix X X ℝ (structure Chain), rewards R : X → X → ℝ, features φ : X → Fin m → ℝ. Condition (2) is m = Fintype.card X; condition (1) is LinearIndependent ℝ φ.
"Ergodic" is read as irreducible, periodic chains allowed (Kemeny–Snell's aperiodic case is "regular"). "Arbitrary initial state" is read as every initial law $\nu$ , which contains every point mass.
The path is any process $Z$ on any probability space whose finite-dimensional distributions are $\nu(x_0)P(x_0,x_1)\cdots P(x_{n-1},x_n)$ , with measurable events $\{Z_t=x\}$ .
$V$ is the discounted series, never $(I-\gamma P)^{-1}\bar r$ ; Lean's tsum is $0$ on a divergent series, so "θ* is finite" is stated as convergence of the series together with existence of $\theta^*$ with $V=\Phi\theta^*$ . $\theta^*$ is existential, never defined as Lemma 5's limit.
(11) uses the transitions $k=0,\dots,t-1$ (the paper prints $k=1,\dots,t$ with $\phi_{t+1}$ ; an index shift), keeps the factors $1/t$ , and uses Lean's matrix inverse, which is $0$ on a singular matrix: the paper notes $\theta_t$ is undefined for small $t$ , and finitely many junk values do not affect convergence. No $\varepsilon I$ regularization, no pseudo-inverse.
$\theta_{\rm LSTD}=\lim_t\theta_t$ is formalized as convergence of $\theta_t$ (existence of the limit is part of the claim).
The convergence is almost sure. A formalization that assumes the visit frequencies converge in the goal, starts the chain from $\pi$ , or weakens the conclusion to convergence in probability or along a subsequence is a different theorem.

Needed infrastructure: the strong law for occupation times of a finite irreducible chain under an arbitrary initial law (milestone 1), the strong Markov property at visit times, positivity of the invariant distribution of an irreducible chain, and the invertibility of $I-\gamma P$ for $|\gamma|<1$ . Contributions to any of these, as standalone lemmas, are welcome.

Selected references

S. J. Bradtke and A. G. Barto, Linear Least-Squares Algorithms for Temporal Difference Learning, Machine Learning 22, 33–57, 1996. https://doi.org/10.1023/A:1018056104778
J. G. Kemeny and J. L. Snell, Finite Markov Chains, Springer, 1976.
J. A. Boyan, Technical Update: Least-Squares Temporal Difference Learning, Machine Learning 49, 233–246, 2002. https://doi.org/10.1023/A:1017936530646
J. N. Tsitsiklis and B. Van Roy, An Analysis of Temporal-Difference Learning with Function Approximation, IEEE Transactions on Automatic Control 42(5), 674–690, 1997. https://doi.org/10.1109/9.580874
R. S. Sutton and A. G. Barto, Reinforcement Learning: An Introduction, 2nd ed., MIT Press, 2018. http://incompleteideas.net/book/the-book-2nd.html

8 thms2 active usersReviewed

Completed

Markov Chain Probability·Captain: mikedeng1

Linear Least-Squares Algorithms for Temporal Difference Learning I: Probability-One Convergence of Trial-Based LS TD on Absorbing Markov ChainsResearch Paper

Motivation

Temporal-difference learning estimates the value of a policy from observed state transitions and rewards. In a finite Markov decision process, fixing a policy produces a Markov chain, so policy evaluation becomes the task of estimating the expected return from each state. Bradtke and Barto's 1996 paper introduced a least-squares temporal-difference method, LS TD, that uses each observed transition in a linear system instead of selecting a learning-rate schedule. Their Theorem 1 states probability-one convergence for trials that end at absorbing states under explicit conditions on state access, rewards, and features. This mission formalizes that result and the statements the authors use to reach it. Bradtke and Barto, 1996.

The result matters for episodic policy evaluation: a learner may collect many short trajectories, each begun from a prescribed start distribution, and update the same estimate as data accumulate. The theorem identifies conditions under which the limit is the true value parameter even when the discount factor is one. That endpoint is useful for undiscounted tasks ending in an absorbing goal state; it also makes the convergence claim more delicate than the standard discounted case. The paper proves the result mathematically. The Lean statements in this mission are targets for machine-checked proofs, not claims of proofs already present in Mathlib. Bradtke and Barto, Theorem 1, pp. 43–44.

Setting

Let $X$ be a finite, nonempty set of states. After a policy is fixed, $P(x,y)$ is the probability of a transition from $x$ to $y$ , so each row of $P$ is nonnegative and sums to one. A transition earns a deterministic real reward $R(x,y)$ . A state is absorbing when $P(x,x)=1$ ; let $\mathcal T$ be the absorbing states and $\mathcal N=X\setminus\mathcal T$ the others. The chain is absorbing when some absorbing state can be reached with positive probability from every state. A start distribution $S$ gives the state at the beginning of each trial. No state is inaccessible when every state can be reached from the positive support of $S$ .

For a discount $\gamma$ , the expected immediate reward is $\bar r(x)=\sum_yP(x,y)R(x,y)$ . The true value function is defined by the expected return

V(x)=\sum_{k=0}^{\infty}\gamma^k(P^k\bar r)(x).

A feature vector $\phi_x\in\mathbb R^m$ represents state $x$ . The matrix $\Phi$ has row $x$ equal to $\phi_x^\top$ . The target parameter $\theta^*$ is a vector for which $V(x)=\phi_x^\top\theta^*$ at every state; it is something the theorem must establish, not an input chosen by a formula. Equation (11) forms an LS TD estimate $\theta_n$ from the observed feature differences and rewards. Bradtke and Barto, §2, Table 1, Eq. (11).

Figure 2 collects trials. Each starts from $S$ , follows $P$ while the current state is non-absorbing, and ends upon entry into $\mathcal T$ . The next trial starts with a fresh draw from $S$ . The estimator includes transitions taken within trials; a draw that starts the next trial is not an observed transition for Eq. (11). Bradtke and Barto, Figure 2, p. 42.

Formalization targets

Theorem 1: convergence of trial-based LS TD

If every state is accessible from $S$ , rewards between absorbing states vanish, the feature vectors on $\mathcal N$ are linearly independent, features on $\mathcal T$ are zero, $m=|\mathcal N|$ , and $0\le\gamma\le1$ , then the expected-return series converges and there is a parameter $\theta^*$ satisfying

V(x)=\phi_x^\top\theta^*\quad(x\in X),\qquad \theta_n\longrightarrow\theta^*\quad\text{with probability one}.

The theorem keeps the paper's endpoint $\gamma=1$ . The return series' convergence is explicit because a real infinite sum in Lean has a default value when it diverges. Bradtke and Barto, Theorem 1, p. 43.

Supporting targets

The milestone list follows the statements used in the paper: almost-sure visits and departure proportions for the trials; invertibility of the non-absorbing block of $I-\gamma P$ ; invertibility of $\Phi^\top\Pi(I-\gamma P)\Phi$ for positive non-absorbing weights; Lemma 5's probability-one limit $[\Phi^\top\Pi(I-\gamma P)\Phi]^{-1}\Phi^\top\Pi\bar r$ ; and Eq. (12), $\bar r=(I-\gamma P)\Phi\theta^*$ , together with finiteness of the true parameter. Here $\Pi=\operatorname{diag}(\pi)$ . Bradtke and Barto, Lemma 5, p. 43; Proof of Theorem 1, p. 44.

Significance

Theorem 1 identifies the target of the asymptotic LS TD estimate: the value function defined from rewards, rather than merely a vector satisfying a sampled linear system. It covers an undiscounted absorbing chain, where a general fixed-point equation for values would fail to determine the values of absorbing states. The zero-reward and zero-feature conditions determine that boundary correctly. The result also explains the dimension condition: one independent feature vector for each non-absorbing state permits exact representation of the return. Bradtke and Barto, pp. 43–44.

A complete formal development would connect finite-state stochastic-process laws, visit frequencies, matrix limits, and the return-defined value function in one checked statement. The reusable parts include a finite row-stochastic chain model, a path-law description of restarts, a filtered least-squares estimator, and results about transient blocks of stochastic matrices. The paper's mathematical proof exists; this mission asks for formal proofs of its Lean targets. It also leaves room for alternative proofs and sharper, separately stated variants without weakening Theorem 1.

Difficulty

Ordinary matrix convergence cannot be applied until the observed transition frequencies are known to converge and the limiting matrix is invertible. A trial has random length, and the process resets after absorption, so a sequence indexed by all restart-process steps does not have the same raw state proportions as a count indexed by trials. The proof must account for both clocks while retaining the in-trial data of Eq. (11). At $\gamma=1$ , a direct geometric-series argument for the value function is unavailable; its finiteness depends on absorption and the reward convention. The matrix $I-\gamma P$ itself is singular at the undiscounted endpoint because of absorbing states, while its non-absorbing block is the relevant invertible matrix. Bradtke and Barto, Proof of Theorem 1, p. 44.

Formalization scope

The Lean state type is finite and nonempty. The paper evaluates one fixed policy, so $P$ is a real row-stochastic matrix and $R$ is a deterministic real reward on transitions; there is no action type in the formal statement. Absorbing states are exactly those with $P(x,x)=1$ , and “absorbing chain” means that an absorbing state is reachable from every state. The paper does not define “inaccessible”; the formalization reads it as unreachable from the positive support of $S$ . The state space carries the discrete measurable structure. Theorem 1's restart process and Lemma 5's ordinary Markov chain are each constrained by their finite-dimensional cylinder probabilities, not by assumed transition frequencies.

The feature space is $\mathbb R^m$ , and $m$ equals the cardinality of the subtype $\mathcal N$ . LS TD uses only departures from $\mathcal N$ . Index $n$ counts restart-process steps, so the estimate repeats at a restart draw; the paper counts in-trial transitions. These indices have the same asymptotic estimate when transitions continue. The $1/t$ factors in Eq. (11) cancel, and early singular inverses take Lean's total-inverse default. The value function is the return series, and the goal explicitly asserts its summability. The true parameter is existential, never defined by the formula whose convergence the theorem is meant to prove.

The paper defines $\pi_x$ for absorbing chains as expected departures from $x$ per trial. The Theorem 1 visit-frequency milestone normalizes by restart-process steps, which rescales all weights by one positive common factor; Lemma 5's matrix expression is invariant under that rescaling. Lemma 5 itself counts every ordinary-chain transition and carries the paper's “any Markov chain” scope. The milestone on invertibility allows arbitrary weights at absorbing states because their feature rows are zero. These conventions are recorded with each Lean item. Contributions toward the path-law frequency theorem, transient-matrix invertibility, return-series summability, and the matrix limit are all within scope. A vacuous path law or a value function defined from the desired linear equation would not establish the stated goal.

Selected references

S. J. Bradtke and A. G. Barto, Linear Least-Squares Algorithms for Temporal Difference Learning, Machine Learning 22, 33–57 (1996). DOI: 10.1023/A:1018056104778.

8 thms2 active usersReviewed

Completed

Machine Learning Probability·Captain: mikedeng1

Minimax Regret Bounds for Reinforcement Learning II: High-Probability Regret Bound for UCBVI with a Bernstein–Freedman BonusResearch Paper

Why finite-horizon reinforcement learning needs a variance-sensitive bound

An agent can learn to act in an unknown environment by repeatedly running a finite episode, observing the states reached after its actions, and updating its model of the environment. The agent must trade off rewards in the current episode against information that may improve later decisions. A regret bound measures the cumulative value lost relative to an optimal policy that knows the true transition probabilities. Its dependence on the number of states, actions, episode steps, and interactions says how much exploration that uncertainty can force.

Azar, Osband, and Munos study this question for a finite-horizon Markov decision process with known, bounded rewards and an unknown, stationary transition kernel. Their UCBVI algorithm estimates action values from observed transitions and adds an exploration bonus. Their second version, UCBVI-BF, uses the empirical variance of the next-state value in that bonus. Their Theorem 2 gives an explicit high-probability regret bound whose leading dependence on the horizon is smaller than the bound they give for the simpler UCBVI-CH bonus. The paper states that, in a sufficiently long-run regime, its leading order matches the cited lower-bound scale up to logarithmic factors. This mission targets the explicit theorem, including its lower-order terms, rather than only that asymptotic comparison.

The MDP, interaction, and algorithm

Let $\mathcal S$ and $\mathcal A$ be nonempty finite state and action sets with cardinalities $S$ and $A$ . A stationary transition kernel $P(y\mid x,a)$ is a probability distribution on next states $y$ for every current state $x$ and action $a$ . The reward $R(x,a)$ is deterministic, known to the learner, and lies in $[0,1]$ . These are the conditions of Assumption 1 and §2. Episodes have $H\ge1$ steps; $K$ episodes comprise $T=KH$ interactions.

A policy $\pi$ chooses an action for each state and step. Its value $V_h^\pi(x)$ is the expected reward from step $h$ through the final step when the state at $h$ is $x$ ; the terminal value is $V_{H+1}^\pi=0$ . The optimal value $V_h^*(x)=\sup_\pi V_h^\pi(x)$ ranges over all deterministic policies of this form. At the start of episode $k$ , the environment may choose the initial state using the completed episodes. The learner then fixes a policy $\pi_k$ , observes transitions during the episode, and updates counts for the next episode. Its regret is

\operatorname{Regret}(K)=\sum_{k=1}^{K}\bigl(V_1^*(x_{k,1})-V_1^{\pi_k}(x_{k,1})\bigr).

For each state-action pair, $N_k(x,a,y)$ counts transitions to $y$ in episodes before $k$ , and $N_k(x,a)=\sum_yN_k(x,a,y)$ . When the latter is positive, $\widehat P_k(y\mid x,a)=N_k(x,a,y)/N_k(x,a)$ . The count $N'_{k,h}(y)$ records previous episodes whose state at step $h$ was $y$ . Algorithms 2 and 4 compute optimistic $Q_{k,h}$ backward from zero terminal value, take a minimum with the previous episode's $Q$ estimate and with $H$ , and choose a maximizing action at every state. Previously unseen pairs receive $Q_{k,h}=H$ . The Bernstein–Freedman bonus uses the empirical variance of $V_{k,h+1}$ under $\widehat P_k$ and an additional term based on $N'_{k,h+1}$ ; the algorithm uses $L_{\rm alg}=\ln(5SAT/\delta)$ .

Formalization targets

The goal is Theorem 2 on p. 5. For any MDP and interaction described above and every $\delta>0$ , write $L=\ln(5HSAT/\delta)$ . The target is the exact bad-event form of the printed high-probability bound:

\Pr\!\left\{\operatorname{Regret}(K)>30HL\sqrt{SAK}+2500H^2S^2AL^2+4H^{3/2}\sqrt{KL}\right\}\le\delta.

The milestone list contains three empirical-transition deviations from the proof of Lemma 1: Eq. (9) for a value-weighted transition error, the displayed count bound before Eq. (11), and Eq. (12) for the full transition row's $\ell_1$ error. It also contains Lemma 2's variance comparison and Eq. (26), which relates cumulative conditional next-value variance to the variance of an episode return. These are source-indexed targets, with their printed constants retained.

What the result and its formalization supply

The theorem gives a quantitative guarantee for a particular executable decision rule: its regret grows sublinearly in $K$ in the leading term, with explicit dependence on $S$ , $A$ , and $H$ . The result lets one compare the horizon dependence of a variance-sensitive bonus with a value-agnostic bonus under the same finite-horizon model. It also fixes which logarithm belongs in the algorithm and which appears in the reported bound; replacing either changes the claim.

A formal proof would connect a fully specified adaptive interaction to its finite probability law, empirical counts, backward value iteration, and the stated high-probability conclusion. The local prior-art search found reusable transition-kernel vocabulary and general concentration tools, but no published formal statement of this exact UCBVI-BF algorithm or theorem. The mission's finite path and variance definitions can also support other episodic reinforcement-learning bounds that use conditional variance.

Where the difficulty lies

The bonus is computed using a value function that itself depends on earlier observations and the same episode's backward recursion. A concentration inequality for a fixed transition row and a fixed test function therefore does not directly control every value estimate encountered by the algorithm. The number of samples in a row is also random and changes with the learner's past actions. The regret compares a policy's value at an environment-chosen initial state with a supremum over all policies, while the learner's greedy action must be defined at states it never visits. These dependencies are the central obstacle to turning local concentration statements into the episode-level bound.

Formalization scope and conventions

The Lean model uses finite sums rather than measure theory. A published predicate supplies the stationary, real-valued transition kernel; a local MDP adds the known deterministic reward. State and action types are finite and nonempty. Policies are deterministic and depend on the step. The supremum defining $V^*$ ranges over their finite function type. A theorem quantifies over every maximizing tie-breaking rule and every initial-state rule that reads only completed episodes. The probability of an event is constructed as a sum over finite outcome sequences, each weighted by the product of true transition probabilities. Counts use all past transitions and no current or future outcomes. These choices rule out a trivialization that assumes the desired law or optimizes over an unbounded class of arbitrary functions.

Lean indexes the $H$ steps from zero, while the paper indexes them from one. The last observed next state is kept because Algorithm 4 counts states at the terminal index $H+1$ . At $N'_{k,h+1}(y)=0$ , Algorithm 4's quotient is interpreted as infinite and the capped term is $H^2$ ; Lean's ordinary division by zero would incorrectly produce zero. The algorithm uses $L_{\rm alg}=\ln(5SAT/\delta)$ , while Theorem 2's bound uses $L=\ln(5HSAT/\delta)$ . For Eq. (26), the appendix ends its sums at $H-1$ under a shifted terminal convention; the local statement includes all $H$ reward steps and the terminal value $V_{H+1}=0$ used by Algorithm 2. The milestone text remains the printed text. The count milestone is the display before Eq. (11), since Eq. (11) drops a factor of $2$ under the square root present in that display.

Theorem 2 retains its printed $2500H^2S^2AL^2$ term. The appendix's displayed Lemma 13 calculation does not reproduce that second-order constant when propagated to Lemma 14; this is a source proof gap, not a hypothesis of the theorem. Work on the probability normalization, random-count concentration, adaptive value estimates, variance identity, and a valid route to the printed explicit constants is welcome. A proof with altered constants or an asymptotic-only conclusion would be a different target.

Selected references

M. G. Azar, I. Osband, and R. Munos, Minimax Regret Bounds for Reinforcement Learning, arXiv:1703.05449v2, 2017. Preprint.

13 thms2 active usersReviewed

Completed

Dynamic Programming Machine Learning Markov Chain·Captain: mikedeng1

Reinforcement Learning: An Introduction IX: Average Reward and the Futility of Discounting in Continuing ProblemsTextbook

Motivation

Reinforcement learning formulates control as maximizing reward accumulated over time. For continuing tasks, where interaction never terminates, the standard textbook objective is the discounted return with a discount rate $\gamma < 1$ . Chapter 10 of Sutton and Barto, Reinforcement Learning: An Introduction (2nd ed., MIT Press, 2018), argues that once values are approximated by a function of features rather than stored per state, this objective is the wrong one, and it proposes the average-reward setting, long standard in dynamic programming (Puterman, Markov Decision Processes, 1994), as its replacement.

The central piece of evidence is a short calculation printed in the box The Futility of Discounting in Continuing Problems (p. 254). If one tries to rescue discounting by averaging discounted values over the states the policy actually visits, the resulting objective is a constant multiple of the average reward, so the discount rate has no effect on which policy is preferred. This mission formalizes that calculation together with the definitions of §10.3 that it rests on, and the two exercises of §10.3 that illustrate the differential value (10.13).

Setting

A finite MDP has finite state set $\mathcal S$ , finite action set $\mathcal A$ , finite reward set $\mathcal R \subset \mathbb R$ and dynamics $p(s', r \mid s, a)$ , a probability distribution over next state and reward for each state–action pair (3.2)–(3.3). Write $p(s' \mid s, a) = \sum_r p(s', r\mid s,a)$ . A policy $\pi(a \mid s)$ is a distribution over actions for each state. It turns the MDP into a Markov chain with transition matrix $P_\pi(s, s') = \sum_a \pi(a\mid s)\, p(s'\mid s,a)$ and expected one-step reward $r_\pi(s) = \sum_a \pi(a\mid s)\sum_{s',r} p(s',r\mid s,a)\, r$ , so that $\Pr\{S_t = s\mid S_0=s_0\} = P_\pi^t(s_0,s)$ and $\mathbb E[R_{t+1}\mid S_0 = s_0] = (P_\pi^t r_\pi)(s_0)$ .

A stationary distribution of $\pi$ is a probability vector $\mu$ on $\mathcal S$ with

\sum_s \mu(s)\sum_a \pi(a\mid s)\,p(s'\mid s,a) = \mu(s') \quad\text{for all } s' \qquad (10.8).

The average reward of $\pi$ is

r(\pi) = \lim_{h\to\infty}\frac1h\sum_{t=1}^h \mathbb E[R_t\mid S_0, A_{0:t-1}\sim\pi] \quad (10.6), \qquad r(\pi) = \sum_s \mu_\pi(s)\sum_a\pi(a\mid s)\sum_{s',r}p(s',r\mid s,a)\,r \quad (10.7),

the second form holding when the steady-state distribution $\mu_\pi(s) = \lim_{t\to\infty}\Pr\{S_t = s\}$ exists and does not depend on $S_0$ (an ergodic MDP).

The discounted value function is $v^\gamma_\pi(s) = \mathbb E_\pi\big[\sum_{k\ge0}\gamma^k R_{t+k+1}\mid S_t = s\big]$ , and the objective of the box is

J(\pi) = \sum_s \mu_\pi(s)\, v^\gamma_\pi(s).

Finally, the differential value of a state (10.13) is $v_\pi(s) = \lim_{\gamma\to1}\lim_{h\to\infty}\sum_{t=0}^h\gamma^t\big(\mathbb E_\pi[R_{t+1}\mid S_0 = s] - r(\pi)\big)$ .

Formalization targets

Goal: the futility of discounting

For $0 \le \gamma < 1$ , every policy $\pi$ and every stationary distribution $\mu_\pi$ of $\pi$ ,

J(\pi) = \sum_s \mu_\pi(s)\, v^\gamma_\pi(s) = \frac{1}{1-\gamma}\, r(\pi),

and therefore, for a fixed $\gamma$ and policies $\pi, \pi'$ with their own stationary distributions,

J(\pi) \le J(\pi') \iff r(\pi) \le r(\pi').

Milestones

(10.6)–(10.7): if $\Pr\{S_t = s\mid S_0 = s_0\}\to\mu(s)$ for all $s_0, s$ , then from every start both $\lim_t \mathbb E[R_t]$ and the Cesàro limit (10.6) exist and equal the $\mu$ -sum.
(10.8): such a limit $\mu$ is a stationary distribution.
(3.14): $v^\gamma_\pi$ satisfies the Bellman equation, the step "(Bellman Eq.)" of the box.
Offset invariance (p. 250): the differential Bellman equations for $v_\pi, q_\pi, v_*, q_*$ and the differential TD errors (10.10)–(10.11) are unchanged when all values are shifted by a constant.
Exercise 10.6: for expected rewards $1,0,1,0,\dots$ from $\mathsf A$ and $0,1,0,1,\dots$ from $\mathsf B$ , the average reward is $\tfrac12$ , the limit (10.7) and a steady-state distribution do not exist, and $v_\pi(\mathsf A) = \tfrac14$ , $v_\pi(\mathsf B) = -\tfrac14$ .
Exercise 10.7: in the three-state ring with reward $+1$ on arrival in $\mathsf A$ , the average reward is $\tfrac13$ and the differential values are $v(\mathsf A) = -\tfrac13$ , $v(\mathsf B) = 0$ , $v(\mathsf C) = \tfrac13$ .

The book prints no answers to Exercises 10.6 and 10.7; the values above were computed for this mission.

Significance

The result itself. The identity shows that the discount rate cannot enter the ranking of policies once performance is measured over the on-policy state distribution: any objective of the form "discounted value averaged over where the policy goes" is the average reward up to a positive factor. The book draws from it the conclusion (p. 253) that $\gamma$ changes from a problem parameter to a solution-method parameter, and that discounting algorithms with function approximation, which do not optimize this averaged objective, are not guaranteed to optimize average reward either. Milestones 1–2 connect the closed form of $r(\pi)$ to its definition as a long-run rate; milestone 4 explains why differential methods determine values only up to an offset; the exercises show that (10.13) gives finite differential values in periodic chains where the differential return (10.9) has no limit.

Formalizing it. The results are classical and elementary, but the book's derivation is informal: it takes the Bellman equation for granted, sums a geometric series of equalities, and leaves implicit which distribution $\mu_\pi$ is meant and when (10.6) and (10.7) agree. This mission fixes each of those points: $v^\gamma_\pi$ is defined from returns, the identity is proved for every stationary distribution, and the ergodicity hypothesis is made the exact limit condition the text states. No machine-checked version of these statements is known to exist; the platform's Markov-chain and average-reward libraries (Puterman's unichain optimality equation, Doeblin convergence) state different results.

Difficulty

The box reads as a chain of equalities, and each individual step is short. The one step that is not algebra is "(Bellman Eq.)": with $v^\gamma_\pi$ defined as an expected discounted return, the Bellman equation requires exchanging an infinite sum with a finite expectation and shifting the index of a convergent series, which needs absolute convergence for $\gamma < 1$ and bounded rewards. The final line, which unrolls $J = r + \gamma J$ into a geometric series, is only valid because $J$ is finite. For milestone 1, the book's hypothesis is the existence of an $S_0$ -independent limiting distribution, not irreducibility or aperiodicity; replacing it by either would change the statement. The exercises require the iterated limit in (10.13) to be computed explicitly: the inner limit is a periodic series summed in closed form, and the outer limit is a removable singularity at $\gamma = 1$ .

Formalization scope

The Lean development lives in the namespace SuttonBartoRL.AverageReward. States, actions and rewards are finite; one action set serves every state; the dynamics are the four-argument $p(s', r\mid s,a)$ . Probabilities $\Pr\{S_t = s\mid S_0 = s_0\}$ and $\mathbb E[R_{t+1}\mid S_0=s_0]$ are computed from the matrix powers $P_\pi^t$ . The discounted value $v^\gamma_\pi$ is a real series $\sum_k \gamma^k (P_\pi^k r_\pi)(s)$ ; it is not defined as the solution of the Bellman equation, since that definition would reduce the goal to three lines of algebra. The average reward and $J$ take the state distribution $\mu$ as an explicit argument; the goal holds for every stationary distribution of $\pi$ and assumes no ergodicity, which is all the box uses (under ergodicity $\mu_\pi$ is the unique one). $\gamma = 0$ is allowed. The differential value (10.13) is stated as the existence of both limits with the given value, with $\gamma \to 1$ from below, so no default value of a nonexistent limit can make a statement true. The optimality equations use a nonempty action set. The sum $\sum_{t=1}^h \mathbb E[R_t]$ of (10.6) is written with the index shifted to $t = 0,\dots,h-1$ .

The Lean does not formalize a trajectory probability space: expectations and probabilities are the matrix expressions above, which is what they equal for a Markov chain. The Exercise 10.6 hypothesis constrains expected rewards of one policy, which is all the exercise uses.

Reusable parts: the finite-MDP layer duplicates the one drafted for the other missions of this series and is expected to be merged with it; the Cesàro and stationary-distribution lemmas of milestones 1–2 are general facts about finite Markov chains. Contributions welcome: proofs of any milestone, and a proof of the goal from milestone 3.

Selected references

R. S. Sutton, A. G. Barto, Reinforcement Learning: An Introduction, 2nd ed., MIT Press, 2018, ISBN 9780262039246, §§10.3–10.4, pp. 249–254. http://incompleteideas.net/book/the-book-2nd.html
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887
S. Mahadevan, "Average reward reinforcement learning: foundations, algorithms, and empirical results", Machine Learning 22, 159–195, 1996. https://doi.org/10.1007/BF00114727

11 thms2 active usersReviewed

Completed

Linear algebra Machine Learning Markov Chain·Captain: mikedeng1

Reinforcement Learning: An Introduction VIII: The TD Fixed Point of Linear Semi-gradient TD(0) and Its Error BoundTextbook

Motivation

Reinforcement learning methods estimate the value function $v_\pi$ of a policy $\pi$ : the expected discounted sum of future rewards from each state. When the state space is large, $v_\pi$ cannot be stored as a table and is approximated by a parametrized function. The most studied case is linear function approximation, where each state $s$ carries a feature vector $\mathbf x(s) \in \mathbb R^d$ and the estimate is $\hat v(s, \mathbf w) = \mathbf w^\top \mathbf x(s)$ . Temporal-difference learning with this approximation, linear semi-gradient TD(0), is one of the basic algorithms of the field, and Chapter 9 of Sutton and Barto's Reinforcement Learning: An Introduction (2nd ed., MIT Press, 2018) presents its analysis: where the algorithm can converge, why that point exists, and how good it is.

The history is short. Sutton (1988, doi:10.1007/BF00115009) introduced TD learning and showed positive definiteness of the matrix governing its expected update. Dayan (1992, doi:10.1007/BF00992701) extended convergence to TD(λ). Tsitsiklis and Van Roy (1997, doi:10.1109/9.580874) proved convergence with probability one for linear TD(λ) under on-policy sampling and bounded the error of the limit. Bradtke and Barto (1996) introduced least-squares TD (LSTD), which computes the same limit directly.

Setting

A finite Markov decision process has finite sets of states $\mathcal S$ , actions $\mathcal A$ and rewards $\mathcal R \subset \mathbb R$ , and dynamics $p(s', r \mid s, a)$ , the probability of next state $s'$ and reward $r$ after action $a$ in state $s$ . A policy $\pi(a \mid s)$ is a probability distribution over actions for each state. It induces a Markov chain on states with transition matrix $\mathbf P$ , $\mathbf P(s, s') = p(s' \mid s) = \sum_a \pi(a \mid s) \sum_r p(s', r \mid s, a)$ , and expected one-step reward $r_\pi(s)$ . For a discount rate $0 \le \gamma < 1$ , the true value is $v_\pi(s) = \sum_{k \ge 0} \gamma^k (\mathbf P^k r_\pi)(s)$ , the expected discounted return.

A state distribution $\mu$ is stationary if $\mu^\top \mathbf P = \mu^\top$ ; write $\mathbf D = \mathrm{diag}(\mu)$ . The feature matrix $\mathbf X$ is the $|\mathcal S| \times d$ matrix with rows $\mathbf x(s)$ . The mean square value error of a weight vector is

\overline{\mathrm{VE}}(\mathbf w) = \sum_{s} \mu(s)\,[v_\pi(s) - \mathbf w^\top \mathbf x(s)]^2 .

Linear semi-gradient TD(0) updates $\mathbf w_{t+1} = \mathbf w_t + \alpha(R_{t+1} + \gamma \mathbf w_t^\top \mathbf x_{t+1} - \mathbf w_t^\top \mathbf x_t)\mathbf x_t$ . In steady state its expected update involves

\mathbf b = \mathbb E[R_{t+1}\mathbf x_t], \qquad \mathbf A = \mathbb E[\mathbf x_t(\mathbf x_t - \gamma \mathbf x_{t+1})^\top],

and the TD fixed point is $\mathbf w_{\mathrm{TD}} = \mathbf A^{-1}\mathbf b$ . A real square matrix $M$ , not necessarily symmetric, is positive definite if $y^\top M y > 0$ for every $y \ne 0$ . The key matrix is $\mathbf D(\mathbf I - \gamma\mathbf P)$ .

Formalization targets

Goal: the TD fixed point exists and its error bound (9.12), (9.14)

Under the hypotheses above, with every $\mu(s) > 0$ and linearly independent feature columns, $\mathbf A$ is invertible, $\mathbf b = \mathbf A \mathbf w_{\mathrm{TD}}$ , and

\overline{\mathrm{VE}}(\mathbf w_{\mathrm{TD}}) \le \frac{1}{1-\gamma}\min_{\mathbf w} \overline{\mathrm{VE}}(\mathbf w).

Milestones

The expected update (9.13): $\mathbb E[\mathbf w_{t+1} \mid \mathbf w_t] = (\mathbf I - \alpha \mathbf A)\mathbf w_t + \alpha \mathbf b$ .
The matrix form $\mathbf A = \mathbf X^\top \mathbf D(\mathbf I - \gamma \mathbf P)\mathbf X$ .
The criterion of Sutton (1988): positive diagonal, nonpositive off-diagonal entries, positive row sums and nonnegative column sums give positive definiteness.
The column sums of the key matrix, $\mathbf 1^\top \mathbf D(\mathbf I - \gamma \mathbf P) = (1-\gamma)\mu^\top$ .
The key matrix and $\mathbf A$ are positive definite.
A positive definite $\mathbf A$ is invertible and $\mathbf A^{-1}\mathbf b$ is the unique solution of $\mathbf b = \mathbf A \mathbf w$ (9.12).
The Sherman–Morrison update (9.22) of the LSTD inverse $\hat{\mathbf A}_t^{-1}$ .

Significance

Positive definiteness of $\mathbf A$ is the reason on-policy linear TD(0) is stable: it makes the expected iteration contract toward the fixed point for small step sizes, and it guarantees that the fixed point exists and is unique. The error bound (9.14) quantifies the price of bootstrapping: the limit of TD can be worse than the best linear approximation, but by at most the factor $1/(1-\gamma)$ . The same objects $\mathbf A$ , $\mathbf b$ and the key matrix reappear in LSTD, in the analysis of off-policy divergence (Chapter 11 of the book, where $\mathbf D$ is no longer the stationary distribution of $\mathbf P$ and positive definiteness fails), and in gradient-TD methods.

All results here are known. The book gives the positive definiteness argument in a box and cites (9.14) without proof. None of them has a machine-checked proof on the platform; the general Woodbury identity (FamousTheorems.woodbury_identity) is available, and (9.22) is its rank-one case written for the LSTD recursion. The mission produces a formal account of the finite-state theory of linear TD(0), with every hypothesis the book leaves implicit stated.

Difficulty

The key matrix $\mathbf D(\mathbf I - \gamma \mathbf P)$ is not symmetric, so the usual tools for symmetric positive definite matrices do not apply directly, and $\mathbf A$ is positive definite only because of the specific interplay between $\mathbf D$ and $\mathbf P$ : if $\mu$ is replaced by a non-stationary distribution the claim is false (this is the off-policy counterexample of Chapter 11). The error bound (9.14) is not a consequence of positive definiteness alone. The TD fixed point is not the minimizer of $\overline{\mathrm{VE}}$ , and $\overline{\mathrm{VE}}(\mathbf w_{\mathrm{TD}})$ has to be compared with the error of the $\mu$ -weighted projection of $v_\pi$ , which requires controlling $\mathbf P$ in the $\mu$ -weighted norm. The book gives no argument for this step.

Formalization scope

The Lean development lives in the namespace SuttonBartoRL.LinearTD. The MDP has four-argument dynamics $p(s', r \mid s, a)$ with a finite reward set and one action set for all states; policies are stochastic. $v_\pi$ is defined from expected discounted returns as the series $\sum_k \gamma^k \mathbf P^k r_\pi$ , never from a Bellman equation or from $\mathbf w_{\mathrm{TD}}$ . $\mathbf A$ and $\mathbf b$ are defined as the book's steady-state expectations (9.11), as finite sums over $\mu$ , $\pi$ and $p$ ; the matrix form is a milestone, not a definition. Features are a matrix Matrix S (Fin d) ℝ with rows $\mathbf x(s)$ ; linear independence of its columns is LinearIndependent ℝ Xᵀ. Positive definiteness is a custom predicate $\forall y \ne 0,\ 0 < y^\top M y$ , not Mathlib's Matrix.PosDef, which requires symmetry. The minimum in (9.14) is expressed by quantifying over every $\mathbf w$ . The matrix inverse is Mathlib's, which is zero on singular matrices; the goal therefore asserts invertibility of $\mathbf A$ explicitly.

Hypotheses the book leaves implicit and the statements make explicit: $0 \le \gamma < 1$ (the continuing case); $\mu$ a stationary distribution of the chain induced by $\pi$ with $\mu(s) > 0$ for every $s$ (otherwise the key matrix is only positive semidefinite); linearly independent feature columns (the book's "degenerate cases", p. 205). The box calls the off-diagonal entries of the key matrix "negative"; they are zero wherever $p(s' \mid s) = 0$ , so the criterion is stated with nonpositive entries. The book's sentence that $\varepsilon\mathbf I$ "ensures that $\hat{\mathbf A}_t$ is always invertible" (p. 229) is false in general, because the summands $\mathbf x_k(\mathbf x_k - \gamma \mathbf x_{k+1})^\top$ are not positive semidefinite: with $d = 1$ , $\varepsilon = 1/10$ , $\gamma = 1/2$ , $\mathbf x_0 = 1$ , $\mathbf x_1 = 11/5$ one gets $\hat{\mathbf A}_1 = 0$ . It is not stated; (9.22) carries invertibility of $\hat{\mathbf A}_{t-1}$ and a nonzero denominator as hypotheses.

A statement in which $v_\pi$ is defined as the solution of the projected equation, or in which $\mathbf A$ is assumed invertible or positive definite, would make the goal trivial or empty; neither is done. Convergence of the stochastic algorithm with probability one is not stated, since the book says it needs conditions and a step-size schedule it does not give. The bound for the episodic case and for other bootstrapping methods (p. 208) is stated only by reference in the book and is not a target.

Useful infrastructure: the $\mu$ -weighted inner product and orthogonal projection onto the column space of $\mathbf X$ , the non-expansiveness of a stochastic matrix in the norm of its stationary distribution, and the positive definiteness criterion for non-symmetric matrices. All of these are reusable in the off-policy and average-reward chapters of the book. Contributions of these lemmas, and of alternative proofs of the milestones, are welcome.

Selected references

Richard S. Sutton and Andrew G. Barto, Reinforcement Learning: An Introduction, 2nd ed., MIT Press, 2018, ISBN 9780262039246, §§9.2, 9.4, 9.8.
Richard S. Sutton, Learning to predict by the methods of temporal differences, Machine Learning 3, 1988. doi:10.1007/BF00115009
John N. Tsitsiklis and Benjamin Van Roy, An analysis of temporal-difference learning with function approximation, IEEE Transactions on Automatic Control 42(5), 1997. doi:10.1109/9.580874
Steven J. Bradtke and Andrew G. Barto, Linear least-squares algorithms for temporal difference learning, Machine Learning 22, 1996. doi:10.1007/BF00114723
Richard S. Varga, Matrix Iterative Analysis, Prentice-Hall, 1962.

11 thms2 active usersReviewed

Completed

Machine Learning Probability Statistics·Captain: mikedeng1

Reinforcement Learning: An Introduction V: Off-policy Prediction by Importance SamplingTextbook

Motivation

Reinforcement learning methods must explore in order to find good behaviour, yet the quantity they usually want to evaluate is the value of a different, often deterministic, policy. Off-policy prediction separates the two roles: episodes are generated by a behaviour policy $b$ , and the goal is the value function $v_\pi$ of a target policy $\pi$ . Almost every off-policy method in Sutton and Barto's Reinforcement Learning: An Introduction (2nd ed., MIT Press, 2018), and in the literature that follows it, rests on importance sampling: a return observed under $b$ is reweighted by the relative probability of its trajectory under $\pi$ and $b$ . Section 5.5 of the book introduces the idea for Monte Carlo prediction, §5.6 gives the incremental form of the weighted estimator, and §§5.8–5.9 refine the weights using the internal structure of the return: discounting-aware importance sampling, after Sutton, Mahmood, Precup and van Hasselt (2014), and per-decision importance sampling, introduced by Precup, Sutton and Singh (2000). The book's remarks on the variance of the two estimators (p. 105) cite Precup, Sutton and Dasgupta (2001). Later chapters (7, 11, 12) reuse the same ratios for $n$ -step, gradient-TD and eligibility-trace methods.

This mission is the fifth in a series formalizing the book's central mathematical claims. It covers §§5.5–5.9 (pp. 103–115).

Setting

A finite Markov decision process has finite sets of states $\mathcal S$ (terminal states included), actions $\mathcal A$ and rewards $\mathcal R \subset \mathbb R$ , and dynamics $p(s', r \mid s, a)$ : for each $(s, a)$ a probability distribution over next state and reward. The state-transition probability is $p(s' \mid s, a) = \sum_r p(s', r \mid s, a)$ . A policy $\mu$ gives a distribution $\mu(\cdot \mid s)$ over actions in every state.

An episode from a start state $s$ is a sequence $S_0 = s, A_0, R_1, S_1, \dots, A_{T-1}, R_T, S_T$ in which $S_0, \dots, S_{T-1}$ are nonterminal and $S_T$ is terminal. Under $\mu$ it has probability $\prod_{k=0}^{T-1} \mu(A_k \mid S_k)\, p(S_{k+1}, R_{k+1} \mid S_k, A_k)$ . The return is $G_0 = \sum_{k=0}^{T-1} \gamma^k R_{k+1}$ with discount rate $\gamma \in [0, 1]$ , and the value $v_\pi(s)$ is the expected return of an episode generated by $\pi$ from $s$ .

The behaviour policy covers the target policy if $\pi(a \mid s) > 0$ implies $b(a \mid s) > 0$ . The importance-sampling ratio of decisions $0, \dots, j$ is

\rho_{0:j} = \prod_{k=0}^{j} \frac{\pi(A_k \mid S_k)}{b(A_k \mid S_k)},

and the per-decision return weights each reward only by the ratio of the decisions that precede it:

\tilde G_0 = \rho_{0:0} R_1 + \gamma \rho_{0:1} R_2 + \dots + \gamma^{T-1} \rho_{0:T-1} R_T .

The book writes these objects at a general time $t$ and conditions on $S_t = s$ ; by the Markov property this is the same as starting the episode at $s$ , which is what the formal statements do.

Formalization targets

Goal: unbiasedness of ordinary and per-decision importance sampling

For episodes generated by $b$ from $s$ ,

\mathbb E_b\bigl[\rho_{0:T-1} G_0 \mid S_0 = s\bigr] = v_\pi(s) = \mathbb E_b\bigl[\tilde G_0 \mid S_0 = s\bigr].

The first equality is Eq. (5.4) (p. 104); the second is the statement $\mathbb E[\rho_{t:T-1}G_t] = \mathbb E[\tilde G_t]$ of §5.9 (p. 114).

Milestones

(5.3): the trajectory probability is a product, and the ratio of trajectory probabilities under $\pi$ and $b$ is $\rho_{0:T-1}$ , independent of the dynamics.
(5.4) alone.
(5.13): $\sum_a b(a \mid x)\, \pi(a \mid x)/b(a \mid x) = \sum_a \pi(a \mid x) = 1$ under coverage.
(5.14) and its $k$ -th form: $\mathbb E_b[\rho_{0:T-1} R_k] = \mathbb E_b[\rho_{0:k-1} R_k]$ for every $k \ge 1$ (Exercise 5.13).
Example 5.5: in a one-state MDP with a loop, $v_\pi(s) = 1$ and $\mathbb E_b[\rho_{0:T-1}G_0] = 1$ , yet $\mathbb E_b[(\rho_{0:T-1}G_0)^2] = \infty$ .
(5.7)–(5.8): the incremental rule $V_{n+1} = V_n + (W_n/C_n)(G_n - V_n)$ computes the weighted average $\sum_{k<n} W_k G_k / \sum_{k<n} W_k$ (Exercise 5.10).
§5.8: $G_t = (1-\gamma)\sum_{h=t+1}^{T-1}\gamma^{h-t-1}\bar G_{t:h} + \gamma^{T-t-1}\bar G_{t:T}$ with flat partial returns $\bar G_{t:h} = R_{t+1} + \dots + R_h$ .

Significance

Eq. (5.4) is the reason the first-visit ordinary importance-sampling estimator (5.5) is unbiased, and it is the template for every importance-sampling correction in the rest of the book. The per-decision identity shows that an estimator with fewer ratio factors per reward, (5.15), has the same expectation, which is the starting point for per-decision and control-variate methods for multi-step off-policy learning (Precup, Sutton and Singh 2000). Example 5.5 shows that unbiasedness says nothing about variance: the ordinary estimator can have infinite variance on a two-action problem, which motivates weighted importance sampling and the incremental weighted update of §5.6.

The results of these sections are classical and proved informally in the book, partly as exercises (5.10, 5.13) left without solution. No machine-checked version exists on the platform: a search for importance sampling, off-policy and per-decision returned no statements. The mission produces a formal trajectory model of an episodic MDP under two policies, which later missions on $n$ -step off-policy returns and off-policy traces can reuse.

Difficulty

Eq. (5.4) itself is a termwise identity: for every episode, $\Pr_b(\text{episode})\,\rho_{0:T-1} = \Pr_\pi(\text{episode})$ under coverage. The per-decision identity is not termwise. The later factors of $\rho_{0:T-1}$ multiply a reward that was received before the corresponding decisions, and removing them requires summing over all continuations of an episode prefix, of every remaining length, and using that each factor has conditional expectation one (5.13) and that the continuation terminates with probability one. The obvious attempt, cancelling the factors episode by episode, fails: on a single episode $\rho_{0:T-1}R_1$ and $\rho_{0:0}R_1$ differ.

In Example 5.5 the episodes have no length bound, so the expected square is an infinite series over episode lengths whose divergence must be shown directly.

Formalization scope

States, actions and rewards are finite types; the terminal states are a finite subset of the state type. Policies are stochastic, one action set is used in every state, and $v_\pi$ is defined as an expected return, never as the solution of a Bellman equation.
Expectations are series over episode lengths of finite sums over episodes. Lean assigns $0$ to a divergent series, so the goal and milestones 2 and 4 assume that under $b$ every episode from $s$ terminates within a fixed number $H$ of steps with probability one. The book leaves termination implicit; this bounded-horizon hypothesis is a restriction relative to the book's episodic setting and is stated as such. Example 5.5, whose episodes are unbounded, is stated without it, with the expected square in $[0, \infty]$ .
The discount rate is kept general in $[0, 1]$ .
The importance-sampling ratio uses real division; a factor with $b(A_k \mid S_k) = 0$ evaluates to $0$ in Lean, but such episodes have probability $0$ under $b$ .
The flat-partial-return decomposition is an algebraic identity and is stated for every real $\gamma$ , which is more general than the book's "for any $\gamma \in [0,1)$ ".
The incremental weighted update is stated with nonnegative weights and $W_1 > 0$ . The book's $C_0 = 0$ makes (5.8) divide by zero at $n = 1$ when $W_1 = 0$ ; the hypothesis excludes that case.
A trivializing formalization is ruled out: $v_\pi$ is the expected return of $\pi$ 's own episodes, the ratio is computed from the episode, and the per-decision identity, which carries the chapter's content beyond (5.4), is part of the goal.
Not stated: the bias and variance comparisons of ordinary and weighted importance sampling (p. 105) and the discounting-aware estimators (5.9)–(5.10) as estimators; these are statistical claims about estimators over a random number of visits that the book does not make precise.

Contributions welcome: proofs of the milestones, a general measure-theoretic version of the trajectory model without the bounded-horizon hypothesis, and variants for action values $q_\pi$ (Exercise 5.6).

Selected references

R. S. Sutton and A. G. Barto, Reinforcement Learning: An Introduction, 2nd ed., MIT Press, 2018, ISBN 9780262039246, §§5.5–5.9, pp. 103–115. http://incompleteideas.net/book/the-book-2nd.html
D. Precup, R. S. Sutton and S. Singh, Eligibility Traces for Off-Policy Policy Evaluation, Proceedings of the 17th International Conference on Machine Learning (ICML), 2000, pp. 759–766 (cited in the book's bibliography).
D. Precup, R. S. Sutton and S. Dasgupta, Off-Policy Temporal-Difference Learning with Function Approximation, Proceedings of the 18th International Conference on Machine Learning (ICML), 2001, pp. 417–424 (cited in the book, p. 105).

14 thms2 active usersReviewed

Completed

Dynamic Programming Machine Learning·Captain: mikedeng1

Reinforcement Learning: An Introduction IV: Policy Iteration for ε-Soft PoliciesTextbook

Motivation

Policy iteration alternates two steps: evaluate the current policy, then replace it by a policy that is greedy with respect to the evaluated action values. The policy improvement theorem guarantees that each greedy step does not make the policy worse, and that the process stops only at an optimal policy. When the action values are estimated from experience rather than computed from a model, as in Monte Carlo control, a greedy policy is a problem: it never tries the actions it does not currently prefer, so their values are never re-estimated. Sutton and Barto, Reinforcement Learning: An Introduction (2nd ed., 2018), §5.4, resolve this without the unrealistic assumption of exploring starts by moving the policy only toward a greedy one, to an ε-greedy policy that keeps every action's probability at least ε/|A|.

The question this mission formalizes is whether policy iteration still works under that restriction. The book's answer (pp. 101–102) is yes, in a precise sense: an ε-greedy step never makes an ε-soft policy worse, and it fails to make it strictly better only when the policy is already the best among all ε-soft policies. This is the dynamic-programming fact that justifies on-policy first-visit Monte Carlo control for ε-soft policies, and more broadly every ε-greedy on-policy control scheme that is analysed with exact action values.

Setting

A finite Markov decision process has a finite state set S, a finite nonempty action set A used in every state, a finite reward set R ⊂ ℝ and dynamics p(s′, r | s, a) ≥ 0 with $\sum_{s', r} p(s', r \mid s, a) = 1$ . A policy π gives, for each state s, a probability distribution π(· | s) on A. With a discount rate $0 \le \gamma < 1$ , the state value $v_\pi(s)$ is the expected discounted return $\mathbb E_\pi[\sum_{k \ge 0} \gamma^k R_{t+k+1} \mid S_t = s]$ , and the action value is

q_\pi(s, a) = \sum_{s', r} p(s', r \mid s, a)\,[r + \gamma v_\pi(s')].

For ε > 0, a policy is ε-soft if $\pi(a \mid s) \ge \varepsilon/|A|$ for all s and a. A policy π′ is ε-greedy with respect to $q_\pi$ if at each state some maximizer $A^*(s)$ of $q_\pi(s, \cdot)$ receives probability $1 - \varepsilon + \varepsilon/|A|$ and every other action receives $\varepsilon/|A|$ ; ties among maximizers are broken arbitrarily. A policy π is optimal among the ε-soft policies if it is ε-soft and $v_{\pi''}(s) \le v_\pi(s)$ for every ε-soft π″ and every state s.

The book's analysis uses a new environment with the same states, actions and rewards, in which with probability 1 − ε the chosen action is executed and with probability ε a uniformly random action replaces it:

\tilde p(s', r \mid s, a) = (1 - \varepsilon)\, p(s', r \mid s, a) + \sum_{a'} \frac{\varepsilon}{|A|}\, p(s', r \mid s, a').

Its optimal value function is written $\tilde v_*$ .

Formalization targets

Goal: ε-greedy improvement with the equality case

For $0 \le \gamma < 1$ , $0 < \varepsilon \le 1$ , an ε-soft policy π and any ε-greedy policy π′ with respect to $q_\pi$ ,

v_{\pi'}(s) \ge v_\pi(s) \quad \text{for all } s, \qquad \text{and} \qquad v_{\pi'} = v_\pi \;\Longrightarrow\; \pi, \pi' \text{ are optimal among the ε-soft policies}.

The goal is stated in terms of the original MDP and ε-soft policies only; the new environment appears only in the milestones.

Milestones

Policy improvement theorem for stochastic policies (4.7)–(4.8), p. 78: $\sum_a \pi'(a \mid s) q_\pi(s, a) \ge v_\pi(s)$ for all s implies $v_{\pi'} \ge v_\pi$ , strictly at every state where the hypothesis is strict.
Eq. (5.2), pp. 101–102: $\sum_a \pi'(a \mid s) q_\pi(s, a) = \frac{\varepsilon}{|A|}\sum_a q_\pi(s, a) + (1-\varepsilon)\max_a q_\pi(s, a) \ge v_\pi(s)$ .
Characterization, p. 102: an ε-soft π is optimal among ε-soft policies if and only if $v_\pi = \tilde v_*$ .
Uniqueness, p. 102: $\tilde v_*$ is the unique solution of the Bellman optimality equation with the altered transition probabilities $\tilde p$ , and that equation splits as $(1-\varepsilon)\max_a(\cdot) + \frac{\varepsilon}{|A|}\sum_a(\cdot)$ .
Fixed-point equation, p. 102: if $v_{\pi'} = v_\pi$ , then $v_\pi(s) = (1-\varepsilon)\max_a q_\pi(s, a) + \frac{\varepsilon}{|A|}\sum_a q_\pi(s, a)$ .

Significance

The result is what makes ε-greedy on-policy control a form of generalized policy iteration: monotone improvement at every step, and a characterization of where the process can stop. It also locates precisely what is lost by exploring, namely that the fixed point is optimal among ε-soft policies, not among all policies. The value $\tilde v_*$ of the new environment is the benchmark against which ε-greedy methods converge when action values are exact.

The book presents the argument informally and states the stochastic policy improvement theorem without proof ("we will not go through the details", p. 79). A formalization supplies the missing proof of the stochastic case, the identification of the best ε-soft policy value with the optimal value of a modified MDP, and the uniqueness of that value. As far as a search of the platform shows, no statement about ε-soft or ε-greedy policies has been formalized there; existing finite-MDP results (Bellman optimality in the Foundations of Machine Learning and Bertsekas series) use different reward models and do not cover the modified environment.

Difficulty

The improvement half follows from (5.2) and the policy improvement theorem, but both need work in the return-based model: the theorem requires comparing infinite discounted sums under two different Markov chains, and (5.2) uses the identity $v_\pi(s) = \sum_a \pi(a \mid s) q_\pi(s, a)$ , which is a theorem about returns, not a definition. The equality half is where the obvious argument fails. The deterministic-policy argument of Chapter 4 shows that an unimproved greedy policy satisfies the ordinary Bellman optimality equation; here the unimproved policy satisfies a different equation, and nothing in the original MDP identifies its solution with the best ε-soft value. That identification needs two further facts: every policy of the new environment corresponds to an ε-soft policy of the original one with the same values, and conversely (at ε = 1 only the uniform policy is ε-soft); and the altered optimality equation has exactly one solution.

Formalization scope

Everything is stated in the namespace SuttonBartoRL.EpsSoft on a finite MDP with four-argument dynamics, one finite nonempty action set for all states (so $|A(s)| = |A|$ , the book's footnote 3, p. 48), and a finite reward set. The conventions are:

$v_\pi$ is defined from expected discounted returns as $\sum_k \gamma^k (P_\pi^k r_\pi)(s)$ with $0 \le \gamma < 1$ ; Bellman equations are theorems, never definitions. $q_\pi$ is the one-step lookahead (4.6) on this $v_\pi$ .
$\tilde v_*$ is the supremum of the new environment's policy values over all stochastic policies, a bounded family for $\gamma < 1$ .
ε ranges over (0, 1]: the book requires ε > 0, and for ε > 1 no ε-soft policy exists. The equality in (5.2) is stated without the book's intermediate division by 1 − ε, so the case ε = 1 is included.
"Any ε-greedy policy" is encoded by quantifying over every choice of maximizer at every state.
"Optimal among ε-soft policies" means ε-soft and pointwise at least as good as every ε-soft policy.

Defining $v_\pi$ as the solution of the Bellman expectation equation, or $\tilde v_*$ as the solution of the altered optimality equation, would make milestones 3–5 and the goal's equality half hold by definition; the formalization does neither. The goal is not the statement " $v_{\pi'} \ge v_\pi$ " alone: the equality case is part of the book's claim and part of the goal.

The finite-MDP definitions duplicate those of other missions in this series and are expected to be merged later. Useful contributions include the Neumann-series identity $v_\pi = (I - \gamma P_\pi)^{-1} r_\pi$ , the Bellman expectation equation, the contraction property of Bellman operators, and the correspondence between policies of the new environment and ε-soft policies of the original one; these are reusable for the other finite-MDP missions of the series.

Selected references

R. S. Sutton and A. G. Barto, Reinforcement Learning: An Introduction, 2nd ed., MIT Press, 2018, ISBN 9780262039246, §4.2 (pp. 76–79) and §5.4 (pp. 100–103). http://incompleteideas.net/book/the-book-2nd.html
R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960 (policy iteration).
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994, doi:10.1002/9780470316887.

11 thms2 active usersReviewed

Completed

Machine Learning Markov Chain Optimization·Captain: mikedeng1

Reinforcement Learning: An Introduction XII: The Policy Gradient TheoremTextbook

Motivation

Policy gradient methods learn a parameterized policy $\pi(a \mid s, \theta)$ directly, by stochastic gradient ascent on a scalar performance measure $J(\theta)$ , instead of deriving the policy from learned action values. They are how reinforcement learning handles continuous action spaces, stochastic optimal policies and prior knowledge built into the policy's form, and they underlie REINFORCE (Williams, 1992) and the actor–critic family. Every such method needs an estimate of $\nabla J(\theta)$ . The difficulty is that $J$ depends on $\theta$ in two ways: through the action choices in each state, and through the distribution of states those choices produce. The second effect depends on the unknown environment dynamics.

The policy gradient theorem (Sutton, McAllester, Singh and Mansour, 2000; Marbach and Tsitsiklis, 2001) gives $\nabla J(\theta)$ as an expectation over the on-policy state distribution that involves no derivative of that distribution. Chapter 13 of Sutton and Barto's Reinforcement Learning: An Introduction (2nd ed., 2018) states it as Eq. (13.5), proves it in a box for the episodic case (p. 325) and in a second box for the continuing case (pp. 334–335), and builds REINFORCE, REINFORCE with baseline and actor–critic methods on it. This mission formalizes that chapter's theorem and the identities around it, in the book's own model.

Setting

A finite episodic MDP has a finite set $\mathcal S$ of nonterminal states, a terminal state, a finite action set $\mathcal A$ , a finite reward set $\mathcal R \subset \mathbb R$ and dynamics $p(s', r \mid s, a)$ : for each nonterminal $s$ and action $a$ , a probability distribution over next state $s' \in \mathcal S^+ = \mathcal S \cup \{\text{terminal}\}$ and reward $r$ . The terminal state is absorbing and pays nothing. Write $p(s' \mid s, a) = \sum_r p(s', r \mid s, a)$ and $r(s, a)$ for the expected reward.

A differentiable policy parameterization assigns to every $\theta \in \mathbb R^{d'}$ and state $s$ a distribution $\pi(\cdot \mid s, \theta)$ over actions, with $\theta \mapsto \pi(a \mid s, \theta)$ differentiable. Under $\pi_\theta$ the nonterminal states form a substochastic chain with matrix $P_\theta(s, s') = \sum_a \pi(a \mid s, \theta) p(s' \mid s, a)$ ; $\Pr(s \to x, k, \pi) = P_\theta^k(s, x)$ . Episodes terminate when $\sum_{k} P_\theta^k(s, s') < \infty$ for all $s, s'$ .

There is no discounting ( $\gamma = 1$ , p. 324). The state value $v_{\pi}(s) = \sum_{k \ge 0} (P_\theta^k r_\theta)(s)$ is the expected total reward from $s$ , with $r_\theta(s) = \sum_a \pi(a\mid s,\theta) r(s,a)$ ; the action value $q_\pi(s,a)$ is the expected total reward after taking $a$ in $s$ . The episode starts in a fixed state $s_0$ , and the performance is $J(\theta) = v_{\pi_\theta}(s_0)$ (13.4). The expected number of visits to $s$ in an episode is $\eta(s) = \sum_{k \ge 0} \Pr(s_0 \to s, k, \pi)$ , and the on-policy distribution is $\mu(s) = \eta(s) / \sum_{s'} \eta(s')$ (9.3).

In the continuing case there is no terminal state, $J(\theta) = r(\pi)$ is the average reward per step (13.15), $\mu$ is the steady-state distribution, and $v_\pi$ , $q_\pi$ are differential values, defined from the return $\sum_k (R_{t+k+1} - r(\pi))$ (13.17).

Formalization targets

Goal: the policy gradient theorem, episodic case (13.5)

If episodes terminate under $\pi_{\theta_0}$ , then $J$ is differentiable at $\theta_0$ and

\nabla J(\theta_0) = \sum_s \eta(s) \sum_a q_\pi(s,a)\, \nabla \pi(a \mid s, \theta_0) = \Big(\sum_{s'} \eta(s')\Big) \sum_s \mu(s) \sum_a q_\pi(s,a)\, \nabla \pi(a \mid s, \theta_0),

with $\sum_{s'} \eta(s') \ge 1$ . The book writes $\nabla J(\theta) \propto \sum_s \mu(s) \sum_a q_\pi(s,a) \nabla \pi(a \mid s,\theta)$ and names the constant, the average length of an episode, in words (p. 326). The goal states it.

Milestones

Exercises 3.18–3.19 with $\gamma = 1$ : $v_\pi(s) = \sum_a \pi(a\mid s) q_\pi(s,a)$ and $q_\pi(s,a) = \sum_{s',r} p(s',r\mid s,a)(r + v_\pi(s'))$ .
The recursion $\nabla v_\pi(s) = \sum_a [\nabla\pi(a\mid s) q_\pi(s,a) + \pi(a\mid s) \sum_{s'} p(s'\mid s,a) \nabla v_\pi(s')]$ , including the differentiability of $v_\pi$ .
The unrolled gradient $\nabla v_\pi(s) = \sum_{x} \sum_{k=0}^\infty \Pr(s \to x, k, \pi) \sum_a \nabla\pi(a\mid x) q_\pi(x,a)$ for every $s$ .
The theorem with a baseline (13.10): $\sum_a b(s) \nabla \pi(a\mid s,\theta) = 0$ , hence $q_\pi$ may be replaced by $q_\pi - b$ .
The log form behind REINFORCE: where $\pi(\cdot\mid s,\theta) > 0$ , $\sum_a q_\pi(s,a) \nabla\pi(a\mid s,\theta) = \sum_a \pi(a\mid s,\theta) q_\pi(s,a) \nabla \ln \pi(a\mid s,\theta)$ , and hence $\nabla J(\theta) = (\sum_{s'}\eta(s')) \sum_s \mu(s) \sum_a \pi(a\mid s,\theta) q_\pi(s,a) \nabla \ln \pi(a\mid s,\theta)$ , the exact form of $\nabla J \propto \mathbb E_\pi[q_\pi(S_t,A_t) \nabla\pi(A_t\mid S_t,\theta)/\pi(A_t\mid S_t,\theta)]$ .
Exercise 13.3, (13.9): for the linear soft-max, $\nabla \ln \pi(a\mid s,\theta) = x(s,a) - \sum_b \pi(b\mid s,\theta) x(s,b)$ .
Exercise 13.4: the eligibility vectors of the Gaussian policy (13.19)–(13.20).
The continuing case: under ergodicity, $\nabla r(\pi_\theta) = \sum_s \mu(s) \sum_a \nabla\pi(a\mid s,\theta) q_\pi(s,a)$ with differential $q_\pi$ .

Significance

The theorem turns $\nabla J$ into a quantity that can be sampled by following the policy: weighting states by $\mu$ is what visiting them under $\pi$ does, and the log form makes the action sum an expectation over $A_t \sim \pi$ . REINFORCE (13.8), REINFORCE with baseline (13.11) and one-step and eligibility-trace actor–critic methods all rest on it, and so does their claim that the expected update is in the direction of the performance gradient (p. 329). The baseline identity is why a learned state value can reduce variance without introducing bias.

The results are proved, in the book and in the literature. What this mission adds is a machine-checked version in the book's model: random episode lengths with $\gamma = 1$ , vector parameters $\theta \in \mathbb R^{d'}$ , four-argument dynamics, and values defined from expected returns. The platform already has a proved finite-horizon policy gradient theorem (policy_gradient_finite_horizon, with a baseline and log-form companion) for a fixed horizon $T$ , a scalar parameter $\theta \in \mathbb R$ and an expected-reward kernel; it does not cover the book's statement. The mission also makes explicit two points the text leaves informal: that episodes terminate, and what exact constant hides behind " $\propto$ ".

Difficulty

The book's proof is a formal manipulation: differentiate the Bellman equation, substitute it into itself, and "unroll" infinitely often. Two steps are not justified on the page. First, it presupposes that $\nabla v_\pi(s)$ exists; with $\gamma = 1$ the value is an infinite series whose convergence depends on $\theta$ through termination, so differentiability of $v_\pi$ at $\theta_0$ has to be established, and termination is assumed only at $\theta_0$ . Second, "repeated unrolling" is a limit: after $n$ unrollings a remainder $\sum_x P_\theta^{n}(s,x) \nabla v_\pi(x)$ is left over, and it vanishes only because $P_\theta^n \to 0$ . Differentiating the series for $v_\pi$ term by term is not an alternative shortcut without a uniform bound on the derivatives of $P_\theta^k$ .

In the continuing case the corresponding obstacle is the differentiability of the steady-state distribution and of the differential values, which the book's proof uses without comment; here they are part of what is to be proved, from ergodicity at $\theta_0$ alone.

Formalization scope

Model. $\mathcal S^+$ is Option S, with none the single terminal state (several terminal states can be merged, all having value 0). One action type for all states. $\theta$ lives in EuclideanSpace ℝ (Fin d), and $\nabla$ is Mathlib's gradient; conclusions are HasGradientAt, so differentiability is asserted, not assumed.
Values from returns. $v_\pi$ , $q_\pi$ , $\eta$ are series in powers of $P_\theta$ ; Bellman equations are theorems (milestone 1). The continuing-case average reward and steady-state distribution are the limits of (13.15), and the differential values are the series of (13.17).
Implicit hypotheses made explicit. Termination under $\pi_{\theta_0}$ is a hypothesis of every episodic result that involves values; the continuing case assumes the book's ergodicity (the limit of $\Pr\{S_t = s'\}$ exists and does not depend on $S_0$ ) at $\theta_0$ . The positivity of $\pi(a \mid s,\theta_0)$ is assumed where a logarithm is differentiated.
"∝". The episodic goal states the exact equality with the constant $\sum_{s'} \eta(s')$ and proves it is at least 1. A formalization of the form " $\exists c,\ \nabla J = c \cdot \ldots$ " is ruled out: it holds with $c = 0$ and loses the book's constant.
Fixed start state. $s_0$ is a fixed state, as in the book (p. 324); no start distribution.
Not included. Convergence of REINFORCE or actor–critic under stochastic-approximation conditions (p. 329) rests on unstated conditions and is not an item. The baseline is a deterministic function of the state, not the random variable the book also allows.

Reusable infrastructure: the episodic value layer (substochastic chains, expected visits, termination) is needed by any undiscounted episodic RL result; the soft-max and Gaussian eligibility computations are needed by every policy-gradient algorithm. Proofs of any milestone, and general lemmas on the differentiability of values and stationary distributions of parameterized finite Markov chains, are welcome.

Selected references

R. S. Sutton and A. G. Barto, Reinforcement Learning: An Introduction, 2nd ed., MIT Press, 2018, ISBN 9780262039246, Chapter 13. http://incompleteideas.net/book/the-book-2nd.html
R. S. Sutton, D. McAllester, S. Singh and Y. Mansour, Policy Gradient Methods for Reinforcement Learning with Function Approximation, NeurIPS 12, 2000. https://proceedings.neurips.cc/paper/1999/hash/464d828b85b0bed98e80ade0a5c43b0f-Abstract.html
P. Marbach and J. N. Tsitsiklis, Simulation-Based Optimization of Markov Reward Processes, IEEE Transactions on Automatic Control 46(2), 2001. https://doi.org/10.1109/9.905687
R. J. Williams, Simple Statistical Gradient-Following Algorithms for Connectionist Reinforcement Learning, Machine Learning 8, 1992. https://doi.org/10.1007/BF00992696

14 thms2 active usersReviewed

Completed

Linear algebra Machine Learning·Captain: mikedeng1

Reinforcement Learning: An Introduction XI: Dutch Traces and the Equivalence of Forward and Backward Views in Monte Carlo LearningTextbook

Motivation

Eligibility traces are one of the basic mechanisms of reinforcement learning. A trace is a short-term memory vector $z_t$ with one component per weight. It records which components contributed to recent value estimates, so that an error observed now can be credited to the right components without storing the past. Chapter 12 of Sutton and Barto's Reinforcement Learning: An Introduction (2nd ed., 2018) organizes the topic around two ways of describing an algorithm. A forward view updates each state toward a target built from rewards that arrive later. A backward view makes an update at every step from the current error and the trace.

The chapter proves one exact equivalence between the two views itself, in §12.6: "This is the only equivalence of forward- and backward-views that we explicitly demonstrate in this book" (p. 301). The setting is linear Monte Carlo prediction, and the backward view uses a dutch trace. The same trace appears in true online TD( $\lambda$ ), whose exact equivalence to the online $\lambda$ -return algorithm (van Seijen and Sutton, 2014; van Seijen et al., 2016) the book cites without proof. Of that proof, §12.6 "gives some of the flavor ... but is much simpler" (p. 301).

The older equivalence of §§12.1–12.2 goes back to Sutton (1988). If the weights are held fixed during an episode, the summed updates of TD( $\lambda$ ) with accumulating traces equal the summed updates of the off-line $\lambda$ -return algorithm. The book leaves it as Exercises 12.3–12.4.

Setting

Fix a dimension $d$ , a step size $\alpha$ and an episode of length $T \ge 1$ with feature vectors $x_0, \dots, x_{T-1} \in \mathbb R^d$ . The episode ends with a single return $G \in \mathbb R$ ("a single reward received at the end of the episode ... and ... no discounting", p. 301). The forward view is the linear gradient Monte Carlo, or LMS, rule (12.13): from an initial $w_0$ ,

w_{t+1} = w_t + \alpha\,[G - w_t^\top x_t]\,x_t, \qquad 0 \le t < T .

Let $F_t = I - \alpha x_t x_t^\top$ be the fading matrix. The backward view keeps two vectors that are updated at each step in $O(d)$ time without knowledge of $G$ . The dutch trace is $z_0 = x_0$ , $z_t = z_{t-1} + (1 - \alpha z_{t-1}^\top x_t)\,x_t$ . The auxiliary vector is $a_t = a_{t-1} - \alpha x_t x_t^\top a_{t-1}$ , with $a_0 = F_0 w_0$ .

For the second part, an episode $S_0, R_1, S_1, \dots, R_T, S_T$ carries states and rewards, and $\hat v(s, w)$ is a differentiable value function with $\hat v(\text{terminal}, \cdot) = 0$ . For one fixed weight vector $w$ , define the following, with $\gamma \in [0,1]$ and $\lambda \in [0,1)$ :

the return $G_t$ ;
the $n$ -step return $G_{t:t+n}$ (12.1), with $G_{t:t+n} = G_t$ once $t + n \ge T$ ;
the $\lambda$ -return $G^\lambda_t = (1-\lambda)\sum_{n \ge 1}\lambda^{n-1} G_{t:t+n}$ (12.2);
the TD error $\delta_t = R_{t+1} + \gamma\hat v(S_{t+1}, w) - \hat v(S_t, w)$ (12.6);
the accumulating trace $z_{-1} = 0$ , $z_t = \gamma\lambda z_{t-1} + \nabla\hat v(S_t, w)$ (12.5).

Formalization targets

Goal: the dutch-trace equivalence (12.14), corrected

w_T = a_{T-1} + \alpha G\, z_{T-1}.

The left side is the forward view after $T$ LMS updates. On the right, $a_{T-1}$ and $z_{T-1}$ are produced by the incremental recursions above. The goal is about the two algorithms, not only about the closed-form product identity.

Milestones on the goal's path (§12.6, p. 302)

$w_{t+1} = F_t w_t + \alpha G x_t$ .
$w_T = F_{T-1}\cdots F_0 w_0 + \alpha G \sum_{k=0}^{T-1} F_{T-1}\cdots F_{k+1} x_k$ , the first line of (12.14).
$z_t = \sum_{k=0}^{t} F_t \cdots F_{k+1} x_k$ for the dutch-trace recursion.
$a_t = F_t \cdots F_0 w_0$ for the auxiliary-vector recursion (corrected initialization).

Milestones on the $\lambda$ -return (§§12.1–12.2)

(12.3): $G^\lambda_t = (1-\lambda)\sum_{n=1}^{T-t-1}\lambda^{n-1}G_{t:t+n} + \lambda^{T-t-1}G_t$ for $t < T$ .
Exercise 12.1: $G^\lambda_t = R_{t+1} + \gamma[(1-\lambda)\hat v(S_{t+1}, w) + \lambda G^\lambda_{t+1}]$ .
Exercise 12.3: $G^\lambda_t - \hat v(S_t, w) = \sum_{k=t}^{T-1}(\gamma\lambda)^{k-t}\delta_k$ .
Exercise 12.4: $\sum_{t<T}\alpha\delta_t z_t = \sum_{t<T}\alpha[G^\lambda_t - \hat v(S_t, w)]\nabla\hat v(S_t, w)$ .

Significance

The goal says that an $O(d)$ -per-step algorithm reproduces the Monte Carlo/LMS result exactly. That algorithm never stores the feature vectors or the $T$ intermediate weight vectors. The book draws the conclusion that eligibility traces "are not specific to TD learning at all" (p. 303). The dutch trace in the case $\gamma\lambda = 1$ is the same object that true online TD( $\lambda$ ) (12.11) uses for general $\gamma\lambda$ . The fading-matrix products and their incremental forms are therefore the vocabulary of any later formalization of true online TD( $\lambda$ ) and of the online $\lambda$ -return algorithm.

Exercises 12.3–12.4 are the fixed-weight equivalence of TD( $\lambda$ ) and the off-line $\lambda$ -return algorithm. They are the standard justification for calling TD( $\lambda$ ) an approximation of the $\lambda$ -return algorithm. Exercise 12.1 and (12.3) are the identities the rest of the chapter uses to manipulate $\lambda$ -returns.

On status: all of these results are known and elementary on paper, and the book prints the derivation of (12.14). To our knowledge none of them has a machine-checked proof, and the platform has no statement about $\lambda$ -returns, eligibility traces or TD( $\lambda$ ). What this mission adds is formal statements with every convention fixed, including one correction to the printed text. It also adds reusable definitions of $n$ -step returns, $\lambda$ -returns and traces.

Difficulty

The algebra is elementary. The difficulty lies in the conventions, and a careless reading of the page produces a false statement. The book initializes $a_0 = w_0$ , and taken literally that makes the goal false. The $\lambda$ -return is an infinite series, whose tail collapses only because every $n$ -step return that reaches past termination equals the full return. That convention has to be built into the definition of $G_{t:t+n}$ , together with the terminal value $\hat v(\text{terminal}, \cdot) = 0$ . Exercises 12.3 and 12.4 are true only when the weights stay fixed. With the algorithms' changing weights $w_t$ the $n$ -step returns (12.1) use $w_{t+n-1}$ , and neither identity holds. The boundary indices ( $t = T-1$ , the empty product at $k = T-1$ , $G^\lambda_T = 0$ ) must come out right.

Formalization scope

Namespace SuttonBartoRL.Traces. Vectors of §12.6 are Fin d → ℝ, matrices Matrix (Fin d) (Fin d) ℝ, and $x x^\top$ is Matrix.vecMulVec x x. The ordered product fadeProd α x j t is $F_t \cdots F_j$ , the identity when $t < j$ . Feature sequences are indexed by $\mathbb N$ ; only $x_0, \dots, x_{T-1}$ enter. $T \ge 1$ is a hypothesis wherever $T - 1$ appears. The identities of §12.6 are stated for every real $\alpha$ and $G$ , a harmless strengthening of the book's positive step size.

For §§12.1–12.2, weights are EuclideanSpace ℝ (Fin d), $\nabla$ is Mathlib's gradient, and each $\hat v(s,\cdot)$ is assumed differentiable in Exercise 12.4. An episode is a length $T$ , states and rewards. The value at time $t \ge T$ is $0$ . (12.2) is a tsum over $n \ge 0$ of $\lambda^n G_{t:t+n+1}$ , and $\lambda \in [0,1)$ , the range the book gives with (12.2). Milestone 5 concludes summability, so the junk value of a divergent tsum cannot make it trivial. Exercises 12.3–12.4 take one weight binder w, used in every return, TD error and gradient. That is the book's fixed- $w$ assumption, stated in the binders.

Correction. The printed initialization $a_0 = w_0$ (p. 302) contradicts the printed definition $a_t \doteq F_t\cdots F_0 w_0$ and (12.14). The counterexample is $d = 1$ , $T = 1$ , $x_0 = 1$ , $\alpha = 1/2$ , $w_0 = 1$ , $G = 0$ : the forward view gives $w_1 = 1/2$ , while $a_0 + \alpha G z_0 = 1$ . The mission states the corrected result with $a_0 = F_0 w_0$ , equivalently the same recursion started from $a_{-1} = w_0$ . The printed text is kept verbatim in the milestone.

A trivializing formalization is ruled out: the goal is not the closed-form identity with $a_{T-1}$ and $z_{T-1}$ defined as the products and sums. Those vectors are defined by their $G$ -free incremental recursions, and the closed forms are separate milestones.

Out of scope: the equivalence of true online TD( $\lambda$ ) and the online $\lambda$ -return algorithm (cited, p. 300), the truncated-return identity (12.10), the error bound (12.8), and all convergence claims. Proofs of the milestones, and reuse of the definitions in later missions on true online TD( $\lambda$ ), are welcome.

Selected references

R. S. Sutton and A. G. Barto, Reinforcement Learning: An Introduction, 2nd ed., MIT Press, 2018, ISBN 9780262039246, Chapter 12, pp. 287–320. http://incompleteideas.net/book/the-book-2nd.html
R. S. Sutton, "Learning to predict by the methods of temporal differences", Machine Learning 3 (1988), 9–44. https://doi.org/10.1007/BF00115009
H. van Seijen and R. S. Sutton, "True online TD(λ)", Proceedings of ICML 2014, PMLR 32, 692–700. https://proceedings.mlr.press/v32/seijen14.html
H. van Seijen, A. R. Mahmood, P. M. Pilarski, M. C. Machado and R. S. Sutton, "True online temporal-difference learning", Journal of Machine Learning Research 17 (2016), 1–40. https://jmlr.org/papers/v17/15-599.html

11 thms2 active usersReviewed

Completed

Machine Learning Markov Chain·Captain: mikedeng1

Reinforcement Learning: An Introduction VII: The Error Reduction Property of n-step ReturnsTextbook

Motivation

Temporal-difference (TD) learning estimates the value of a policy by moving a current estimate toward a target built from observed rewards and from the estimate itself. Chapter 7 of Sutton and Barto's Reinforcement Learning: An Introduction (2nd ed., MIT Press, 2018) interpolates between the two extreme targets of the preceding chapters: the one-step TD target, which uses one reward and then bootstraps, and the Monte Carlo target, which uses every reward until the end of the episode. The intermediate target, the $n$ -step return, uses $n$ rewards and then bootstraps from the current estimate. The family underlies $n$ -step TD, $n$ -step Sarsa, the off-policy per-decision methods and the tree-backup algorithm, and it is the introduction to eligibility traces (Chapter 12).

The book justifies the whole family with one inequality, the error reduction property (7.3), p. 144: the expected $n$ -step return is closer to the true value than the estimate it bootstraps from, by a factor $\gamma^n$ in the worst state. It is the reason given for calling $n$ -step TD methods "sound". The same chapter states, mostly as exercises without solutions, a series of exact identities that rewrite each kind of $n$ -step return as a sum of one-step TD errors.

Setting

A finite Markov decision process has finite state and action sets $\mathcal S$ , $\mathcal A$ , a finite reward set $\mathcal R \subset \mathbb R$ , and dynamics $p(s', r \mid s, a)$ , the probability of next state $s'$ and reward $r$ after action $a$ in state $s$ (Eqs. (3.2)–(3.3)). A policy $\pi(a \mid s)$ is a probability distribution over actions for each state. Following $\pi$ from $S_t = s$ produces a random trajectory $A_t, R_{t+1}, S_{t+1}, A_{t+1}, R_{t+2}, \dots$ For a discount factor $0 \le \gamma < 1$ the state-value function is the expected discounted return (3.12),

v_\pi(s) = \mathbb E_\pi\Big[\sum_{k=0}^{\infty} \gamma^k R_{t+k+1} \,\Big|\, S_t = s\Big].

Given any function $V : \mathcal S \to \mathbb R$ (an estimate of $v_\pi$ ), the $n$ -step return (7.1) is

G_{t:t+n} = R_{t+1} + \gamma R_{t+2} + \cdots + \gamma^{n-1} R_{t+n} + \gamma^n V(S_{t+n}).

In an episode that terminates at time $T$ it is replaced by the complete return $G_t$ when $t + n \ge T$ . The TD error (6.5) is $\delta_k = R_{k+1} + \gamma V(S_{k+1}) - V(S_k)$ . Off-policy variants use a behavior policy $b$ that generates the data, the per-decision ratio $\rho_t = \pi(A_t \mid S_t)/b(A_t \mid S_t)$ , and the return with control variate (7.13), $G_{t:h} = \rho_t(R_{t+1} + \gamma G_{t+1:h}) + (1-\rho_t) V(S_t)$ , $G_{h:h} = V(S_h)$ . The tree-backup return (7.15)–(7.16) uses action values $Q$ and the expected approximate value $\bar V(s) = \sum_a \pi(a \mid s) Q(s, a)$ (7.8).

Formalization targets

Goal: the error reduction property (7.3)

For a finite MDP, a policy $\pi$ , $0 \le \gamma < 1$ , any $V : \mathcal S \to \mathbb R$ and every $n \ge 1$ ,

\max_s \big|\mathbb E_\pi[G_{t:t+n} \mid S_t = s] - v_\pi(s)\big| \le \gamma^n \max_s \big|V(s) - v_\pi(s)\big|.

Milestones, in the book's order

Exercise 7.1, p. 143: with $V$ fixed and $V(S_T) = 0$ , $G_{t:t+n} - V(S_t) = \sum_{k=t}^{\min(t+n,T)-1} \gamma^{k-t}\delta_k$ .
Exercise 7.4, Eq. (7.6), p. 148: the $n$ -step Sarsa return equals $Q_{t-1}(S_t, A_t) + \sum_{k=t}^{\min(t+n,T)-1} \gamma^{k-t}[R_{k+1} + \gamma Q_k(S_{k+1}, A_{k+1}) - Q_{k-1}(S_k, A_k)]$ , with estimates changing from step to step.
Eq. (7.12), p. 150: $G_{t:h} = R_{t+1} + \gamma G_{t+1:h}$ for $t < h < T$ , $G_{h:h} = V(S_h)$ .
Exercise 7.6, p. 151, for (7.13): under coverage, $\mathbb E_b$ of the control-variate return equals $\mathbb E_b$ of the same return without the control variate, and both equal $\mathbb E_\pi[G_{t:t+n} \mid S_t = s]$ .
Exercise 7.8, p. 151: $G_{t:h} - V(S_t) = \sum_{k=t}^{h-1} \gamma^{k-t} \big(\prod_{i=t}^{k}\rho_i\big) \delta_k$ for the return (7.13).
Exercise 7.11, p. 153: the tree-backup return equals $Q(S_t, A_t) + \sum_{k=t}^{\min(t+n-1,T-1)} \delta_k \prod_{i=t+1}^{k} \gamma\pi(A_i \mid S_i)$ with the expectation-based TD error $\delta_k = R_{k+1} + \gamma\bar V(S_{k+1}) - Q(S_k, A_k)$ .

Significance

The result. The error reduction property makes the expected $n$ -step target a $\gamma^n$ -contraction toward $v_\pi$ in the sup norm, uniformly over the estimate it starts from. It is the one-line reason the book offers for the soundness of every $n$ -step TD method, and the same contraction is what the $\lambda$ -return of Chapter 12 averages over $n$ . The TD-error identities are the algebra behind implementations that accumulate TD errors instead of storing returns, and behind the forward/backward-view equivalences of Chapter 12. Exercise 7.6 is the unbiasedness of the control-variate return, which is what allows (7.13) to replace plain importance weighting without changing the expected update.

Formalizing it. All results are elementary and well known, but the book gives no proofs: (7.3) is asserted, and the identities are exercises without published solutions. None is formalized on Prove2Me. The mission produces machine-checked versions with every hypothesis explicit (discounting, the fixed estimate, terminal values, coverage), and a trajectory-level expectation for finite MDPs that other chapters of the series can reuse.

Difficulty

The obvious proof of (7.3) is a matrix computation: $\mathbb E_\pi[G_{t:t+n} \mid S_t = s] - v_\pi(s) = \gamma^n (P_\pi^n (V - v_\pi))(s)$ , and a stochastic matrix does not increase the sup norm. The difficulty lies in the step before it. The left side is an expectation over trajectories, and $v_\pi$ is an infinite discounted series; neither is a matrix power by definition. Connecting them requires a Chapman–Kolmogorov identity for the finite-trajectory distribution induced by $\pi$ and $p(s', r \mid s, a)$ , the splitting of $v_\pi$ at time $n$ , and summability of the discounted series. Defining the expected $n$ -step return as the matrix expression would reduce the goal to the last line and remove its content; that shortcut is ruled out below.

The TD-error identities are telescoping sums, but each has its own boundary: termination inside the $n$ steps, the convention that terminal states have value zero, the index $Q_{-1}$ at $t = 0$ in (7.6), the special case $G_{T-1:t+n} = R_T$ of the tree backup, and ratios with vanishing denominators in (7.13).

Formalization scope

Model. The finite MDP, policies and $v_\pi$ follow the series conventions: dynamics $p(s', r \mid s, a)$ over a finite reward set, one action set for all states, $v_\pi(s) = \sum_k \gamma^k (P_\pi^k r_\pi)(s)$ computed from expected rewards and never defined as a Bellman solution.
Expectations are over trajectories. $\mathbb E_\pi[\,\cdot \mid S_t = s]$ is the finite sum over $n$ -step segments $(A_{t+k}, S_{t+k+1}, R_{t+k+1})_{k<n}$ weighted by $\prod_k \pi(A_{t+k}\mid S_{t+k})\,p(S_{t+k+1}, R_{t+k+1}\mid S_{t+k}, A_{t+k})$ . The expected $n$ -step return is not defined as $\sum_{k<n}\gamma^k P_\pi^k r_\pi + \gamma^n P_\pi^n V$ , which would make the goal a two-line matrix inequality.
The estimate is fixed. In the algorithm, $V_{t+n-1}$ is the current random estimate. Every statement takes a fixed function $V$ (or $Q$ ), which is the book's own reading ("if the value estimates don't change"). The only exception is Exercise 7.4, whose estimates $Q_k$ are indexed by time $k \in \mathbb Z$ exactly as in (7.6).
Discounting. The goal assumes $0 \le \gamma < 1$ and takes the maximum over all states. Episodic tasks enter through absorbing zero-reward terminal states. The undiscounted episodic case $\gamma = 1$ is not stated.
Episodes. Sample-path identities use sequences $S_k, A_k, R_k$ and a termination time $T$ . The book's convention that terminal states have value $0$ is a hypothesis ( $V(S_T) = 0$ , $Q(S_T, \cdot) = 0$ ).
Exercise 7.6 is stated for the state-value return (7.13) of p. 150, although the exercise follows the action-value return (7.14). Its conclusion includes, besides the literal "does not change the expected value", equality with the on-policy expected return, the property the book states on p. 150. Coverage ( $\pi(a\mid s) > 0 \Rightarrow b(a\mid s) > 0$ ) is assumed.
Not stated. The convergence of $n$ -step TD methods "under appropriate technical conditions" (p. 144), and the programming exercises.

Needed infrastructure: finite sums over function types, Chapman–Kolmogorov for the segment distribution, summability of $\sum_k \gamma^k P_\pi^k r_\pi$ . The trajectory layer is reusable for the importance-sampling and eligibility-trace chapters. Alternative proofs of the goal, and proofs of the undiscounted episodic version as a separate theorem, are welcome.

Selected references

R. S. Sutton and A. G. Barto, Reinforcement Learning: An Introduction, 2nd ed., MIT Press, 2018, ISBN 9780262039246, Chapter 7, pp. 141–158. http://incompleteideas.net/book/the-book-2nd.html
C. J. C. H. Watkins, Learning from Delayed Rewards, PhD thesis, University of Cambridge, 1989 (the $n$ -step return and its error reduction property, as credited on p. 158 of the book). https://www.cs.rhul.ac.uk/~chrisw/new_thesis.pdf
D. Precup, R. S. Sutton and S. Singh, Eligibility traces for off-policy policy evaluation, Proceedings of the 17th International Conference on Machine Learning (ICML), 2000, pp. 759–766 (the tree-backup algorithm, as credited on p. 158 of the book; no DOI).

10 thms2 active usersReviewed

Completed

Machine Learning Probability·Captain: mikedeng1

Minimax Regret Bounds for Reinforcement Learning I: High-Probability Regret Bound for UCBVI with a Chernoff–Hoeffding BonusResearch Paper

Motivation

An agent learning to control an unknown environment must balance rewards it can collect now against information that improves later decisions. In a finite Markov decision process (MDP), every action changes the distribution of the next state, so a mistaken transition estimate can affect decisions many steps later. Regret measures this loss against a policy that already knows the transition probabilities. The paper of Azar, Osband and Munos gives high-probability regret bounds for two variants of upper confidence bound value iteration (UCBVI) in finite-horizon reinforcement learning. This mission targets its Chernoff–Hoeffding variant, UCBVI-CH, whose bonus depends only on the horizon and the visit count. Theorem 1 improves the paper's cited earlier dependence on the number of states from $S$ to $\sqrt S$ in the leading term for sufficiently many interactions. Azar, Osband and Munos, 2017, pp. 2, 4–5.

The paper was released in 2017 alongside work on the attainable dependence of episodic regret on the horizon $H$ , state count $S$ , action count $A$ , and total interaction time $T$ . Its second algorithm, UCBVI-BF, uses a variance-dependent bonus and is the subject of the next mission in this series. UCBVI-CH has a simpler bonus and its own explicit bound, making it a distinct mathematical target. Azar, Osband and Munos, 2017, pp. 1–5.

Setting

The state set $\mathcal S$ and action set $\mathcal A$ are finite and nonempty, with cardinalities $S$ and $A$ . A stationary transition kernel $P(y\mid x,a)$ gives the probability of moving to state $y$ after action $a$ in state $x$ ; each row is nonnegative and sums to one. The known, deterministic reward $R(x,a)$ lies in $[0,1]$ . An episode lasts $H\ge1$ steps. The environment chooses its starting state $x_{k,1}$ before episode $k$ and may base that choice on earlier episodes. It cannot see the current episode's future random draws. Azar, Osband and Munos, 2017, §2 and Assumption 1, pp. 2–3.

A policy $\pi$ selects an action from the current state and the step number. Its value $V_h^\pi(x)$ is the expected sum of rewards from step $h$ through step $H$ when starting in state $x$ . The terminal value is $V_{H+1}^\pi=0$ , and $V_h^*(x)$ is the maximum of $V_h^\pi(x)$ over all such policies. Since the state, action and step sets are finite, this maximum is over a finite nonempty policy class. The paper's sentence describing $H-h$ rewards uses a shifted terminal convention; this series follows the $H$ reward steps of Algorithms 1–2. Azar, Osband and Munos, 2017, pp. 3–4.

At the start of episode $k$ , UCBVI-CH forms visit counts $N_k(x,a,y)$ and $N_k(x,a)$ from earlier completed transitions. On a visited pair it uses the empirical row $\widehat P_k(y\mid x,a)=N_k(x,a,y)/N_k(x,a)$ . Algorithm 2 computes values backward from zero at the terminal step. For a visited pair, $Q_{k,h}(x,a)$ is the minimum of the preceding episode's $Q_{k-1,h}(x,a)$ , $H$ , and the empirical Bellman value plus Algorithm 3's bonus. For an unvisited pair, $Q_{k,h}(x,a)=H$ . A maximizing action is chosen at every state, including states outside the realized path. Azar, Osband and Munos, 2017, Algorithms 1–3, pp. 3–4.

Formalization targets

Theorem 1: UCBVI-CH regret

For $K$ episodes and $T=KH$ , regret sums the gap $V_1^*(x_{k,1})-V_1^{\pi_k}(x_{k,1})$ . The goal is the paper's printed bound, with its constants:

\Pr\!\left\{\operatorname{Regret}(K)>20H^{3/2}L\sqrt{SAK}+250H^2S^2AL^2\right\}\le\delta, \qquad L=\ln(5HSAT/\delta),\quad \delta>0.

Algorithm 3 itself uses $L_{\rm alg}=\ln(5SAT/\delta)$ in its bonus $7HL_{\rm alg}/\sqrt{N_k(x,a)}$ . Both logarithms remain as printed. The probability is over the MDP's next-state draws, for every admissible starting-state rule and every way of breaking ties between maximizing actions. Azar, Osband and Munos, 2017, Algorithm 3, p. 4; Theorem 1, p. 5.

Supporting results

Four milestones retain the source's indexed attack path: the Bernstein bound (9) for the empirical value error, the count-deviation display before (11), Lemma 18 on optimism, and the weighted recursion displayed in the proof of Lemma 3. The last milestone preserves the signed weights that appear before the paper's final simplification. Azar, Osband and Munos, 2017, pp. 17, 20–21, 28.

Significance

Theorem 1 gives a finite-sample failure probability with explicit dependence on $H,S,A,K$ and $\delta$ . It covers a learner whose initial state can change between episodes, a feature that matters in episodic learning where the experimenter does not fix a single starting distribution. For the regime stated after Theorem 1, the leading rate is $\widetilde O(H\sqrt{SAT})$ . This is a result claimed by the paper; the present Lean declarations are open proof targets, not machine-checked proofs of that claim. Azar, Osband and Munos, 2017, p. 5.

Formalizing the result creates reusable finite objects for adaptive interaction: a constructed probability law on complete paths, empirical transition counts pooled across steps, a policy value defined by its expected reward, and confidence events with their domains stated explicitly. The concentration and optimism milestones can then be investigated independently of the final regret bound. The later UCBVI-BF mission uses the same paper's model with a different bonus. Azar, Osband and Munos, 2017, pp. 3–5, 14–17.

Difficulty

The visit count $N_k(x,a)$ is random and depends on earlier observations and decisions. A concentration inequality for a predetermined number of samples therefore does not immediately give a statement that holds at every episode start. The algorithm also reuses the previous episode's $Q$ estimate through a minimum. Any optimism claim must account for this dependence across episodes as well as the backward dependence across steps. In the regret analysis, the terms called martingale differences can have either sign, so replacing a positive weight by a larger common bound can reverse an inequality. These are concrete obstacles to the printed chain of estimates. Azar, Osband and Munos, 2017, pp. 4, 17, 20–21, 28.

Formalization scope

States, actions, steps, episodes and complete outcome arrays are finite. Probabilities are finite sums of products of transition rows. The transition-row predicate is a published general definition; this mission defines the paper-specific reward-bounded MDP, policies, UCBVI-CH recursion, and path law on top of it. The starting-state rule can inspect only earlier episodes. Greedy tie-breaking is universally quantified. $V^*$ is a maximum over policies, and the bonus is read only at positive counts. A model that assigns an arbitrary probability law, fixes one starting state, or omits Algorithm 2's minimum does not represent this target. Azar, Osband and Munos, 2017, pp. 2–4.

Lean uses steps $0,\dots,H-1$ and terminal index $H$ in place of the paper's algorithmic $1,\dots,H+1$ . The appendix sometimes puts the terminal value at $H$ . The weighted recursion therefore runs through the final reward step, rather than ending one step early. Its typical-state threshold is $4H^2L$ , as required by (34)–(36), whereas Appendix B.1 prints $2H^2L$ . The proof's correction term $c_4$ dominates its other terms under $A\ge2$ , which is made explicit in that milestone. The printed (11) loses a factor of two from the count display before it; only the preceding display is a milestone. Lemma 18 is stated under the empirical-model part of the confidence event and $\delta\le1$ , the domain on which its bonus comparison holds. The weighted milestone retains its coefficients because the bracketed martingale terms can be negative. Azar, Osband and Munos, 2017, pp. 14–17, 20–21, 28.

The goal retains Theorem 1's constant $20$ . Appendix C.1 cites Lemmas 15 and 18, but the sketch of Lemma 15 does not track that constant explicitly. Formalizing the printed bound may therefore expose a gap in its proof; the mission records the claim without weakening its constants. Contributions establishing or repairing the explicit bound, as well as the four stated milestones and reusable finite concentration results, are within scope. Azar, Osband and Munos, 2017, pp. 5, 27, 29.

Selected references

M. G. Azar, I. Osband and R. Munos, Minimax Regret Bounds for Reinforcement Learning, arXiv:1703.05449v2, 2017. Pinned preprint.

9 thms2 active usersReviewed

Completed

Machine Learning Markov Chain Statistics·Captain: mikedeng1

Reinforcement Learning: An Introduction VI: Batch TD(0) Converges to the Certainty-Equivalence EstimateTextbook

Why batch TD(0) and batch Monte Carlo disagree

Temporal-difference (TD) learning estimates the value of each state of a Markov reward process from observed experience, updating an estimate toward a target built from the next reward and the current estimate of the next state. Monte Carlo (MC) methods instead update toward the full observed return. Both are standard prediction methods in reinforcement learning, and their relationship is a recurring question of the field (Sutton 1988).

When only a finite amount of experience is available, a common practice is to present the same data repeatedly until the estimates stop changing. Chapter 6 of Sutton and Barto's Reinforcement Learning: An Introduction (2nd ed., MIT Press, 2018) uses this setting to explain why TD(0) is often faster: under such batch updating, both methods converge deterministically, but to different answers. Batch MC finds the least-squares fit to the observed returns; batch TD(0) finds the value function of the maximum-likelihood Markov model of the data, the certainty-equivalence estimate. The comparison appears in §6.3, Optimality of TD(0) (pp. 126–128), and is illustrated by Example 6.4, You are the Predictor. The book states these conclusions without proof. This mission formalizes them.

Setting

Let $\mathcal S$ be a finite set of nonterminal states and $\mathcal S^+ = \mathcal S \cup \{\text{terminal}\}$ . An episode is a finite sequence $S_0, R_1, S_1, \dots, S_{T-1}, R_T, S_T$ with $S_0, \dots, S_{T-1} \in \mathcal S$ , real rewards $R_1, \dots, R_T$ , and $S_T$ terminal. A batch is a finite list of episodes. A visit of $s$ is an (episode, time $t < T$ ) pair with $S_t = s$ , and $n(s)$ counts all visits (every-visit counting).

A value array $V : \mathcal S \to \mathbb R$ is extended by $V(\text{terminal}) = 0$ . For a discount rate $\gamma \in [0,1]$ , the return is $G_t = \sum_{k=t+1}^{T}\gamma^{k-t-1}R_k$ and the TD error is $\delta_t = R_{t+1} + \gamma V(S_{t+1}) - V(S_t)$ .

Batch TD(0) with step size $\alpha$ computes the TD(0) increment for every visit in the batch and changes $V$ once, by their sum:

V_{m+1}(s) = V_m(s) + \alpha\sum_{\text{visits } t \text{ of } s}\big[R_{t+1} + \gamma V_m(S_{t+1}) - V_m(S_t)\big].

Batch constant- $\alpha$ MC is the same iteration with the increment $G_t - V_m(S_t)$ .

The maximum-likelihood model of the batch has transition probabilities $\hat p(j \mid i) = N(i,j)/n(i)$ , where $N(i,j)$ counts the observed transitions from $i$ to $j \in \mathcal S^+$ , and expected rewards $\hat r(i,j)$ equal to the average reward observed on those transitions. With $\hat P = (\hat p(s'\mid s))_{s,s'\in\mathcal S}$ and $\hat r(s) = \sum_j \hat p(j\mid s)\hat r(s,j)$ , the certainty-equivalence estimate is the value function of this Markov reward process,

\hat v(s) = \sum_{k\ge0}\gamma^k\big(\hat P^k\hat r\big)(s).

Formalization targets

Goal: batch TD(0) converges to the certainty-equivalence estimate

For every finite batch and every $\gamma \in [0,1]$ , the series defining $\hat v$ converges, and there is $\bar\alpha > 0$ such that for all $\alpha \in (0,\bar\alpha)$ and all initial arrays $V_0$ ,

\lim_{m\to\infty} V_m(s) = \hat v(s)\quad\text{for every visited } s, \qquad V_m(s) = V_0(s)\ \text{otherwise}.

The limit depends neither on $\alpha$ nor on $V_0$ at visited states.

Milestones

(6.6): with $V$ held fixed, $G_t - V(S_t) = \sum_{k=t}^{T-1}\gamma^{k-t}\delta_k$ .
Exercise 6.8: the same identity for action values, $\delta_t = R_{t+1} + \gamma Q(S_{t+1},A_{t+1}) - Q(S_t,A_t)$ .
Least squares: the sample averages $\bar G(s)$ of the returns after the visits to $s$ minimize $\sum_{\text{visits}}(G_t - V(S_t))^2$ over all arrays $V$ .
Batch MC: for small $\alpha$ , batch constant- $\alpha$ MC converges to $\bar G(s)$ at every visited $s$ .
Fixed points: the batch TD(0) increments vanish everywhere if and only if $V = \hat v$ on visited states.
Example 6.4: on the eight episodes $A,0,B,0$ ; $B,1$ (six times); $B,0$ with $\gamma = 1$ , the certainty-equivalence estimate is $\hat v(A) = \hat v(B) = 3/4$ and batch TD(0) converges to it, while batch MC converges to $V(A) = 0$ , $V(B) = 3/4$ .

Significance

The result explains the empirical observation of Figure 6.2 in the book: batch TD(0) has lower error than batch MC on Markov data, because it computes the certainty-equivalence estimate, while batch MC fits the training returns. It also gives a precise meaning to the claim that TD methods approximate the certainty-equivalence solution with memory linear in the number of states, where computing it directly needs a model of quadratic size and cubic time (p. 128). Identity (6.6) is the starting point of the $n$ -step and eligibility-trace methods of later chapters.

The comparison under repeated presentation of a finite training set goes back to Sutton 1988, but the textbook states the conclusions without proof, and no machine-checked version is known to exist. The formalization pins down every hypothesis the text leaves implicit: the step-size threshold, the treatment of unvisited states, every-visit counting, and the undiscounted case.

Difficulty

The fixed-point equation of batch TD(0) is $D(\hat r + \gamma\hat PV - V) = 0$ on visited states, with $D$ the diagonal of visit counts, and convergence of the iteration $V \mapsto V + \alpha D(\hat r + \gamma\hat P V - V)$ requires every eigenvalue of $D(I - \gamma\hat P)$ to have positive real part. For $\gamma < 1$ this follows from $\hat P$ being substochastic. For $\gamma = 1$ , the case of Example 6.4, $\hat P$ is only substochastic and the naive contraction argument fails: invertibility of $I - \hat P$ must be derived from the structure of the data, since every episode ends in the terminal state. The matrix $D(I - \gamma\hat P)$ is not symmetric, so symmetric positive-definiteness arguments do not apply. The same issue makes convergence of the series defining $\hat v$ nontrivial at $\gamma = 1$ .

Formalization scope

An episode is a Lean List (X × ℝ) of transitions $(S_t, R_{t+1})$ , with the terminal state represented by none : Option X; a batch is a list of episodes; states form a Fintype. Values at the terminal state are $0$ by definition. The certainty-equivalence estimate is defined from returns as the series $\sum_k\gamma^k\hat P^k\hat r$ , not as the solution of a Bellman equation, and its convergence is part of the goal, not assumed. "Sufficiently small $\alpha$ " is an existential threshold $\bar\alpha > 0$ quantified before $\alpha$ and $V_0$ ; a statement for one fixed $\alpha$ , or for some $\alpha$ , would be weaker than the book's and is ruled out. Unvisited states receive no increment and keep their initial value; the goal records this rather than claiming convergence to $\hat v$ there. The standing assumption $\gamma \in [0,1]$ includes $\gamma = 1$ . Every visit is counted in both the TD increments and the model; mixing first-visit and every-visit counts would make the goal false.

The mission needs only finite sums, matrix powers and limits of real sequences; Mathlib's Matrix and Filter.Tendsto suffice. A lemma that a nonnegative matrix whose rows reach an absorbing mass has spectral radius below one would be reusable beyond this mission, as would a convergence criterion for $V \mapsto V + \alpha(b - MV)$ when $M$ is a nonsingular M-matrix. Contributions of either kind, and of the elementary milestones 1–3, are welcome.

Selected references

Richard S. Sutton and Andrew G. Barto, Reinforcement Learning: An Introduction, 2nd ed., MIT Press, 2018, ISBN 9780262039246, §6.1 and §6.3, pp. 119–129. http://incompleteideas.net/book/the-book-2nd.html
Richard S. Sutton, Learning to predict by the methods of temporal differences, Machine Learning 3, 9–44, 1988. https://doi.org/10.1007/BF00115009

9 thms2 active usersReviewed

Completed

Dynamic Programming Machine Learning Optimization·Captain: mikedeng1

Reinforcement Learning: An Introduction III: The Policy Improvement Theorem and Policy IterationTextbook

Why policy improvement matters

Reinforcement learning methods search for good behaviour by alternating two activities: estimating how good the current behaviour is, and changing the behaviour in the direction those estimates suggest. Sutton and Barto call this pattern generalized policy iteration and use it as the organizing idea of their textbook (Sutton & Barto 2018, §4.6). Its mathematical justification is a single result of Chapter 4, the policy improvement theorem (p. 78): a comparison made one step ahead, at each state separately, certifies that a changed policy is at least as good everywhere. Policy iteration, value iteration, Monte Carlo control with ε-greedy policies (Chapter 5), Sarsa and Q-learning are all motivated by it.

The chapter's results go back to the foundations of dynamic programming: the Bellman optimality equation (Bellman 1957), and policy iteration with its finite termination for discounted finite Markov decision processes (Howard 1960). Standard modern treatments are Puterman 1994, Ch. 6, and Bertsekas 2012, Vol. II, Ch. 1.

Setting

A finite Markov decision process has a finite state set $\mathcal S$ , a finite nonempty action set $\mathcal A$ , a finite reward set $\mathcal R\subset\mathbb R$ and dynamics $p(s', r\mid s, a)$ : for each state $s$ and action $a$ , a probability distribution over the next state $s'$ and reward $r$ (Eqs. (3.2)–(3.3)). A policy $\pi$ gives probabilities $\pi(a\mid s)$ of choosing each action in each state; a deterministic policy is a map $\pi:\mathcal S\to\mathcal A$ .

Fix a discount rate $0\le\gamma<1$ . The state-value function of $\pi$ is the expected discounted return

v_\pi(s) = E_\pi\Big[\sum_{k=0}^\infty \gamma^k R_{t+k+1}\ \Big|\ S_t=s\Big],

and the action-value function is defined from it by (4.6):

q_\pi(s,a) = \sum_{s',r} p(s',r\mid s,a)\,\big[r+\gamma v_\pi(s')\big],

the value of taking $a$ once in $s$ and following $\pi$ afterwards. A policy is optimal if its value is at least that of every policy at every state, and the optimal value function is $v_*(s)=\max_\pi v_\pi(s)$ . A deterministic policy $\pi'$ is greedy with respect to $q_\pi$ if $\pi'(s)\in\operatorname{argmax}_a q_\pi(s,a)$ for all $s$ (4.9).

Formalization targets

Goal: the policy improvement theorem, (4.7)–(4.8), p. 78

For deterministic policies $\pi,\pi'$ ,

\big(\forall s,\ q_\pi(s,\pi'(s))\ge v_\pi(s)\big)\ \Longrightarrow\ \big(\forall s,\ v_{\pi'}(s)\ge v_\pi(s)\big),

and at every state where the hypothesis is strict, the conclusion is strict at that same state.

Milestones

Iterative policy evaluation (4.5), p. 74. From any $v_0$ , the iterates $v_{k+1}(s)=\sum_a\pi(a\mid s)\sum_{s',r}p(s',r\mid s,a)[r+\gamma v_k(s')]$ converge to $v_\pi$ .
Greedy improvement (4.9), p. 79. A greedy $\pi'$ with respect to $q_\pi$ satisfies (4.7), hence $v_{\pi'}\ge v_\pi$ .
The stochastic case, p. 79. For stochastic $\pi,\pi'$ , with $q_\pi(s,\pi'(s))=\sum_a\pi'(a\mid s)q_\pi(s,a)$ as in (5.2), the theorem holds as stated, strictness included.
Equality forces optimality, p. 79. If a greedy $\pi'$ has $v_{\pi'}=v_\pi$ , then $v_{\pi'}$ solves the Bellman optimality equation (4.1), $v_{\pi'}=v_*$ , and $\pi$ and $\pi'$ are optimal.
Policy iteration, p. 80. For every sequence of deterministic policies with $\pi_{k+1}$ greedy with respect to $q_{\pi_k}$ : each step is a strict improvement unless $\pi_k$ is optimal, and from some $K$ on every $\pi_k$ is optimal with $v_{\pi_k}=v_*$ .
Value iteration (4.10), p. 83. $v_*$ is attained by one policy at all states, and from any $v_0$ the iterates $v_{k+1}(s)=\max_a\sum_{s',r}p(s',r\mid s,a)[r+\gamma v_k(s')]$ converge to $v_*$ .

Significance

The results. The policy improvement theorem turns a local test into a global guarantee: it is enough to check, state by state, that one step of the new policy followed by the old one does no worse than the old one. Combined with the finiteness of the set of deterministic policies, it yields the finite termination of policy iteration and, with the equality case, the existence of a deterministic optimal policy. The stochastic form is what Chapter 5 invokes for ε-greedy control. Value iteration is the other classical way to compute $v_*$ .

Formalizing them. All of these results are classical and proved in the literature cited above; they are not open. The textbook presents them informally ("we chose not to produce a rigorous formal treatment", p. xiii): the improvement theorem is argued by an unbounded chain of expansions, and the policy evaluation and value iteration convergence claims are stated without proof. The mission makes each claim precise with explicit hypotheses and asks for machine-checked proofs against the book's own model with four-argument dynamics and stochastic policies. Related platform results use different models (cost minimization with deterministic policies in Bertsekas's Dynamic Programming; an expected-reward kernel and an assumed fixed point in Foundations of Machine Learning), and none states the policy improvement theorem itself.

Difficulty

The book's proof expands $q_\pi$ with (4.6) and reapplies (4.7) indefinitely, ending with " $\le\cdots=v_{\pi'}(s)$ ". Made rigorous, the chain is an inequality between truncated returns plus a remainder $\gamma^n E_{\pi'}[v_\pi(S_{t+n})]$ , and the passage to the limit needs the remainder to vanish and the truncated returns to converge to $v_{\pi'}$ . Since $v_\pi$ is defined here as a series of expected rewards under the induced Markov chain, connecting it to the one-step quantities requires first establishing the Bellman equation for $v_\pi$ from that series. The strictness part does not follow from the weak inequality alone: strictness at one state must be shown to survive the averaging over later states, which requires tracking the contribution of the first step exactly. The policy iteration statement additionally requires handling ties: a greedy step taken from an optimal policy can move to a different optimal policy, so the sequence need not become constant.

Formalization scope

All objects live in the namespace SuttonBartoRL.DP. States and actions are finite types, actions nonempty where a maximum is taken; one action set serves all states (footnote 3, p. 48). Rewards form a finite set $\mathcal R\subset\mathbb R$ , and the dynamics are a function $p(s',r\mid s,a)$ whose values off $\mathcal R$ are never used. Policies are stochastic; deterministic policies are embedded as policies that choose one action with probability one.

Committed conventions:

Discount $0\le\gamma<1$ throughout. The book also allows $\gamma=1$ when "eventual termination is guaranteed" (p. 74) but never states that hypothesis precisely; the episodic case with a terminal state is out of scope. This is the only restriction relative to the text.
$v_\pi$ from returns. $v_\pi(s)=\sum_k\gamma^k(P_\pi^k r_\pi)(s)$ , with $P_\pi$ the state transition matrix of $\pi$ and $r_\pi$ its expected one-step reward. $q_\pi$ is defined by (4.6), as the book does. The Bellman equation (4.4) is not assumed. Defining $v_\pi$ as the fixed point of a Bellman operator would make the goal an order property of that operator and is excluded.
$v_*$ is the real supremum over all stochastic policies; the value iteration item also asserts it is attained. Optimality of a policy means dominance over all stochastic policies.
Greedy means $\pi'(s)$ is any maximizer of $q_\pi(s,\cdot)$ ; tie-breaking is arbitrary and may differ between iterations.
Stochastic case. The book only says the theorem "carries through as stated"; the meaning $q_\pi(s,\pi'(s))=\sum_a\pi'(a\mid s)q_\pi(s,a)$ is taken from the book's (5.2), p. 101.
Policy iteration is the idealized sequence with exact evaluation. The item does not claim that the boxed pseudocode on p. 80 stops, which it may fail to do under ties (Exercise 4.4, p. 82).
Convergence of iterates is in the product topology on $\mathbb R^{\mathcal S}$ , equivalent to the sup norm for finite $\mathcal S$ .

In-place (asynchronous) sweeps (§4.5) and truncated policy iteration are not formalized.

Needed infrastructure: summability of discounted series of bounded expected rewards, the Bellman equation for $v_\pi$ derived from the return definition, contraction arguments in the sup norm on $\mathbb R^{\mathcal S}$ , and finiteness of the set of deterministic policies. The definitions here duplicate those of the series' Chapter 3 mission and are intended to be merged with them; lemmas about $v_\pi$ , the Bellman equation and contraction are reusable by every later mission of the series, and contributions of such lemmas are welcome.

Selected references

R. S. Sutton and A. G. Barto, Reinforcement Learning: An Introduction, 2nd ed., MIT Press, 2018, ISBN 9780262039246, Chapter 4. http://incompleteideas.net/book/the-book-2nd.html
R. Bellman, Dynamic Programming, Princeton University Press, 1957. https://press.princeton.edu/books/paperback/9780691146683/dynamic-programming
R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960. https://mitpress.mit.edu/9780262080095/dynamic-programming-and-markov-processes/
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887
D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. II, 4th ed., Athena Scientific, 2012. http://www.athenasc.com/dpbook.html

9 thms2 active usersReviewed

Completed

Dynamic Programming Machine Learning Markov Chain·Captain: mikedeng1

Reinforcement Learning: An Introduction II: The Bellman Optimality Equation and the Existence of an Optimal PolicyTextbook

Motivation

Sutton and Barto's Reinforcement Learning: An Introduction (2nd ed., MIT Press, 2018) is the standard introductory text of the field. Its Chapter 3 sets up the model that the rest of Part I works in: the finite Markov decision process (MDP), the value functions of a policy, and the Bellman equations that relate the value of a state to the values of its successors. Section 3.6 then states the fact every planning and control method of the book relies on: in a finite MDP there is an optimal policy, its value is the unique solution of a system of nonlinear equations, and a policy that acts greedily with respect to that solution is optimal. Dynamic programming (Chapter 4), Monte Carlo control (Chapter 5), Sarsa and Q-learning (Chapter 6) are all methods for solving the Bellman optimality equation; their correctness statements presuppose that it has exactly one solution and that it identifies optimal behaviour.

The book is deliberately informal ("we chose not to produce a rigorous formal treatment", p. xiii): §3.6 asserts these facts without proof. The results themselves are classical, going back to Bellman (1957), Howard (1960) and Blackwell (1965); a textbook proof for discounted finite MDPs is in Puterman, Markov Decision Processes (Wiley, 1994), Chapter 6.

Setting

A finite MDP has a finite set of states $\mathcal S$ , a finite nonempty set of actions $\mathcal A$ , a finite set of rewards $\mathcal R \subset \mathbb R$ , and dynamics

p(s', r \mid s, a) = \Pr\{S_t = s', R_t = r \mid S_{t-1} = s, A_{t-1} = a\}, \qquad \sum_{s' \in \mathcal S}\sum_{r \in \mathcal R} p(s', r \mid s, a) = 1,

Eqs. (3.2)–(3.3). From $p$ one derives $p(s' \mid s, a) = \sum_r p(s', r \mid s, a)$ and $r(s, a) = \sum_r r \sum_{s'} p(s', r \mid s, a)$ , Eqs. (3.4)–(3.5).

A policy $\pi$ gives a probability $\pi(a \mid s)$ of each action in each state. Fix a discount rate $0 \le \gamma < 1$ . The return of a reward sequence is $G_t = \sum_{k \ge 0} \gamma^k R_{t+k+1}$ (3.8). The state-value function and action-value function of $\pi$ are the expected returns

v_\pi(s) = \mathbb E_\pi[G_t \mid S_t = s], \qquad q_\pi(s, a) = \mathbb E_\pi[G_t \mid S_t = s, A_t = a] \qquad (3.12)\text{–}(3.13).

In the Lean development these are stateValue M γ π s and actionValue M γ π s a, computed as $\sum_k \gamma^k (P_\pi^k r_\pi)(s)$ from the transition matrix $P_\pi(s, s') = \sum_a \pi(a \mid s)\,p(s' \mid s, a)$ and the expected reward $r_\pi(s) = \sum_a \pi(a \mid s)\,r(s, a)$ of the Markov chain the policy induces. A policy $\pi$ is optimal (IsOptimalPolicy) if $v_\pi(s) \ge v_{\pi'}(s)$ for every policy $\pi'$ and every state $s$ . The optimal value functions are

v_*(s) = \max_\pi v_\pi(s) \quad (3.15), \qquad q_*(s, a) = \max_\pi q_\pi(s, a) \quad (3.16),

optimalValue and optimalActionValue, with the maximum over all stochastic policies.

Formalization targets

Goal: the Bellman optimality equation and optimal policies (§3.6, pp. 62–64)

For every finite MDP and $0 \le \gamma < 1$ :

the maximum in (3.15) is attained at every state;
an optimal policy exists;
$v_*$ satisfies the Bellman optimality equation

v_*(s) = \max_{a} \sum_{s', r} p(s', r \mid s, a)\big[r + \gamma v_*(s')\big] \quad \text{for all } s; \qquad (3.19)

$v_*$ is the only function on $\mathcal S$ satisfying (3.19);
every policy that assigns positive probability only to actions attaining the maximum in (3.19) is optimal.

Milestones

(3.9) $G_t = R_{t+1} + \gamma G_{t+1}$ for bounded rewards, with the series convergent.
(3.14) the Bellman equation $v_\pi(s) = \sum_a \pi(a \mid s) \sum_{s', r} p(s', r \mid s, a)[r + \gamma v_\pi(s')]$ , and (p. 60) its uniqueness: $v_\pi$ is its only solution.
Exercise 3.15 adding a constant $c$ to all rewards adds $v_c = c/(1-\gamma)$ to every value.
Exercises 3.18 and 3.19 $v_\pi(s) = \sum_a \pi(a \mid s)\,q_\pi(s, a)$ and $q_\pi(s, a) = \sum_{s', r} p(s', r \mid s, a)[r + \gamma v_\pi(s')]$ .
(3.16)–(3.17) the maximum defining $q_*$ is attained and $q_*(s, a) = \sum_{s', r} p(s', r \mid s, a)[r + \gamma v_*(s')]$ .
(3.20) the Bellman optimality equation for action values, $q_*(s, a) = \sum_{s', r} p(s', r \mid s, a)[r + \gamma \max_{a'} q_*(s', a')]$ .

Significance

The goal is what turns "find a good policy" into "solve a system of equations". Parts 3 and 4 identify $v_*$ with the unique solution of (3.19), so any procedure that finds a solution of (3.19) has found $v_*$ ; part 5 converts $v_*$ into an optimal policy by a one-step search. Parts 1 and 2 say that the book's definition (3.15) makes sense: a single policy is simultaneously best at every state, so "the optimal value function" is well defined and shared by all optimal policies. Chapter 4's policy iteration and value iteration, and the fixed points of Q-learning, are statements about this equation. Exercises 3.18 and 3.19 are used, by number, in the proof of the policy gradient theorem (p. 325).

The mathematics is classical and proved in many texts; what is missing is a machine-checked version in the book's own model. Platform relatives exist in different models: FoundationsML.ReinforcementLearning.bellman_equations_unique_solution (uniqueness for a fixed policy, with an expected-reward kernel instead of $p(s', r \mid s, a)$ ), BertsekasDP.discounted_main_theorem (cost minimization over deterministic stationary policies), BanditAlgorithm.mdp_discounted_bellman_solution (existence of a solution with a greedy deterministic policy, rewards in $[0,1]$ ) and FoundationsRL.RLBasics.bellman_optimality (finite horizon). None of them states the book's result: the four-argument dynamics, stochastic policies, the maximum over all of them, uniqueness of the solution of (3.19), and optimality of every policy supported on greedy actions. This mission produces that statement and, with it, a vocabulary of finite-MDP definitions that the later missions of the series reuse.

Difficulty

The book's derivation of (3.19) (p. 63) starts from $v_*(s) = \max_a q_{\pi_*}(s, a)$ with a policy $\pi_*$ that is optimal at every state at once. The existence of such a policy is the substance of the goal, and it does not follow from the definition: (3.15) takes a separate maximum at each state, and a priori the maximizing policy could depend on the state. Uniqueness for (3.19) is likewise not a consequence of linear algebra, as it is for (3.14): the equation is nonlinear because of the maximum. The fixed point must be related to the value of an actual policy, and every policy's value must be bounded above by it.

Formalization scope

Model. S and A are finite types with A nonempty (without an action, $\max_a$ is undefined). One action set serves every state, as the book's footnote 3 (p. 48) allows. Rewards form a finite set M.R : Finset ℝ and the dynamics are the four-argument M.p s a s' r with the normalization (3.3).
Discounting. All statements assume $0 \le \gamma < 1$ (the continuing discounted case of §3.3). The episodic case with $\gamma = 1$ is not covered: the book's uniqueness claims then need every episode to terminate under every policy, which the chapter never states, and without it (3.19) can have many solutions (a state that loops to itself with reward $0$ satisfies $v(s) = v(s)$ for any value).
Value functions from returns. $v_\pi$ and $q_\pi$ are expected discounted returns, computed from the Markov chain the policy induces. They are not defined as solutions of the Bellman equations, and $v_*$ is not defined as a solution of (3.19): either would make the goal true by definition. The Bellman equations are theorems.
Maxima. $v_*$ and $q_*$ are real suprema over the type of stochastic policies (Lean gives a supremum that does not exist the value $0$ ); the goal and milestone (3.17) assert that these suprema are attained, so they are the book's maxima.
Conditional expectations. (3.17), (3.18) and (3.20) are stated in their finite-sum form over $(s', r)$ .
Exercises. Exercises 3.15, 3.18 and 3.19 have no printed solutions; the statements give the formalization's answers ( $v_c = c/(1-\gamma)$ and the two displayed identities).
Reusable infrastructure. The definitions (MDP, Policy, trans, expReward, policyTrans, policyReward, stateValue, actionValue, optimalValue, optimalActionValue, IsOptimalPolicy) follow the conventions shared by the whole series and are meant to be merged with the finite-MDP layers of the later chapters. Lemmas on summability of the value series, the Bellman operator as a $\gamma$ -contraction in the sup norm, and the Markov-chain identities for $P_\pi^k$ are welcome as separate contributions.

Selected references

R. S. Sutton, A. G. Barto, Reinforcement Learning: An Introduction, 2nd ed., MIT Press, 2018, ISBN 9780262039246, Chapter 3. http://incompleteideas.net/book/the-book-2nd.html
R. Bellman, Dynamic Programming, Princeton University Press, 1957. https://doi.org/10.2307/j.ctv1nxcw0f
R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
D. Blackwell, "Discounted dynamic programming", Annals of Mathematical Statistics 36(1), 1965, 226–235. https://doi.org/10.1214/aoms/1177700285
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

11 thms2 active usersReviewed

Completed

Bandit Algorithms Machine Learning Optimization·Captain: mikedeng1

Reinforcement Learning: An Introduction I: The Gradient Bandit Algorithm Is Stochastic Gradient AscentTextbook

Motivation

The multi-armed bandit is the simplest setting in which a learner must trade off exploiting what it knows against exploring what it does not: one situation, $k$ actions, and a reward drawn from an unknown distribution each time an action is taken. Chapter 2 of Sutton and Barto's Reinforcement Learning: An Introduction (2nd ed., MIT Press, 2018) uses it to introduce, in the smallest possible setting, ideas that run through the rest of the book: incremental estimation with a step size, the bias introduced by the initial estimate, soft-max policies over learned preferences, and learning by following the gradient of expected reward.

The chapter ends with the gradient bandit algorithm (§2.8), which learns a numerical preference for each action instead of a value estimate. A shaded box on pp. 38–40 shows that its expected update is exactly a gradient-ascent step on the expected reward, so the algorithm is an instance of stochastic gradient ascent. The same argument, a score-function (likelihood-ratio) identity with a baseline, reappears in Chapter 13 as the REINFORCE algorithm and the policy gradient theorem. The bandit case is where the book first carries it out in full.

Setting

Actions are $1, \dots, k$ . Each action $x$ has a reward distribution $\nu_x$ on $\mathbb R$ with finite mean $q_*(x)$ , the true action value. At each step the learner holds a vector of action preferences $H = (H(1), \dots, H(k)) \in \mathbb R^k$ and selects action $A$ with the soft-max probability

\pi(a) = \frac{e^{H(a)}}{\sum_{b=1}^k e^{H(b)}} \qquad (2.11).

Given $A = x$ , a reward $R \sim \nu_x$ is received. The expected reward is $\mathbb E[R] = \sum_x \pi(x)\, q_*(x)$ , a smooth function of $H$ . With a step size $\alpha > 0$ and a baseline $B \in \mathbb R$ , the gradient bandit update (2.12) is

H'(A) = H(A) + \alpha (R - B)(1 - \pi(A)), \qquad H'(a) = H(a) - \alpha (R - B)\,\pi(a) \ \ (a \ne A).

The chapter's estimation sections use a single action's rewards $R_1, R_2, \dots$ . The sample average after $n-1$ selections is $Q_n = (R_1 + \cdots + R_{n-1})/(n-1)$ , with an arbitrary initial value $Q_1$ . A constant step size $\alpha \in (0,1]$ updates $Q_{n+1} = Q_n + \alpha [R_n - Q_n]$ (2.5). The trace of one $\bar o_0 = 0$ , $\bar o_n = \bar o_{n-1} + \alpha (1 - \bar o_{n-1})$ defines the step size $\beta_n = \alpha / \bar o_n$ (2.8)–(2.9).

Formalization targets

Goal: the expected update is the gradient step

For every action $a$ , with $A \sim \pi$ and $R \mid A = x \sim \nu_x$ ,

\mathbb E\bigl[H'(a)\bigr] = H(a) + \alpha\, \frac{\partial\, \mathbb E[R]}{\partial H(a)} ,

that is, the update (2.12) equals the exact gradient-ascent step (2.13) in expected value, for every baseline $B$ that does not depend on the selected action.

Milestones

(2.3): $Q_{n+1} = Q_n + \tfrac1n [R_n - Q_n]$ for $n \ge 1$ , including $Q_2 = R_1$ for arbitrary $Q_1$ .
(2.6): $Q_{n+1} = (1-\alpha)^n Q_1 + \sum_{i=1}^n \alpha(1-\alpha)^{n-i} R_i$ , with weights summing to one.
Exercise 2.7: with $\beta_n = \alpha/\bar o_n$ , $Q_{n+1} = \sum_{i=1}^n \frac{\alpha(1-\alpha)^{n-i}}{\bar o_n} R_i$ for $n \ge 1$ , weights summing to one, and no dependence on $Q_1$ .
Shift invariance (p. 37): adding a constant $c$ to every preference leaves $\pi$ unchanged.
Exercise 2.9: for $k = 2$ , $\pi(1) = \sigma(H(1) - H(2))$ with $\sigma(x) = 1/(1+e^{-x})$ .
Soft-max derivative (p. 40): $\partial \pi(x)/\partial H(a) = \pi(x)(\mathbb 1_{a=x} - \pi(a))$ .
Zero-sum gradient (p. 39): $\sum_x \partial \pi(x)/\partial H(a) = 0$ .
Performance gradient as an expectation (p. 39): $\partial \mathbb E[R]/\partial H(a) = \mathbb E[(R - B)(\mathbb 1_{a=A} - \pi(a))]$ .

Significance

The result. The identity makes a model-free algorithm, which uses only the sampled action and reward, an unbiased estimator of the gradient of a quantity that depends on the unknown $q_*$ . It therefore places the gradient bandit algorithm within stochastic approximation, where convergence theory for stochastic gradient methods applies. It also explains the role of the baseline: any baseline independent of the action leaves the expected update unchanged, so the choice of baseline can only affect the variance of the update, as Figure 2.5 shows empirically. The estimation milestones make precise two claims the chapter uses repeatedly: sample averages can be maintained incrementally, and constant step sizes produce an exponentially recency-weighted average biased by $Q_1$ . Exercise 2.7 removes that bias.

Formalizing it. All of these results are elementary and proved (or left as routine exercises) in the book. None of them is formalized on Prove2Me or, as far as is known, in Mathlib. What this mission adds is a machine-checked version of the book's argument with the reward model and baseline condition stated precisely, and a reusable soft-max layer (definition, partial derivatives, shift invariance) for later missions of this series, in particular the policy gradient theorem of Chapter 13.

Difficulty

The mathematics is beginning calculus, as the book says. The formal difficulty lies elsewhere. The goal is an identity between an expectation over a two-stage random experiment (an action from $\pi$ , then a reward from $\nu_A$ ) and a partial derivative in one coordinate of a vector-valued parameter. A proof has to justify exchanging the finite sum with the derivative and splitting the reward integral, and it has to use integrability of each $\nu_x$ . It also needs the fact that the baseline term vanishes because $\sum_x \partial\pi(x)/\partial H(a) = 0$ . A scalar-parameter version of the log-sum-exp derivative does not suffice: the book differentiates in one coordinate $H(a)$ while all other preferences are held fixed. For Exercise 2.7 the obvious unrolling of (2.6) does not apply directly, because the step size $\beta_n$ varies with $n$ and the book states neither the weights nor the range of $\alpha$ .

Formalization scope

Actions are Fin k. Every statement quantifies over some action, so $k \ge 1$ whenever it has content. Preferences are vectors Fin k → ℝ. The partial derivative in coordinate $a$ is the derivative of $h \mapsto f(\text{update } H\ a\ h)$ at $H(a)$ . The soft-max derivative milestone is stated with HasDerivAt, so it also asserts differentiability.
Rewards: each $\nu_x$ is a probability measure on $\mathbb R$ with Integrable identity and mean $q_*(x)$ . The expectation of a function of $(A, R)$ is $\sum_x \pi(x) \int \cdot \, d\nu_x$ . The book's normal-distribution testbed is only an example.
The baseline is a fixed real $B$ , the book's "any scalar that does not depend on" the action (pp. 39–40). The book's $B_t = \bar R_t$ , the average of past rewards, is covered once one conditions on the past. Footnote 1 on p. 37 states that the chapter's experiments used a $\bar R_t$ that also included $R_t$ . That baseline depends on $A_t$ , and the identity does not cover it.
Rewards of one action are a sequence indexed from $1$ . $Q_1$ is arbitrary, and $0^0 = 1$ as in the book (p. 33), so $\alpha = 1$ is included in (2.6).
Exercise 2.7 speaks of "a conventional constant step size $\alpha > 0$ ". The formalization takes $\alpha \in (0,1]$ , the range of the constant step size in (2.5). For $\alpha = 2$ the trace $\bar o_n$ vanishes at every even $n$ and $\beta_n$ is undefined. "Without initial bias" is read as "for $n \ge 1$ , $Q_{n+1}$ is the displayed weighted average of $R_1, \dots, R_n$ with weights summing to one", which in particular does not involve $Q_1$ .
Exercise 2.9 is read as the two equalities $\pi(1) = \sigma(H(1)-H(2))$ and $\pi(2) = \sigma(H(2)-H(1))$ .
A trivializing formalization is ruled out: the goal is about the expected value of the algorithm's update (2.12) under the joint law of action and reward, not the soft-max derivative alone and not a version in which the reward is replaced by its mean or the expectation is taken over $A$ only.
Not formalized: the UCB rule (2.10) and the 10-armed testbed, which carry no provable claim in the chapter, and the stochastic-approximation conditions (2.7), which the book cites without proof.
Welcome contributions: a general soft-max library (derivatives, Jacobian, log-sum-exp) over a finite type, reusable for Chapter 13, and proofs of the milestones in the listed order.

Selected references

R. S. Sutton, A. G. Barto, Reinforcement Learning: An Introduction, 2nd ed., MIT Press, 2018, ISBN 9780262039246, Chapter 2, pp. 25–46. http://incompleteideas.net/book/the-book-2nd.html
R. J. Williams, Simple statistical gradient-following algorithms for connectionist reinforcement learning, Machine Learning 8 (1992) 229–256. https://doi.org/10.1007/BF00992696
H. Robbins, S. Monro, A stochastic approximation method, Annals of Mathematical Statistics 22 (1951) 400–407. https://doi.org/10.1214/aoms/1177729586

11 thms2 active usersReviewed

Completed

Dynamic Programming Machine Learning Operations Research·Captain: mikedeng1

Approximately Optimal Approximate Reinforcement Learning II: Near-Optimality of a Policy with Small Policy AdvantageResearch Paper

Motivation

Approximate policy iteration and policy-gradient methods stop when they can no longer find a direction of improvement. Kakade and Langford (ICML 2002) asked what such a stopping point guarantees. Their algorithm, conservative policy iteration, halts at a policy $\pi$ for which no policy can improve much on $\pi$ as measured under a restart distribution $\mu$ ; the quantity that is small is the optimal policy advantage $\mathrm{OPT}(\mathbb A_{\pi,\mu})$ . Theorem 6.2 of the paper translates this local condition into a global statement: the performance of $\pi$ is close to optimal, with a loss controlled by how well $\mu$ covers the states an optimal policy visits.

The bound is the origin of the distribution mismatch coefficient $\|d_{\pi^*,\tilde\mu}/\mu\|_\infty$ , which reappears in the analysis of approximate dynamic programming (concentrability coefficients, Munos 2003), of conservative and trust-region methods, and of the convergence of policy gradient methods (Agarwal, Kakade, Lee, Mahajan 2021), where it governs the rate. The performance difference lemma (Lemma 6.1) used in its proof has become a standard tool of reinforcement learning theory.

Setting

A finite Markov decision process has a finite nonempty state set $S$ , a finite nonempty action set $A$ , transition probabilities $P(s';s,a)$ (for each $s,a$ a probability distribution over $s'$ ), a reward function $\mathcal R:S\times A\to[0,R]$ with $R>0$ , and a discount factor $0\le\gamma<1$ . A stochastic policy $\pi(a;s)$ is, for each state $s$ , a probability distribution over actions. A state distribution is a probability vector $\mu$ on $S$ .

The normalized value function is $V_\pi(s)=(1-\gamma)E[\sum_{t\ge0}\gamma^t\mathcal R(s_t,a_t)\mid\pi,s]$ , where $s_0=s$ , $a_t\sim\pi(\cdot;s_t)$ and $s_{t+1}\sim P(\cdot;s_t,a_t)$ . The state–action value is $Q_\pi(s,a)=(1-\gamma)\mathcal R(s,a)+\gamma\sum_{s'}P(s';s,a)V_\pi(s')$ and the advantage is $A_\pi(s,a)=Q_\pi(s,a)-V_\pi(s)$ . The discounted future state distribution from $\mu$ is

d_{\pi,\mu}(s)=(1-\gamma)\sum_{t\ge0}\gamma^t\Pr(s_t=s;\pi,\mu),\qquad s_0\sim\mu,

and the performance of $\pi$ from $\mu$ is $\eta_\mu(\pi)=\sum_s\mu(s)V_\pi(s)$ .

The policy advantage of $\pi'$ with respect to $\pi$ and $\mu$ is $\mathbb A_{\pi,\mu}(\pi')=\sum_sd_{\pi,\mu}(s)\sum_a\pi'(a;s)A_\pi(s,a)$ : the expected advantage of $\pi'$ over $\pi$ on the states $\pi$ itself visits. Its maximum over all stochastic policies is $\mathrm{OPT}(\mathbb A_{\pi,\mu})=\max_{\pi'}\mathbb A_{\pi,\mu}(\pi')$ (Definition 4.3). An optimal policy $\pi^*$ satisfies $V_\pi(s)\le V_{\pi^*}(s)$ for every policy $\pi$ and every state $s$ . For nonnegative $f,g$ on $S$ , $\|f/g\|_\infty=\max_sf(s)/g(s)$ (p. 5).

Formalization targets

Goal: Theorem 6.2 (p. 6)

If $\mathrm{OPT}(\mathbb A_{\pi,\mu})<\varepsilon$ and $\pi^*$ is optimal, then for every state distribution $\tilde\mu$

\eta_{\tilde\mu}(\pi^*)-\eta_{\tilde\mu}(\pi)\le\frac{\varepsilon}{1-\gamma}\left\|\frac{d_{\pi^*,\tilde\mu}}{d_{\pi,\mu}}\right\|_\infty\le\frac{\varepsilon}{(1-\gamma)^2}\left\|\frac{d_{\pi^*,\tilde\mu}}{\mu}\right\|_\infty.

The goal states both inequalities and the outer bound. The evaluation distribution $\tilde\mu$ is arbitrary and unrelated to the restart distribution $\mu$ ; taking $\tilde\mu=D$ , the start distribution, gives Corollary 4.5 (p. 5).

Milestone: Lemma 6.1 (p. 6)

For any policies $\tilde\pi$ , $\pi$ and any starting distribution $\mu$ ,

\eta_\mu(\tilde\pi)-\eta_\mu(\pi)=\frac{1}{1-\gamma}E_{(a,s)\sim\tilde\pi d_{\tilde\pi,\mu}}\big[A_\pi(s,a)\big].

The states are weighted by the future state distribution of the new policy $\tilde\pi$ , the advantage is that of the old policy $\pi$ .

Significance

Theorem 6.2 is the quality guarantee for conservative policy iteration: combined with the paper's Theorem 4.4 (the algorithm stops with $\mathrm{OPT}(\mathbb A_{\pi,\mu})<2\varepsilon$ after polynomially many calls), it bounds the suboptimality of the returned policy for any target distribution, independently of the size of the state space except through the mismatch coefficient. It also explains the role of the restart distribution: a more uniform $\mu$ makes $\|d_{\pi^*,\tilde\mu}/\mu\|_\infty$ small. Lemma 6.1 is used throughout later theory, from trust-region policy optimization to the global convergence of policy gradient methods.

Both results are proved in the paper, with short arguments. The contribution of this mission is a machine-checked version of the infinite-horizon discounted statement in the paper's normalization, with the $\|\cdot\|_\infty$ ratios handled exactly, including states where a denominator vanishes. Neither the discounted performance difference lemma for stochastic policies nor the distribution mismatch bound is known to be formalized in Mathlib; a finite-horizon performance difference identity has been formalized separately and is a different statement.

Difficulty

The mathematics is short; the difficulty is in the infinite-horizon bookkeeping. The value function and $d_{\pi,\mu}$ are infinite series, and Lemma 6.1 relates the series of two different policies: its natural one-line argument uses the Bellman equation for $V_\pi$ , which is not the definition here, together with interchanges of infinite sums over time with finite sums over states and actions, each of which needs summability. Theorem 6.2 then needs two facts that are not stated as results in the paper: that $\mathrm{OPT}(\mathbb A_{\pi,\mu})$ equals $\sum_sd_{\pi,\mu}(s)\max_aA_\pi(s,a)$ (the supremum over policies is attained by a greedy policy, and $\max_aA_\pi(s,a)\ge0$ ), and that $d_{\pi,\mu}(s)\ge(1-\gamma)\mu(s)$ . Reading the $\ell_\infty$ ratio with real division would give a false statement when a denominator is zero; the statement avoids this.

Formalization scope

States and actions are finite nonempty types; policies and kernels are real-valued functions π s a (the paper's $\pi(a;s)$ ) and P s a s' (the paper's $P(s';s,a)$ ), with their distribution properties as explicit hypotheses. The published definitions IsTransitionKernel, IsPolicy, InducedTransition, OccupationDist, InducedReward and PolicyValue from the Foundations of Machine Learning series are reused; $V_\pi$ is $(1-\gamma)$ times PolicyValue, the defining series. $\mathrm{OPT}$ is the supremum of the policy advantages over stochastic policies, which is the paper's maximum. Optimality of $\pi^*$ is relative to stationary stochastic policies, the paper's policy class; the existence of an optimal policy (the paper's "well known result", p. 2) is not part of this mission.

Every hypothesis is explicit: rewards in $[0,R]$ with $R>0$ , $0\le\gamma<1$ , $P$ a kernel, $\pi$ and $\pi^*$ stochastic policies, $\mu$ and $\tilde\mu$ state distributions. Each $\|f/g\|_\infty$ bound is stated multiplicatively: " $X\le K\|f/g\|_\infty$ " is " $X\le KC$ for every $C$ with $f(s)\le Cg(s)$ for all $s$ ". When some $g(s)=0<f(s)$ no such $C$ exists and the bound is empty, which matches $\|f/g\|_\infty=+\infty$ ; no full-support assumption is made on $\mu$ or $\tilde\mu$ . The hypothesis $\mathrm{OPT}(\mathbb A_{\pi,\mu})<\varepsilon$ is on the supremum itself, not on the closed form $\sum_sd_{\pi,\mu}(s)\max_aA_\pi(s,a)$ , which is a step of the proof; a formalization that assumed the closed form, or that divided by $d_{\pi,\mu}$ in real arithmetic, would not be this theorem. The proof of the theorem uses only that $\pi^*$ is a policy; optimality is kept as a hypothesis because the paper states it.

The proof on p. 7 twice writes $d_{\pi,\mu}(s)\le(1-\gamma)\mu(s)$ ; the inequality it uses, and the one stated on p. 5, is $d_{\pi,\mu}(s)\ge(1-\gamma)\mu(s)$ . This slip is in the proof, not in the statement. Pages are PDF pages; the paper has no printed page numbers.

Useful reusable infrastructure: summability and Bellman equations for the normalized discounted value, $d_{\pi,\mu}$ as a probability distribution with $d_{\pi,\mu}\ge(1-\gamma)\mu$ , and attainment of $\mathrm{OPT}$ by a greedy policy. Contributions of any of these as separate lemmas are welcome.

Selected references

S. Kakade, J. Langford, Approximately Optimal Approximate Reinforcement Learning, Proceedings of the 19th International Conference on Machine Learning (ICML), 2002. https://dl.acm.org/doi/10.5555/645531.656005
R. Munos, Error Bounds for Approximate Policy Iteration, ICML 2003. https://dl.acm.org/doi/10.5555/3041838.3041903
A. Agarwal, S. Kakade, J. Lee, G. Mahajan, On the Theory of Policy Gradient Methods: Optimality, Approximation, and Distribution Shift, Journal of Machine Learning Research 22(98), 2021. https://jmlr.org/papers/v22/19-736.html
J. Schulman, S. Levine, P. Abbeel, M. Jordan, P. Moritz, Trust Region Policy Optimization, ICML 2015. https://arxiv.org/abs/1502.05477

10 thms2 active usersReviewed

Completed

Dynamic Programming Machine Learning Operations Research+1·Captain: mikedeng1

Approximately Optimal Approximate Reinforcement Learning I: Conservative Policy Iteration Improves Monotonically and Returns a Near-Greedy PolicyResearch Paper

Motivation

Approximate policy iteration and policy gradient methods are the two classical families of reinforcement learning algorithms that work with approximate, sampled information instead of an exact model. Kakade and Langford (ICML 2002) observed that neither family answers three basic questions: is there a performance measure that is guaranteed to improve at every step, how hard is it to verify that an update improves it, and what performance is reached after a reasonable number of updates. Greedy approximate policy iteration can make the policy worse when the value estimates are slightly wrong at a few states, and policy gradient methods can stall on plateaus where estimating the gradient needs an enormous number of samples.

Their answer is conservative policy iteration: instead of jumping to a greedy policy, move only a controlled fraction of the way toward it, with a step size chosen from an estimate of how much the greedy policy helps. The paper proves that this update improves a restart-distribution performance measure monotonically, terminates after a number of iterations that depends only on the reward range and the target accuracy, and stops at a policy that the greedy oracle can no longer improve by much. The idea is the direct ancestor of trust-region and proximal policy optimization methods (TRPO, Schulman et al. 2015; PPO, Schulman et al. 2017), whose improvement bounds are refinements of the paper's Theorem 4.1.

Setting

A finite Markov decision process has a finite nonempty set of states $S$ , a finite nonempty set of actions $A$ , transition probabilities $P(s';s,a)$ (for each state $s$ and action $a$ , a probability distribution over next states $s'$ ), a reward function $\mathcal R : S\times A\to[0,R]$ with $R>0$ , and a discount factor $0\le\gamma<1$ . A stochastic policy $\pi(a;s)$ gives, for each state $s$ , a probability distribution over actions.

The normalized value of $\pi$ from $s$ is $V_\pi(s) = (1-\gamma)E[\sum_{t\ge0}\gamma^t\mathcal R(s_t,a_t)\mid\pi,s]$ , where $s_0=s$ , $a_t\sim\pi(\cdot\,;s_t)$ , $s_{t+1}\sim P(\cdot\,;s_t,a_t)$ ; it lies in $[0,R]$ . The state-action value is $Q_\pi(s,a) = (1-\gamma)\mathcal R(s,a)+\gamma E_{s'\sim P(s';s,a)}[V_\pi(s')]$ and the advantage is $A_\pi(s,a) = Q_\pi(s,a)-V_\pi(s)\in[-R,R]$ .

For a state distribution $\mu$ (a restart distribution), the discounted future state distribution is $d_{\pi,\mu}(s) = (1-\gamma)\sum_{t\ge0}\gamma^t\Pr(s_t=s;\pi,\mu)$ (eq. (2.1)), and the performance measure is $\eta_\mu(\pi) = E_{s\sim\mu}[V_\pi(s)]$ .

The policy advantage of a policy $\pi'$ with respect to $\pi$ and $\mu$ is

\mathbb A_{\pi,\mu}(\pi') = E_{s\sim d_{\pi,\mu}}\big[E_{a\sim\pi'(a;s)}[A_\pi(s,a)]\big],

and $\mathrm{OPT}(\mathbb A_{\pi,\mu}) = \max_{\pi'}\mathbb A_{\pi,\mu}(\pi')$ . The conservative update (4.1) is $\pi_{new} = (1-\alpha)\pi+\alpha\pi'$ with $\alpha\in[0,1]$ . An $\varepsilon$ -greedy policy chooser $G_\varepsilon$ (Definition 4.3) returns, for every policy $\pi$ , a policy $\pi'$ with $\mathbb A_{\pi,\mu}(\pi')\ge\mathrm{OPT}(\mathbb A_{\pi,\mu})-\varepsilon$ .

Conservative policy iteration (§5) starts from any policy and repeats: call $G_\varepsilon(\pi,\mu)$ to get $\pi'$ ; form an $\frac\varepsilon3$ -accurate estimate $\hat{\mathbb A}$ of $\mathbb A_{\pi,\mu}(\pi')$ from $\mu$ -restarts; if $\hat{\mathbb A}<\frac{2\varepsilon}3$ , stop and return $\pi$ ; otherwise apply (4.1) with $\alpha = \frac{(1-\gamma)(\hat{\mathbb A}-\varepsilon/3)}{4R}$ and repeat.

Formalization targets

Goal: Theorem 4.4 (p. 5)

With probability at least $1-\delta$ , conservative policy iteration (i) strictly improves $\eta_\mu$ with every policy update, (ii) stops after at most $72R^2/\varepsilon^2$ policy updates, and (iii) returns a policy $\pi$ with

\mathrm{OPT}(\mathbb A_{\pi,\mu}) < 2\varepsilon.

The estimation step is represented by its guarantee: each reached loop's estimate fails to be $\frac\varepsilon3$ -accurate with probability at most $\delta/(N+1)$ , $N=\lfloor72R^2/\varepsilon^2\rfloor$ .

Milestones

Lemma 6.1 (p. 6), the performance difference identity:

\eta_\mu(\tilde\pi)-\eta_\mu(\pi) = \frac1{1-\gamma}E_{(a,s)\sim\tilde\pi d_{\tilde\pi,\mu}}[A_\pi(s,a)].

Theorem 4.1 (p. 4), with $\varepsilon=\max_s|E_{a\sim\pi'(a;s)}[A_\pi(s,a)]|$ and all $\alpha\in[0,1]$ :

\eta_\mu(\pi_{new})-\eta_\mu(\pi)\ge\frac{\alpha}{1-\gamma}\Big(\mathbb A-\frac{2\alpha\gamma\varepsilon}{1-\gamma(1-\alpha)}\Big).

Corollary 4.2 (p. 5): if $\mathbb A\ge0$ , the step size $\alpha=\frac{(1-\gamma)\mathbb A}{4R}$ gives

\eta_\mu(\pi_{new})-\eta_\mu(\pi)\ge\frac{\mathbb A^2}{8R}.

Significance

Theorem 4.4 is the first guarantee of its kind for approximate reinforcement learning: the number of iterations is bounded by $72R^2/\varepsilon^2$ , independent of the number of states and of the restart distribution, and every iteration provably helps. Lemma 6.1 is the standard performance difference lemma, used throughout the analysis of policy optimization, including natural policy gradient and trust-region methods; Theorem 4.1 is the prototype of the "surrogate objective minus a penalty" bound that TRPO refines.

These results are proved in the paper. As far as a search of the platform shows, none is formalized: the platform's finite-horizon performance difference lemma (Foster and Rakhlin's Lemma 13) is a different statement, for episodic problems with non-stationary policies. This mission produces machine-checked versions of the discounted performance difference identity, the conservative improvement bound with its exact constants, and the high-probability termination and quality guarantee of the algorithm, all on top of an explicit infinite-horizon model rather than an assumed Bellman equation.

Difficulty

The obvious argument for the improvement bound expands $\eta_\mu(\pi_{new})$ to first order in $\alpha$ ; that only gives $\frac{\alpha}{1-\gamma}\mathbb A+O(\alpha^2)$ with an unspecified constant, which cannot fix a step size. The exact bound needs control of how far the state distribution of the mixed policy drifts from that of the old policy, uniformly in time, and the performance difference identity is only useful once the states are weighted by the new policy's distribution. On the formal side, $V_\pi$ and $d_{\pi,\mu}$ are infinite discounted series, so summability, exchanges of sums and the identities $\sum_s d_{\pi,\mu}(s)=1$ and $\sum_a\pi(a;s)A_\pi(s,a)=0$ must all be established from the definitions. For Theorem 4.4, the algorithm is a random process whose policies depend on all earlier estimates; the argument has to be made pathwise on the event that every reached loop is accurate, together with a union bound over the loops that can be reached.

Formalization scope

Policies are functions π : S → A → ℝ with π s a the paper's $\pi(a;s)$ , and P s a s' is $P(s';s,a)$ ; both are constrained by the published predicates IsPolicy and IsTransitionKernel. $V_\pi$ is $(1-\gamma)$ times the published series PolicyValue, so values are normalized as in the paper. $\mathrm{OPT}$ is a real supremum over all stochastic policies; the set is nonempty and bounded, and the maximum is attained. Every theorem carries the standing assumptions of §2: finite nonempty $S$ and $A$ , a transition kernel, rewards in $[0,R]$ with $R>0$ , $0\le\gamma<1$ , and a state distribution $\mu$ . In Corollary 4.2, $R$ is any upper bound on the rewards rather than necessarily the attained maximum.

In Theorem 4.4 the run is formalized pathwise, driven by arbitrary real random estimates on a probability space; the conclusion bounds the probability of the failure event by $\delta$ . Two deviations from the printed statement are disclosed. First, (ii) is stated for policy updates: the proof bounds updates, and the algorithm calls $G_\varepsilon$ once more than it updates, so "at most $72R^2/\varepsilon^2$ calls" is off by one. Second, the per-loop failure budget is $\delta/(N+1)$ , which covers the $N+1$ loops that may be reached. The Hoeffding estimate (5.1) is not formalized: as printed it concerns the $\frac\varepsilon6$ -biased target, and its role is taken by the accuracy hypothesis. The step size is clipped at $1$ , which never binds when the estimate is accurate. No trivializing reading is available: the accuracy hypothesis is satisfied by a perfect estimator and a $0$ -greedy chooser exists, so the theorem is not vacuous, and strict improvement at every update is required, not merely nonnegative change.

Pages are PDF pages; the paper has no printed page numbers.

A complete development needs summability and algebra of discounted occupation measures, the performance difference identity, and a union bound over the loops of a random process; the first two are reusable for any discounted policy-optimization result. Proofs of the milestones in any order are welcome.

Selected references

S. Kakade and J. Langford, Approximately Optimal Approximate Reinforcement Learning, Proceedings of the 19th International Conference on Machine Learning (ICML), 2002. https://dl.acm.org/doi/10.5555/645531.656005
J. Schulman, S. Levine, P. Moritz, M. Jordan, P. Abbeel, Trust Region Policy Optimization, ICML 2015. https://arxiv.org/abs/1502.05477
J. Schulman, F. Wolski, P. Dhariwal, A. Radford, O. Klimov, Proximal Policy Optimization Algorithms, 2017. https://arxiv.org/abs/1707.06347
D. J. Foster and A. Rakhlin, Foundations of Reinforcement Learning and Interactive Decision Making, 2023. https://arxiv.org/abs/2312.16730

13 thms2 active usersReviewed

Dynamical Systems Probability Stochastic Systems·Captain: mikedeng1

The O.D.E. Method for Convergence of Stochastic Approximation and Reinforcement Learning I: Stability and Almost-Sure Convergence under Tapering StepsizesResearch Paper

Motivation

Stochastic approximation is the family of recursive algorithms that locate a zero of a function observed only through noisy evaluations. It goes back to Robbins and Monro (1951) and today underlies stochastic gradient descent, temporal-difference learning, Q-learning and actor–critic methods in reinforcement learning, and models of learning by boundedly rational agents.

The standard analysis is the O.D.E. method (Ljung 1977; see Kushner and Yin 1997): the interpolated iterates are compared with the solutions of an ordinary differential equation, and convergence of the algorithm follows from the stability of that ODE. The method has one well-known gap. It assumes, rather than proves, that the iterates remain bounded with probability one. In applications this stability hypothesis is often the hardest part: for asynchronous Q-learning and adaptive critic algorithms, almost sure boundedness had been proved only for discounted cost or after adding a projection step (Borkar and Meyn, p. 460).

Borkar and Meyn (SIAM J. Control Optim. 38 (2000)) close this gap with a scaling argument borrowed from the fluid-model approach to the stability of queueing networks (Dai 1995; Dai and Meyn 1995). They show that boundedness itself follows from the asymptotic stability of the origin for a second, "fluid-limit" ODE obtained by rescaling the drift. This mission formalizes that stability theorem for tapering step sizes, and the convergence theorem that follows from it.

Setting

Fix $d\ge 0$ and work in $\mathbb R^d$ with the Euclidean norm. Let $h:\mathbb R^d\to\mathbb R^d$ and let $\{a(n)\}_{n\ge0}$ be a deterministic sequence of positive step sizes. On a probability space $(\Omega,\mathcal F,\mathsf P)$ , random vectors $X(n)$ and $M(n)$ satisfy the stochastic approximation recursion

X(n+1) = X(n) + a(n)\big[h(X(n)) + M(n+1)\big], \qquad n\ge0. \tag{1.1}

Its mean ODE is $\dot x = h(x)$ (1.2). For $r>0$ the scaled field is $h_r(x)=h(rx)/r$ , with the scaled ODE $\dot x = h_r(x)$ (1.4).

(A1) $h$ is Lipschitz; $h_r(x)\to h_\infty(x)$ as $r\to\infty$ for every $x$ ; and the origin is an asymptotically stable equilibrium of the fluid-limit ODE $\dot x = h_\infty(x)$ (1.5).
(A2) With $\mathcal F_n$ the history of the iterates up to time $n$ , $\{M(n)\}$ is a martingale difference sequence, $\mathsf E[M(n+1)\mid\mathcal F_n]=0$ , and for some constant $C_0<\infty$ , $\mathsf E[\|M(n+1)\|^2\mid\mathcal F_n]\le C_0(1+\|X(n)\|^2)$ .
(TS) Tapering step sizes: $0<a(n)\le1$ , $\sum_n a(n)=\infty$ , $\sum_n a(n)^2<\infty$ .

A point $x^*$ is globally asymptotically stable for $\dot x = h(x)$ if it is a Lyapunov-stable equilibrium and every solution converges to it.

Formalization targets

Goal: Theorem 2.2 (almost sure convergence)

Under (A1), (A2) and (TS), if $\dot x=h(x)$ has a unique globally asymptotically stable equilibrium $x^*$ , then for every initial condition $X(0)\in\mathbb R^d$ ,

X(n)\longrightarrow x^* \qquad \text{almost surely.}

The goal contains no constants and no rates, only the qualitative conclusion.

Milestone: Theorem 2.1 (i) (almost sure boundedness)

Under (A1), (A2) and (TS), for every initial condition,

\sup_n \|X(n)\| < \infty \qquad \text{almost surely.}

Milestones: the lemmas of Section 4.1

Lemma 4.1: the fluid-limit ODE is globally exponentially asymptotically stable.
Lemma 4.2: the piecewise ODE solutions $\hat\phi$ , $\phi^\infty$ used for comparison are bounded by a constant independent of the initial condition.
Lemma 4.3 (i), (ii): two discrete Bellman–Gronwall inequalities.
Lemma 4.4: for large scale $r$ , every solution of $\dot x = h_r(x)$ from the unit ball is $\epsilon$ -small on a window $[T,T+1]$ .
Lemma 4.5: the rescaled iterates have uniformly bounded second moments, and the rescaled noise sum $\xi$ is an $L^2$ -bounded martingale.
Lemma 4.6: almost surely the rescaled interpolated iterates $\phi$ track $\hat\phi$ and stay bounded.

Significance

The result. Theorem 2.1 (i) turns the stability hypothesis of the O.D.E. method into a checkable condition on a deterministic ODE. Theorem 2.2 then gives convergence to $x^*$ with no a priori boundedness assumption. The paper applies this to reinforcement learning, obtaining the first convergence proof for asynchronous Q-learning and adaptive critic algorithms for average-cost Markov decision processes (the asynchronous extension, Theorem 2.5, is sketched in the paper and is not part of this mission). The same fluid-limit criterion is now a textbook tool; see Borkar, Stochastic Approximation: A Dynamical Systems Viewpoint (2008), Chapter 3.

Formalizing it. The theorems are proved in the paper, and the proofs are short but rely on several standard facts stated informally: uniform convergence of $h_r$ to $h_\infty$ on compact sets, continuous dependence of ODE solutions on initial data and on the vector field, and the martingale convergence theorem. No machine-checked version of the O.D.E. method or of this stability criterion is known to exist. A formal development would give a verified link between discrete-time stochastic recursions, martingale convergence in Mathlib, and the stability theory of Lipschitz ODEs.

Difficulty

The obvious approach is to compare the iterates with solutions of $\dot x = h(x)$ over windows of fixed ODE time and to control the accumulated noise by martingale convergence. This fails without boundedness: the noise bound in (A2) grows with $\|X(n)\|$ , so the deviation from the ODE can only be controlled relative to the current size of the iterate, and nothing prevents the iterates from escaping to infinity.

A second difficulty is that the hypothesis (A1) concerns only the fluid limit $h_\infty$ , which describes the drift at infinite scale. It says nothing directly about $h$ at any finite state, and nothing about the noise. Any argument therefore has to transfer information from the limit $r\to\infty$ to the recursion at random, path-dependent scales, uniformly over those scales, while the noise is controlled only relative to the current size of the iterate. In Lean this involves ODE comparison and Gronwall estimates on a random partition of the time axis, conditional second-moment estimates for a rescaled recursion, and a vector-valued $L^2$ martingale convergence argument, none of which is available off the shelf for this setting.

Formalization scope

The state space is EuclideanSpace ℝ (Fin d). An ODE solution is a forward solution on $[0,\infty)$ : the derivative is taken within $[0,\infty)$ at each $t\ge0$ , which makes solutions continuous there. Stability notions are the standard ones (Lyapunov stability; asymptotic, global asymptotic and global exponential stability, the last in the form $\|x(t)-x^*\|\le b e^{-\delta t}\|x(0)-x^*\|$ ). All vector fields in the mission are Lipschitz, so forward solutions exist and are unique, and quantifying over "every solution" is meaningful.

The filtration in (A2) is the natural filtration of the iterates. Because $a(n)>0$ , it carries the same information as the paper's $\sigma(X(i),M(i),i\le n)$ . (A2) includes integrability of $M(n+1)$ and $\|M(n+1)\|^2$ , so that the conditional expectations are meaningful. The theorems quantify over every probability space and every noise process satisfying (A2); the goal and Theorem 2.1 (i) take a deterministic initial condition, as the paper does. Stating the goal for a particular noise model (no noise, or i.i.d. noise) would be a different and much weaker theorem, and is ruled out. " $\sup_n\|X(n)\|<\infty$ " is boundedness above of the set of norms, not a real supremum, which Lean sets to $0$ on unbounded sets. Second-moment suprema in Lemma 4.5 are taken in $[0,\infty]$ .

The proof objects of Section 4.1 (time grid $t(n)$ , blocks $m(j)$ and $T(j)$ , scales $r(j)$ , the interpolation $\phi$ , the rescaled iterates and noise sum) are separate definitions built from the step sizes and the sample path, as on the page. The piecewise ODE solutions $\hat\phi$ and $\phi^\infty$ are characterized by a predicate, and the lemmas hold for every function satisfying it.

Useful infrastructure, reusable beyond this mission: Lipschitz ODE comparison and continuous-dependence estimates in Mathlib's ODE library, uniform convergence of $h_r$ on compact sets, the discrete Gronwall lemmas, and $L^2$ -bounded vector-valued martingale convergence. Contributions are welcome on any milestone. The two Gronwall lemmas and Lemma 4.1 are self-contained entry points.

Selected references

V. S. Borkar and S. P. Meyn, The O.D.E. Method for Convergence of Stochastic Approximation and Reinforcement Learning, SIAM J. Control Optim. 38(2):447–469, 2000. https://doi.org/10.1137/S0363012997331639
H. Robbins and S. Monro, A Stochastic Approximation Method, Ann. Math. Statist. 22(3):400–407, 1951. https://doi.org/10.1214/aoms/1177729586
L. Ljung, Analysis of Recursive Stochastic Algorithms, IEEE Trans. Automat. Control 22(4):551–575, 1977. https://doi.org/10.1109/TAC.1977.1101561
H. J. Kushner and G. G. Yin, Stochastic Approximation Algorithms and Applications, Springer, 1997. https://doi.org/10.1007/978-1-4899-2696-8
J. G. Dai, On Positive Harris Recurrence of Multiclass Queueing Networks: A Unified Approach via Fluid Limit Models, Ann. Appl. Probab. 5(1):49–77, 1995. https://doi.org/10.1214/aoap/1177004828
J. G. Dai and S. P. Meyn, Stability and Convergence of Moments for Multiclass Queueing Networks via Fluid Limit Models, IEEE Trans. Automat. Control 40(11):1889–1904, 1995. https://doi.org/10.1109/9.471210
V. S. Borkar, Stochastic Approximation: A Dynamical Systems Viewpoint, Cambridge University Press / Hindustan Book Agency, 2008. https://doi.org/10.1007/978-93-86279-38-5

17 thms2 active usersReviewed

Reinforcement Learning

Missions

The Statistical Complexity of Interactive Decision Making IV: Log-Loss Regret Controls Hellinger Estimation Error, Est_H ≤ Reg_KL + 2 log(1/δ) with Probability 1−δResearch Paper

Motivation

Setting

Formalization targets

Main high-probability bound

Supporting results

Significance

Difficulty

Formalization scope

Selected references

The Statistical Complexity of Interactive Decision Making V: The Multi-Armed Bandit Has Localized DEC at Least 2⁻⁶·A/γ, via Hard Families of ModelsResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 5.3

Milestones

Companions

Significance

Difficulty

Formalization scope

Selected references

On the Sample Complexity of Reinforcement Learning III: Non-Stationary Approximate Policy Iteration Is Within 2T Times the Regression Error Averaged over Any Competitor's State-Time DistributionTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 5.3.2 (p. 64)

Milestones

Significance

Difficulty

Formalization scope

Selected references

On the Sample Complexity of Reinforcement Learning V: Exact Conservative Policy Iteration Improves at Every Update and Halts within 8H²/ε² Updates with Future Advantages at Most ε/HTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 7.3.2, explicit-constant form

Milestones

Significance

Difficulty

Formalization scope

Selected references

An Analysis of Temporal-Difference Learning with Function Approximation 2: For Every Sampling Distribution q and 5/6 < α < 1, Off-Line q-Sampled TD(0) Can Diverge in ExpectationResearch Paper

Motivation

Setting

Formalization targets

Divergence of the mean

Supporting statements

Significance

Difficulty

Formalization scope

Selected references

On the Theory of Policy Gradient Methods: Optimality, Approximation, and Distribution Shift 3: Softmax Policy Gradient Ascent with Step Size η ≤ (1−γ)³/8 Converges to the Optimal ValuesResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 5.1

Milestones (Appendices C.1 and D)

Significance

Difficulty

Formalization scope

Selected references

Learning in Structured MDPs with Convex Cost Functions: Improved Regret Bounds for Inventory Management: Base-Stock Values from Any Two Starting States Differ by at Most 36 max(h,p)LxResearch Paper

Motivation

Setting

Formalization targets

Goal: Lemma 2.5 (p. 8)

Milestones (Appendix B and the proof of Lemma 2.5)

Significance

Difficulty

Formalization scope

Selected references

Linear Least-Squares Algorithms for Temporal Difference Learning II: Probability-One Convergence of LS TD on Ergodic Markov ChainsResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2 (p. 44)

Milestones, in the order of the proof

Significance