Machine Learning

Motivation

In multi-agent reinforcement learning several agents act in a shared, changing environment, each pursuing its own reward. The standard model is the Markov game (stochastic game), going back to Shapley (1953). When agents learn from experience rather than from a known model, the natural target is an equilibrium of the game, and the natural question is how many episodes of play are needed to find one.

Before V-learning, sample-efficient algorithms for general-sum Markov games were centralized and model-based: they estimated quantities indexed by the joint action, so their sample complexity grew with $\prod_{j=1}^m A_j$, exponentially in the number of players $m$. This is the curse of multiagents. Jin, Liu, Wang and Yu (arXiv:2110.14555, journal version in Mathematics of Operations Research, 2024) introduced V-learning, in which every agent runs its own simple algorithm, sees only its own reward and the states, and never needs the other agents' actions. Theorem 6 of the paper shows that the agents' combined output is an approximate coarse correlated equilibrium (CCE) after a number of episodes polynomial in $H$, $S$ and $\max_j A_j$ only.

Timeline:

• 2018: Jin, Allen-Zhu, Bubeck and Jordan analyse optimistic Q-learning with the learning rate $\alpha_t=(H+1)/(H+t)$, the rate V-learning reuses (arXiv:1807.03765).
• 2020: Bai and Jin (arXiv:2002.04017) and Xie et al. give the first sample-efficient algorithms for two-player zero-sum Markov games, based on optimistic value iteration. Bai, Jin and Yu (arXiv:2006.12007, NeurIPS 2020) introduce V-learning, coupled with FTRL, for Nash equilibria of two-player zero-sum games.
• 2021: Liu, Yu, Bai and Jin (arXiv:2010.01604, ICML 2021) learn Nash, CE and CCE of multi-player general-sum games with a centralized model-based method in $O(H^4S^2\prod_jA_j/\varepsilon^2)$ episodes.
• 2021: the present paper (arXiv v1, 27 October 2021) presents V-learning as a generic class of algorithms with any adversarial bandit subroutine and proves Theorem 6; two concurrent works (references [32] and [47] of the paper) obtain CCE guarantees for V-learning-style algorithms with one more factor of $H$.

Setting

A tabular episodic $m$-player Markov game has $S$ states, episodes of $H$ steps, and $A_j$ actions for player $j$; $A=\max_jA_j$. At step $h$ in state $s$ the players choose actions simultaneously, forming a joint action $\boldsymbol a$; player $j$ receives the deterministic reward $r_{j,h}(s,\boldsymbol a)\in[0,1]$, and the next state is drawn from $\mathbb P_h(\cdot\mid s,\boldsymbol a)$. Every episode starts at a fixed state $s_1$.

A joint policy $\pi$ may be correlated: the players share a random seed. $V^\pi_{j,1}(s_1)$ is player $j$'s expected total reward. The best response value $V^{\dagger,\pi_{-j}}_{j,1}(s_1)$ is the largest value player $j$ can obtain by switching to a policy of its own, independent of the shared seed, while the others keep playing $\pi_{-j}$. A joint policy is an $\varepsilon$-CCE if $\max_j\big(V^{\dagger,\pi_{-j}}_{j,1}-V^\pi_{j,1}\big)(s_1)\le\varepsilon$.

V-learning (Algorithm 1). Each player keeps, for every state $s$ and step $h$, a visit count $N_h(s)$, a value estimate $V_{j,h}(s)$ and an adversarial bandit algorithm. After visiting $s$ at step $h$ for the $t$-th time it updates

$$\tilde V_{j,h}(s)\leftarrow(1-\alpha_t)\tilde V_{j,h}(s)+\alpha_t\big(r_{j,h}+V_{j,h+1}(s_{h+1})+\beta_{j,t}\big),\qquad V_{j,h}(s)\leftarrow\min\{H+1-h,\tilde V_{j,h}(s)\},$$

with $\alpha_t=(H+1)/(H+t)$ and a bonus $\beta_{j,t}$, and feeds the loss $(H-r_{j,h}-V_{j,h+1}(s_{h+1}))/H$ of its own action to the $(s,h)$-th bandit, whose next strategy becomes the policy at $(s,h)$. The weights $\alpha^i_t=\alpha_i\prod_{j=i+1}^t(1-\alpha_j)$ express $\tilde V$ as a weighted average of past updates.

The bandit subroutine must satisfy Assumption 1: against any adaptive adversary with noisy, conditionally unbiased feedback, with probability at least $1-\delta$ the $\alpha^i_t$-weighted regret after $t$ rounds is at most $\xi(B,t,\log(1/\delta))$, where $\xi$ is non-decreasing in the number of arms $B$ and has a partial-sum upper bound $\Xi(B,t,\cdot)$ concave in $t$.

The output policy $\hat\pi$ (Algorithm 3) samples an episode index $k$ uniformly from $[K]$; at each step, in state $s$ with $t=N^k_h(s)$ earlier visits in episodes $k^1<\dots<k^t$, it samples $i$ with probability $\alpha^i_t$, sets $k\leftarrow k^i$, and plays the policies the players held at the beginning of episode $k^i$. For the CCE all players use the same sample $i$ (shared seed, §5.1).

Formalization targets

Goal: Theorem 6

With $\iota=\log(mHSAK/\delta)$ and bonuses satisfying $\sum_{i=1}^t\alpha^i_t\beta_{j,i}=\Theta\big(H\xi(A_j,t,\iota)+\sqrt{H^3\iota/t}\big)$ for $t\in[K]$, with probability at least $1-\delta$

$$\max_{j\in[m]}\Big[V^{\dagger,\hat\pi_{-j}}_{j,1}(s_1)-V^{\hat\pi}_{j,1}(s_1)\Big]\le O\Big(\frac{H^2S}{K}\,\Xi(A,K/S,\iota)+\sqrt{\frac{H^5S\iota}{K}}\Big).$$

The goal leaves the bandit algorithm abstract: it holds for every subroutine satisfying Assumption 1.

Milestones

1. Lemma 10: the properties of the weights $\alpha^i_t$.
2. Lemma 11: $\tilde V$ as a weighted sum of past updates.
3. Lemma 12: Assumption 1 transported to every $(s,h,j)$-bandit of the run, with failure probability $\delta$.
4. Lemma 13 (optimism): $V^k_{j,h}\ge V^{\dagger,\hat\pi^k_{-j,h}}_{j,h}$.
5. Lemma 14 (pessimism): $\underline V^k_{j,h}\le V^{\hat\pi^k_h}_{j,h}$ for the analysis-only estimate $\underline V$.
6. The summed gap $\sum_k\max_j[V^k_{j,1}-\underline V^k_{j,1}](s_1)\le O(H^2S\Xi(A,K/S,\iota)+\sqrt{H^5SK\iota})$ (p. 24).

Two further steps of the proof of Theorem 6 are included as items without milestone status: the one-step recursion of $\delta^k_h=\max_j(V^k_{j,h}-\underline V^k_{j,h})(s^k_h)$ (p. 23) and the pigeonhole bound on the summed bonus terms (pp. 23–24).

Significance

With the FTRL subroutine of the paper (Corollary 19: $\Xi(B,t,\log(1/\delta))=20\sqrt{HBt\log(B/\delta)}$), Theorem 6 gives an $\varepsilon$-CCE after $\tilde O(H^5SA/\varepsilon^2)$ episodes, against $H^4S^2\prod_jA_j/\varepsilon^2$ for the earlier centralized method. The same analysis, with a swap-regret subroutine, gives correlated equilibria (Theorem 7) and, specialized to two players with opposite rewards, Nash equilibria of zero-sum games (Theorem 5). The algorithm is decentralized: each agent's computation depends only on the visited states and its own actions and rewards.

The result is proved in the paper; to our knowledge no part of it has been machine-checked. A formalization adds a precise statement of what "independent learning finds a CCE" means for non-Markov, history-dependent output policies, and of the adversary class Assumption 1 must cover for the reduction from the Markov game to the bandits to go through. It also makes explicit the boundary cases the paper leaves implicit (first visits, the last step, the initialization of $\tilde V$).

Difficulty

The deterministic steps (Lemmas 10–11, the recursion and the pigeonhole bound) are algebra on weighted sums. The difficulty is probabilistic. Lemma 12 must view each $(s,h,j)$-bandit as playing against an adversary formed by the rest of the run: the other players, the transitions and the player's own other bandits, all adapted to the past. Lemmas 13 and 14 need concentration of $\alpha^i_t$-weighted martingale sums over random visit times, uniformly over all states, steps, episodes and players.

The best response is the other obstacle. The output policy is not Markov: it carries a latent episode index. The opponent of $\hat\pi_{-j}$ may use the whole history of states and joint actions, and the best response to a non-Markov policy is not given by a Bellman equation. Lemma 13's step (v) handles this; the obvious per-state argument does not apply.

Formalization scope

Everything is finite and real-valued. States, players, actions, steps and episodes are Fin types; steps and episodes are 0-based, so the cap $H+1-h$ is H - h. The bandit rule is a deterministic function from the feedback history to a probability vector, starting uniform. The adversaries of Assumption 1 range over a finitary class: private randomness in an arbitrary finite type, losses chosen from the past before the learner's action, and conditionally unbiased feedback in $[0,1]$. The training law is a finite product of policy and transition probabilities, and every probability is a finite sum over episode sequences. The best response is a supremum over deterministic history-dependent deviations, taken outside the average over the output policy's initial index. $\Theta$ and $O$ are read with a universal lower constant $c_0$ before every instance and an $O$-constant depending only on the upper constant $c_1$.

Added hypotheses, each disclosed in its item: nonnegative bonuses; $K\ge1$; per-player bandit rules sharing one $\xi$; $\xi\ge0$ in the pigeonhole step and the summed-gap milestone; $mHSAK\ge2$ in milestone 6, whose printed form is false without it. The output policy's convention at a first visit ($t=0$) keeps the current index and plays the uniform initial policy.

Two formalizations would trivialize the goal and are ruled out: an Assumption 1 that no algorithm satisfies (a sorry-free check shows every valid rule satisfies it with $\xi\equiv1$), and a best response averaged per latent index or restricted to Markov deviations.

Needed infrastructure: weighted martingale concentration (Azuma–Hoeffding is on the platform), finite-sum manipulation of the training law, and Jensen's inequality for concave functions. Contributions to any milestone are welcome; the deterministic milestones 1, 2 and 6, and the recursion and pigeonhole steps, are independent of the probabilistic ones.

Selected references

• C. Jin, Q. Liu, Y. Wang, T. Yu, V-Learning—A Simple, Efficient, Decentralized Algorithm for Multiagent RL, arXiv:2110.14555v1, 2021; Mathematics of Operations Research, 2024. https://arxiv.org/abs/2110.14555
• C. Jin, Z. Allen-Zhu, S. Bubeck, M. I. Jordan, Is Q-learning Provably Efficient?, NeurIPS 2018. https://arxiv.org/abs/1807.03765
• Y. Bai, C. Jin, Provable Self-Play Algorithms for Competitive Reinforcement Learning, ICML 2020. https://arxiv.org/abs/2002.04017
• Y. Bai, C. Jin, T. Yu, Near-Optimal Reinforcement Learning with Self-Play, NeurIPS 2020. https://arxiv.org/abs/2006.12007
• Q. Liu, T. Yu, Y. Bai, C. Jin, A Sharp Analysis of Model-based Reinforcement Learning with Self-Play, ICML 2021. https://arxiv.org/abs/2010.01604
• L. S. Shapley, Stochastic Games, PNAS 39(10), 1953. https://doi.org/10.1073/pnas.39.10.1095

Motivation

In contextual stochastic optimization a decision $z\in\mathbb R^d$ is chosen after observing features $X\in\mathbb R^p$, and the ideal policy solves, for each feature value,

$$z^*(x)\in\arg\min_{z}\ \mathbb E[c(z;Y)\mid X=x]$$

for a cost $c(z;y)$ and an uncertain outcome $Y$ (inventory demand, asset returns). Kallus and Mao (arXiv:2008.07473, Management Science 2023, doi:10.1287/mnsc.2022.4458) estimate such policies with stochastic optimization forests: random forests whose trees are grown to minimize the downstream decision cost rather than the prediction error of $Y$.

The bottleneck is choosing a split. The natural rule, the oracle criterion, re-solves an optimization problem for every candidate split of every node, which is too expensive inside a forest. The paper replaces it by an approximate risk criterion that needs only a gradient per child and one Hessian per parent, and justifies the replacement by a second-order perturbation analysis. This mission formalizes that justification.

Setting

Let $\mu$ be the law of $X$ on $\mathbb R^p$ and let $\bar c(x,z)=\mathbb E[c(z;Y)\mid X=x]$ be the regression cost. For a region $R\subseteq\mathbb R^p$ with $\mu(R)>0$ write

$$p_R=\mu(R),\qquad f_R(z)=\mathbb E[c(z;Y)\mid X\in R]=\frac1{\mu(R)}\int_R\bar c(x,z)\,d\mu(x).$$

A node of a tree is a region $R_0$; a candidate split is a partition $R_0=R_1\cup R_2$ into disjoint measurable pieces. Abbreviate $p_j=p_{R_j}$, $f_j=f_{R_j}$ for $j=0,1,2$; note $p_1f_1+p_2f_2=p_0f_0$. Let $z_0$ be the unique minimizer of $f_0$, $\nabla f$ the gradient and $\nabla^2 f$ the Hessian in $z$, and $\mathcal D_0=\sup_{x,x'\in R_0}\|x-x'\|_2$ the diameter of $R_0$.

The oracle criterion (eq. (8)) is the optimal cost after the split,

$$\mathcal C^{\mathrm{oracle}}(R_1,R_2)=p_1\min_z f_1(z)+p_2\min_z f_2(z),$$

and the approximate risk criterion (eq. (13)) is

$$\mathcal C^{\mathrm{apx\text{-}risk}}(R_1,R_2)=-\frac12\sum_{j=1,2}p_j\,\nabla f_j(z_0)^\top\bigl(\nabla^2 f_0(z_0)\bigr)^{-1}\nabla f_j(z_0).$$

For $g:\mathbb R^d\to\mathbb R$ the norm (70) is $\|g\|_{\mathcal F}=\max\{\sup_z|g|,\sup_z\|\nabla g\|_2,\sup_z\|\nabla^2 g\|\}$, and $v(f)=\min_z f(z)$.

Formalization targets

Goal: Theorem 2 (pp. 9–10)

Assume $\bar c(x,\cdot)$ is $C^2$ for every $x$; $\bar c$, $\nabla_z\bar c$, $\nabla_z^2\bar c$ are $L$-Lipschitz in $x$ uniformly in $z$; and at an anchor point $\bar x$ the function $\bar c(\bar x,\cdot)$ has a unique, nondegenerate, level-bounded minimizer. Then for every $\varepsilon>0$ there is $\delta>0$ such that every split of a region $R_0\subseteq B(\bar x,\delta)$ satisfying the paper's conditions 1–3 for $j=1,2$ obeys

$$\bigl|\mathcal C^{\mathrm{oracle}}(R_1,R_2)-p_0f_0(z_0)-\mathcal C^{\mathrm{apx\text{-}risk}}(R_1,R_2)\bigr|\le\varepsilon\,p_0\,\mathcal D_0^2 .$$

Since $p_0f_0(z_0)$ does not depend on the split, the two criteria rank splits of a small node alike.

Milestones

1. Region identity (p. 8): $p_1f_1(z)+p_2f_2(z)=p_0f_0(z)$.
2. Example 5 (p. 11): region averages are $C^2$, with gradient and Hessian the region averages of those of $\bar c$.
3. Lipschitz step (p. 81): $\|f_j-f_0\|_{\mathcal F}\le L\mathcal D_0$.
4. Minimizer consistency (p. 74): minimizers of uniformly close functions are close to a unique, level-bounded minimizer.
5. Corollary 1 (p. 64): $v(f+t\delta_f)=v(f)+t\delta_f(z^*)-\tfrac12t^2\nabla\delta_f(z^*)^\top(\nabla^2f(z^*))^{-1}\nabla\delta_f(z^*)+o(t^2)$, and the first-order expansion of the minimizer.
6. Theorem 9 (p. 65): the same expansions at $t=1$ with errors $o(\|\delta_f\|^2_{\mathcal F})$ and $o(\|\delta_f\|_{\mathcal F})$.
7. Uniform Theorem 9 (p. 81): the value expansion of Theorem 9, uniformly over base functions $f_0$ that are $\mathcal F$-close to a fixed nondegenerate $\bar f$.

Significance

Theorem 2 is the guarantee behind the paper's algorithm: the criterion that is cheap to evaluate agrees with the expensive oracle criterion to second order in the node size, so a forest grown with it splits nodes the way a forest grown with the oracle would, while inverting only one Hessian per node. The same perturbation analysis drives the approximate solution criterion (Theorem 3) and, with constraints, Theorems 4 and 6; the unconstrained milestones here (Corollary 1, Theorem 9) are the reusable core.

The result is proved in the paper; nothing here is open. No part of it has a machine-checked proof. The mission produces a formal model of region-averaged costs, a quantitative second-order perturbation theory for unconstrained minimization (Corollary 1 and Theorem 9, which are standard in the Bonnans–Shapiro theory but absent from Mathlib), and a version of Theorem 2 with its limit, uniformity and error scale made explicit.

Difficulty

The expansions are about global minima, and Taylor's theorem only controls local behaviour. The obvious argument expands $f_0+\delta_f$ around $z_0$ and minimizes the quadratic model; it fails when the perturbation creates a competing minimum far from $z_0$, which a small $\|\delta_f\|_{\mathcal F}$ does not rule out when $f_0$ is flat at infinity. Theorem 9 is true only because the minimizer is unique along the whole path $f_0+t\delta_f$, $t\in[0,1]$, which keeps it from jumping.

The second obstacle is uniformity. Theorem 9 is stated for a fixed $f_0$, but in Theorem 2 the base function $f_0$ is the average over $R_0$ and moves as $R_0$ shrinks. The little-$o$ must hold uniformly over base functions near the limit $\bar c(\bar x,\cdot)$; Milestone 7 isolates this step.

Finally, a literal reading of the printed bound $o(\mathcal D_0^2)$ is weak: both $\mathcal C^{\mathrm{oracle}}-p_0f_0(z_0)$ and $\mathcal C^{\mathrm{apx\text{-}risk}}$ are $O(p_0\mathcal D_0^2)$, so the printed bound holds without any second-order cancellation whenever $p_0\to0$. The content is the factor $p_0$.

Formalization scope

Features are EuclideanSpace ℝ (Fin p), decisions EuclideanSpace ℝ (Fin d) (unconstrained, §2). The law $\mu$ is a probability measure. The regression cost $\bar c$ is the primitive; $Y$ and $c(z;y)$ enter only through it (tower property). Gradients are Mathlib's gradient; the Hessian is the derivative of the gradient, and the inverse Hessian is ContinuousLinearMap.inverse, always paired with a positive-definiteness hypothesis so that it is a true inverse. Minima are real infima, and every statement assumes or derives attainment. Little-$o$ claims are $\varepsilon$–$\delta$ statements; "$\|\delta_f\|_{\mathcal F}\le N$" bounds the value, the gradient and the Hessian pointwise, with the Hessian in operator norm (weaker than the paper's Frobenius norm, so the statements are stronger).

Choices made where the page is silent or misprinted, all disclosed in the items:

• the anchor point $\bar x$ and regions in $B(\bar x,\delta)$ name the limit "as the partition becomes finer";
• the error bound carries the factor $p_0$, which implies the printed $o(\mathcal D_0^2)$;
• condition 4 is read as $x$-Lipschitz bounds on $\bar c$, $\nabla_z\bar c$, $\nabla^2_z\bar c$, uniformly in $z$, which is how the proof uses it;
• the minimizer in condition 3 depends on $t$ (the page calls it $z_0$ for every $t$);
• the Lipschitz step is $\|f_j-f_0\|_{\mathcal F}=O(\mathcal D_0)$, not the printed $O(\mathcal D_0^2)$, which is false.

The bound without the factor $p_0$, a reading of condition 3 that forces $f_1=f_2=f_0$ at the optimum, a sup-norm defined by a supremum that is $0$ for unbounded functions, and a radius $\delta$ chosen after the regions would each make the goal trivial; the statements exclude all four.

Infrastructure needed: differentiation of set integrals with $C^2$ integrands (Mathlib's dominated-derivative lemmas suffice), consistency of minimizers under uniform perturbation, local strong convexity from a positive definite Hessian, and the second-order Taylor bound with remainder. The perturbation results (Milestones 4–7) are reusable for any unconstrained parametric minimization. Proofs of any milestone, and of the goal from Milestones 1, 3 and 7, are welcome.

Selected references

• N. Kallus, X. Mao, Stochastic Optimization Forests, Management Science 69(4), 2023. arXiv:2008.07473v6 (2022): https://arxiv.org/abs/2008.07473 ; https://doi.org/10.1287/mnsc.2022.4458
• J. F. Bonnans, A. Shapiro, Perturbation Analysis of Optimization Problems, Springer, 2000. https://doi.org/10.1007/978-1-4612-1394-9
• A. Shapiro, D. Dentcheva, A. Ruszczyński, Lectures on Stochastic Programming: Modeling and Theory, 2nd ed., SIAM, 2014. https://doi.org/10.1137/1.9781611973433
• S. Athey, J. Tibshirani, S. Wager, Generalized Random Forests, Annals of Statistics 47(2), 2019. https://doi.org/10.1214/18-AOS1709

Motivation

Retail inventory records are often wrong. A store's system may report units on the shelf that are not there (phantom inventory), so the replenishment system never reorders and the product silently stops selling. Audits fix such errors but are expensive, so a retailer wants to decide which store–SKU pairs to audit from sales data alone. The classical way, studying each pair's sales history over a long period, needs time-homogeneous data that rarely exists.

Farias, Li and Peng (arXiv:2006.13126v3, Manufacturing & Service Operations Management, 2024) instead use a single cross-sectional snapshot of sales across $n$ stores and $m$ SKUs. Expected demand is modelled as a low-rank matrix, anomalies corrupt a random subset of entries, and only some entries are observed. The paper proposes the entrywise (EW) algorithm and proves that its expected decision cost approaches that of an oracle knowing the model, at rate $\log^{1.5}(m)/\sqrt m$. A matching $\Omega(1/\sqrt m)$ lower bound (Proposition 1) is also proved. The paper evaluates the method on synthetic data and on real data from a consumer goods retailer.

Setting

An instance has an expected-demand matrix $M^*\in\mathbb R_+^{n\times m}$ with $2\le m\le n$, rank $r$ and SVD $M^*=U\Sigma V^\top$ with singular values $\sigma_1^*\ge\dots\ge\sigma_r^*>0$ and $\kappa=\sigma_1^*/\sigma_r^*$. It also has an anomaly model $\mathrm{Anom}(\alpha,M)$, which is a family of laws on $\mathbb N$ indexed by a parameter $\alpha\in\Gamma\subset\mathbb R^d$ and a mean level $M\ge0$. The remaining data are a true parameter $\alpha^*$, an anomaly probability $p_A^*$, an observation probability $p_O$, and costs $c^{(0)}_{ij}$ (flagging a normal entry) and $c^{(1)}_{ij}$ (missing an anomaly). Independently for every entry:

1. the entry is observed with probability $p_O$; the observed set is $\Omega$;
2. $B_{ij}\sim\mathrm{Bernoulli}(p_A^*)$ marks an anomaly;
3. sales are $X_{ij}\sim\mathrm{Poisson}(M^*_{ij})$ if $B_{ij}=0$ and $X_{ij}\sim\mathrm{Anom}(\alpha^*,M^*_{ij})$ if $B_{ij}=1$.

Assumptions (§2):

• $\|M^*\|_{\max}$ lies between a constant $c_M>0$ and $L$.
• Incoherence: $\|U\|_{2,\infty}\le\sqrt{\mu r/n}$ and $\|V\|_{2,\infty}\le\sqrt{\mu r/m}$.
• Sparsity: $\sqrt{p_O}\ge C\log^{1.5}(m)\mu r\kappa^2/\sqrt m$.
• $p_A^*\le1-c_A$.
• $\mathrm{Anom}(\alpha^*,M^*_{ij})$ has sub-exponential norm $\le L$.
• $\mathbb P(\mathrm{Anom}(\alpha,M)=k)$ is $K$-Lipschitz in $(\alpha,M)$.
• Mean decomposition: $\mathbb E\,\mathrm{Anom}(\alpha,M)=g(\alpha)M$ with $g$ valued in $[0,1]$ and $K$-Lipschitz.

The oracle $\pi^*$ knows $\theta^*=(\alpha^*,p_A^*)$ and $M^*$. It computes the posterior $f^*_{ij}=\mathbb P(B_{ij}=0\mid X_\Omega)=y^*_{ij}/(x^*_{ij}+y^*_{ij})$, where $x^*_{ij}=p_A^*\mathbb P_{\mathrm{Anom}(\alpha^*,M^*_{ij})}(X_{ij})$ and $y^*_{ij}=(1-p_A^*)\mathbb P_{\mathrm{Poisson}(M^*_{ij})}(X_{ij})$. It flags $(i,j)$ iff $c^{(1)}_{ij}/(c^{(0)}_{ij}+c^{(1)}_{ij})\ge f^*_{ij}$. The EW algorithm $\pi^{EW}$ runs four steps:

1. It computes $\hat M=\frac{nm}{|\Omega|}\mathrm{SVD}(X_\Omega)_r$, a rescaled best rank-$r$ approximation of the zero-filled observations.
2. It estimates $\hat\theta$ by matching $T$ empirical CDF values $|\{X_{ij}\le t,(i,j)\in\Omega\}|/|\Omega|$ to their model predictions $g_t(\theta,\hat M/e(\theta))$, where $e(\theta)=p_Ag(\alpha)+1-p_A$.
3. It forms plug-in estimates $\hat f_{ij}$ of $f^*_{ij}$.
4. It applies the oracle's threshold rule to $\hat f$.

The cost of decisions $A$ is

$$\mathrm{cost}^A(X_\Omega)=\frac1{|\Omega|}\sum_{(i,j)\in\Omega}\Big(c^{(0)}_{ij}\mathbf 1\{A_{ij}=1\}f^*_{ij}+c^{(1)}_{ij}\mathbf 1\{A_{ij}=0\}(1-f^*_{ij})\Big).$$

Formalization targets

Goal: Theorem 1 (p. 12)

$$\mathbb E_{X_\Omega}\Big(\mathrm{cost}^{\pi^{EW}}(X_\Omega)-\mathrm{cost}^{\pi^*}(X_\Omega)\Big)\le c_{\max}\,C_0\,(1+K+L+\kappa+\mu+r+p_O^{-1})^k\,\frac{\log^{1.5}(m)}{\sqrt m}.$$

The constants $C_0$ and $k$ and the sparsity constant depend only on $d$, $c_M$, $c_A$ and the regularity constant $C_{RC}$. The statement asserts the paper's rate with polynomial dependence on the model parameters. It does not fix the polynomial, so a sharper analysis still proves it.

Milestones, in the proof's order

• Lemma 8: $\|\mathrm{Poisson}(\lambda)\|_{\psi_1}\le4\lambda+1$.
• Lemma 14: a Bernstein bound for $\sum_{(i,j)\in\Omega}T_{ij}$.
• Theorem 2: the entrywise bound $\|\hat M-e(\theta^*)M^*\|_{\max}\le C\delta'$ with $\delta'=\kappa^4\mu rL\sqrt{\log m/(p_Om)}$.
• Lemmas 15 and 16: the model moments and the objective $h(\theta^*)$.
• Lemma 2: $\|F(\hat\theta)-F(\theta^*)\|\lesssim(K+L)\delta'$.
• Lemma 17: a quantitative inverse-function bound.
• Lemma 1: $\|\hat\theta-\theta^*\|\lesssim(K+L)\delta'$.
• Lemmas 18 and 19: plug-in likelihoods and the ratio perturbation bound.
• Lemma 3: $|f^*_{ij}-\hat f_{ij}|\le\min(C\delta/(x^*_{ij}+y^*_{ij}),1)$.
• Step 4 of the proof sketch: the excess cost is at most $\frac1{|\Omega|}\sum_\Omega|a_{ij}-b_{ij}|$.

Significance

Theorem 1 says that the value of cross-sectional data grows with the number of stores and SKUs. A retailer that can only see one snapshot does nearly as well as one that knows the demand matrix and the anomaly law exactly. With Proposition 1, the rate is optimal up to the logarithmic factor. Theorem 2 is, per the authors, the first entrywise guarantee for matrix completion under Poisson (more generally sub-exponential) noise, and it is reusable outside inventory problems.

The results are proved on paper: Theorem 1 by a proof sketch in §5.1 plus Appendix B, and Theorem 2 in Appendix A, which builds on a cited entrywise eigenvector perturbation theorem of Abbe et al. None of this is formalized. A machine-checked proof would also settle the constants and conventions that the paper leaves implicit. These include the dimension restriction in Lemma 17, the unspecified constant in Lemma 3, the form of the sparsity assumption used in the proof of Theorem 2, and the closed range of $p_A$ in $\Theta$.

Difficulty

The obvious argument plugs consistent estimates of $M^*$ and $\theta^*$ into the Bayes rule. It breaks at the first step: a Frobenius-norm bound for $\hat M$, which is what standard matrix completion gives, does not control any single $\hat f_{ij}$. An entrywise bound is needed, under heavy-tailed (sub-exponential, not sub-Gaussian) noise, and with the anomalies corrupting the mean by the unknown factor $e(\theta^*)$. The second step inverts the moment map $F$. Closeness of moments yields closeness of parameters only through a quantitative inverse-function argument, which needs the regularity conditions of Lemma 1. A third subtlety is that $f^*_{ij}$ is a ratio whose denominator $x^*_{ij}+y^*_{ij}$ can be tiny. The error bound of Lemma 3 therefore degrades on rare sales values, and Theorem 1 averages this over the law of $X$.

Formalization scope

One definitions module, InventoryAnomaly.EW.Model, holds the instance, the product sampling law over $\{$observed$\}\times\{$anomalous$\}\times\mathbb N$ per entry, the estimators, the costs and four predicates:

• Model: §2's assumptions;
• SparsityMax: the sparsity condition as read in the proof of Theorem 2, p. 41;
• Regular: Lemma 1's conditions;
• CostBound: costs in $[0,c_{\max}]$.

The sub-exponential norm is the published HighDimProb.Concentration.subexponentialNorm.

Conventions:

• Parameters. $\theta=(\alpha,p_A)\in\mathbb R^{d+1}$, and $T=d+1$ moments are matched.
• Parameter set. $\Theta=\Gamma\times[0,1-c_A]$.
• Clamped means. Laws are evaluated at the mean $\max(M,0)$.
• Cost. The cost is the closed form (5) with $f^*$ by Bayes' rule (8). $c^{(0)}$ is the false-positive cost (the display on p. 12 swaps the labels).
• Estimators. $\mathrm{SVD}_r$ is any exact best rank-$r$ approximation. $\hat\theta$ is any point of $\Theta$ with $h(\hat\theta)\le h(\theta^*)$, which every minimiser of (7) satisfies.
• Constants. "$O(\cdot)$" and "with probability $1-O(1/nm)$" are existential constants. They come after $d,c_M,c_A,C_{RC}$ and before the instance.
• Added conditions. $2\le m\le n$, $1\le r\le m$, finite anomaly means, and nonnegative costs. Lemma 17 is stated for square Jacobians. Lemma 3 has a constant $C$ in place of 2. Lemma 19's $\delta/(\hat x+\hat y)$ clause is stated when $\hat x+\hat y>0$. Each item's Formalization Note lists these.

The algorithm's selections are universally quantified together with their defining properties. Neither may be replaced by unconstrained functions. The cost of $\pi^*$ must use $f^*$, not $\hat f$. The goal must keep the explicit rate $\log^{1.5}(m)/\sqrt m$ and the full probability model, without assuming Theorem 2's event.

Not formalized: Proposition 1 (the lower bound), Appendix E (the TPR/FPR-constrained variant), the cited Lemmas 6–7, and the internal Lemmas 9–13 and Propositions 2–3 of Appendix A.

Useful infrastructure includes entrywise singular-subspace perturbation bounds, Bernstein's inequality for bounded independent sums, and Orlicz-norm bounds for Poisson variables. All three are reusable beyond this mission. Proofs of individual milestones are welcome, especially Lemmas 8, 14, 17 and 19 and Step 4, which are self-contained.

Selected references

• V. F. Farias, A. A. Li, T. Peng, Fixing Inventory Inaccuracies at Scale, Manufacturing & Service Operations Management, 2024; arXiv:2006.13126v3 (2022). https://arxiv.org/abs/2006.13126
• E. Abbe, J. Fan, K. Wang, Y. Zhong, Entrywise Eigenvector Analysis of Random Matrices with Low Expected Rank, Annals of Statistics 48(3), 2020. https://arxiv.org/abs/1709.09565
• A. D. McRae, M. A. Davenport, Low-rank matrix completion and denoising under Poisson noise, Information and Inference 10(2), 2021. https://arxiv.org/abs/1907.05325
• R. Vershynin, High-Dimensional Probability, Cambridge University Press, 2018. https://doi.org/10.1017/9781108231596

Motivation

Several problems in machine learning and game theory are optimization problems over probability measures. Training a wide two-layer neural network can be viewed as minimizing a functional $F(\nu)$ of the distribution $\nu$ of the network's parameters (Mei, Montanari, Nguyen, PNAS 2018; Hu, Ren, Šiška, Szpruch, arXiv:1905.07769). Adding a relative-entropy penalty $\eta H(\nu)$ makes the problem strictly convex in the density and connects its minimizers to the invariant measures of Langevin-type diffusions, the mean-field Langevin dynamics. The first-order condition for the unconstrained problem is Hu et al., Proposition 2.4.

Conforti, Kazeykina and Ren (arXiv:2004.02457v2) add a random environment: a variable $y$ with a fixed law $\mathsf m$ that every player observes, such as the time index in a dynamic game or a shared signal. The strategies are then probability measures on $\mathbb R^d\times\mathbb Y$ whose $\mathbb Y$-marginal is prescribed. Their Theorem 3.1 extends the first-order condition to this constrained problem. The introduction names it "one of our main contributions": it gives the necessary condition for Nash equilibria of games on a random environment (Corollary 3.3), and it identifies the invariant measure of the mean-field Langevin system studied in the rest of the paper.

Setting

Let $\mathbb Y$ be a Polish space with a probability measure $\mathsf m$, and let $p\ge1$. Write $\bar{\mathbb R}^d=\mathbb R^d\times\mathbb Y$ and $\bar x=(x,y)$. The strategy set is

$$\Pi=\{\bar\pi\in\mathcal P_p(\bar{\mathbb R}^d):\ \bar\pi(\mathbb R^d,\cdot)=\mathsf m\},$$

the probability measures on $\bar{\mathbb R}^d$ with finite $p$-th moment and $\mathbb Y$-marginal $\mathsf m$. By disintegration, $\bar\pi(d\bar x)=\pi(dx|y)\,\mathsf m(dy)$.

A function $F:\Pi\to\mathbb R$ has a linear functional derivative $\frac{\delta F}{\delta\bar\pi}:\Pi\times\bar{\mathbb R}^d\to\mathbb R$ if for all $\nu,\nu'\in\Pi$

$$F(\nu')-F(\nu)=\int_0^1\int_{\bar{\mathbb R}^d}\frac{\delta F}{\delta\bar\pi}\big((1-\lambda)\nu+\lambda\nu',\bar x\big)\,(\nu'-\nu)(d\bar x)\,d\lambda. \tag{2.1}$$

Assumption 2.1 asks that $F$ have such a derivative, that $F$ and $\frac{\delta F}{\delta\bar\pi}(\cdot,\bar x)$ be continuous for the $p$-Wasserstein distance $\mathcal W_p$, that $\frac{\delta F}{\delta\bar\pi}(\bar\pi,\cdot,y)$ be continuously differentiable in $x$, and that $\sup_{\bar\pi\in\Pi}|\frac{\delta F}{\delta\bar\pi}(\bar\pi,\bar x)|\le C(1+|\bar x|^p)$.

The regularizer is the relative entropy with respect to $\mathrm{Leb}\times\mathsf m$: if $\bar\pi$ has density $\pi(x|y)$ with respect to $\mathrm{Leb}\times\mathsf m$, then $H(\bar\pi)=\int\ln\pi(x|y)\,\bar\pi(d\bar x)$, and $H(\bar\pi)=+\infty$ otherwise. For $\eta>0$ the objective is

$$V(\bar\pi)=F(\bar\pi)+\eta H(\bar\pi).$$

Formalization targets

Goal: Theorem 3.1 (p. 4)

If $\bar\pi^*\in\operatorname{argmin}_{\bar\pi\in\Pi}V(\bar\pi)$, then $\bar\pi^*$ has a density $\pi^*(x|y)$ which, for $\mathsf m$-a.e. $y$, is positive with $\ln\pi^*(\cdot|y)$ differentiable and

$$\nabla_x\frac{\delta F}{\delta\bar\pi}(\bar\pi^*,x,y)+\eta\nabla_x\ln\pi^*(x|y)=0\qquad\text{for all }x\in\mathbb R^d. \tag{3.1}$$

Conversely, if $F$ is also convex on $\Pi$, every $\bar\pi^*\in\Pi$ satisfying (3.1) minimizes $V$ over $\Pi$. The goal states both directions, as printed.

Milestones (proof of Theorem 3.1, §5.1, pp. 9–11)

1. Step 1 (p. 9): for $\bar\pi,\bar\pi^*\in\Pi$ and $\bar\pi^\lambda=\lambda\bar\pi+(1-\lambda)\bar\pi^*$, $\frac1\varepsilon\int_0^\varepsilon\int\frac{\delta F}{\delta\bar\pi}(\bar\pi^\lambda,\cdot)\,d(\bar\pi-\bar\pi^*)\,d\lambda\to\int\frac{\delta F}{\delta\bar\pi}(\bar\pi^*,\cdot)\,d(\bar\pi-\bar\pi^*)$.
2. (5.1) (p. 10): for a minimizer $\bar\pi^*$ and $\bar\pi\in\Pi$ with $H(\bar\pi)<\infty$, $0\le\int\big(\frac{\delta F}{\delta\bar\pi}(\bar\pi^*,\cdot)+\eta\ln\pi^*\big)\,d(\bar\pi-\bar\pi^*)$.
3. (5.2) (p. 10): for a minimizer, $\Xi_y=\frac{\delta F}{\delta\bar\pi}(\bar\pi^*,\cdot,y)+\eta\ln\pi^*(\cdot|y)$ is $\pi^*(\cdot|y)$-a.s. constant for $\mathsf m$-a.e. $y$.
4. Step 3 (p. 11): a minimizer is equivalent to $\mathrm{Leb}\times\mathsf m$.
5. Sufficiency, $F$-part (p. 11): for convex $F$, $F(\bar\pi)-F(\bar\pi^*)\ge\int\frac{\delta F}{\delta\bar\pi}(\bar\pi^*,\cdot)\,d(\bar\pi-\bar\pi^*)$.
6. Sufficiency, entropy part (p. 11): under (3.1), $H(\bar\pi)-H(\bar\pi^*)\ge\int\ln\pi^*\,d(\bar\pi-\bar\pi^*)$.

Significance

Theorem 3.1 says that each fibre of an entropy-regularized minimizer is a Gibbs measure, $\pi^*(x|y)\propto\exp\big(-\frac1\eta\frac{\delta F}{\delta\bar\pi}(\bar\pi^*,x,y)\big)$. In the paper this yields the Nash-equilibrium condition (3.2) for $n$-player games on a random environment, the uniqueness of equilibria under a monotonicity condition (Corollary 3.4), and the identification of the stationary measures of the mean-field Langevin system (2.2) with these equilibria, the basis of the convergence results (Theorems 3.8–3.12). For a one-player problem it is the optimality condition behind gradient-descent training of mean-field neural networks with an environment variable.

The result is proved in the paper; it is not formalized anywhere known. The mission produces the first machine-checked first-order condition for optimization over probability measures, with or without a marginal constraint, and the supporting objects: the strategy set $\Pi$, the linear functional derivative, and relative entropy with respect to the infinite reference measure $\mathrm{Leb}\times\mathsf m$. The unconstrained case ($\mathbb Y$ a point) is a special case.

Difficulty

The sufficiency direction is two convexity inequalities and a cancellation of the $y$-dependent constants, which uses the common marginal $\mathsf m$. The necessity direction is harder. The first variation of $V$ at $\bar\pi^*$ gives only an inequality (5.1) in the directions $\bar\pi-\bar\pi^*$ with $H(\bar\pi)<\infty$, and the entropy's difference quotient is not dominated where $\pi^*$ is small, so the limit requires a one-sided Fatou argument. The inequality (5.1) is not yet a pointwise equation. Converting it into "$\Xi_y$ is constant" needs admissible competitors with bounded density relative to $\bar\pi^*$, built fibre by fibre in $y$, and these only reach the support of $\bar\pi^*$. Ruling out zeros of $\pi^*$ (Step 3) needs a separate competitor that charges a set where $\pi^*$ vanishes. Finally (3.1) concerns a smooth version of the density, which has to be produced from an almost-everywhere identity. The obvious idea of differentiating $V$ along $\bar\pi^*+\varepsilon\varphi$ for a signed perturbation $\varphi$ fails: such perturbations leave $\Pi$ unless they preserve positivity and the $\mathbb Y$-marginal.

Formalization scope

$\mathbb R^d$ is EuclideanSpace ℝ (Fin d) with Lebesgue measure; $\mathbb Y$ is a complete separable metric space with its Borel $\sigma$-algebra (a Polish space with a fixed compatible metric, needed to state moments and $\mathcal W_p$); $\bar{\mathbb R}^d$ carries the max product metric, and $|\bar x|$ in the growth bound is the distance to a base point $(0,y_0)$, with $C$ and $y_0$ fixed once for all $\bar\pi\in\Pi$. $\mathcal W_p$ is the coupling infimum over this metric, valued in $[0,\infty]$, and continuity is the $\varepsilon$–$\delta$ notion on $\Pi$. $F$ and $\frac{\delta F}{\delta\bar\pi}$ are functions on all measures of which only the values on $\Pi$ matter; $\frac{\delta F}{\delta\bar\pi}$ is part of the data and the theorem holds for every derivative satisfying (2.1). The definition of the derivative makes explicit what (2.1) presupposes: joint measurability in $\bar x$ and integrability in $\lambda$. Mixtures are $(1-t)\nu+t\nu'$ for $t\in[0,1]$, and convexity of $F$ is along these mixtures. $H$ and $V$ take values in $(-\infty,+\infty]$, with $H=+\infty$ off absolute continuity. (3.1) is required of some measurable version of the density, for $\mathsf m$-a.e. $y$ and every $x$, together with positivity and differentiability of $\ln\pi^*(\cdot|y)$.

The Lean logarithm satisfies $\ln 0=0$, a non-integrable Bochner integral is $0$, and the gradient of a non-differentiable function is $0$. These would trivialize the statements, so (3.1) demands differentiability, and the milestones that integrate $\ln\pi^*$ assert integrability and that $\bar\pi$ does not charge $\{\pi^*=0\}$, which is what the paper's convention $\ln0=-\infty$ encodes.

A complete development needs: mixtures and moments of measures in $\Pi$; $\mathcal W_p$-convergence of mixtures; dominated convergence along mixtures; the entropy of a mixture and its one-sided derivative; disintegration with respect to the $\mathbb Y$-marginal; and the passage from an a.e. identity to a smooth version of the density. The mixture, moment and entropy lemmas are reusable for any mean-field optimization problem. Contributions of any of these intermediate results, and of proofs of the milestones in any order, are welcome.

Selected references

• G. Conforti, A. Kazeykina, Z. Ren, Game on random environment, mean-field Langevin system and neural networks, arXiv:2004.02457v2, 2020; Mathematics of Operations Research, 2023. https://arxiv.org/abs/2004.02457v2
• K. Hu, Z. Ren, D. Šiška, L. Szpruch, Mean-field Langevin dynamics and energy landscape of neural networks, arXiv:1905.07769, 2019. https://arxiv.org/abs/1905.07769
• S. Mei, A. Montanari, P.-M. Nguyen, A mean field view of the landscape of two-layer neural networks, PNAS 115 (2018), E7665–E7671. https://doi.org/10.1073/pnas.1806579115
• P. Cardaliaguet, F. Delarue, J.-M. Lasry, P.-L. Lions, The master equation and the convergence problem in mean field games, arXiv:1509.02505, 2015. https://arxiv.org/abs/1509.02505
• R. Jordan, D. Kinderlehrer, F. Otto, The variational formulation of the Fokker–Planck equation, SIAM J. Math. Anal. 29 (1998), 1–17. https://doi.org/10.1137/S0036141096303359

Why neural temporal-difference learning needs a convergence theory

Temporal-difference (TD) learning estimates the value of a policy in a Markov decision process from sampled transitions, by repeatedly moving a parametrized value function towards a one-step bootstrapped target (Sutton, 1988). With a linear parametrization its behaviour is well understood: TD converges to the fixed point of the projected Bellman equation (Tsitsiklis and Van Roy, 1997), with finite-sample rates for projected and stochastic variants (Bhandari, Russo and Singal, 2018). With a nonlinear parametrization the same update can diverge: Tsitsiklis and Van Roy (1997) give an example, and the TD direction is not the gradient of any objective. Deep reinforcement learning nonetheless runs TD with neural networks as a matter of course.

Cai, Yang, Lee and Wang (arXiv:1905.10027v2, Mathematics of Operations Research, 2024) prove that TD with an overparametrized two-layer ReLU network, projected onto a ball around its random initialization, converges at rate $T^{-1/2}$ to the global optimum of the mean-squared projected Bellman error (MSPBE) over a function class that becomes richer as the width grows. This mission formalizes that theorem for the stochastic-semigradient algorithm (Theorem 4.6 of the paper).

Setting

Transitions are tuples $(x, r, x')$ drawn i.i.d. from a sampling law $\mu$: $x, x' \in \mathbb R^d$ are feature vectors of the current and next state–action pair, with $\|x\|_2 = \|x'\|_2 = 1$, the reward satisfies $|r| \le \bar r$, and $x$ and $x'$ have the same distribution (they are drawn from the stationary distribution of the policy). The discount factor is $0 \le \gamma < 1$ and $d \ge 3$.

The value function is the two-layer network

$$\widehat Q(x; W) = \frac{1}{\sqrt m}\sum_{r=1}^m b_r\,\sigma(W_r^\top x), \qquad \sigma(y) = \max\{0, y\},$$

of width $m$, with hidden weights $W = (W_1, \dots, W_m) \in \mathbb R^{md}$ and output weights $b \in \mathbb R^m$. At initialization $b_r \sim \mathrm{Unif}\{-1, 1\}$ and $W_r(0) \sim N(0, I_d/d)$, all independent; only $W$ is trained. The training set is the ball $S_B = \{W : \|W - W(0)\|_2 \le B\}$.

Algorithm 1 (neural TD) samples a tuple at each step $t = 0, \dots, T-2$, forms the Bellman residual $\delta = \widehat Q(x; W(t)) - r - \gamma \widehat Q(x'; W(t))$, takes the semigradient step $W(t) - \eta\,\delta\,\nabla_W \widehat Q(x; W(t))$, projects it onto $S_B$, and outputs $\widehat Q_{\mathrm{out}} = \widehat Q(\cdot\,; \overline W)$ with $\overline W = \frac1T \sum_{t=0}^{T-1} W(t)$.

The linearization of the network at initialization is

$$\widehat Q_0(x; W) = \frac{1}{\sqrt m}\sum_{r=1}^m b_r\,\mathbb 1\{W_r(0)^\top x > 0\}\, W_r^\top x,$$

a linear function of $W$ with random features. Writing $\delta_0$ for the Bellman residual of $\widehat Q_0$, an approximate stationary point is a $W^* \in S_B$ with

$$\mathbb E_\mu\big[\delta_0(x, r, x'; W^*)\,\nabla_W \widehat Q_0(x; W^*)\big]^\top (W - W^*) \ge 0 \quad \text{for all } W \in S_B .$$

The function $\widehat Q_0(\cdot\,; W^*)$ solves the projected Bellman equation over the class $\mathcal F_{B,m} = \{\widehat Q_0(\cdot\,; W) : W \in S_B\}$. The regularity condition (Assumption 4.3) asks for $c_0 > 0$ with $\mu(|w^\top x| \le \tau) \le c_0 \tau$ for every unit vector $w$ and every $\tau \ge 0$.

Formalization targets

Goal: Theorem 4.6

With $\eta = \min\{(1-\gamma)/8,\ 1/\sqrt T\}$ and under Assumption 4.3, there is a constant $C = C(c_0, d, \bar r, \gamma)$ such that for all $m \ge 1$, $B \ge 1$, $T \ge 1$ and every approximate stationary point $W^*$,

$$\mathbb E_{\mathrm{init},\mu}\Big[\big(\widehat Q_{\mathrm{out}}(x) - \widehat Q_0(x; W^*)\big)^2\Big] \le \frac{16\,(B^2 + \sigma_g^2)}{(1-\gamma)^2\sqrt T} + C\big(B^3 m^{-1/2} + B^{5/2} m^{-1/4}\big),$$

where $\sigma_g^2 = 12 + 12B^2 + 3\bar r^2$ and the expectation is over the initialization, the samples of the run and a fresh $x \sim \mu$.

Milestones

1. Lemma 4.2: approximate stationary points exist for every initialization; $\widehat Q_0(\cdot\,; W^*)$ is unique $\mu$-a.e. and is the MSPBE optimum over $\mathcal F_{B,m}$.
2. Lemmas H.1, H.2: the expected fraction of hidden units whose activation can flip inside $S_B$ is $O(B m^{-1/2})$, alone and weighted by $\mathbb E_\mu[\widehat Q(x; W(0))^2]$.
3. Lemmas 5.1, 5.2: the network and its population semigradient stay within $O(B^3 m^{-1/2})$ (in mean square) of their linearizations, for every random parameter in $S_B$.
4. Lemma 4.5: the stochastic semigradient has variance at most $\sigma_g^2$.
5. (C.16): the linearized population semigradient is monotone with modulus $1-\gamma$ in the $\mu$-norm.
6. Lemma 5.4: the stochastic descent inequality for $\mathbb E\|W(t) - W^*\|_2^2$.

Significance

The theorem gives a non-asymptotic guarantee for TD with a nonlinear function class, a setting in which the algorithm can diverge without further structure. The limit object $\widehat Q_0(\cdot\,; W^*)$ is a projected Bellman fixed point over a class that, as $m \to \infty$, approaches a ball in the reproducing kernel Hilbert space of the neural tangent kernel; the paper uses this to bound the distance to the true value function $Q^\pi$ (Proposition 4.7) and to analyze neural Q-learning and policy gradient methods (Section 6). The argument is an instance of the "lazy training" or neural-tangent-kernel regime, in which an overparametrized network trained from a random initialization stays close to its linearization.

The result is proved in the paper and, to our knowledge, has no machine-checked proof. A formalization would also produce reusable components: Gaussian anti-concentration of random ReLU activation patterns (Lemmas H.1–H.2), the linearization error of wide two-layer networks (Lemma 5.1), and a projected stochastic-approximation template with averaged iterates. The appendix proofs are short and pass over several measure-theoretic steps (conditioning on the current iterate, independence of the samples from the initialization, Jensen for the averaged iterate), which a formal proof has to supply.

Difficulty

The TD update is not a gradient, so the convergence proof cannot be a descent argument on an objective. The paper's route is to compare the update with that of the linear TD problem defined by $\widehat Q_0$, whose population semigradient is monotone, and to control the difference by overparametrization. The obvious first approach, linearizing the network in a deterministic neighbourhood of $W(0)$, fails: the ReLU activation pattern $\mathbb 1\{W_r^\top x > 0\}$ can change for some units whatever $m$ is. The comparison holds only in expectation over the random initialization and a fresh input, through Assumption 4.3 and the finiteness of $\mathbb E\,\|w\|_2^{-2}$ for $w \sim N(0, I_d/d)$, which is where $d \ge 3$ enters. The iterates and $W^*$ depend on the initialization, so these bounds are needed for random parameters that are correlated with $W(0)$ but independent of the evaluation point.

Formalization scope

Lean represents points as EuclideanSpace ℝ (Fin d) and parameters as PiLp 2 over Fin m, so all norms on $\mathbb R^{md}$ are $\ell_2$. The MDP, the policy and the feature map are not modelled; the statements see only the sampling law $\mu$ on tuples $(x, r, x')$ with the properties listed above. The run's samples form an $\mathbb N$-indexed i.i.d. sequence (product measure) independent of the initialization, and the evaluation tuple is a fresh draw. Expectations of nonnegative quantities are lower Lebesgue integrals, so non-integrability cannot make a bound hold vacuously. The ReLU semigradient uses the strict convention $\mathbb 1\{W_r^\top x > 0\}$ and keeps the factor $m^{-1/2}$ of (3.2).

Conventions and readings fixed by the formalization, all disclosed in the item statements:

• the paper's "$\sigma_g^2 = O(B^2)$" is pinned to the value $12 + 12B^2 + 3\bar r^2$ produced by its proof;
• the paper's $O(B^3 m^{-1/2} + B^{5/2} m^{-1/4})$ is a constant $C$ depending only on $(c_0, d, \bar r, \gamma)$ and chosen before $m$, $B$, $T$, $\mu$ and $W^*$, with $B \ge 1$ so that lower powers of $B$ are absorbed;
• approximate stationary points are required to lie in $S_B$, as the proof uses;
• Lemmas 5.1 and 5.2 are posed for every random parameter in $S_B$ (the paper's proofs need nothing else and apply them to $\overline W$);
• Lemma 5.4 carries the coefficient $4\eta B$, which is what its proof establishes ($\|W(t) - W^*\|_2 \le 2B$), in place of the printed $2\eta B$.

A formalization in which the comparison point $W^*$ may lie outside $S_B$, the expectation is a Bochner integral of a possibly non-integrable function, or the constant $C$ may depend on $m$, $T$ or $\mu$, would not express the theorem and is excluded. Approximate stationary points are compared through $\widehat Q_0(\cdot\,; W^*)$, never through $\widehat Q(\cdot\,; W^*)$.

A complete development needs Gaussian measures on $\mathbb R^d$ with the integrability of $\|w\|_2^{-2}$ for $d \ge 3$, product and infinite-product probability measures with conditioning on the past of a sequence, existence of solutions to variational inequalities on compact convex sets, and nonexpansiveness of Euclidean projection onto a ball. Proofs of individual milestones are welcome independently; Lemmas H.1, 5.1 and (C.16) are self-contained.

Selected references

• Q. Cai, Z. Yang, J. D. Lee, Z. Wang, Neural temporal-difference and Q-learning provably converge to global optima, Mathematics of Operations Research, 2024; arXiv:1905.10027v2. https://arxiv.org/abs/1905.10027
• R. S. Sutton, Learning to predict by the methods of temporal differences, Machine Learning 3, 1988. https://doi.org/10.1007/BF00115009
• J. N. Tsitsiklis, B. Van Roy, An analysis of temporal-difference learning with function approximation, IEEE Transactions on Automatic Control 42(5), 1997. https://doi.org/10.1109/9.580874
• J. Bhandari, D. Russo, R. Singal, A finite time analysis of temporal difference learning with linear function approximation, COLT 2018. https://arxiv.org/abs/1806.02450
• A. Jacot, F. Gabriel, C. Hongler, Neural tangent kernel: convergence and generalization in neural networks, NeurIPS 2018. https://arxiv.org/abs/1806.07572