Reinforcement Learning

Motivation

Policy gradient methods for Markov decision processes are frequently run on a regularized objective rather than on the cost of interest: a convex penalty on the action distribution is added to every single-period cost. Regularization smooths the problem, makes optimal policies strictly stochastic, and keeps iterates away from the boundary of the probability simplex, where gradients of common parameterizations vanish. Entropy and relative-entropy penalties are standard in this role; a unified treatment of regularized MDPs is given by Geist, Scherrer and Pietquin (2019), and Agarwal, Kakade, Lee and Mahajan (2021) analyse policy gradient with a log-barrier penalty added to the softmax objective.

Regularization changes the problem being solved. Anyone who uses it needs a quantitative answer to one question: how suboptimal, for the original costs, is a policy that is exactly optimal for the regularized costs? Bhandari and Russo (arXiv:1906.01786v3), whose main results establish that policy gradient objectives have no suboptimal stationary points under a closure condition, answer this question for a relative-entropy regularizer in finite MDPs (their Lemma 10). Bounds of this type for the negative-entropy regularizer are in Geist et al.; as Bhandari and Russo note (p. 20), those bounds do not apply to the unbounded log-barrier regularizer used here.

Setting

The state space $\mathcal S=\{1,\dots,n\}$ is finite. There are $k$ deterministic actions $e_1,\dots,e_k$, and an action is a probability vector $a\in\Delta_{k-1}$. A policy $\pi$ chooses $\pi(s)=(\pi(1|s),\dots,\pi(k|s))\in\Delta_{k-1}$ at each state; $\Pi$ is the set of all such policies. Transitions are linear in the action,

$$P(s'|s,a)=\sum_{i=1}^kP(s'|s,e_i)\,a_i ,$$

where each $P(\cdot|s,e_i)$ is a probability vector. Each state has a nonnegative cost vector $g_s\in\mathbb R^k_+$. For $\lambda\ge0$, the regularized cost is

$$g_\lambda(s,a)=g_s^\top a+\lambda\,D_{\mathrm{KL}}(U\|a),\qquad D_{\mathrm{KL}}(U\|a)=\sum_{i=1}^k\frac1k\log\frac{1/k}{a_i},$$

where $U$ is the uniform distribution. The divergence is $+\infty$ unless every $a_i>0$, so $g_\lambda$ takes values in $[0,\infty]$.

Given a discount factor $\gamma\in(0,1)$ and an initial distribution $\rho$, the discounted average cost of a policy is

$$\ell_\lambda(\pi)=(1-\gamma)\sum_{s}\rho(s)\,J_{\lambda,\pi}(s),\qquad J_{\lambda,\pi}(s)=\mathbb E^\pi_s\Big[\sum_{t\ge0}\gamma^tg_\lambda(s_t,\pi(s_t))\Big].$$

$\ell_0$ is the unregularized cost. The discounted occupancy of $\pi$ is $\eta_\pi(s')=(1-\gamma)\sum_s\rho(s)\sum_{t\ge0}\gamma^t\Pr^\pi(s_t=s'\mid s_0=s)$. $J^*_0$ and $Q^*_0$ denote the optimal cost-to-go and state-action cost-to-go of the unregularized problem. The constant of the result is

$$c=\frac{2\max_{s,i}|g_{s,i}|}{1-\gamma}.$$

Formalization targets

Goal: Lemma 10 (impact of regularization)

If $\pi^*_\lambda\in\arg\min_{\pi\in\Pi}\ell_\lambda(\pi)$ with $\lambda\ge0$, then

$$\ell_0(\pi^*_\lambda)\le\min_{\pi\in\Pi}\ell_0(\pi)+\lambda\Big(1+\log\Big(1+\frac c\lambda\Big)\Big).$$

Milestones (the steps of the proof in Appendix E.2)

1. Cost decomposition (34): $\ell_\lambda(\pi)=\sum_s\eta_\pi(s)g_\lambda(s,\pi(s))=\ell_0(\pi)+\lambda\sum_s\eta_\pi(s)D(U\|\pi(s))$ for every $\pi\in\Pi$.
2. One-step bound (37): for a policy $\pi_\lambda$ that, at every state, minimizes $a\mapsto\sum_iQ^*_0(s,e_i)a_i+\lambda D(U\|a)$ over the simplex (construction (36)),

$$\sum_iQ^*_0(s,e_i)\pi_\lambda(i|s)\le\min_{a\in\Delta_{k-1}}\sum_iQ^*_0(s,e_i)a_i+\lambda,\qquad T^{\pi_\lambda}_0J^*_0\le J^*_0+\lambda e.$$

3. Suboptimality of $\pi_\lambda$ (35): $\ell_0(\pi_\lambda)\le\min_{\pi\in\Pi}\ell_0(\pi)+\lambda$.
4. Divergence bound (Step 3): $\lambda\,D(U\|\pi_\lambda(s))\le\lambda\log(1+c/\lambda)$ for every state $s$.

Significance

The result. Lemma 10 says that the price of regularization is of order $\lambda\log(1/\lambda)$ as $\lambda\downarrow0$, with an explicit constant depending only on the cost scale and the effective horizon $1/(1-\gamma)$. Together with the paper's landscape results (Example 4 shows the regularized policy-iteration objective is strongly convex and the policy class is closed under policy improvement, so the regularized objective is gradient dominated), it turns convergence of first-order methods on the regularized problem into near-optimality for the original problem, and it gives a principled rule for choosing $\lambda$ as a function of the target accuracy. The bound holds for the log-barrier (relative entropy from the uniform distribution) regularizer, which is unbounded on the simplex, a case the negative-entropy analyses do not cover.

Formalizing it. The result and its proof are published (arXiv:1906.01786v3; Operations Research, 2024). No machine-checked proof of Lemma 10 or of its steps is known. The mission produces Lean statements of the lemma and of the four steps of its proof, built on a published finite-MDP layer, and invites proofs. Step 2 relies on the duality-gap bound for log-barrier problems from interior-point theory, which the paper cites from Boyd and Vandenberghe; a formal proof of that bound (in the simplex case) is reusable for any log-barrier analysis.

Difficulty

The first idea, comparing $\pi^*_\lambda$ with an unregularized optimal policy $\pi^*_0$, fails: $\pi^*_0$ is typically deterministic, so $D(U\|\pi^*_0(s))=\infty$ and $\ell_\lambda(\pi^*_0)=\infty$, giving no information. The comparison policy has to be built by hand: it must be strictly stochastic, nearly optimal for the unregularized problem, and have bounded divergence from the uniform distribution at every state. Each of these three properties is a separate argument: a duality-gap bound for a barrier problem on the simplex, a propagation of a one-step Bellman inequality to the whole horizon, and a quantitative lower bound on the smallest action probability of the barrier minimizer.

A second pitfall is the printed form of the lemma, whose right-hand side is $\min_\pi\ell_\lambda(\pi)+\lambda(1+\log(1+c/\lambda))$; since $D_{\mathrm{KL}}\ge0$ gives $\ell_0(\pi^*_\lambda)\le\ell_\lambda(\pi^*_\lambda)=\min_\pi\ell_\lambda(\pi)$, that inequality is trivially true. The proof establishes, and the text on p. 20 announces, the bound against $\min_\pi\ell_0(\pi)$, which is the goal here.

Formalization scope

States and deterministic actions are finite types S and I (nonempty, as on the page, so that $c$ is defined); $k=|I|$. Policies, transition kernels, the occupation distributions, the cost-to-go $J_{0,\pi}$ and $Q_{0,\pi}$ come from the published FoundationsML.ReinforcementLearning layer (IsPolicy, IsTransitionKernel, OccupationDist, PolicyValue, QFunction), with the cost vector passed in the reward slot: PolicyValue is a plain discounted sum, so this is the cost-to-go. Optimality is the cost-minimizing notion, defined locally.

$D_{\mathrm{KL}}(U\|\cdot)$, $g_\lambda$ and $\ell_\lambda$ take values in $[0,\infty]$, with $D_{\mathrm{KL}}=+\infty$ off the open simplex; real-valued junk such as $\log0=0$ never stands in for $+\infty$, and $\ell_\lambda$ is never coerced to $\mathbb R$ (that would make boundary policies look optimal). At $\lambda=0$ the convention $0\cdot\infty=0$ gives $g_0(s,a)=g_s^\top a$, and Lean's $c/0=0$ makes the goal's bound $0$, the limit of the page's bound. $\min_\pi\ell_0(\pi)$ is written as "$\le\ell_0(\pi)+\dots$ for every policy $\pi$". The minimizer $\pi^*_\lambda$ is a hypothesis (any minimizer); the barrier-greedy policy $\pi_\lambda$ of (36) appears only in the milestones, never in the goal. A statement of the goal with the printed right-hand side $\min_\pi\ell_\lambda(\pi)+\dots$, or one that assumes (35) or the divergence bound, would be a trivializing formalization and is ruled out.

Welcome contributions: proofs of the four milestones and the goal; a general Lean lemma that the discounted cost of a stationary policy in a finite MDP equals the occupancy-weighted single-period cost (milestone 1), which is reusable across policy gradient formalizations; and the log-barrier duality-gap bound on the simplex.

Selected references

• J. Bhandari and D. Russo, Global Optimality Guarantees for Policy Gradient Methods, arXiv:1906.01786v3, 2022; Operations Research, 2024. https://arxiv.org/abs/1906.01786 (DOI 10.1287/opre.2021.0014)
• M. Geist, B. Scherrer and O. Pietquin, A Theory of Regularized Markov Decision Processes, ICML, 2019. https://arxiv.org/abs/1901.11275
• A. Agarwal, S. M. Kakade, J. D. Lee and G. Mahajan, On the Theory of Policy Gradient Methods: Optimality, Approximation, and Distribution Shift, Journal of Machine Learning Research 22(98), 2021. https://arxiv.org/abs/1908.00261
• S. Boyd and L. Vandenberghe, Convex Optimization, Cambridge University Press, 2004, Chapter 11. https://web.stanford.edu/~boyd/cvxbook/

Motivation

A reinforcement-learning agent that does not know its environment has to act and learn at once. Each step spent gathering information about unfamiliar states is a step not spent collecting reward, and an agent that only exploits what it already knows may never find better behaviour. Chapter 8 of Kakade's thesis (Kakade 2003) turns this trade-off into a counting question. Run an algorithm for an arbitrarily long time on one unbroken path of experience, with no resets. At how many timesteps does it fail to act optimally with respect to a fixed planning horizon $T$? Kakade calls this number the sample complexity of exploration.

The question builds on two algorithms. $E^3$ (Kearns and Singh 2002) gave the first polynomial-time guarantee for near-optimal behaviour in an unknown MDP. $R_{max}$ (Brafman and Tennenholtz 2002) replaced $E^3$'s explicit explore-or-exploit switch by optimism: unknown states are treated as maximally rewarding. Kakade's chapter sharpens the analysis of $R_{max}$. For deterministic MDPs it shows that the number of non-optimal steps is at most $NAT$, which matches its own lower bound. The thesis notes that its deterministic results are similar to those of Koenig and Simmons (1993), with the dependence on $N$, $A$ and $T$ made explicit (pp. 99, 104). The later PAC-MDP literature (for example Strehl, Li and Littman 2009) took this counting notion as its standard measure of exploration efficiency.

Setting

An MDP $M$ has a finite set $S$ of $N$ states, a finite nonempty set of $A$ actions, a transition model $P(s'\mid s,a)$ and a deterministic reward $r(s,a)\in[0,1]$. A deterministic MDP has a next-state map $f$, with $P(s'\mid s,a)=1$ exactly when $s'=f(s,a)$.

Online model. An algorithm $\mathcal A$ is a deterministic function that maps the path observed so far, $(s_0,a_0,r_0,\dots,s_t)$, to the next action $a_t$. Started at $s_0$, it produces one path $c=(s_0,a_0,s_1,a_1,\dots)$; $c_t$ is the subpath up to $s_t$. The $T$-step end time $t'$ of $t$ is the smallest multiple of $T$ larger than $t$. The $T$-step value of the algorithm on $c_t$ is the normalized reward it collects until $t'$,

$$U_{\mathcal A}(c_t)=\frac1T\,\mathbb E\Big[\sum_{\tau=t}^{t'-1}r(s_\tau,a_\tau)\Big],$$

and $U^*(c_t)$ is the supremum of this quantity over all algorithms continuing from $c_t$.

$T$-step policies. A $T$-step policy $\pi$ is a sequence of deterministic decision rules $\pi(\cdot,0),\dots,\pi(\cdot,T-1)$. Its $t$-value is $U_{\pi,t,M}(s)=\frac1T\mathbb E[\sum_{\tau=t}^{T-1}r(s_\tau,a_\tau)\mid s_t=s]$, and $U^*_{t,M}(s)$ is the supremum over $T$-step policies. For a set of states $K$, the induced MDP $M_K$ agrees with $M$ on $K$ and makes every state outside $K$ absorbing with reward $1$. The escape probability $\Pr(\text{escape from }K\mid\pi,M,s_t=s)$ is the probability that the path $(s_t,\dots,s_{T-1})$ of $\pi$ in $M$ leaves $K$. A transition model $\hat P$ is an $\varepsilon$-approximation to $P$ if $\sum_{s'}|\hat P(s'\mid s,a)-P(s'\mid s,a)|<\varepsilon$ for every $(s,a)$.

Formalization targets

Goal: Theorem 8.3.5 (deterministic sample complexity)

For every $N$, $A$ and $T\ge1$ there is one algorithm $\mathcal A$ such that, for every deterministic MDP with rewards in $[0,1]$, every start state and every $L$,

$$\#\{\,t<L:\ U_{\mathcal A}(c_t)\neq U^*(c_t)\,\}\ \le\ NAT .$$

Milestones

• Lemma 8.4.4 (induced inequalities). For every $T$-step policy, every $t<T$ and every state $s$,

$$U_{\pi,t,M_K}(s)\ge U_{\pi,t,M}(s)\ge U_{\pi,t,M_K}(s)-\Pr(\text{escape from }K\mid\pi,M,s_t=s).$$

• Corollary 8.4.5 (implicit explore or exploit). If $\pi$ is $T$-step optimal in $M_K$, then for every $t<T$ and every state $s$,

$$U_{\pi,t,M}(s)\ge U^*_{t,M}(s)-\Pr(\text{escape from }K\mid\pi,M,s_t=s).$$

• Deterministic escapes (p. 114). In a deterministic MDP every escape probability is $0$ or $1$.
• Non-escaping steps are optimal (p. 114). In a deterministic MDP, an optimal policy of $M_K$ that does not escape from $(s,t)$ satisfies $U_{\pi,t,M}(s)=U^*_{t,M}(s)$.
• Lemma 8.5.4 ($\varepsilon$-approximation condition). If $\hat P$ is an $\varepsilon$-approximation to $P$ and the rewards agree, then $|U_{\pi,t,\hat M}(s)-U_{\pi,t,M}(s)|<\varepsilon T$ for all $\pi$, $s$ and $t<T$.
• Lemma 8.5.5, pinned. If $m\ge\frac{8N}{\varepsilon^2}\log\frac{2N}\delta$ with $\varepsilon>0$, $0<\delta<1$, then the empirical distribution of $m$ independent samples from a distribution $p$ on $N$ points satisfies $\sum_i|\hat p(i)-p(i)|\le\varepsilon$ with probability greater than $1-\delta$.

Significance

The result. The bound $NAT$ does not depend on $L$. However long the agent runs, only a fixed number of its steps fail to be $T$-step optimal. The thesis's Theorem 8.3.6 shows that every algorithm has $\Omega(NAT)$ such steps on some deterministic MDP, so for deterministic MDPs the upper and lower bounds coincide. The induced-MDP lemmas carry over unchanged to stochastic MDPs. Together with Lemmas 8.5.4 and 8.5.5, they give the chapter's general bound (Theorem 8.3.1). They are the template for later optimism-based analyses, which compare an optimistic model with the true one and charge the difference to the probability of leaving the known region.

Formalizing it. The results are proved in the thesis; neither Mathlib nor the Prove2Me catalog contains a machine-checked version of any of them. A complete development would contain:

• a verified finite-horizon dynamic-programming layer (backward recursions, optimal $T$-step values as suprema);
• a simulation lemma in $\ell_1$;
• a concentration bound for empirical distributions whose sample size is linear in $N$;
• an explicit construction of an online exploration algorithm, with a counting argument about its run.

The proof of Lemma 8.5.5 in the thesis uses a Chernoff bound of the form $P(|\hat p_i-p_i|>\alpha p_i)\le2e^{-\alpha^2p_im/2}$. This form fails for the upper tail when $\alpha>1$, so the pinned statement needs a different argument.

Difficulty

The algorithm must be fixed before the MDP. It knows nothing about $f$ or $r$ beyond what its own path reveals, yet the count has to hold for every MDP, every start state and every run length at once. A direct approach could explore each state-action pair once and then plan. That does not bound the count. Exploration is interleaved with exploitation, the agent can only reach unknown pairs through known states, and every step on the way is judged against the full $T$-step optimum of the current cycle. The work lies in charging each non-optimal step to a distinct newly tried state-action pair, with at most $T$ steps charged per pair, while the planning policy is recomputed every time the set of known states grows. In the stochastic lemmas, the main issue is that $U^*_{t,M}$ is a supremum over all $T$-step policies, so the comparison has to go through $M_K$ for every competing policy, not only the planner's.

Formalization scope

• Model. $S$ and $A$ are finite types, $A$ nonempty; $N=|S|$ and $A=|A|$. Rewards are deterministic, with $0\le r\le1$ a hypothesis of every statement. Transition models are IsTransitionKernel functions $P(s'\mid s,a)$.
• Normalization and time. Values carry the factor $1/T$, so they lie in $[0,1]$; epochs are 0-based. $T$-step policies are functions $\mathbb N\to S\to A$, entered into the canonical stochastic $T$-epoch layer as indicator policies. $U^*_{t,M}$ is the supremum over these policies, which is bounded under the hypotheses.
• Online model. In the online model the algorithm has type List (S × A × ℝ) → S → A. The run is defined by recursion and is infinite. $U_{\mathcal A}(c_t)$ is the realised normalized sum up to the end time, and $U^*(c_t)$ is the backward recursion $W_{t'-t}(s_t)$, which is the supremum over algorithms by the Markov property. The count runs over $t<L$ for every $L$.
• Corrections to the printed text. Corollary 8.4.5 is stated for $t<T$, where its quantities are defined; the printed range is $t\le T$. Lemma 8.5.5 carries an explicit sample size in place of $O(\cdot)$.

Four formalizations would make the goal trivial or false, and each is excluded:

• quantifying the algorithm after the MDP, which lets it read $f$ and $r$;
• giving the algorithm a type that takes $f$ or $r$ as an argument;
• defining $U^*$ as a junk real supremum;
• hiding rewards from the observed path, which makes the statement false.

Reusable beyond this mission are the finite-horizon value layer, the induced-MDP and escape-probability lemmas, and the $\ell_1$ concentration bound. Contributions to any of these are useful independently of the goal.

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/
• R. I. Brafman and M. Tennenholtz, R-max — a general polynomial time algorithm for near-optimal reinforcement learning, Journal of Machine Learning Research 3, 2002. https://www.jmlr.org/papers/v3/brafman02a.html
• M. Kearns and S. Singh, Near-optimal reinforcement learning in polynomial time, Machine Learning 49, 2002. https://doi.org/10.1023/A:1017984413808
• A. L. Strehl, L. Li and M. L. Littman, Reinforcement learning in finite MDPs: PAC analysis, Journal of Machine Learning Research 10, 2009. https://jmlr.org/papers/v10/strehl09a.html

Motivation

Planning in a Markov decision process with a large or infinite state space cannot visit every state. The trajectory tree method of Kearns, Mansour and Ng (2000) finds a near-best policy in a class $\Pi$ with a number of generative-model calls independent of the state space, but exponential in the horizon $T$. Chapter 6 of S. M. Kakade's PhD thesis, On the Sample Complexity of Reinforcement Learning (University College London, 2003), trades that exponential factor for a weaker notion of optimality. The weaker notion is tied to a reset distribution $\mu$ that encodes prior knowledge of where good policies spend their time, such as a desired trajectory in robotic control or a known operating regime of a queueing network.

The resulting algorithm, μ-PolicySearch, chooses one decision rule per time step, backward in time, from a hypothesis class $\Pi_1$, optimizing each against states drawn from $\mu$. The same idea was later published as Policy Search by Dynamic Programming (Bagnell, Kakade, Ng and Schneider, NeurIPS 2003). Conservative policy iteration (Kakade and Langford, ICML 2002) carries the same reset-distribution idea into the discounted setting.

Timeline:

• 2000 — Kearns, Mansour and Ng: trajectory trees; uniform convergence over $\Pi$ with $O(2^T)$ dependence on the horizon.
• 2002 — Kakade and Langford: the performance difference lemma for discounted values and conservative policy iteration under a reset distribution.
• 2003 — Kakade's thesis, Chapter 6: μ-optimality (Theorem 6.3.1) and μ-PolicySearch, with sample complexity polynomial in $T$ (Theorem 6.3.3, an $O(\cdot)$ statement not part of this mission).

Setting

A T-epoch MDP has a finite state set $S$, a finite nonempty action set $A$, a transition kernel $P(s'\mid s,a)$, a deterministic reward $r(s,a)\in[0,1]$ and a horizon $T\ge1$. Decision epochs are $t=0,\dots,T-1$. A non-stationary policy $\pi$ gives a distribution $\pi(\cdot\mid s,t)$ over actions at each state and epoch. A decision rule is a map $h:S\to A$. A class $\Pi_1$ of decision rules induces the class $\Pi=\Pi_1^T$ of deterministic policies that use a rule of $\Pi_1$ at every epoch.

Values are normalized. The $t$-value $V_{\pi,t}(s)$ is $\frac1T$ times the expected reward collected from epoch $t$ to $T-1$ when starting in $s$ at epoch $t$, so $V_{\pi,t}(s)\in[0,1]$. The value is $V_\pi(s)=V_{\pi,0}(s)$. 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')]$, and the advantage is $A_{\pi,t}(s,a)=Q_{\pi,t}(s,a)-V_{\pi,t}(s)$. The future state-time distribution of $\pi$ from $s_0$ is $d_{\pi,s_0}(s,t)=\frac1T\Pr(s_t=s\mid\pi,s_0)$ on $S\times\{0,\dots,T-1\}$.

A μ-reset distribution $\mu$ is a family of distributions $\mu(\cdot\mid t)$ on $S$, one per epoch $t<T$. Its joint law, uniform over epochs, is $\mu(s,t)=\mu(s\mid t)/T$. For a decision rule $h$ the μ-advantage is

$$A_{\pi,t}(\mu,h)=\mathbb E_{s\sim\mu(\cdot\mid t)}\big[A_{\pi,t}(s,h(s))\big],$$

and $Q_{\pi,t}(\mu,h)$ is defined in the same way. The ℓ1 distance of two functions on $S\times\{0,\dots,T-1\}$ is $\|p-q\|_1=\sum_s\sum_{t<T}|p(s,t)-q(s,t)|$.

Formalization targets

Goal: μ-optimality (Theorem 6.3.1, p. 75)

If a policy $\pi$ satisfies $A_{\pi,t}(\mu,h)\le\varepsilon/T$ for all $h\in\Pi_1$ and $t<T$, then for all $\pi'\in\Pi$ and all start states $s_0$,

$$V_\pi(s_0)\ge V_{\pi'}(s_0)-\varepsilon-T\,\|d_{\pi',s_0}-\mu\|_1 .$$

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)]$ for all policies $\pi,\pi'$.
• Change of measure, p. 76. $T\,\mathbb E_{d_{\pi',s_0}}\mathbb E_{\pi'}[A_{\pi,t}]\le T\,\mathbb E_{\mu}\mathbb E_{\pi'}[A_{\pi,t}]+T\|d_{\pi',s_0}-\mu\|_1$.
• Lemma 5.3.1, p. 63. The policy returned by non-stationary approximate policy iteration (NAPI) has the same $Q_{\pi,t}$ as the input policy of update $t$. Its advantages are bounded by the per-state errors $\varepsilon_t(s)$ of the PolicyChooser.
• Theorem 6.3.2, p. 76. Exact μ-PolicySearch returns $\tilde\pi$ with $A_{\tilde\pi,t}(\mu,h)\le0$ for all $h\in\Pi_1$, $t<T$.

Significance

Theorem 6.3.1 states what μ-PolicySearch buys. The guarantee holds at every start state, whereas the trajectory tree guarantee holds only at the root it was built for. The policy is guaranteed to compete with each policy of $\Pi$ whose future state-time distribution is close to $\mu$. The penalty $T\|d_{\pi',s_0}-\mu\|_1$ makes the role of the reset distribution precise: it is the price of the change from the "training" distribution $\mu$ to the "test" distribution $d_{\pi',s_0}$. With Theorem 6.3.2 at $\varepsilon=0$, the exact algorithm attains the bound with no slack. The sample-based analysis (Theorem 6.3.3) reduces to controlling the $\varepsilon/T$ condition.

The results are proved in the thesis, and no machine-checked version is known to exist. The mission produces a Lean development of the normalized T-epoch model (non-stationary policies, $t$-values, advantages, future state-time distributions) together with the undiscounted performance difference lemma. These pieces are the common substrate of Chapters 4–6 of the thesis and of later finite-horizon policy-search analyses.

Difficulty

The performance difference lemma relates two objects defined in opposite directions of time: the state distribution of $\pi'$ runs forward from $s_0$, while the $t$-values of $\pi$ are defined backward from the horizon. A formal statement must keep the epochs of the two aligned, including the boundary epochs $t=0$ and $t=T-1$. The change of measure needs the bound $|A_{\pi,t}(s,a)|\le1$, which holds only because values are normalized and rewards lie in $[0,1]$. With unnormalized rewards the constant $T$ in front of the ℓ1 term is wrong.

A first idea is to read the hypothesis as "the advantages are small under $d_{\pi',s_0}$". That reading is not available. The hypothesis controls averages under $\mu$ only, and the gap between the two distributions is exactly the penalty term.

Formalization scope

• The state space is finite (Fintype S), so expectations and the ℓ1 distance are finite sums. The thesis also allows infinite state spaces in this chapter, with integrals in place of sums.
• Epochs are 0-based, $t\in\{0,\dots,T-1\}$, with $T\ge1$.
• Values carry the factor $1/T$. $V_{\pi,t}$ is defined by backward recursion and is $0$ for $t\ge T$.
• Policies are real functions π t s a together with a validity predicate. Deterministic policies $h=(h_t)$ enter as indicator policies $\pi(a\mid s,t)=\mathbf 1[a=h_t(s)]$.
• $\Pi_1$ is an arbitrary set of deterministic decision rules, not assumed finite. Exact μ-PolicySearch is described as a run: the chosen rule at each update is an exact maximizer over $\Pi_1$ of $Q_{\pi,t}(\mu,\cdot)$ for the current policy $\pi$, and the run is stated by hypotheses rather than by a choice of argmax.
• The policy $\pi$ in the goal may be stochastic. The competitors $\pi'$ range over $\Pi_1^T$.
• The μ-mismatch term must stay in the goal. Dropping it, or replacing $d_{\pi',s_0}$ by $\mu$, gives a different and false statement. An empty class $\Pi_1$ makes the conclusion vacuous. That case is harmless, since the conclusion only quantifies over $\pi'\in\Pi_1^T$, and the source has it too.

The T-epoch layer (policies, state distributions, values, advantages, the future state-time distribution) is shared with the other missions of this series (namespaces SampleComplexityRL.PolicyGrad and SampleComplexityRL.Mismeasure); the μ-reset objects are defined in SampleComplexityRL.MuPolicySearch; IsTransitionKernel and IsPolicy are published definitions. Contributions of the performance difference lemma and of general facts about the T-epoch layer (values in $[0,1]$, $d_{\pi,s_0}$ sums to one) are welcome.

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/
• M. Kearns, Y. Mansour, A. Y. Ng, Approximate planning in large POMDPs via reusable trajectories, NeurIPS 12, 2000. https://papers.nips.cc/paper_files/paper/1999
• S. Kakade, J. Langford, Approximately optimal approximate reinforcement learning, ICML 2002. https://dl.acm.org/doi/10.5555/645531.656005
• J. A. Bagnell, S. Kakade, A. Y. Ng, J. Schneider, Policy search by dynamic programming, NeurIPS 16, 2003. https://papers.nips.cc/paper_files/paper/2003

Motivation

Reinforcement-learning methods for Markov decision processes split into critic-only methods, which learn an approximate value function and act greedily with respect to it, and actor-only methods, which adjust a parameterized policy along a simulated estimate of the gradient of its performance. Critic-only methods with function approximation can fail to converge; actor-only gradient estimates have high variance. Actor–critic methods combine the two: a critic learns, by temporal-difference (TD) learning, just enough about the value function to give the actor a low-variance gradient direction.

Konda and Tsitsiklis (SIAM J. Control Optim. 42 (2003)) gave the first convergence proof for actor–critic algorithms whose critic uses linear function approximation. Their key observation, found independently by Sutton, McAllester, Singh and Mansour (NIPS 1999), is that the critic need not approximate the value function: it suffices to compute its projection onto a low-dimensional subspace spanned by features determined by the policy parameterization. Earlier convergence results (Konda and Borkar, 1999) covered lookup-table representations only. Actor–critic algorithms, in many later variants, are now a standard tool of reinforcement learning, and this paper is the reference for their asymptotic analysis in the average-cost setting.

Setting

A finite cost MDP consists of finite sets $\mathbb X$ (states) and $\mathbb U$ (actions), transition probabilities $p(y\mid x,u)$ and a one-stage cost $c(x,u)\in\mathbb R$. A randomized stationary policy with parameter $\theta\in\mathbb R^n$ chooses action $u$ in state $x$ with probability $\mu_\theta(u\mid x)$. Under the policy $\theta$, the states $\{X_k\}$ form a Markov chain with transition matrix $P(\theta)_{xy}=\sum_u\mu_\theta(u\mid x)p(y\mid x,u)$, and the pairs $\{X_k,U_k\}$ a chain with matrix $P_\theta$. When these chains are irreducible and aperiodic, $\pi_\theta$ denotes the stationary law of $\{X_k\}$, $\eta_\theta(x,u)=\pi_\theta(x)\mu_\theta(u\mid x)$, and the average cost is

$$\bar\alpha(\theta)=\sum_{x,u}c(x,u)\,\eta_\theta(x,u).$$

The score is $\psi_\theta(x,u)=\nabla\ln\mu_\theta(u\mid x)\in\mathbb R^n$, and $\langle f,g\rangle_\theta=\sum_{x,u}\eta_\theta(x,u)f(x,u)g(x,u)$.

The critic approximates Q-values by $r'\phi_\theta(x,u)$ with features $\phi_\theta(x,u)\in\mathbb R^m$ whose span contains the components of $\psi_\theta$. Along one simulated trajectory $(\hat X_k,\hat U_k)$, where $\hat U_{k+1}$ is drawn from $\mu_{\theta_k}(\cdot\mid\hat X_{k+1})$, the algorithm updates an average-cost estimate $\alpha_k$, the critic parameter $r_k$ and an eligibility trace $\hat Z_k$ at step size $\gamma_k$ (equation (3.1)), and the actor parameter by

$$\theta_{k+1}=\theta_k-\beta_k\Gamma(r_k)\,r_k'\phi_{\theta_k}(\hat X_{k+1},\hat U_{k+1})\,\psi_{\theta_k}(\hat X_{k+1},\hat U_{k+1})\qquad(3.2)$$

at a slower step size $\beta_k$. The TD(1) critic resets its trace when the state $x^*$ is entered; the TD($\lambda$) critic discounts it by $\lambda\in(0,1)$.

Formalization targets

Goal: Theorem 3.4

Under Assumptions 2.1 (positive, smooth policies; irreducible aperiodic chains; uniform reachability of $x^*$), 3.1–3.2 (bounded smooth features spanning the scores, uniformly nondegenerate) and 3.3 (two-time-scale step sizes and the scaling $\Gamma$),

$$\text{(a) TD(1): }\ \liminf_k|\nabla\bar\alpha(\theta_k)|=0\ \text{ w.p.1};\qquad \text{(b) }\forall\epsilon>0\ \exists\bar\lambda<1\ \forall\lambda\in[\bar\lambda,1):\ \liminf_k|\nabla\bar\alpha(\theta_k)|<\epsilon\ \text{ w.p.1}.$$

The statement leaves the initial parameters and the initial state–action law arbitrary.

Milestones

In attack order: the gradient formula $\nabla\bar\alpha(\theta)=\langle\psi_\theta,Q_\theta\rangle_\theta$ for every Poisson solution, with bounded Hessian (Theorem 4.6); boundedness of the regenerative quantities (Lemma 5.1) and of the trace moments (Lemma 5.2); uniform positive definiteness of the critic's mean matrix $\bar G(\theta)$ for TD(1) and TD($\lambda$) (Lemmas 5.3, 5.6); critic tracking, $|\bar G(\theta_k)R_k-\bar h(\theta_k)|\to0$ (Theorem 5.7); the bias of the actor direction, $\sup_\theta|f(\theta)-\nabla\bar\alpha(\theta)|\le C(1-\lambda)$ (Lemma 6.1); the descent inequality (6.1); and the convergence of the noise terms (Lemma 6.2).

Significance

The theorem says that a policy-gradient method whose gradient is estimated by a linearly parameterized TD critic, rather than by Monte Carlo returns, still converges to a stationary point of the average cost (exactly for TD(1), approximately for TD($\lambda$)). It justifies the compatible features principle (the critic's features must span the score functions), the two-time-scale step-size design, and the trade-off in $\lambda$ between variance and bias of the actor direction. The intermediate results are of independent use: Theorem 4.6 is the average-cost policy-gradient theorem for arbitrary Poisson solutions, and Theorem 5.7 is a tracking result for linear stochastic approximation driven by a Markov chain whose kernel changes slowly.

The result is proved in the paper, but the proofs of Theorem 4.6, of parts of the verification of the stochastic-approximation hypotheses and of Theorem 6.3 are given as outlines, with details deferred to a separate appendix and to Theorem A.7, recalled from another paper. No machine-checked proof of the theorem, or of the convergence of any actor–critic method, is known. The mission asks for a formal proof of the finite-case theorem and its milestones, which fills in the outlined steps. The finite-case gradient formula of §2 (Theorem 2.2, recalled from Marbach and Tsitsiklis) is posed, unproved, elsewhere on the platform in a reward-MDP form; it is a special case of milestone Theorem 4.6.

Difficulty

The obvious argument treats the actor as a stochastic gradient method with a noisy gradient estimate. It fails at the first step: the critic's estimate $r_k'\phi_{\theta_k}$ is biased at every finite time, and the bias does not vanish unless the critic converges, while the critic's target $\bar r(\theta_k)$ moves with the actor. The noise is Markovian, generated by a chain whose transition kernel depends on the current parameter, not a martingale difference sequence. Making the two time scales interact correctly requires a Poisson-equation decomposition of the Markov noise that is uniform in $\theta$, together with moment bounds for the eligibility trace, which for TD(1) is an unbounded sum over a regeneration cycle. Uniformity in $\theta$ is essential, because the actor iterates $\theta_k$ are not assumed to stay in a bounded set.

Formalization scope

State and action sets are finite types; parameters live in EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m), so $|\cdot|$ is the Euclidean norm and Mathlib's gradient is $\nabla$. The transition probability $p(y\mid x,u)$ is stored as p x u y. $\pi_\theta$ is a stationary probability vector of $P(\theta)$, unique under Assumption 2.1(c). The law of the simulated path is built on $(\mathbb X\times\mathbb U)^{\mathbb N}$ by the Ionescu-Tulcea construction (Kernel.trajMeasure), with the next action drawn under the actor parameter that the recursion computes from the history; nothing about the critic or the actor's behaviour is assumed.

Readings and corrections, each also recorded in the affected items:

• Assumption 3.3(b) is corrected. The printed $|r|\Gamma(r)\in[C_1,C_2]$ for all $r$ is unsatisfiable at $r=0$ and would make the theorem vacuous; it is formalized as $(1+|r|)\Gamma(r)\in[C_1,C_2]$, which $\Gamma(r)=1/(1+|r|)$ satisfies. The second inequality of (3.3) is quantified over $\mathbb R^m$, the domain of $\Gamma$, not the printed $\mathbb R^n$.
• Assumption 4.9 (the features have zero mean under $\mu_\theta(\cdot\mid x^*)$) is added to part (a), and to the TD(1) cases of Theorem 5.7 and Lemma 6.2: the TD(1) analysis uses it and Theorem 6.3 assumes it, though Theorem 3.4 does not list it.
• "$\lambda$ sufficiently close to 1" means: some $\bar\lambda<1$ such that all $\lambda\in[\bar\lambda,1)$ work.
• The $\alpha$-update of (3.1) uses $c(\hat X_{k+1},\hat U_{k+1})$ as printed.
• In (6.1), $\Gamma(\bar r(\theta))$ is read as $\Gamma(\bar r(\theta_k))$.
• The matrix $\langle P_\theta^{k+1}\phi_\theta,\phi_\theta'\rangle_\theta$ in the TD($\lambda$) $\bar G_1$ is oriented so that $\bar G_1$ is the steady-state mean of the critic's update matrix.
• Results stated in the paper for Polish spaces (Theorems 4.6, 5.7) are stated under the finite assumptions that the paper says imply them; "w.p.1" in Theorem 5.7 is made explicit.

The $\liminf$ is taken in $[0,\infty]$, so a sequence with $|\nabla\bar\alpha(\theta_k)|\to\infty$ cannot satisfy the conclusion through a junk value, and differentiability of $\bar\alpha$ is part of the conclusion, so the statement cannot hold because Lean's gradient returns $0$ at non-differentiable points. Series (tsum) and matrix inverses in the milestone objects converge, respectively are invertible, under the assumptions. The hypotheses are satisfiable: $\Gamma(r)=1/(1+|r|)$, $\beta_k=(k+1)^{-1}$, $\gamma_k=(k+1)^{-2/3}$ and the features $\phi_\theta=\psi_\theta$ (which satisfy Assumption 4.9 at every state) meet the parts that could be in doubt.

A complete development needs finite Markov-chain theory uniform in a parameter (existence, uniqueness and smooth dependence of stationary laws; geometric ergodicity; Poisson equations; regeneration), differentiation of $\theta\mapsto\pi_\theta$, almost-sure convergence of linear stochastic approximation with Markov noise, and martingale convergence. The Markov-chain and stochastic-approximation parts are reusable well beyond this mission. Contributions of proofs of any milestone, of auxiliary lemmas on parameterized finite Markov chains, and of the general two-time-scale tracking theorem (the paper's Theorem A.7) are welcome.

Selected references

• V. R. Konda and J. N. Tsitsiklis, On Actor-Critic Algorithms, SIAM J. Control Optim. 42(4), 1143–1166, 2003. https://doi.org/10.1137/S0363012901385691
• R. S. Sutton, D. McAllester, S. Singh and Y. Mansour, Policy Gradient Methods for Reinforcement Learning with Function Approximation, NIPS 12, 2000. https://papers.nips.cc/paper/1713-policy-gradient-methods-for-reinforcement-learning-with-function-approximation
• V. R. Konda and V. S. Borkar, Actor-Critic–Type Learning Algorithms for Markov Decision Processes, SIAM J. Control Optim. 38(1), 94–123, 1999. https://doi.org/10.1137/S036301299731669X
• J. N. Tsitsiklis and B. Van Roy, Average Cost Temporal-Difference Learning, Automatica 35(11), 1799–1808, 1999. https://doi.org/10.1016/S0005-1098(99)00099-0
• P. Marbach and J. N. Tsitsiklis, Simulation-Based Optimization of Markov Reward Processes, IEEE Trans. Automat. Control 46(2), 191–209, 2001. https://doi.org/10.1109/9.905687

Why the gradient of the value matters

Policy gradient methods search a parameterized family of stochastic policies $\pi(a\mid s,\theta)$, $\theta\in\mathbb R^k$, by following the gradient of the policy's performance. They are the standard tool when the state space is too large for tabular dynamic programming and when a compact policy class (a neural network, a linear softmax) is easier to represent than a value function. Every such method rests on one identity: a formula for the gradient of the value with respect to $\theta$ that involves only quantities of the current policy, so that it can be estimated from the policy's own trajectories.

Chapter 4 of S. M. Kakade's PhD thesis, On the Sample Complexity of Reinforcement Learning (University College London, 2003), states this identity in two settings, the $T$-epoch undiscounted setting and the $\gamma$-discounted setting, both in the thesis's normalized convention, in which values lie in $[0,1]$. The thesis then uses the formula to analyse how many samples a gradient estimate needs (§4.2.3), and in §5.4.2 rewrites it in terms of advantages to explain why gradient methods can stall far from optimal: the gradient weights advantages by the current policy's state distribution, not by the distribution of an optimal policy.

Timeline:

• 1992: R. J. Williams introduces the likelihood-ratio (REINFORCE) estimator for episodic tasks.
• 2000: Sutton, McAllester, Singh and Mansour state the policy gradient theorem with function approximation, for discounted and average-reward criteria (NeurIPS 1999 proceedings, 2000); Konda and Tsitsiklis give actor-critic counterparts.
• 2001: Baxter and Bartlett analyse biased gradient estimation in the infinite-horizon setting.
• 2003: Kakade's thesis restates both theorems for normalized values, introduces the future state-time distribution $d_{\pi,s_0}$ for non-stationary $T$-epoch policies, and draws the "mismeasure" consequence.

Setting

A finite MDP has a finite state set $S$, a finite nonempty action set $A$, a transition kernel $P(s'\mid s,a)$ and a deterministic reward $r(s,a)\in[0,1]$.

$T$-epoch case. Epochs are $t\in\{0,\dots,T-1\}$, $T\ge1$. A non-stationary policy chooses $a$ at epoch $t$ in state $s$ with probability $\pi(a\mid s,t)$. Starting from $s_0$, $\Pr(s_t=s\mid\pi,s_0)$ is the probability of being in $s$ at epoch $t$. The normalized $t$-value is

$$V_{\pi,t}(s)=\frac1T\,\mathbb E\Big[\sum_{\tau=t}^{T-1}r(s_\tau,a_\tau)\,\Big|\,\pi,s_t=s\Big],\qquad V_\pi=V_{\pi,0},$$

the $t$ 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')]$ with $V_{\pi,T}=0$, and the future state-time distribution on $S\times\{0,\dots,T-1\}$ is $d_{\pi,s_0}(s,t)=\frac1T\Pr(s_t=s\mid\pi,s_0)$.

Discounted case. For a stationary policy $\pi(a\mid s)$ and $0\le\gamma<1$, the normalized value, state-action value, advantage and discounted future state distribution are

$$V_{\pi,\gamma}(s)=(1-\gamma)\,\mathbb E\Big[\sum_{\tau\ge0}\gamma^\tau r(s_\tau,a_\tau)\,\Big|\,\pi,s_0=s\Big],\qquad Q_{\pi,\gamma}(s,a)=(1-\gamma)r(s,a)+\gamma\,\mathbb E_{s'}[V_{\pi,\gamma}(s')],$$ $$A_\pi(s,a)=Q_{\pi,\gamma}(s,a)-V_{\pi,\gamma}(s),\qquad d_{\pi,s_0,\gamma}(s)=(1-\gamma)\sum_{t\ge0}\gamma^t\Pr(s_t=s\mid\pi,s_0).$$

A parameterized policy is a family $\pi(a\mid s,\theta)$ (resp. $\pi(a\mid s,t,\theta)$) of policies indexed by $\theta\in\mathbb R^k$, each entry differentiable in $\theta$; $\nabla$ is the gradient in $\theta$.

Formalization targets

Goal: Theorem 4.2.4 (p. 48)

$$\nabla V_{\pi,\gamma}(s_0)=\frac1{1-\gamma}\,\mathbb E_{s\sim d_{\pi,s_0,\gamma}}\Big[\sum_a\nabla\pi(a\mid s,\theta)\,Q_{\pi,\gamma}(s,a)\Big].$$

The statement asserts that $\theta\mapsto V_{\pi_\theta,\gamma}(s_0)$ is differentiable at the given parameter and that its derivative is the right-hand side. It is the thesis's version of the Sutton–McAllester–Singh–Mansour theorem, and the result the rest of the thesis's discussion of gradient methods builds on.

Milestones

• Value representations (p. 47): $V_\pi(s_0)=\mathbb E_{(s,t)\sim d_{\pi,s_0}}\mathbb E_{a\sim\pi(\cdot\mid s,t)}[r(s,a)]$ and $V_{\pi,\gamma}(s_0)=\mathbb E_{s\sim d_{\pi,s_0,\gamma}}\mathbb E_{a\sim\pi(\cdot\mid s)}[r(s,a)]$.
• Theorem 4.2.3 (p. 48), the $T$-epoch gradient:

$$\nabla V_\pi(s_0)=T\,\mathbb E_{(s,t)\sim d_{\pi,s_0}}\Big[\sum_a\nabla\pi(a\mid s,t,\theta)\,Q_{\pi,t}(s,a)\Big].$$

• The advantage form (§5.4.2, p. 66), with $A=|A|$ the number of actions:

$$\nabla V_\pi(s_0)=\frac{A}{1-\gamma}\,\mathbb E_{s\sim d_{\pi,s_0}}\,\mathbb E_{a\sim\mathrm{Uniform}}\big[A_\pi(s,a)\,\nabla\pi(a\mid s,\theta)\big].$$

Significance

The result. The gradient formula contains no derivative of the state distribution: the effect of $\theta$ on which states are visited cancels, and the gradient is an expectation over states drawn from the current policy, weighted by a sum over actions. This is what makes Monte Carlo and actor-critic estimators possible, and it is the reason the thesis's sample-size analysis of §4.2.3 has no dependence on the size of the state space. The advantage form makes the limitation equally explicit: a small gradient certifies small advantages only under $d_{\pi,s_0}$, while the performance difference lemma (Lemma 5.2.1) shows that closeness to optimal is governed by advantages under $d_{\pi^*,s_0}$. That gap motivates the conservative policy iteration of Chapter 7.

Formalizing it. The theorems are proved in the thesis and in the cited literature; none of them is machine-checked in this normalized convention. The platform has a proved finite-horizon policy gradient theorem for a scalar parameter, a stationary policy and unnormalized values (policy_gradient_discounted_finite, policy_gradient_finite_horizon), and a posed direct-parameterization gradient for Agarwal et al.'s unnormalized discounted value (PolicyGradTheory.ProjGA.direct_gradient). This mission adds the multi-parameter statements, the non-stationary $T$-epoch version with its state-time distribution, and the infinite-horizon discounted version, where differentiability of an infinite series must be established rather than computed from a finite recursion.

Difficulty

In the $T$-epoch case the value is a finite polynomial in the policy entries, and the work is bookkeeping: unrolling the backward recursion for $V_{\pi,t}$ against the forward recursion for $\Pr(s_t=\cdot)$ so that the terms involving $\nabla V_{\pi,t+1}$ telescope. In the discounted case the obvious route, differentiating the recursion $V=(1-\gamma)r_\pi+\gamma P_\pi V$ term by term and recursing forever, presupposes that $\theta\mapsto V_{\pi_\theta,\gamma}(s)$ is differentiable, which the thesis's proof takes for granted. The value is an infinite series in $t$, so that differentiability is a genuine part of the claim, and the resulting formula must be matched with $d_{\pi,s_0,\gamma}$ and $Q_{\pi,\gamma}$, which are themselves defined as infinite series.

Formalization scope

• Finite $S$ and $A$ (Fintype), $A$ nonempty; transition kernel IsTransitionKernel P; rewards in $[0,1]$ as a standing hypothesis of every statement; $0\le\gamma<1$; $T\ge1$. The thesis's later chapters allow infinite state spaces; this mission is finite.
• Normalization exactly as in the thesis: $T$-epoch values and $d_{\pi,s_0}$ carry $1/T$, discounted values and $d_{\pi,s_0,\gamma}$ carry $1-\gamma$. Hence the factors $T$ and $1/(1-\gamma)$ in the gradient formulas.
• The discounted layer is the published normalized model ApproxOptRL.Shared.Model (value, qValue, advantage, futureStateDist; $d_{\pi,s_0,\gamma}$ is futureStateDist at the point mass on $s_0$). The $T$-epoch layer is defined in this mission (TEpoch): 0-based epochs, tValue by backward recursion, tQValue, stateDist, stateTimeDist.
• Parameters live in EuclideanSpace ℝ (Fin k). Every statement assumes that $\pi(\cdot\mid s,\theta)$ (resp. $\pi(\cdot\mid s,t,\theta)$ for $t<T$) is a probability distribution for every $\theta$, and that each entry is differentiable at the parameter $\theta_0$ ("the derivatives $\nabla\pi$ exist", p. 48). Differentiability of the value is not assumed.
• Gradients are stated with HasFDerivAt: the value map has the right-hand side as its Fréchet derivative at $\theta_0$. A statement with fderiv of the value alone, or with a policy that does not depend on $\theta$, would reduce to $0=0$ and is ruled out.
• Expectations over finite sets are finite sums; the uniform expectation over actions is $\frac1{|A|}\sum_a$.
• Contributions welcome: the forward/backward recursion identity for $T$-epoch values, summability and differentiability of the discounted series, and the closed form of $V_{\pi,\gamma}$ via $(I-\gamma P_\pi)^{-1}$; all are reusable by the other missions of this series.

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/
• R. S. Sutton, D. McAllester, S. Singh, Y. Mansour, Policy Gradient Methods for Reinforcement Learning with Function Approximation, Advances in Neural Information Processing Systems 12, 2000. https://proceedings.neurips.cc/paper/1999/hash/464d828b85b0bed98e80ade0a5c43b0f-Abstract.html
• R. J. Williams, Simple statistical gradient-following algorithms for connectionist reinforcement learning, Machine Learning 8, 229–256, 1992. https://doi.org/10.1007/BF00992696
• J. Baxter, P. L. Bartlett, Infinite-Horizon Policy-Gradient Estimation, Journal of Artificial Intelligence Research 15, 319–350, 2001. https://doi.org/10.1613/jair.806
• V. R. Konda, J. N. Tsitsiklis, Actor-Critic Algorithms, Advances in Neural Information Processing Systems 12, 2000. https://proceedings.neurips.cc/paper/1999/hash/6449f44a102fde848669bdd9eb6b76fa-Abstract.html

Motivation

Most practical reinforcement-learning methods do not compute value functions exactly. They alternate between estimating a value function from data, usually with a parametric approximator, and acting greedily with respect to that estimate. Approximate value iteration and approximate policy iteration are the two classical schemes of this kind, and their error analysis decides how accuracy in the estimation step translates into quality of the policies produced. Chapter 3 of S. M. Kakade's thesis On the Sample Complexity of Reinforcement Learning (University College London, 2003) collects the basic guarantees, developed from Bertsekas (Dynamic Programming: Deterministic and Stochastic Models, 1987) for greedy policies, Singh and Yee (1994), and Bertsekas and Tsitsiklis, Neuro-Dynamic Programming (Athena Scientific, 1996). The bounds are stated in terms of the worst-case (max-norm) error of the evaluation step, and the thesis uses them to argue that max-norm error is the obstacle to state-space-independent sample complexity results for these methods, which motivates the later chapters of the thesis.

Setting

A finite discounted Markov decision process consists of a finite set of states $S$, a finite nonempty set of actions $A$, a transition kernel $P(s'\mid s,a)$ (for every $(s,a)$ a probability distribution over $S$), a deterministic reward $r(s,a)\in[0,1]$, and a discount factor $0\le\gamma<1$. A policy $\pi(a\mid s)$ is a probability distribution over actions for every state; a deterministic policy is a map $f:S\to A$, identified with the policy that plays $f(s)$ with probability one.

Values are normalized: the value of $\pi$ at $s$ 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],$$

and 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')]$. With rewards in $[0,1]$, every value lies in $[0,1]$. An optimal policy $\pi^*$ has $V_{\pi^*}(s)\ge V_\pi(s)$ for every policy $\pi$ and state $s$; write $V^*=V_{\pi^*}$ and $Q^*=Q_{\pi^*}$. The max norm is $\|x\|_\infty=\max_s|x(s)|$ on state vectors and $\max_{s,a}|x(s,a)|$ on state-action arrays.

The backup operator is $[BJ](s)=\max_a\big((1-\gamma)r(s,a)+\gamma\,\mathbb E_{s'\sim P(\cdot\mid s,a)}[J(s')]\big)$. A deterministic policy $f$ is greedy with respect to $Q$ if $f(s)\in\arg\max_a Q(s,a)$ for every $s$.

• $\gamma$-approximate value iteration produces vectors $J_0=0,J_1,J_2,\dots$ with $\|J_t-BJ_{t-1}\|_\infty\le\varepsilon$, and greedy policies $\pi_t$ for the lookahead $(1-\gamma)r(s,a)+\gamma\,\mathbb E_{s'}[J_t(s')]$.
• $\gamma$-approximate policy iteration starts from any deterministic $\pi_0$, forms an estimate $\tilde Q_t$ of $Q_{\pi_t}$ with $\|\tilde Q_t-Q_{\pi_t}\|_\infty\le\varepsilon$, and takes $\pi_{t+1}$ greedy with respect to $\tilde Q_t$.

Formalization targets

Goal: Theorem 3.2.2 (approximate policy iteration)

$$\limsup_{t\to\infty}\|V^*-V_{\pi_t}\|_\infty\le\frac{2\varepsilon}{(1-\gamma)^2}.$$

The policies need not converge; the statement bounds where they end up.

Milestones

• Theorem 3.1.1: if $\|\tilde Q-Q^*\|_\infty\le\varepsilon$ and $\pi$ is greedy for $\tilde Q$, then $V_\pi(s)\ge V^*(s)-\frac{2\varepsilon}{1-\gamma}$ for all $s$.
• Lemma 3.2.3: $\|V^*-V_{\pi_{t+1}}\|_\infty\le\gamma\|V^*-V_{\pi_t}\|_\infty+\frac{2\varepsilon}{1-\gamma}$.
• Rate of approximate policy iteration (p. 41): $\|V^*-V_{\pi_t}\|_\infty\le\gamma^t+\frac{2\varepsilon}{(1-\gamma)^2}$.
• Contraction of the backup (p. 26): $\|BJ-BJ'\|_\infty\le\gamma\|J-J'\|_\infty$.
• Approximate value iteration (p. 40): $\|V^*-J_t\|_\infty\le\gamma^t+\frac{\varepsilon}{1-\gamma}$.
• Rate of approximate value iteration (p. 41): $\|V^*-V_{\pi_t}\|_\infty\le\frac{2\gamma^t}{1-\gamma}+\frac{2\varepsilon}{(1-\gamma)^2}$.
• Theorem 3.2.1: the same lim sup bound $\frac{2\varepsilon}{(1-\gamma)^2}$ for approximate value iteration.

Significance

The results give the standard performance guarantee for greedy approximate dynamic programming: an evaluation error of $\varepsilon$ in max norm costs at most $2\varepsilon/(1-\gamma)^2$ in max-norm suboptimality, uniformly over the asymptotic set of policies, with a geometric rate of approach. Example 3.1.2 of the thesis shows that the factor $2\varepsilon/(1-\gamma)$ of Theorem 3.1.1 is attained, so the greedy step itself cannot be improved; the two factors of the horizon $1/(1-\gamma)$ in the limit bound are the reason the thesis turns to other error measures in later chapters.

All the statements are classical and proved in the literature (Bertsekas–Tsitsiklis 1996, Chapter 6, in the unnormalized model and with a factor $\gamma$ to spare in the limit bounds); Lemma 3.2.3 and Theorem 3.2.2 are stated in the thesis without proof. To our knowledge none has a machine-checked proof. The mission produces formal proofs in the normalized model shared with the formalization of Kakade–Langford (2002) on this platform, so later chapters of the series (conservative policy iteration, policy search) can compare against them.

Difficulty

Approximate policy iteration is not monotone: with evaluation errors, $V_{\pi_{t+1}}$ can be worse than $V_{\pi_t}$ at some states, so the argument of exact policy iteration, which uses $V_{\pi_{t+1}}\ge V_{\pi_t}$ everywhere, does not apply. The difficulty of Lemma 3.2.3 is to control the distance to optimality without improvement at each step, combining the greedy step with the lack of monotonicity of the new policy's value; the thesis calls the proof of Theorem 3.2.2 "somewhat technical" and omits it. A second, mechanical difficulty is that the normalized value $V_\pi$ is defined as an infinite series, so its Bellman equation $V_\pi(s)=Q_\pi(s,\pi(s))$, the optimality equation $V^*=BV^*$ and the bound $0\le V_\pi\le1$ have to be derived from that definition before any of the recursions can be run.

Formalization scope

• The model is the published normalized model ApproxOptRL.Shared.Model: value P r γ π is $V_\pi$ (defined as $(1-\gamma)$ times a tsum), qValue is $Q_\pi$. $S$ and $A$ are finite types, $A$ nonempty; $P$ satisfies IsTransitionKernel; every statement assumes $0\le r\le1$ and $0\le\gamma<1$.
• The optimal policy is a binder $\pi^*$ with IsOptimalPolicy P r γ πstar (a stationary stochastic policy dominating every stationary stochastic policy at every state). Such a policy exists for every finite MDP (p. 26 of the thesis), and for finite MDPs it is optimal among all policies.
• Policies of the runs are deterministic, S → A, and are evaluated through the indicator policy detPolicy. "Greedy" is the relation ∀ s a, Q s a ≤ Q s (f s): every tie-breaking rule is covered.
• The runs are sequences indexed by ℕ, with the greedy and accuracy conditions as hypotheses at every index; the value-iteration condition is written for indices $t+1$ and $t$.
• $\|\cdot\|_\infty$ is Mathlib's sup norm on S → ℝ and S → A → ℝ.
• The lim sup statements are in $\varepsilon$–$N$ form: for every $\delta>0$ the bound plus $\delta$ holds eventually.
• Ruled out: the accuracy hypothesis is stated against $Q_{\pi_t}$, the value of the current policy, not against $Q^*$, and the greedy relation genuinely constrains $\pi_{t+1}$; with either changed, the hypotheses would be unsatisfiable or the policies unconstrained and the theorem empty.
• Infrastructure needed and reusable beyond this mission: the Bellman equation of the normalized value for indicator policies, $V^*=BV^*$, monotonicity and contraction of policy-evaluation and backup operators in the normalized model, and the bound $0\le V_\pi\le1$. Contributions of these lemmas are welcome.

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/
• D. P. Bertsekas and J. N. Tsitsiklis, Neuro-Dynamic Programming, Athena Scientific, 1996. ISBN 1-886529-10-8.
• S. P. Singh and R. C. Yee, An upper bound on the loss from approximate optimal-value functions, Machine Learning 16 (1994), 227–233. https://doi.org/10.1007/BF00993104
• S. M. Kakade and J. Langford, Approximately optimal approximate reinforcement learning, ICML 2002. https://dl.acm.org/doi/10.5555/645531.656005