Machine Learning

Motivation

Min-max problems $\min_x\max_y f(x,y)$ model two-player zero-sum games and appear across machine learning and operations research: adversarial training of classifiers, generative adversarial networks, and robust optimization against an adversarial perturbation. When $f$ is convex in $x$ and concave in $y$, von Neumann's minimax theorem gives a saddle point, and first-order methods find approximate ones. In the nonconvex–nonconcave case, which is the case of every neural-network objective, a global min-max point is intractable to find, and local notions such as local min-max points or local Nash equilibria need not exist at all (Jin, Netrapalli and Jordan, ICML 2020; Daskalakis, Skoulakis and Zampetakis, STOC 2021). Without existence there is nothing for an algorithm to converge to.

Mangoubi and Vishnoi propose an equilibrium notion that exists for every smooth bounded objective and can be computed in time polynomial in the dimension and the accuracy (arXiv:2006.12363). The max-player is modelled as an adversary that can only improve $f$ by local, "greedy" moves, and the min-player minimizes the value the adversary can reach this way.

Setting

Write $\mathbb R^d$ for each player's strategy space, with the Euclidean norm, and give $\mathbb R^d\times\mathbb R^d$ the norm $\sqrt{\|x\|^2+\|y\|^2}$. Throughout, $f:\mathbb R^d\times\mathbb R^d\to\mathbb R$ is $C^2$, $b$-bounded ($|f(x,y)|\le b$) and has an $L$-Lipschitz Hessian, $\|\nabla^2f(x,y)-\nabla^2f(\tilde x,\tilde y)\|_{\mathrm{op}}\le L\sqrt{\|x-\tilde x\|^2+\|y-\tilde y\|^2}$.

A point $y$ is an $(\varepsilon,\sqrt{L\varepsilon})$-approximate local maximum of $f(x,\cdot)$ if $\|\nabla_yf(x,y)\|\le\varepsilon$ and $\lambda_{\max}(\nabla_y^2f(x,y))\le\sqrt{L\varepsilon}$.

An $\varepsilon$-greedy path for $f(x,\cdot)$ is a continuous path $\varphi:[0,\tau]\to\mathbb R^d$, differentiable at all but finitely many points, travelling at unit speed, along which $\frac{d}{dt}f(x,\varphi_t)\ge-\varepsilon$ and, at every point, either $f$ increases at rate more than $\varepsilon$ or its second derivative in the direction of travel exceeds $\sqrt{L\varepsilon}$. Let $S_{\varepsilon,x,y}$ be the set of endpoints of $\varepsilon$-greedy paths starting at $y$. The greedy max is

$$g_\varepsilon(x,y)=\sup\{f(x,z):z\in S_{\varepsilon,x,y}\}.$$

The greedy max is in general discontinuous in $x$, so the min-player's stationarity is defined after truncation and Gaussian smoothing. For a bounded $\psi$, a point $x^\star$ is an $(\varepsilon,\sigma)$-approximate local minimum of $\psi$ if

$$\mathcal S(x)=\mathbb E_{\zeta\sim N(0,I_d)}\big[\min(\psi(x+\sigma\zeta),\psi(x^\star))\big]$$

satisfies $\|\nabla\mathcal S(x^\star)\|\le\varepsilon$ and $\lambda_{\min}(\nabla^2\mathcal S(x^\star))\ge-\sqrt\varepsilon$.

A pair $(x^\star,y^\star)$ is an $(\varepsilon,\sigma)$-greedy adversarial equilibrium if $y^\star$ is an $(\varepsilon,\sqrt{L\varepsilon})$-approximate local maximum of $f(x^\star,\cdot)$ and $x^\star$ is an $(\varepsilon,\sigma)$-approximate local minimum of $g_\varepsilon(\cdot,y^\star)$.

Formalization targets

Goal: existence (Theorem 3.1, first two sentences, p. 10)

For every $d\ge1$, $\varepsilon,\sigma>0$ with $\sigma\le1/\sqrt{\varepsilon d}$, and every $f$ as above,

$$\exists\,\varepsilon^\star\in(0,\varepsilon]\ \ \exists\,(x^\star,y^\star):\quad (x^\star,y^\star)\text{ is an }(\varepsilon^\star,\sigma)\text{-greedy adversarial equilibrium of }f.$$

The accuracy $\varepsilon^\star$ is not fixed in advance; the theorem asserts that some accuracy at least as fine as $\varepsilon$ is attained.

Milestones

1. Lemma 7.2 (24)–(25): the output $y_{\mathrm{LocalMax}}$ of the greedy-path subroutine (Algorithm 1) satisfies $\|\nabla_yf\|\le\varepsilon'$ and $\lambda_{\max}(\nabla_y^2f)\le\sqrt{L\varepsilon'}+\mu_4$.
2. Proposition 7.4: the polygonal path traced by Algorithm 1 is a $\frac1{1+\delta}\varepsilon'$-greedy path.
3. Proposition 7.5: the computable lower bound $h_{\varepsilon^\circ}(x,y)=f(x,y_{\mathrm{LocalMax}})$ satisfies $h_{\varepsilon^\circ}\le g_{\varepsilon^\circ}$.
4. Proposition 7.7: the zeroth-order estimator $\hat\Gamma=[\mathbb h(x+\sigma u)-c]\frac1\sigma u$ is unbiased for $\nabla_x\mathfrak h$ and has a sub-Gaussian tail.
5. Lemma 7.3: if $h_\varepsilon$ is a lower bound for $g_\varepsilon$ that agrees with it at $(x^\star,y^\star)$, and the smoothed truncated $h_\varepsilon$ is very nearly second-order stationary at $x^\star$ with a small stochastic gradient, then $x^\star$ is an $(\varepsilon,\sigma)$-approximate local minimum of $g_\varepsilon(\cdot,y^\star)$.

Significance

The theorem gives the first equilibrium notion for nonconvex–nonconcave min-max optimization that is both guaranteed to exist for every $C^2$ bounded objective with Lipschitz Hessian and computable with polynomially many gradient, Hessian and function evaluations. It requires no convexity, monotonicity, bilinearity or initialization near an equilibrium. At an equilibrium, neither player can improve by a local move of the kind second-order methods make: the max-player cannot climb by a greedy path, and the min-player cannot decrease the value the adversary will reach. Appendix A of the paper shows that in the strongly convex–strongly concave case the duality gap at such a point is small, so the notion refines the classical saddle point.

The result is proved on paper and has not been machine-checked. A formalization adds three things beyond the paper. First, a verified calculus of second-order approximate stationarity for discontinuous functions through truncated Gaussian smoothing, reusable for other nonsmooth objectives. Second, a precise account of the paper's conventions: Definition 2.1's second derivative has to be read directionally, (25) holds only with an added $\mu_4$, and Lemma 7.3 holds only for $\sigma,\varepsilon\le1$, as its proof requires. Third, it settles whether the existence statement holds for every $\sigma\le1/\sqrt{\varepsilon d}$, including $\sigma>1$, which the printed proof does not cover.

Difficulty

The obvious approach is to minimize $x\mapsto\max_zf(x,z)$, but that function is intractable to evaluate and need not have approximate local minima reachable by local moves. The greedy max $g_\varepsilon$ replaces it, but $g_\varepsilon$ is a supremum over an uncountable family of paths, cannot be computed exactly, and jumps as $x$ moves: Example 2.4 shows a smooth $f$ whose greedy max is discontinuous. Convolution with a Gaussian restores smoothness but moves local minima (Example 5.5), which is why the definition truncates at $\psi(x^\star)$ before smoothing. The central difficulty is to obtain second-order information about the smoothed truncated $g_\varepsilon$ while only ever evaluating a computable lower bound $h_\varepsilon$; Lemma 7.3 is the step that transfers stationarity from one to the other, and its constants are tight enough that the transfer fails if any hypothesis is weakened.

Formalization scope

$\mathbb R^d$ is EuclideanSpace ℝ (Fin d) and the joint variable lives in WithLp 2 (ℝᵈ × ℝᵈ), so that the Lipschitz-Hessian condition uses the paper's Euclidean norm rather than Lean's sup norm on products. Eigenvalue bounds are quadratic-form bounds on the second Fréchet derivative. Expectations over $N(0,I_d)$ are integrals against stdGaussian, and Gaussian smoothing is the published definition RandomGradFree.Shared.smoothing.

Conventions and readings, each disclosed in the item it affects:

• Definition 2.1 is read with the second derivative of $f(x,\cdot)$ along the direction of travel, $\dot\varphi^\top\nabla_y^2f\,\dot\varphi$, as the paper's proofs use it; "points of differentiability" are interior points.
• $d\ge1$ is added to every statement involving $\sqrt d$ or $1/\sqrt{\varepsilon d}$.
• Definition 2.3 requires the Gaussian integrand to be integrable and asserts the first and second derivatives of $\mathcal S$ before bounding them.
• Algorithm 1 takes an eigen-oracle with $\lambda\ge\lambda_{\max}-\mu_4$ and its hyperparameters $\delta,\mu_1,\mu_3,\mu_4$ as parameters; each milestone assumes exactly the step-size inequalities its proof uses, with $L_2$ a Lipschitz constant of $\nabla f$.
• Lemma 7.2's (25) carries $+\mu_4$, as in the proof's (29).
• Lemma 7.3 carries $\sigma\le1$, $\varepsilon\le1$ and $b\ge1$, which its proof uses; the printed form fails for $\sigma>1$.

The goal cannot be satisfied through Lean's junk values: a non-integrable truncated greedy max would make $\mathcal S\equiv0$, and fderiv of a non-differentiable function is $0$, so Definition 2.3 demands integrability and asserted derivatives, and the supremum defining $g_\varepsilon$ ranges over a set that contains $y$ and is bounded by $b$.

Not formalized: the algorithmic sentences of Theorem 3.1 (success probability $9/10$, polynomial oracle complexity), Algorithm 2 and the milestones about its randomized run (Lemma 7.1, Lemma 7.2 (26)–(27), Propositions 7.6, 7.8–7.10), Lemma 5.1, Corollary 5.2, Appendix A and Appendix B. Algorithm 2 and Propositions 7.8–7.10 are natural follow-up contributions, as is the strongly convex–strongly concave duality-gap bound (Theorem A.1), which reuses this mission's definitions. A complete development needs Gaussian integration by parts in $\mathbb R^d$, differentiation under the integral for Gaussian convolutions of bounded measurable functions, and concentration of $\|\zeta\|$ for $\zeta\sim N(0,I_d)$; all three are reusable beyond this mission.

Selected references

• O. Mangoubi, N. K. Vishnoi, Greedy Adversarial Equilibrium: An Efficient Alternative to Nonconvex–Nonconcave Min-Max Optimization, Mathematics of Operations Research, 2025; read as arXiv:2006.12363v4, 2021. https://arxiv.org/abs/2006.12363
• C. Jin, P. Netrapalli, M. I. Jordan, What is Local Optimality in Nonconvex–Nonconcave Minimax Optimization?, ICML 2020. https://arxiv.org/abs/1902.00618
• C. Daskalakis, S. Skoulakis, M. Zampetakis, The Complexity of Constrained Min-Max Optimization, STOC 2021. https://arxiv.org/abs/2009.09623
• Y. Nesterov, B. T. Polyak, Cubic regularization of Newton method and its global performance, Mathematical Programming 108, 2006. https://doi.org/10.1007/s10107-006-0706-8
• Y. Nesterov, V. Spokoiny, Random Gradient-Free Minimization of Convex Functions, Foundations of Computational Mathematics 17, 2017. https://doi.org/10.1007/s10208-015-9296-2

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

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