Machine Learning

Motivation

Estimating a large matrix that is approximately low rank from a few noisy linear measurements is a basic problem of high-dimensional statistics. It covers matrix completion (recovering a ratings table from a small sample of entries), multi-task regression and quantum state tomography. The standard estimator penalizes the nuclear norm, the sum of the singular values, which is the convex surrogate of the rank. Koltchinskii, Lounici and Tsybakov (arXiv:1011.6256v4; Ann. Statist. 39(5), 2011) study a variant of this estimator that uses the known distribution of the design. Their Theorem 1 proves sharp oracle inequalities, with leading constant 1, under a global isometry condition on the design (Assumption 1).

Global isometry is a strong requirement. For sparse vectors, the analogous requirement was relaxed to the restricted eigenvalue condition of Bickel, Ritov and Tsybakov (Ann. Statist. 37, 2009), which only asks for curvature on a cone of approximately sparse directions. The random-design version is due to Koltchinskii (Bernoulli 15, 2009), and a matrix version of the cone appears in Negahban, Ravikumar, Wainwright and Yu (arXiv:1010.2731). Theorem 2 of the paper is the matrix counterpart of the restricted eigenvalue analysis for this estimator. It keeps the leading constant 1, and the price is a stronger tuning condition, λ ≥ 3‖M‖∞ instead of 2‖M‖∞. Section 5.4 of the same paper derives from it a sharp sparsity oracle inequality for the ordinary vector Lasso.

Setting

Observe n pairs (Xᵢ, Yᵢ), i = 1, …, n, where Xᵢ is a random m₁ × m₂ real matrix and Yᵢ a real random variable, satisfying the trace regression model

$$\mathbb E(Y_i \mid X_i) = \operatorname{tr}(X_i^\top A_0),$$

for an unknown matrix A₀. Write ⟨A, B⟩ = tr(AᵀB), and let ‖A‖₁, ‖A‖₂ and ‖A‖∞ be the nuclear, Frobenius and operator norms, the last being the largest singular value. The design enters through the bilinear form

$$\langle A, B\rangle_{L_2(\Pi)} = \frac1n\sum_{i=1}^n \mathbb E\big(\langle A, X_i\rangle\langle B, X_i\rangle\big),$$

with semi-norm ‖A‖_{L₂(Π)}. Two random objects are built from the sample: the noise matrix M = (1/n) Σᵢ (YᵢXᵢ − 𝔼(YᵢXᵢ)), and, for λ > 0 and a set 𝔸 of matrices, the estimator Â^λ, any minimizer over 𝔸 of

$$L_n(A) = \|A\|_{L_2(\Pi)}^2 - \Big\langle \frac2n\sum_{i=1}^n Y_iX_i, A\Big\rangle + \lambda\|A\|_1 .$$

Let A = Σ_{j≤r} σⱼ uⱼvⱼᵀ be a singular value decomposition, with support (S₁, S₂), the spans of the uⱼ and of the vⱼ. Write 𝒫_A⊥(B) = P_{S₁⊥} B P_{S₂⊥} for the part of B orthogonal to both singular spaces, and 𝒫_A(B) = B − 𝒫_A⊥(B). When 𝔸 is a linear subspace and c₀ ≥ 0, the cone ℂ_{A,c₀} consists of the B ∈ 𝔸 with ‖𝒫_A⊥(B)‖₁ ≤ c₀‖𝒫_A(B)‖₁. The restricted constant μ_{c₀}(A) is the infimum of the μ′ > 0 such that ‖𝒫_A(B)‖₂ ≤ μ′‖B‖{L₂(Π)} for every B ∈ ℂ{A,c₀}. The paper uses μ(A) := μ₅(A).

Formalization targets

Goal: Theorem 2, (2.19)

Let 𝔸 be a linear subspace. If λ ≥ 3‖M‖∞, then

$$\|\hat A^\lambda - A_0\|_{L_2(\Pi)}^2 \le \inf_{A \in \mathbb A}\Big[\|A - A_0\|_{L_2(\Pi)}^2 + \lambda^2\mu^2(A)\operatorname{rank}(A)\Big].$$

The bound is deterministic: it holds for every realization of the sample on which λ ≥ 3‖M‖∞. A₀ need not lie in 𝔸, and nothing is assumed about the design beyond what makes the objects finite.

Milestones

The milestones are the displays of the proof, in the order the proof uses them:

1. (2.8), the inequality obtained from the first-order optimality condition of the estimator, which the proof of Theorem 1 already uses;
2. (2.20), in the case ⟨Â^λ − A₀, Â^λ − A⟩_{L₂(Π)} > 0;
3. (2.21), the splitting of ⟨M, Â^λ − A⟩ along 𝒫_A and 𝒫_A⊥;
4. (2.22), the inequality (λ − 2Δ)‖𝒫_A⊥(Â^λ − A)‖₁ ≤ (λ + 2Δ)‖𝒫_A(Â^λ − A)‖₁ with Δ = ‖M‖∞;
5. the membership Â^λ − A ∈ ℂ_{A,5} and the resulting bound by μ(A);
6. the final two-step display with the constant 1 + 2√2/3.

Significance

Theorem 2 gives a sharp oracle inequality whose only design-dependent quantity is a restricted constant. That constant is finite in situations where the global isometry of Theorem 1 fails. The result covers every linear subspace 𝔸, for example all matrices, the diagonal matrices or matrices with a prescribed sparsity pattern. In the diagonal case it becomes a sharp sparsity oracle inequality for the vector Lasso under a restricted eigenvalue condition (the paper's Theorem 14). The oracle inequalities of Bickel, Ritov and Tsybakov under the same condition have a leading constant larger than 1.

The result is proved in the paper, in about half a page that leans on the proof of Theorem 1. No machine-checked version exists. A formalization pins down two things the printed proof leaves to the reader: the convex-analytic optimality condition behind (2.8), and the "obvious modification of (2.10)" and "some algebra" behind (2.20) and the final display. It also reuses and extends the platform's matrix vocabulary: nuclear and operator norms, SVD data, and the tangent and normal projections of the matrix completion missions.

Difficulty

The estimator is defined implicitly as a minimizer, so the analysis has to go through first-order conditions. Those require the subdifferential of the nuclear norm and a choice of subgradient that matches the support of the comparison matrix A. Mathlib has neither a characterization of this subdifferential nor the monotonicity argument in matrix form. The obvious route, copying Theorem 1, fails at the step that uses Assumption 1 to pass from Frobenius to L₂(Π) norms: without a global isometry, that comparison is available only on the cone ℂ_{A,5}, and the error is known to lie there only in the case ⟨Â^λ − A₀, Â^λ − A⟩_{L₂(Π)} > 0 and only for λ ≥ 3‖M‖∞. The constant 5 = (λ + 2Δ)/(λ − 2Δ) at λ = 3Δ is not slack. A linear subspace, not just a convex set, is needed so that Â^λ − A lies in 𝔸, where the cone lives.

Formalization scope

Matrices are RealMatrix m₁ m₂ from the published MatrixCompletion definitions. These supply ⟨·,·⟩ (matrixInner), the nuclear, Frobenius and operator norms, SVD data SVD A r, the sign matrix Σuⱼvⱼᵀ, and 𝒫_A, 𝒫_A⊥ (tangentProjection, normalProjection). This mission adds two definition files.

• Model. ⟨·,·⟩{L₂(Π)}, M, L_n and the estimator, all at a fixed outcome ω. The structure TraceRegression holds the standing assumptions: measurable Xᵢ and Yᵢ, square-integrable entries of Xᵢ, integrable Yᵢ and YᵢXᵢ, and 𝔼(Yᵢ | σ(Xᵢ)) = tr(XᵢᵀA₀) almost surely. The page leaves the integrability implicit. Without it a Bochner integral would silently be 0 and ‖·‖{L₂(Π)} would be meaningless. Expectations of matrices are entrywise. Independence of the pairs (p. 1) is not assumed: Theorem 2 does not use it. The estimator is any minimizer of L_n over 𝔸.
• Cone and restricted constant. ℂ_{A,c₀} ⊆ 𝔸 and the predicate "μ′ is a cone constant". μ(A) can be +∞ (no constant exists), and a real infimum of an empty set is 0. So every statement is made for every cone constant μ′ for (A, 5). This is equivalent to the infimum form and makes the bound vacuous exactly when the paper's is. A formalization with a real sInf would make (2.19) false and is ruled out.

The other conventions are these. "inf over A ∈ 𝔸" is a bound for every A ∈ 𝔸. rank(A) is Matrix.rank. n ≥ 1 and λ > 0 are assumed, as on the page. (2.8) is stated for a convex 𝔸, as in the proof of Theorem 1 where it is derived. (2.21) is stated for an arbitrary matrix in place of Â^λ − A. No printed statement needed correction.

A complete development needs the subdifferential of the nuclear norm ((2.1) of the paper), the first-order condition for constrained convex minimization, the identity (2.9) and the facts (2.10), and trace duality, which is on the platform as matrix_trace_duality_inequality. The subdifferential of the nuclear norm and the projection estimates are reusable well beyond this mission. Contributions of those general lemmas are welcome.

Selected references

• V. Koltchinskii, K. Lounici, A. B. Tsybakov, Nuclear-norm penalization and optimal rates for noisy low-rank matrix completion, arXiv:1011.6256v4, 2016 (Ann. Statist. 39(5), 2302–2329, 2011). https://arxiv.org/abs/1011.6256
• P. J. Bickel, Y. Ritov, A. B. Tsybakov, Simultaneous analysis of Lasso and Dantzig selector, Ann. Statist. 37(4), 1705–1732, 2009. https://doi.org/10.1214/08-AOS620
• V. Koltchinskii, The Dantzig selector and sparsity oracle inequalities, Bernoulli 15(3), 799–828, 2009. https://doi.org/10.3150/09-BEJ187
• S. Negahban, P. Ravikumar, M. J. Wainwright, B. Yu, A unified framework for high-dimensional analysis of M-estimators with decomposable regularizers, arXiv:1010.2731, 2010 (Statist. Sci. 27(4), 2012). https://arxiv.org/abs/1010.2731
• G. A. Watson, Characterization of the subdifferential of some matrix norms, Linear Algebra Appl. 170, 33–45, 1992. https://doi.org/10.1016/0024-3795(92)90407-2

Motivation

Distributionally robust optimization replaces the expected loss $\mathbb E_{P_0}[\ell(\theta; X)]$ of a statistical model by its worst case over all distributions $Q$ close to the data distribution $P_0$. When closeness is measured by an $f$-divergence ball $\{Q : D_f(Q\|P_0) \le \rho\}$ of fixed radius $\rho > 0$, the robust risk upper-bounds the risk of every subpopulation of $P_0$ that has sufficiently large probability, so a model with small robust risk performs uniformly well across latent subgroups. This is the program of J. C. Duchi and H. Namkoong, Learning Models with Uniform Performance via Distributionally Robust Optimization (arXiv:1810.08750; Ann. Statist. 49 (2021), doi:10.1214/20-AOS2004).

The robust risk is itself a statistical functional. It is estimated by plugging in the empirical distribution, and the paper shows (its Theorem 2) that for the Cressie–Read family of divergences with parameter $k$ the plug-in estimate concentrates at rate $n^{-1/(k_* \vee 2)}$, with $k_* = k/(k-1)$. For small $k$ (heavy protection against distribution shift) $k_*$ is large and this rate is far slower than the parametric $n^{-1/2}$. This mission formalizes the paper's answer to whether the slow rate is an artefact of the plug-in estimator or intrinsic: its Theorem 3, a minimax lower bound valid for every estimator.

Setting

Fix $k \in (1,\infty)$ and write $k_* = k/(k-1)$. The Cressie–Read function is

$$f_k(t) = \frac{t^k - kt + k - 1}{k(k-1)} \quad (t \ge 0), \qquad f_k(t) = +\infty \quad (t < 0).$$

For a probability measure $P$, a real random variable $Z$ and a radius $\rho > 0$, the robust risk is

$$\mathcal R_k(Z) = \sup\Bigl\{ \mathbb E_P[LZ] : L \ge 0,\ \mathbb E_P[L] = 1,\ \mathbb E_P[f_k(L)] \le \rho \Bigr\},$$

the supremum of $\mathbb E_Q[Z]$ over distributions $Q \ll P$ with likelihood ratio $L = dQ/dP$ and Cressie–Read divergence $D_{f_k}(Q\|P) = \mathbb E_P[f_k(L)]$ at most $\rho$.

Write

$$c_k(\rho) = (1 + k(k-1)\rho)^{1/k}, \qquad p_k = (1 + k(k-1)\rho)^{-1/(k-1)}, \qquad \beta_k = \frac{k(k-1)\rho}{2(1+k(k-1)\rho)} .$$

Fix $M > 0$ and let $\mathcal P$ be the set of all distributions on the two points $\{0, M\}$; each is determined by its mass $p \in [0,1]$ at $M$. An estimator is any function $\widehat R : \{0, M\}^n \to \mathbb R$ of a sample $Z_1^n = (Z_1, \dots, Z_n)$ drawn i.i.d. from $P_0 \in \mathcal P$. The minimax risk of estimating the robust risk is

$$\mathfrak M_n(\mathcal P, f_k) = \inf_{\widehat R}\ \sup_{P_0 \in \mathcal P}\ \mathbb E_{P_0^n}\bigl|\widehat R(Z_1^n) - \mathcal R_k(Z)\bigr|, \qquad Z \sim P_0. \qquad (16)$$

The total variation distance between two product laws $P^n, P'^n$ on the finite set $\{0,M\}^n$ is $\|P^n - P'^n\|_{\mathrm{TV}} = \tfrac12\sum_z |P^n\{z\} - P'^n\{z\}|$, and $D_{\mathrm{kl}}$ denotes the Kullback–Leibler divergence.

Formalization targets

Goal: Theorem 3

For every $n \ge 1$,

$$\mathfrak M_n(\mathcal P, f_k) \ge M \max\Biggl\{ \frac{1}{8 k_* p_k}\Bigl( \sqrt{\frac{p_k(1-p_k)}{16 n}} \wedge \tfrac12(1-p_k) \wedge p_k \Bigr),\ \ \frac18 \beta_k^{1/k} c_k(\rho) \Bigl( \frac{1}{4n} \wedge p_k \wedge \bigl(1 - (1-\beta_k)^{1-k_*} p_k\bigr) \Bigr)^{1/k_*} \Biggr\}.$$

The first branch is of order $n^{-1/2}$, the second of order $n^{-1/k_*}$. The page prints $8n$ in the first branch; the target uses $16n$ (see Formalization scope).

Milestones

1. Lemma 12 (three claims): for $Z$ equal to $z_0 \le z_1$ with probabilities $1-p$, $p$: if $p \ge p_k$ then $\mathcal R_k(Z) = z_1$; if $p \le p_k$ then $\mathcal R_k(Z) \le c_k p^{1/k_*} z_1 + (1 - c_k p^{1/k_*}) z_0$; and if $p \le p_k \wedge (1 - (1-\beta)^{1-k_*} p_k)$ for some $\beta \in (0,1)$ then $\mathcal R_k(Z) \ge \beta^{1/k} c_k p^{1/k_*} z_1 + (1 - \beta^{1/k} c_k p^{1/k_*}) z_0$.
2. The primal two-point formula (p. 47): for $p \in (0,1)$,

$$\mathcal R_k(Z) = z_0 + (z_1 - z_0)\sup\{q \in [0,1] : (1-p)^{1-k}(1-q)^k + p^{1-k}q^k \le c_k^k\}.$$

3. Le Cam's reduction (37): if $|\mathcal R_k(P_0) - \mathcal R_k(P_1)| \ge 2\delta > 0$ then $\mathfrak M_n \ge \frac\delta2(1 - \|P_0^n - P_1^n\|_{\mathrm{TV}})$.
4. The Taylor display $c_k(p_k - \delta)^{1/k_*} \le 1 - \frac{1}{k_*}c_k^{k_*}\delta$ for $0 < \delta \le p_k$.
5. The KL display $D_{\mathrm{kl}}(P_2\|P_1) \le 8\delta^2/(p_k(1-p_k))$ for the laws with masses $p_k \mp \delta$ at $M$.
6. Pinsker for products $\|P_1^n - P_2^n\|_{\mathrm{TV}}^2 \le \frac n2 D_{\mathrm{kl}}(P_2\|P_1)$.
7. The second-branch KL display $-\log(1-\delta) \le \delta/(1-\delta) \le 2\delta$ for $\delta \le \frac12$.

Significance

Theorem 3 shows that the rate $n^{-1/(k_* \vee 2)}$ of the paper's concentration bound for the plug-in robust risk cannot be improved by any estimator, even when the data take only two values. For $k < 2$ the robust risk is therefore intrinsically harder to estimate than a mean: its value depends on how much mass $P_0$ puts on rare large values, and rare events are observed rarely. The same phenomenon drives the paper's lower bounds for minimizing the robust risk (its Section 5.2), which are not part of this mission.

The result is proved in the paper; no machine-checked version of it or of Lemma 12 is known. Formalizing it produces a verified two-point analysis of the Cressie–Read robust risk (Lemma 12 and its primal formula), which is reusable for any lower bound or worked example involving $f$-divergence balls, and a verified finite-sample Le Cam two-point bound for estimating a functional of a distribution on two points. It also corrects a constant in the first branch of the printed statement.

Difficulty

The lower bound needs two distributions on $\{0,M\}$ that are statistically close yet have well-separated robust risks. Both requirements must be quantitative and must hold simultaneously at the stated constants. The robust risk is a supremum over an infinite-dimensional set of likelihood ratios, so the separation needs exact control of that supremum for two-point laws: an exact value above the threshold $p_k$, and matching upper and lower bounds below it. For mass near $p_k$ the separation is linear in $\delta$, while for small mass it is of order $\delta^{1/k_*}$, which is where the slow rate comes from. Closeness requires the KL divergence of each pair to be at most $1/(2n)$, and the two branches need different perturbations. A naive bound on the robust risk by $\max(z_0, z_1)$ or by the mean gives no separation at all.

Formalization scope

The Lean development lives in the namespace UniformDRO.LowerBound. Its conventions are:

• $k > 1$, $\rho > 0$, $M > 0$ (all on the page); $n \ge 1$ in the goal (implicit on the page, since the bound contains $1/n$).
• The robust risk is the real supremum in the likelihood-ratio form above, with the divergence constraint written as a lower Lebesgue integral of $f_k(L) \ge 0$. Absolute continuity $Q \ll P$ is built in. For a two-point law the feasible values lie between the two points, so the supremum is genuine.
• Laws on $\{0,M\}$ are $(1-p)\delta_0 + p\,\delta_M$, $p \in [0,1]$. Expectations under $P_0^n$ are finite sums over $\{0,M\}^n$. The minimax risk takes values in $[0,\infty]$, with the infimum over all real functions of the sample taken outside the supremum over $p$. For these laws it agrees with the platform's general HighDimStat.Minimax.minimaxRisk.
• $D_{\mathrm{kl}}$ between two-point laws is the platform's BanditAlgorithm.bernoulliRelativeEntropy, always evaluated with a second argument in $(0,1)$, where it is the true divergence.
• Real powers are Real.rpow. The primal formula is stated for $p \in (0,1)$, where its negative powers are finite.
• Correction of the print. In Theorem 3 the page has $\sqrt{p_k(1-p_k)/(8n)}$. The paper's argument with that choice gives $D_{\mathrm{kl}} \le 1/n$ and, by Pinsker, total variation at most $1/\sqrt2$, which does not yield the printed constant $1/(8k_*p_k)$. The target uses $16n$, for which the same argument gives total variation at most $\tfrac12$ and exactly the printed constant. The second branch is as printed. The milestone quotes keep the page's text.

The goal is the lower bound on the minimax risk (16) over all estimators and all laws on $\{0,M\}$. It does not mention the two hypotheses, $\delta$, total variation or KL divergence, so it cannot be satisfied by a statement about a particular pair of laws or a particular estimator.

Contributions are welcome at every level: proofs of Lemma 12 through the primal formula or through the dual representation of the robust risk, a general finite-space Le Cam lemma, and tensorization of KL and Pinsker for finite products, which are reusable beyond this mission.

Selected references

• J. C. Duchi and H. Namkoong, Learning Models with Uniform Performance via Distributionally Robust Optimization, Ann. Statist. 49(3), 2021; arXiv:1810.08750v6. https://arxiv.org/abs/1810.08750, https://doi.org/10.1214/20-AOS2004
• L. Le Cam, Asymptotic Methods in Statistical Decision Theory, Springer, 1986. https://doi.org/10.1007/978-1-4612-4946-7
• B. Yu, Assouad, Fano, and Le Cam, in Festschrift for Lucien Le Cam, Springer, 1997, 423–435. https://doi.org/10.1007/978-1-4612-1880-7_29
• A. B. Tsybakov, Introduction to Nonparametric Estimation, Springer, 2009. https://doi.org/10.1007/b13794
• N. Cressie and T. R. C. Read, Multinomial goodness-of-fit tests, J. R. Stat. Soc. B 46(3), 1984, 440–464. https://doi.org/10.1111/j.2517-6161.1984.tb01318.x

Motivation

Support vector machines classify observations by choosing a real-valued function from a reproducing kernel Hilbert space and using its sign as the predicted label. The Gaussian kernel is widely used because it gives a flexible class of functions, but that flexibility alone does not explain how quickly classification error approaches the best possible error as the training sample grows. Steinwart and Scovel's 2007 paper identifies distributional conditions under which a Gaussian-kernel SVM achieves a polynomial, and sometimes nearly linear, excess-risk rate. The conditions describe both ambiguity in the labels and the location of data relative to the decision boundary.

The article's result is already proved mathematically. This mission asks for machine-checked statements and proofs of its finite-geometric-exponent, no-offset rate and selected supporting results. It uses arXiv:0708.1838v1, the electronic reprint of the Annals of Statistics article. Its printed page number equals its PDF page number throughout; all page references below use those numbers.

Setting

Let $X$ be the closed unit ball of $\mathbb R^d$, where $d>0$, and let the label set be $Y=\{-1,1\}$. A distribution $P$ on $X\times Y$ has input marginal $\mu=P_X$ and a measurable regression function $\eta(x)=P(y=1\mid x)$. In the Lean representation, $\mu$ and one version of $\eta$ are carried explicitly; the joint law gives conditional masses $\eta(x)$ and $1-\eta(x)$ to the two labels. Classification predicts $\operatorname{sign}f(x)$, with $\operatorname{sign}(0)=1$. Write $R_P(f)$ for its error probability and $R_P$ for the smallest such risk over measurable decision functions.

The hinge loss is $\ell(y,t)=\max\{0,1-yt\}$. The Gaussian kernel with parameter $\sigma>0$ is $k_\sigma(x,x')=\exp(-\sigma^2\|x-x'\|^2)$, and $H_\sigma(X)$ is its restricted RKHS. Given a sample $T$ of size $n$, an SVM without offset minimizes $\lambda\|f\|^2_{H_\sigma(X)}+R_{\ell,T}(f)$ over that space. The approximation error $a_\sigma(\lambda)$ is the infimum of the corresponding population objective minus the unrestricted Bayes hinge risk; equation (6) uses that unrestricted baseline.

Two assumptions describe the distribution. It has Tsybakov noise exponent $q\in[0,\infty]$ if, for sufficiently small $t>0$, $\mu\{|2\eta-1|\le t\}\le C t^q$ for some $C>0$. To define geometric noise exponent $\alpha>0$, partition $X$ according to whether $\eta$ is below, above, or equal to $1/2$. The distance $\tau_x$ goes from a point in either strict class to the opposite strict class together with the equal-probability class. The geometric condition is

$$\int_X |2\eta(x)-1|\exp(-\tau_x^2/t)\,d\mu(x) \le C t^{\alpha d/2}\qquad(t>0).$$

These are Definitions 2.2 and 2.3 and equation (7) of the paper.

Formalization targets

The goal is the finite-$\alpha$, no-offset clause of Theorem 2.8. With the paper's two-case exponent $\beta=\beta(\alpha,q)$, set $\lambda_n=n^{-(\alpha+1)\beta/\alpha}$ and $\sigma_n=n^{\beta/(\alpha d)}$. For every $\varepsilon>0$, one constant $C>0$ works uniformly for $x\ge1$ and $n\ge1$:

$$\Pr^*\!\left\{T:R_P(f_{T,\lambda_n}) \le R_P+C x^2n^{-\beta+\varepsilon}\right\}\ge1-e^{-x}.$$

Here $\Pr^*$ is outer probability, and the statement applies to every empirical minimizer. The formula for $\beta$ is $\alpha/(2\alpha+1)$ in the first case, $\alpha\le(q+2)/(2q)$, and $2\alpha(q+1)/(2\alpha(q+2)+3q+4)$ otherwise; the paper's limiting convention specifies $q=\infty$.

Three milestones record results used on this path. Theorem 2.1 bounds empirical covering numbers of Gaussian RKHS balls, uniformly in $\sigma$ and the sample. Lemma 4.1 locates balls of radius $\tau_x$ inside the corresponding enlarged decision class. Theorem 2.7 bounds the approximation error by

$$a_\sigma(\lambda)\le c_d\bigl(\sigma^d\lambda+C(2d)^{\alpha d/2}\sigma^{-\alpha d}\bigr),$$

where $c_d$ depends only on dimension. Their exact source text and page positions appear in the milestone list.

Significance

Theorem 2.8 gives a quantitative guarantee for classification risk, rather than only convergence of the regularized hinge objective. The rate responds to both the label-noise exponent and the concentration of input mass near the decision boundary. In the regimes discussed after the theorem, the exponent can approach one; the paper's Remark 2.9 compares it with the $n^{-1/2}$ benchmark.

Formalizing this result adds a concrete Gaussian RKHS norm compatible with a kernel parameter that changes with $n$, an explicit binary-law model, extended-valued risks and covering numbers, and source-indexed bounds on approximation and complexity. Those objects can be reused in later SVM and kernel-learning statements. The paper's argument is a published proof; the Lean theorem files here are open proof obligations, while the definition files have compiled bodies. No claim of a machine-checked proof of the rate is made.

Difficulty

It is not enough to combine a general consistency theorem with the noise assumptions. The kernel parameter grows with sample size, so the relevant hypothesis class changes with $n$; a complexity estimate for one fixed class gives no uniform rate. Geometric noise controls approximation error, while Tsybakov noise controls a different fluctuation quantity, and neither by itself supplies the stated exponent. The probability statement also concerns an event defined by empirical minimizers, whose measurability the source deliberately avoids by using outer probability. These are the points at which a direct fixed-class or ordinary-probability statement would fail to match Theorem 2.8.

Formalization scope

Lean represents functions on all of $\mathbb R^d$ but uses only their restrictions to $X$. The joint distribution is built from a probability marginal and a fixed measurable $\eta:\mathbb R^d\to[0,1]$. This makes the paper's choice of regression-function version explicit. The Gaussian RKHS squared norm is the supremum over finite normalized kernel-section combinations; it is $+\infty$ outside the RKHS. A covering number is the least positive finite cardinality of a cover with centers in the ambient empirical function space, or $+\infty$ if there is no such cover. Hinge and classification risks are extended nonnegative integrals, and Bayes risks range over measurable functions.

The assumptions $d>0$ and $n\ge1$ give the divisions and powers their intended domains. For $q=\infty$, the small-$t$ noise bound uses zero on the right, as in the source convention. The paper leaves distance to an empty set unstated; this mission pins $d(x,\varnothing)=0$. With the infinite-distance convention, Lemma 4.1 and Theorem 2.7 fail for a one-class regression function. The proof display (25) has a volume-factor slip in high dimension; Theorem 2.7 is stated with its printed conclusion, and the issue is recorded in the moderation notes. The goal event includes existence of an empirical minimizer, a fact stated in the paper's setup, and quantifies over every minimizer. This excludes a vacuous SVM predicate. The constant $C$ is chosen before $x$ and $n$.

The clauses for $\alpha=\infty$ and an SVM with offset are outside this mission. The separate series mission addresses the implication from an envelope assumption to geometric noise. Further contributions toward the §5 empirical-process estimates, §6 variance estimates, and §7 shrinking and general-rate theorems are welcome; they are not asserted as milestones in this draft.

Selected references

• Ingo Steinwart and Clint Scovel, Fast Rates for Support Vector Machines Using Gaussian Kernels, Annals of Statistics 35(2), 2007, 575–607. arXiv:0708.1838v1, DOI:10.1214/009053606000001226.

Motivation

Confidence bounds for the mean of a bounded random variable are the basic tool for certifying learned hypotheses, stopping sampling procedures and running bandit algorithms. Hoeffding's inequality gives an interval of width of order $\sqrt{1/n}$ whatever the variance. Bennett's and Bernstein's inequalities do better for low-variance variables, with width of order $\sqrt{\mathbb V Z/n} + 1/n$, but the variance $\mathbb V Z$ is unknown, so the bound cannot be evaluated from data.

Maurer and Pontil (arXiv:0907.3740v1, COLT 2009) prove empirical Bernstein bounds, in which the variance is replaced by the observable sample variance at the cost of a slightly larger $1/n$ term. They extend these bounds uniformly over infinite function classes whose complexity is controlled by a growth function. The uniform bound then suggests a learning rule, sample variance penalization (SVP): minimize the empirical risk plus a multiple of the empirical standard deviation. The paper's final result bounds the excess risk of SVP in terms of the variance of an optimal hypothesis. An analogous empirical Bernstein bound was given by Audibert, Munos and Szepesvári for multi-armed bandits, and Mnih, Szepesvári and Audibert (2008) used such bounds for stopping rules. Variance-penalized risk minimization was later studied as a convex surrogate by Namkoong and Duchi (2017).

Setting

For a vector $x = (x_1,\dots,x_n)$ of reals, the sample mean and sample variance are

$$P_n(x) = \frac1n\sum_{i=1}^n x_i, \qquad V_n(x) = \frac{1}{n(n-1)}\sum_{i,j=1}^n\frac{(x_i-x_j)^2}{2}.$$

Let $\mu$ be a probability distribution on a set $\mathcal X$, and $\mathcal F$ a class of hypotheses (loss functions) $f:\mathcal X\to[0,1]$. For $f\in\mathcal F$, its risk is $P(f,\mu) = \mathbb E f(X)$ and its variance is $V(f,\mu)=\mathbb V f(X)$, with $X\sim\mu$. For a sample $\mathbf X = (X_1,\dots,X_n)\sim\mu^n$, $P_n(f,\mathbf X)$ and $V_n(f,\mathbf X)$ are $P_n$ and $V_n$ of the vector $(f(X_1),\dots,f(X_n))$.

The complexity of $\mathcal F$ enters through the growth function. For $x\in\mathcal X^m$ let $\mathcal F(x) = \{(f(x_1),\dots,f(x_m)) : f\in\mathcal F\}\subseteq\mathbb R^m$, and let $\mathcal N(\epsilon, A, \|\cdot\|_\infty)$ be the least number of sup-norm $\epsilon$-balls centred in $A$ that cover $A$. Then

$$\mathcal N_\infty(\epsilon,\mathcal F,m) = \sup_{x\in\mathcal X^m}\mathcal N(\epsilon,\mathcal F(x),\|\cdot\|_\infty), \qquad \mathcal M(n) = 10\,\mathcal N_\infty(1/n,\mathcal F,2n).$$

For $\lambda\ge0$, sample variance penalization selects

$$SVP_\lambda(\mathbf X) = \arg\min_{f\in\mathcal F}\; P_n(f,\mathbf X) + \lambda\sqrt{\frac{V_n(f,\mathbf X)}{n}}.$$

With $\lambda = 0$ it is empirical risk minimization.

Formalization targets

Goal: Theorem 15 (p. 6)

Fix $\delta\in(0,1)$, $n\ge2$, $\lambda = \sqrt{18\ln(3\mathcal M(n)/\delta)}$ and any $f^*\in\mathcal F$. With probability at least $1-\delta$ in $\mathbf X\sim\mu^n$,

$$P(SVP_\lambda(\mathbf X),\mu) - P(f^*,\mu) \le \sqrt{\frac{32\,V(f^*,\mu)\ln(3\mathcal M(n)/\delta)}{n}} + \frac{22\ln(3\mathcal M(n)/\delta)}{n-1}.$$

The constants are the paper's. The goal is stated for an arbitrary comparator $f^*$, so it covers an optimal one when one exists.

Milestones

In the order of the proof:

• the fourth-moment inequality (Lemma 8, Corollary 9);
• the self-bounding concentration inequality the paper cites (Theorem 7, lower and upper tails);
• the tails (5)–(6) of the sample variance and the standard-deviation bounds of Theorem 10;
• the comparison $W\le\mathbb EV_n$ of (7)–(9);
• Bennett's inequality for independent variables, together with the i.i.d. Theorem 3;
• the empirical Bernstein bounds (Theorem 4 for i.i.d. variables, Theorem 11 for independent ones);
• the Lipschitz properties of the confidence functionals $\Phi,\Psi$ (Lemma 12);
• the symmetrization lemma (Lemma 13) and the swap bound (Lemma 14);
• the uniform bound, Theorem 6:

$$\Pr\Big\{\exists f\in\mathcal F:\ P(f,\mu)-P_n(f,\mathbf X) > \sqrt{\tfrac{18V_n(f,\mathbf X)\ln(\mathcal M(n)/\delta)}{n}} + \tfrac{15\ln(\mathcal M(n)/\delta)}{n-1}\Big\}\le\delta \quad (n\ge16).$$

Significance

Theorem 15 separates SVP from empirical risk minimization. If an optimal hypothesis has zero variance, the excess risk of SVP decays as $\ln\mathcal M(n)/n$; for a finite class $\mathcal M(n)$ does not depend on $n$ and the rate is $1/n$. The paper gives a two-hypothesis example where empirical risk minimization cannot beat order $1/\sqrt n$ (Section 4). No convexity of the class or special structure of the loss is needed beyond the growth-function bound. Theorems 4, 10 and 11 are reused well beyond this paper, in bandit algorithms, racing and stopping procedures, and certified estimation.

All results of the paper are proved there, apart from Theorem 7, which is cited from Maurer (2006), and Bennett's inequality for non-identical variables, which is cited from McDiarmid's survey Concentration (1998). This mission produces machine-checked statements of the chain, from the self-bounding inequality to the excess-risk bound. To our knowledge, none of these results has a machine-checked proof. On this platform, the namkoong-2017 series has an open re-derivation of Theorem 6 with other constants and a $1/n$-normalized variance (VarianceRegularization.Covering.uniform_empirical_bernstein). It is related work, not the printed theorem.

Difficulty

Bennett's inequality cannot be applied directly, because its variance term is not observable. Substituting the sample variance requires a concentration inequality for $V_n$ itself with the right dependence on $\mathbb EV_n$, and $V_n$ is a U-statistic, not a sum of independent terms: bounded-differences inequalities give only a variance-free rate, which is too weak.

The uniform extension does not follow from a union bound once the class is infinite. The classical double-sample argument compares a sample with a ghost sample through a linear functional; the empirical standard deviation is nonlinear, so that comparison does not go through unchanged. After symmetrization the coordinates are independent but not identically distributed, so i.i.d. concentration results do not apply to them.

Formalization scope

Conventions:

• The source is arXiv:0907.3740v1. It has no printed page numbers, so every page cited is the PDF page.
• Indices $i=1,\dots,n$ are i : Fin n.
• A sample is a vector Fin n → 𝒳 under the product measure Measure.pi, with i.i.d. coordinates Measure.pi (fun _ => μ) or independent ones Measure.pi μs. Variables "with values in $[0,1]$" have laws giving zero mass outside $[0,1]$.
• "With probability at least $1-\delta$, $A$" is written as $\mu^n\{\neg A\}\le\delta$. For a set that is not measurable this is the outer measure.
• $P_n$ is the published VarianceRegularization.Expansion.empMean. $V_n$ is a local sampleVar with the $1/(n(n-1))$ normalization. $V(f,\mu)$ is Mathlib's variance.
• The covering number is Mathlib's Metric.coveringNumber (closed balls, centres in the set, values in $\mathbb N\cup\{\infty\}$).
• $\Pr_\sigma$ and $\mathbb E_\sigma$ are uniform averages over the $2^n$ sign vectors.
• $SVP_\lambda$ is an arbitrary selector that returns, for every sample, a minimizer in $\mathcal F$ of the penalized objective. Every minimizer is covered.

Added hypotheses and repaired statements, each disclosed in the item:

• The paper says "questions of measurability will be ignored throughout". This is made precise as follows:
  • Theorems 6 and 15: $\mathcal F$ is countable and its members are measurable.
  • Lemma 13: the function is measurable.
  • Theorem 7: $Z$ is measurable, integrable and nonnegative, and its coordinate-wise infima are measurable.
• Theorems 6 and 15 assume $\mathcal N_\infty(1/n,\mathcal F,2n)<\infty$. With an infinite value the printed bound is vacuous.
• Theorems 4 and 11 and Lemmas 12 and 14 add $n\ge2$. Theorem 3 and Bennett's display add $n\ge1$. Without these, Lean's convention $1/0=0$ makes the printed formulas false at the excluded $n$.
• Corollary 9's "set" $\{x_1,\dots,x_n\}$ is read as a list, so repetitions are allowed.

Ruled-out trivializations:

• SVP is not defined as the comparator $f^*$.
• $\lambda$ is pinned to $\sqrt{18\ln(3\mathcal M(n)/\delta)}$.
• $V_n$ is the sample variance, not the true variance.
• No measurability of the bad event or of the selector is assumed.

A complete development needs the following:

• the entropy method for self-bounding functions (Theorem 7);
• Bennett's inequality for independent non-identical bounded variables;
• product-measure symmetrization;
• covering-number bookkeeping.

The concentration results of Section 2 and the symmetrization lemma are reusable beyond this mission. Proofs of any milestone are welcome. Theorem 7 and Bennett's inequality are natural standalone contributions.

Selected references

• A. Maurer, M. Pontil, Empirical Bernstein Bounds and Sample Variance Penalization, COLT 2009; arXiv:0907.3740v1, 2009. https://arxiv.org/abs/0907.3740
• A. Maurer, Concentration inequalities for functions of independent variables, Random Structures & Algorithms 29, 121–138, 2006. https://doi.org/10.1002/rsa.20105
• C. McDiarmid, Concentration, in Probabilistic Methods for Algorithmic Discrete Mathematics, Springer, 1998.
• J.-Y. Audibert, R. Munos, Cs. Szepesvári, Exploration–exploitation trade-off using variance estimates in multi-armed bandits, Theoretical Computer Science 410(19), 2009. https://doi.org/10.1016/j.tcs.2009.01.016
• V. Mnih, Cs. Szepesvári, J.-Y. Audibert, Empirical Bernstein stopping, ICML 2008. https://doi.org/10.1145/1390156.1390241
• W. Hoeffding, Probability inequalities for sums of bounded random variables, JASA 58, 1963. https://doi.org/10.1080/01621459.1963.10500830
• H. Namkoong, J. C. Duchi, Variance-based regularization with convex objectives, NeurIPS 2017; arXiv:1610.02581. https://arxiv.org/abs/1610.02581

Motivation

Policy gradient methods search directly over parameterized policies of a Markov decision process (MDP) by gradient ascent on the expected discounted reward. They are among the most widely used methods in reinforcement learning, yet the value $V^{\pi_\theta}(\rho)$ is a nonconcave function of the parameters, and until recently little was known about whether, or how fast, such methods reach a globally optimal policy. Agarwal, Kakade, Lee and Mahajan (arXiv:1908.00261v5, JMLR 22(98), 2021) give a systematic answer for tabular and function-approximation settings.

This mission formalizes one of their central results. Under the softmax parameterization, plain gradient ascent converges to optimal values only asymptotically (their Theorem 5.1, rate unknown): parameters can diverge and policies become nearly deterministic early, which stalls progress. Adding a log barrier regularizer, equivalent to a relative-entropy penalty towards the uniform policy, keeps action probabilities away from zero, and the paper shows that this yields an iteration count polynomial in every problem quantity. The result is the "softmax + log barrier" row of the paper's Table 1 and a reference point for later analyses of entropy-regularized policy gradient (for example Mei et al., 2020; Cen et al., 2021).

Setting

A finite MDP consists of finite sets $\mathcal S$ (states) and $\mathcal A$ (actions, nonempty), a transition kernel $P(s'\mid s,a)$, rewards $r(s,a)\in[0,1]$ and a discount factor $\gamma\in[0,1)$. A policy $\pi$ assigns a probability distribution $\pi(\cdot\mid s)$ over actions to every state. Its value is $V^\pi(s)=\mathbb E[\sum_{t\ge0}\gamma^t r(s_t,a_t)\mid\pi,s_0=s]$, and for a distribution $\rho$ over states $V^\pi(\rho)=\mathbb E_{s\sim\rho}V^\pi(s)$. The action value is $Q^\pi(s,a)=r(s,a)+\gamma\sum_{s'}P(s'\mid s,a)V^\pi(s')$ and the advantage is $A^\pi(s,a)=Q^\pi(s,a)-V^\pi(s)$. An optimal policy $\pi^\star$ maximizes $V^\pi(s)$ at every state simultaneously; $V^\star=V^{\pi^\star}$.

The discounted state visitation distribution is $d^\pi_\rho(s)=(1-\gamma)\sum_{t\ge0}\gamma^t\Pr^\pi(s_t=s\mid s_0\sim\rho)$. Given a start distribution $\mu$ used by the algorithm, the distribution mismatch coefficient is $\|d^{\pi^\star}_\rho/\mu\|_\infty=\max_s d^{\pi^\star}_\rho(s)/\mu(s)$.

The softmax policy with parameter $\theta\in\mathbb R^{|\mathcal S||\mathcal A|}$ is $\pi_\theta(a\mid s)=\exp(\theta_{s,a})/\sum_{a'}\exp(\theta_{s,a'})$. For $\lambda>0$ the log barrier regularized objective is

$$L_\lambda(\theta)=V^{\pi_\theta}(\mu)+\frac{\lambda}{|\mathcal S|\,|\mathcal A|}\sum_{s,a}\log\pi_\theta(a\mid s)+\lambda\log|\mathcal A| =V^{\pi_\theta}(\mu)-\lambda\,\mathbb E_{s\sim\mathrm{Unif}_{\mathcal S}}\mathrm{KL}(\mathrm{Unif}_{\mathcal A},\pi_\theta(\cdot\mid s)),$$

and gradient ascent with step size $\eta$ is $\theta^{(t+1)}=\theta^{(t)}+\eta\nabla_\theta L_\lambda(\theta^{(t)})$. Write $V^{(t)}=V^{\pi_{\theta^{(t)}}}$.

Formalization targets

Goal: Corollary 5.1 (iteration complexity)

Let $D\ge d^{\pi^\star}_\rho(s)/\mu(s)$ for all $s$ (for example the mismatch coefficient), $\epsilon>0$, $\lambda=\epsilon(1-\gamma)/(2D)$, $\beta_\lambda=8/(1-\gamma)^3+2\lambda/|\mathcal S|$ and $\eta=1/\beta_\lambda$. Starting from a parameter whose softmax policy is uniform (e.g. $\theta^{(0)}=0$),

$$\min_{t<T}\big\{V^\star(\rho)-V^{(t)}(\rho)\big\}\le\epsilon\quad\text{whenever}\quad T\ge\frac{320\,|\mathcal S|^2|\mathcal A|^2}{(1-\gamma)^6\epsilon^2}\,D^2 .$$

Milestones

1. Lemma 3.2 (performance difference): $V^\pi(s_0)-V^{\pi'}(s_0)=\frac1{1-\gamma}\mathbb E_{s\sim d^\pi_{s_0}}\mathbb E_{a\sim\pi(\cdot|s)}A^{\pi'}(s,a)$.
2. Lemma C.1 (softmax gradient): $\partial V^{\pi_\theta}(\mu)/\partial\theta_{s,a}=\frac1{1-\gamma}d^{\pi_\theta}_\mu(s)\pi_\theta(a|s)A^{\pi_\theta}(s,a)$.
3. Display (14): the same plus $\frac{\lambda}{|\mathcal S|}(\frac1{|\mathcal A|}-\pi_\theta(a|s))$ for $\partial L_\lambda/\partial\theta_{s,a}$.
4. Opening claim of the proof of Theorem 5.2: at an $\epsilon_{\rm opt}$-stationary point with $\epsilon_{\rm opt}\le\lambda/(2|\mathcal S||\mathcal A|)$, $\max_a A^{\pi_\theta}(s,a)\le 2\lambda/(\mu(s)|\mathcal S|)$.
5. Theorem 5.2: under the same hypotheses, $V^{\pi_\theta}(\rho)\ge V^\star(\rho)-\frac{2\lambda}{1-\gamma}\|d^{\pi^\star}_\rho/\mu\|_\infty$.
6. Lemma D.4: $L_\lambda$ has $\beta_\lambda$-Lipschitz gradient, $\beta_\lambda=8/(1-\gamma)^3+2\lambda/|\mathcal S|$.
7. Theorem E.1(3) (Beck, Theorem 10.15), unconstrained ascent form: for $\beta$-smooth $f\le M$ and step $1/\beta$, $\min_{t<T}\|\nabla f(x_t)\|\le\sqrt{2\beta(M-f(x_0))}/\sqrt T$.

Significance

The corollary shows that a first-order method on a nonconcave objective reaches an $\epsilon$-optimal policy in a number of steps polynomial in $|\mathcal S|$, $|\mathcal A|$, $1/(1-\gamma)$, $1/\epsilon$ and the mismatch coefficient, with no dependence on the MDP's structure beyond these quantities. Theorem 5.2 is of independent use: it certifies any approximately stationary point of the regularized objective, however it was found, as approximately optimal for the original problem. The dependence on $\|d^{\pi^\star}_\rho/\mu\|_\infty$ makes precise why the exploratory start distribution $\mu$ matters.

The results are proved in the paper; none of them is machine-checked. A formal development adds a checked softmax policy gradient formula on an infinite-horizon discounted MDP, a checked smoothness bound for the regularized objective, the nonconvex gradient-method rate in Euclidean space, and a corrected statement of the corollary (see the next sections). Lemma 3.2 and Lemma C.1 are reused across the other missions of this series.

Difficulty

The value function is not concave in $\theta$ and its gradient vanishes where policies become deterministic, so the standard route "small gradient implies near-optimal" fails for the unregularized objective. With the regularizer, the link between stationarity and optimality has to hold with explicit constants that do not degrade as policies approach the boundary of the simplex, which is where the unregularized argument breaks down. The second obstacle is smoothness: $V^{\pi_\theta}(\mu)$ is an infinite discounted sum of products of transition probabilities, and its Hessian must be bounded uniformly in $\theta$ by $8/(1-\gamma)^3$, which in Lean means differentiating a tsum of matrix-power–like terms in $\theta$. The policy gradient formula itself requires the same interchange of differentiation and infinite summation.

Formalization scope

States and actions are finite types; $\mathcal A$ is nonempty. Parameters live in EuclideanSpace ℝ (S × A), so $\|\cdot\|$ is the $\ell_2$ norm and $\nabla_\theta$ is Mathlib's gradient. The MDP layer (transition kernel, policy, occupation probabilities, $V^\pi$, $Q^\pi$, optimal policy) is the published FoundationsML.ReinforcementLearning library, and $V^\pi(\rho)$, $A^\pi$, $d^\pi_\rho$ are defined on top of it. Standing assumptions are those of §3: $P$ a kernel, $r\in[0,1]$, $0\le\gamma<1$, $\mu,\rho$ probability distributions, $\pi^\star$ optimal at every state.

Conventions committed to:

• the mismatch coefficient is replaced by any $D$ with $d^{\pi^\star}_\rho\le D\mu$ componentwise; no division by $\mu(s)$ occurs, and the same $D$ sets $\lambda$;
• $\min_{t<T}$ is "there is $t<T$ with …";
• $\lambda>0$, implicit in the paper, is a hypothesis of Theorem 5.2 and its proof-step milestone; $\lambda\ge0$ in Lemma D.4;
• Theorem E.1 is posed for ascent on $\mathbb R^d$ with an upper bound $M$ in place of an attained optimum.

Two corrections of the printed corollary. The printed statement allows "any initial $\theta^{(0)}$", but its proof uses $L_\lambda(\theta^\star)-L_\lambda(\theta^{(0)})\le1/(1-\gamma)$, valid for a uniform initial policy and false in general; the formal goal assumes a uniform start. The printed $\beta_\lambda=8\gamma/(1-\gamma)^3+2\lambda/|\mathcal S|$ contradicts the proof, which takes $\beta_\lambda$ from Lemma D.4, $8/(1-\gamma)^3+2\lambda/|\mathcal S|$; the formal goal uses the latter, with the same iteration count.

The goal is not trivialized by its encoding: the hypotheses fix the run completely from $\theta^{(0)}$, $\lambda$ and $\eta$, they are jointly satisfiable (a sorry-free check exhibits a one-state, two-action MDP with an optimal policy and $D=1$), and the conclusion concerns the unregularized value of the iterates. Theorem 5.2, Lemma D.4 and Theorem E.1 are milestones, not hypotheses of the goal.

Infrastructure that a complete development needs, and that is reusable beyond this mission: differentiability of discounted values in the policy parameters and the policy gradient theorem for the softmax class; Hessian bounds for softmax; the descent lemma and the $O(1/\sqrt T)$ rate of gradient methods for smooth nonconvex functions on Euclidean space. Contributions to any of these, or proofs of single milestones, are welcome.

Selected references

• A. Agarwal, S. M. Kakade, J. D. Lee, G. Mahajan, On the Theory of Policy Gradient Methods: Optimality, Approximation, and Distribution Shift, JMLR 22(98), 2021; arXiv:1908.00261v5. https://arxiv.org/abs/1908.00261v5
• S. Kakade, J. Langford, Approximately Optimal Approximate Reinforcement Learning, ICML 2002. https://dl.acm.org/doi/10.5555/645531.656005
• A. Beck, First-Order Methods in Optimization, SIAM, 2017. https://doi.org/10.1137/1.9781611974997
• J. Mei, C. Xiao, C. Szepesvári, D. Schuurmans, On the Global Convergence Rates of Softmax Policy Gradient Methods, ICML 2020. https://arxiv.org/abs/2005.06392
• S. Cen, C. Cheng, Y. Chen, Y. Wei, Y. Chi, Fast Global Convergence of Natural Policy Gradient Methods with Entropy Regularization, Operations Research 70(4), 2022. https://arxiv.org/abs/2007.06558

Motivation

A retailer that decides which products to display, an online platform that decides which items to show in a recommendation slot, and an airline that decides which fare classes to open all face the same problem: the set of options offered changes what customers buy, and the substitution pattern is not known in advance. The multinomial logit (MNL) model is the standard model of this substitution in revenue management (Talluri and van Ryzin 2004), and optimizing the offered set under a known MNL model is a classical, efficiently solvable problem (e.g. Rusmevichientong, Shen and Shmoys 2010, for a capacity constraint).

The MNL-Bandit asks what happens when the MNL parameters are unknown and must be learned from the purchases themselves, while revenue is being earned. Earlier approaches (Rusmevichientong, Shen and Shmoys 2010; Sauré and Zeevi 2013) separate exploration from exploitation and need the gap between the best and the second-best assortment to be known. Agrawal, Avadhanula, Goyal and Zeevi (Oper. Res. 2019, arXiv:1706.03880) give a single upper-confidence-bound policy whose regret is of order $\sqrt{NT}$ up to logarithmic factors, with no such knowledge. This mission formalizes that result, Theorem 1 of the paper.

Setting

There are $N$ products with known revenues $r_i\in[0,1]$. At each time $t=1,\dots,T$ the seller offers an assortment $S_t$ from a family $\mathcal S$ of feasible subsets of $\{1,\dots,N\}$, and one customer either buys a product $c_t\in S_t$ or buys nothing ($c_t=0$). Given $S_t=S$, the choice follows the MNL model with attraction parameters $v_1,\dots,v_N\ge0$ and $v_0=1$:

$$p_i(S)=\frac{v_i}{1+\sum_{j\in S}v_j}\quad(i\in S\cup\{0\}),\qquad p_i(S)=0\ \text{otherwise},$$

independently of the past. The expected revenue of $S$ is $R(S,v)=\sum_{i\in S}r_iv_i\big/\big(1+\sum_{j\in S}v_j\big)$. The family $\mathcal S$ is described by totally unimodular constraints, $\mathcal S=\{S : A\,x(S)\le b\}$ with $x(S)$ the incidence vector of $S$, $A$ totally unimodular and $b$ integral (cardinality constraints are the main example). A policy chooses $S_t$ from the past choices, and its regret is

$$\mathrm{Reg}_\pi(T,v)=T\,R(S^*,v)-\mathbb E_\pi\Big[\sum_{t=1}^TR(S_t,v)\Big],\qquad R(S^*,v)=\max_{S\in\mathcal S}R(S,v).$$

The seller knows $r$ and $\mathcal S$ but not $v$.

Algorithm 1 works in epochs: epoch $\ell$ offers one assortment $S_\ell$ repeatedly until a customer buys nothing. Let $\hat v_{i,\ell}$ be the number of purchases of $i$ in epoch $\ell$, $T_i(\ell)$ the number of the first $\ell$ epochs that offered $i$, and $\bar v_{i,\ell}$ the average of $\hat v_{i,\tau}$ over those epochs. The algorithm forms the upper confidence bounds

$$v^{\mathrm{UCB}}_{i,\ell}=\bar v_{i,\ell}+\sqrt{\bar v_{i,\ell}\,\frac{48\log(\sqrt N\ell+1)}{T_i(\ell)}}+\frac{48\log(\sqrt N\ell+1)}{T_i(\ell)},$$

starting from $v^{\mathrm{UCB}}_{i,0}=1$, and offers next the assortment in $\mathcal S$ that maximizes $R(S,v^{\mathrm{UCB}}_{\cdot,\ell})$.

Formalization targets

Goal: Theorem 1 (p. 11)

Under Assumption 4.1 (every $v_i\le v_0=1$, and $\mathcal S$ is closed under taking subsets) there are absolute constants $C_1,C_2$ such that for every instance and every horizon $T$,

$$\mathrm{Reg}_\pi(T,v)\le C_1\sqrt{NT\log NT}+C_2N\log^2NT .$$

The constants are not fixed: the goal asserts the order of the regret, which is what the paper claims.

Milestones

The milestones follow the proof in Appendix A of the paper:

1. The law of an epoch's purchase count: Lemma A.1, its moment generating function given the offered assortment.
2. Concentration: Theorem 5, Chernoff bounds for geometric variables; Corollary D.1; and Lemma A.2 for the averages $\bar v_{i,\ell}$ along Algorithm 1.
3. Lemma 4.1: $v^{\mathrm{UCB}}_{i,\ell}\ge v_i$ with probability at least $1-6/(N\ell)$, and its rate of convergence.
4. Optimism of the revenue estimate: Lemma A.3 (monotonicity of the optimal revenue in $v$) and Lemma 4.2.
5. The per-epoch error: Lemma A.4 (a Lipschitz bound) and Lemma 4.3.
6. The epoch decomposition of the regret, (A.14).

Significance

Theorem 1 shows that learning the choice model costs only $\tilde O(\sqrt{NT})$ revenue, with no dependence on how separated the instance is. The paper also proves a lower bound of order $\sqrt{NT/K}$ under a $K$-cardinality constraint (its Theorem 2), so for small $K$ the bound is optimal up to logarithmic factors. The epoch device used here reduces the analysis of a choice model with substitution to unbiased i.i.d. estimates of each $v_i$.

The result is proved in the paper (Appendix A, with the concentration bounds in Appendix D). It has not been machine-checked. A formal proof would also settle several printed slips that the formalization had to repair (listed under Formalization scope). The concentration bounds for geometric variables, Theorem 5 and Corollary D.1, are useful outside this mission.

Difficulty

The estimates $\hat v_{i,\ell}$ are counted in epochs whose assortments are chosen adaptively from earlier estimates, so they are not independent a priori. The paper's argument that they are i.i.d. geometric with mean $v_i$ has to be made rigorous for an adaptive policy. The variables are unbounded, so the standard Chernoff–Hoeffding bounds for bounded variables do not apply, and the number of samples $T_i(\ell)$ is random, which requires a union bound over all its possible values. Finally, the regret is a sum over customers while the analysis is per epoch, and the two are linked through the expected epoch length $1+\sum_{j\in S_\ell}v_j$ under a random number of epochs and a horizon that cuts the last one.

Formalization scope

• Model. Products are Fin N; a choice is none (no purchase) or some i. The parameter $v_0$ is normalized to $1$, as the paper allows. Algorithm 1 is deterministic, so a history of horizon $T$ is a sequence of $T$ choices with the product law $\prod_tp_{c_t}(S_t)$, and every expectation is a finite sum. The revenue $R(S,v)$ is the published definition ChoiceCDLP.MNL.mnlObjective v r 1 S.
• Feasible family. $\mathcal S$ is a finite family with the TU representation (2.3), closed under subsets, and nonempty (the paper presupposes nonemptiness when it writes $S^*=\arg\max$).
• Algorithm. Algorithm 1 is a policy defined by recursion on the history. It receives $r$ and an argmax selector for $\mathcal S$, never $v$. Every statement quantifies over all selectors, that is, over every tie-breaking rule. While a product has never been offered, its $v^{\mathrm{UCB}}$ stays at the initial value $1$.
• Epoch events. The lemmas about epoch $\ell$ are stated for every finite horizon $T$, on the event that epoch $\ell$ is completed by customer $T$; uniformity in $T$ is the paper's infinite-horizon statement.
• Repairs of the page, all disclosed in the items:
  1. Lemma A.2's misprinted $\log(\ell+1)$ is replaced by $\log(\sqrt N\ell+1)$.
  2. Lemmas 4.2 and 4.3 are indexed by the estimate built at the end of epoch $\ell$.
  3. Lemma 4.3's free index $i$ becomes the sum over $i\in S_{\ell+1}$.
  4. Lemmas 4.1 and 4.3 use the explicit constants $C_1=\sqrt{72}+\sqrt{24}$ and $C_2=144$ of the proof.
  5. Lemma A.3 and Lemma 4.2 require positive parameters on the optimal set; the printed versions are false otherwise.
  6. (A.14) is an inequality, since the horizon cuts the last epoch.
• Not stated. Corollary A.1 (the epoch estimates are i.i.d. geometric across the epochs of the adaptive policy) is not posed as an item: a single-epoch law would be a weaker statement than the page's.
• No trivialization. The policy cannot see $v$, the constants of the goal precede every other quantifier, and the regret is the paper's (2.6), so the goal cannot be met by a policy that offers $S^*$ or by constants that depend on the instance.
• Welcome contributions. Infrastructure for adaptive sampling (the i.i.d. property of the epoch estimates), Chernoff bounds for geometric and sub-exponential variables, and a Wald-type identity for epochs.

The paper's own proofs are in its Appendices A and D.

Selected references

• S. Agrawal, V. Avadhanula, V. Goyal, A. Zeevi, MNL-Bandit: A Dynamic Learning Approach to Assortment Selection, Operations Research 67(5):1453–1485, 2019. arXiv:1706.03880v2, doi:10.1287/opre.2018.1832
• P. Rusmevichientong, Z.-J. M. Shen, D. B. Shmoys, Dynamic assortment optimization with a multinomial logit choice model and capacity constraint, Operations Research 58(6):1666–1680, 2010. doi:10.1287/opre.1100.0866
• D. Sauré, A. Zeevi, Optimal dynamic assortment planning with demand learning, Manufacturing & Service Operations Management 15(3):387–404, 2013. doi:10.1287/msom.2013.0429
• K. Talluri, G. van Ryzin, Revenue management under a general discrete choice model of consumer behavior, Management Science 50(1):15–33, 2004. doi:10.1287/mnsc.1030.0147
• M. Mitzenmacher, E. Upfal, Probability and Computing, Cambridge University Press, 2005.

Motivation

Caching (online paging) is one of the oldest problems in online algorithms: a fast memory of $k$ slots serves a sequence of requests, and every request for an element not in the fast memory is a cache miss that forces the element to be loaded, possibly evicting another one. With the whole request sequence known in advance, evicting the element whose next request is furthest in the future is optimal (Bélády, 1966). Without that knowledge, no deterministic algorithm is better than $k$-competitive, and the best randomized algorithms are $\Theta(\log k)$-competitive (Fiat, Karp, Luby, McGeoch, Sleator and Young, 1991).

Lykouris and Vassilvitskii asked what happens in between: an online algorithm receives, with every request, a machine-learned prediction of the element's next arrival time. A good predictor should make the algorithm nearly as good as Bélády's rule (consistency), and a bad predictor should never make it worse than a classical algorithm (robustness). Their paper (arXiv:1802.05399v4; J. ACM 2021) is one of the founding papers of learning-augmented algorithms, and its algorithm, Predictive Marker, is the reference point for the later literature on caching with predictions.

Timeline.

• 1966: Bélády's furthest-in-future rule is optimal offline.
• 1985: Sleator and Tarjan show that deterministic online paging is at best $k$-competitive.
• 1991: Fiat et al. introduce the Marker algorithm, $2H_k$-competitive, and the clean-element lower bound on the optimum.
• 2018: Lykouris and Vassilvitskii (arXiv:1802.05399) introduce Predictive Marker, with ratio $2\min(1+2S_\ell(\epsilon), 2H_k)$ for an $\epsilon$-accurate predictor.
• 2020: Rohatgi (arXiv:1910.12172, SODA 2020) and Wei (arXiv:2005.13716, APPROX/RANDOM 2020) improve the dependence on the error.

Setting

A request sequence $\sigma = (z_1, \dots, z_n)$ lists elements of a set $Z$. A cache of size $k \ge 1$ starts empty. A request for a cached element is a hit; otherwise it is a miss, the element is loaded, and if the cache is full some element is evicted first. The offline optimum $\mathrm{Opt}(\sigma)$ is the least number of misses over all eviction schedules chosen with knowledge of $\sigma$.

With each request $z_i$ the algorithm receives a real prediction $h_i$. The true label $y_i$ is the position of the next request of $z_i$, or $n+1$ if there is none. For a loss function $\ell \ge 0$, the error of the predictions is $\eta_\ell(h,\sigma) = \sum_i \ell(y_i, h_i)$, and the predictions are $\epsilon$-accurate when $\eta_\ell(h,\sigma) \le \epsilon \cdot \mathrm{Opt}(\sigma)$.

The spread of $\ell$ measures how cheaply a predictor can get the order of arrivals completely wrong: $S_\ell(m)$ is the least length $T \ge 1$ such that every strictly increasing integer sequence $a_1 < \dots < a_T$ and every non-increasing real sequence $b_1 \ge \dots \ge b_T$ have total loss $\sum_i \ell(a_i, b_i) \ge m$.

Predictive Marker (Algorithm 1) works in the phases of the Marker algorithm. Requested elements are marked. A phase ends when the cache is full, every cached element is marked, and a miss occurs; then all marks are removed. An element requested in a phase but not in the previous one is clean, and $Q(\sigma)$ is the total number of clean elements. Each clean miss starts a chain. An element evicted in the current phase that is requested again (a stale miss) extends the chain in which it was evicted. Evictions are among unmarked elements. As long as the chain's length $n(r,c)$ is at most $H_k = 1 + \tfrac12 + \dots + \tfrac1k$, the evicted element is one with the largest prediction. After that it is chosen uniformly at random. The expected number of misses of Predictive Marker is $\mathrm{cost}_{PM}(\sigma)$.

Formalization targets

Goal: Theorem 3.3

If $S$ is concave on $[0,\infty)$ and majorizes the spread, then for every $\epsilon \ge 0$, every tie-breaking rule, and every sequence with $\epsilon$-accurate predictions,

$$\mathbb E\bigl[\mathrm{cost}_{PM}(\sigma)\bigr] \le 2\cdot\min\bigl(1 + 2S(\epsilon),\ 2H_k\bigr)\cdot \mathrm{Opt}(\sigma).$$

Milestones

• Claim 1 (Fiat et al.): $Q(\sigma) \le 2\,\mathrm{Opt}(\sigma)$.
• Proof of Theorem 3.3, last sentence: $\mathrm{Opt}(\sigma) \le Q(\sigma)$.
• Lemma 3.3: a chain that evicts by the predictions only has length $n(r,c) \le 1 + S(\eta_{r,c})$, where $\eta_{r,c}$ is the error of the predictions on the elements evicted into it.
• Lemma 3.4: $\mathbb E[n(r,c)] \le \mathbb E[\min(1 + 2S(\eta_{r,c}), 2H_k)]$.

Significance

The result. Theorem 3.3 gives both guarantees at once. For an exact predictor ($\epsilon = 0$) the ratio is a constant, $2(1 + 2S(0))$, independent of $k$; for an arbitrary predictor it is $4H_k$, within a constant factor of the optimal randomized ratio. In between, the ratio degrades with the error at the rate of the spread: for the absolute loss the spread grows like $\sqrt m$, so the ratio grows like $\sqrt\epsilon$. The spread and the chain decomposition are the tools later papers build on to trade consistency against robustness.

Formalizing it. The theorem is proved on paper; no machine-checked proof of it, of the Marker analysis, or of the clean-element bound of Fiat et al. is known. A formalization supplies a precise model of a randomized online algorithm with predictions. It also settles the details the paper leaves implicit: the eviction missing from the clean branch of Algorithm 1 as printed, the cap $2H_k$ printed as $2\log k$ in Lemma 3.4, and the behaviour of the spread at $0$.

Difficulty

The obvious argument charges every miss to a chain and bounds each chain separately. That works for chains that follow the predictions, but a chain that switches to random evictions interacts with every other chain of the phase, because all of them evict from the same pool of unmarked elements. A bound on its expected length must hold whatever the other chains evict, including evictions that depend on earlier coin flips. A second difficulty is summing. The chain errors $\eta_{r,c}$ and the chain lengths are both random, while the hypothesis controls only the total error $\eta_\ell(h,\sigma)$ against $\mathrm{Opt}(\sigma)$, not the number of chains $Q(\sigma)$ in which the error is spread.

Formalization scope

Elements form a type with decidable equality. A request sequence is a list; predictions are one real per request, and every real sequence is allowed. Labels are 1-based next-arrival positions, with $n+1$ for elements never requested again. The paper prints the label with equal features; the element is meant. $\mathrm{Opt}$ is computed as the minimum over all demand-paging schedules from the empty cache, which loses no generality. $H_k$ is harmonic k as a real number, never $\log k$.

Predictive Marker is a PMF over final states. The random eviction of line 21 is uniform over the unmarked cached elements, and ties in the arg max are a parameter quantified universally. The eviction of lines 23–24 is also performed after a clean miss; as printed, it sits only in the stale branch. The expected cost lies in $[0,\infty]$.

The spread takes real arguments and lengths $T \ge 1$. $S$ must be concave on $[0,\infty)$, finite, and at least the spread. It must also be continuous at $0$, which the paper does not say: without it the chain lemma fails for losses whose minimal reversed-order loss stays $0$ over several lengths. $\epsilon$-accuracy is the pointwise condition on the given pair $(\sigma, h)$. The competitive ratio is written as a product, so $\mathrm{Opt}(\sigma) = 0$ needs no special case. Lemma 3.3 is stated pointwise for chains without random evictions, as its proof shows. Lemma 3.4 has $2H_k$ in place of the printed $2\log k$, with the minimum inside the expectation because $\eta_{r,c}$ is random.

The statement must not be trivialized. $\mathrm{Opt}$ is the true offline optimum, not Bélády's rule applied to the predictions. The expectation is taken over Predictive Marker's own run, never compared with itself. The spread hypothesis is satisfiable; for example, the constant loss $1$ has spread $\max(1,\lceil m\rceil) \le m + 1$.

Out of scope: Lemma 3.2 (the special-marking algorithm SM, which enters only through Lemma 3.4's proof); Lemma 3.1 and Corollaries 1–2, whose printed constants are false for small $m$ or disagree with Theorem 3.3; the lower bounds of §3.1 and §3.4; the extensions of §4; the experiments of §5; running time and learnability.

Welcome contributions: the Marker phase structure and its equivalence with the combinatorial phases, the clean-element bounds $Q/2 \le \mathrm{Opt} \le Q$ (reusable for any marking algorithm), and a bound on the expected number of misses caused by elements evicted uniformly at random within a phase.

Selected references

• T. Lykouris, S. Vassilvitskii, Competitive Caching with Machine Learned Advice, arXiv:1802.05399v4, 2020; J. ACM 68(4), 2021. https://arxiv.org/abs/1802.05399v4
• A. Fiat, R. M. Karp, M. Luby, L. A. McGeoch, D. D. Sleator, N. E. Young, Competitive paging algorithms, J. Algorithms 12(4), 1991. https://doi.org/10.1016/0196-6774(91)90041-V
• L. A. Bélády, A study of replacement algorithms for a virtual-storage computer, IBM Systems Journal 5(2), 1966. https://doi.org/10.1147/sj.52.0078
• D. D. Sleator, R. E. Tarjan, Amortized efficiency of list update and paging rules, Comm. ACM 28(2), 1985. https://doi.org/10.1145/2786.2793
• D. Rohatgi, Near-optimal bounds for online caching with machine learned advice, SODA 2020. https://arxiv.org/abs/1910.12172
• A. Wei, Better and simpler learning-augmented online caching, APPROX/RANDOM 2020. https://arxiv.org/abs/2005.13716