Machine Learning

Motivation

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

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

Setting

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

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

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

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

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

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

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

Formalization targets

Goal: Theorem 4.4 (p. 5)

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

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

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

Milestones

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

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

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

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

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

Selected references

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

Motivation

In best arm identification with fixed confidence, a learner samples $K$ unknown distributions ("arms") sequentially and must name the arm with the largest mean, with error probability at most a prescribed $\delta$, using as few samples as possible. Garivier and Kaufmann (arXiv:1602.04589, COLT 2016) showed that every $\delta$-PAC strategy needs, in expectation, at least $T^*(\boldsymbol\mu)\,\mathrm{kl}(\delta,1-\delta)$ samples, where the characteristic time $T^*(\boldsymbol\mu)$ is the value of a max–min optimization problem over the proportions of draws allocated to the arms. The maximizer of that problem, $w^*(\boldsymbol\mu)$, is the allocation any asymptotically optimal strategy must follow; the Track-and-Stop algorithm of the same paper computes $w^*(\hat{\boldsymbol\mu})$ at plug-in estimates and tracks it.

A strategy can only track $w^*$ if $w^*$ can be computed. This mission formalizes the part of the paper (Section 2.2 and Appendix A) that turns the abstract max–min problem into an explicit recipe: a closed form for the inner infimum, and a characterization of $w^*$ through the root of one increasing scalar function. The problem had been solved in closed form before only for special cases, such as Poisson rewards with all suboptimal arms equal (Vaidhyan and Sundaresan, 2015); the paper's result covers every one-parameter exponential family.

Setting

A canonical one-parameter exponential family is a family of laws $\nu_\theta$, $\theta\in\Theta$, on $\mathbb R$ with density $\exp(\theta x-b(\theta))$ with respect to a reference measure $\xi$. The law $\nu_\theta$ has mean $\dot b(\theta)$; the set of attainable means is the mean space $\dot b(\Theta)$. For means $\mu=\dot b(\theta)$ and $\mu'=\dot b(\theta')$ the Kullback–Leibler divergence is

$$d(\mu,\mu')=\mathrm{KL}(\nu_\theta,\nu_{\theta'})=b(\theta')-b(\theta)-\dot b(\theta)(\theta'-\theta).$$

Bernoulli laws and Gaussian laws with known variance are the standard examples.

A bandit model is identified with its vector of means $\boldsymbol\mu=(\mu_1,\dots,\mu_K)\in\dot b(\Theta)^K$. $\mathcal S$ is the set of models with a unique optimal arm $a^*(\boldsymbol\mu)$, and $\mathrm{Alt}(\boldsymbol\mu)=\{\boldsymbol\lambda\in\mathcal S:a^*(\boldsymbol\lambda)\ne a^*(\boldsymbol\mu)\}$ is the set of alternatives. $\Sigma_K$ is the probability simplex. The transportation cost of proportions $w\in\Sigma_K$ and the objects of the paper are

$$c_{\boldsymbol\mu}(w)=\inf_{\boldsymbol\lambda\in\mathrm{Alt}(\boldsymbol\mu)}\sum_{a=1}^Kw_a\,d(\mu_a,\lambda_a),\qquad T^*(\boldsymbol\mu)^{-1}=\sup_{w\in\Sigma_K}c_{\boldsymbol\mu}(w),\qquad w^*(\boldsymbol\mu)=\operatorname*{argmax}_{w\in\Sigma_K}c_{\boldsymbol\mu}(w).$$

The arms are sorted so that $\mu_1>\mu_2\ge\dots\ge\mu_K$. The parameterized Jensen–Shannon divergence is, for $\alpha\in[0,1]$,

$$I_\alpha(\mu_1,\mu_2)=\alpha\,d\big(\mu_1,\alpha\mu_1+(1-\alpha)\mu_2\big)+(1-\alpha)\,d\big(\mu_2,\alpha\mu_1+(1-\alpha)\mu_2\big).$$

For $a\in\{2,\dots,K\}$ let $g_a(x)=(1+x)I_{1/(1+x)}(\mu_1,\mu_a)$ for $x\ge0$, let $x_a=g_a^{-1}$, and let $x_1\equiv1$. Finally

$$F_{\boldsymbol\mu}(y)=\sum_{a=2}^K\frac{d\big(\mu_1,m_a(y)\big)}{d\big(\mu_a,m_a(y)\big)},\qquad m_a(y)=\frac{\mu_1+x_a(y)\mu_a}{1+x_a(y)}.$$

Formalization targets

Goal: Theorem 5 (p. 5)

With $D=d(\mu_1,\mu_2)$: $F_{\boldsymbol\mu}$ is continuous and strictly increasing on $[0,D[$, $F_{\boldsymbol\mu}(0)=0$, $F_{\boldsymbol\mu}(y)\to\infty$ as $y\to D$, the equation $F_{\boldsymbol\mu}(y)=1$ has a unique solution $y^*\in[0,D[$, and

$$w\in w^*(\boldsymbol\mu)\iff w_a=\frac{x_a(y^*)}{\sum_{i=1}^Kx_i(y^*)}\quad\text{for every arm }a.$$

The equivalence says at once that the argmax exists, that it is a single point, and that it is given by eq. (5).

Milestones

1. Lemma 3 (p. 5): for every $w\in\Sigma_K$,

$$c_{\boldsymbol\mu}(w)=\min_{a\ne1}(w_1+w_a)\,I_{\frac{w_1}{w_1+w_a}}(\mu_1,\mu_a).$$

2. Claim after eq. (4) (p. 5): $g_a$ is a strictly increasing one-to-one mapping from $[0,+\infty[$ onto $[0,d(\mu_1,\mu_a)[$.
3. Lemma 4 (p. 5): for every maximizer $w^*$ and all $a,b\in\{2,\dots,K\}$,

$$(w^*_1+w^*_a)I_{\frac{w^*_1}{w^*_1+w^*_a}}(\mu_1,\mu_a)=(w^*_1+w^*_b)I_{\frac{w^*_1}{w^*_1+w^*_b}}(\mu_1,\mu_b).$$

Significance

The result. Theorem 5 reduces a $(K-1)$-dimensional non-smooth max–min problem to finding the root of one continuous increasing function on a bounded interval, each evaluation of which requires $K-1$ scalar inversions. It gives existence and uniqueness of $w^*(\boldsymbol\mu)$, which the paper's lower bound only presupposes, and it is the computational core of Track-and-Stop: without an explicit, well-posed $w^*$ the tracking strategy is not defined. Lemma 3 alone gives the closed form of the inner infimum used again in the analysis of the stopping rule.

Formalizing it. The results are proved in the paper; nothing here is open. To the best of our knowledge none of them has a machine-checked proof: the platform's existing best-arm-identification rows concern Gaussian arms and state the characteristic time at the level of measures, without this characterization. The mission produces a checked reduction for general one-parameter exponential families, including the edge cases the text passes over (ties among suboptimal arms, zero weights, the behaviour of $x_a$ near the end of its domain).

Difficulty

The infimum in Lemma 3 ranges over $\mathrm{Alt}(\boldsymbol\mu)$, a set of models with a unique best arm, so it is an open condition: the minimizing configuration, in which $\lambda_1$ and $\lambda_a$ coincide, lies outside $\mathrm{Alt}(\boldsymbol\mu)$ and is only approached. Other arms may also compete for the best position. A statement in which the infimum is taken over the closed relaxation $\{\lambda_a\ge\lambda_1\}$ is a lemma of the proof, not Lemma 3.

For Theorem 5, the equalization in Lemma 4 needs an argument that holds for every maximizer, not only for one found by a first-order condition, because the objective is a minimum of functions and is not differentiable. The monotonicity of $F_{\boldsymbol\mu}$ needs the monotonicity of each $x_a$ and of each ratio in the moving point $m_a$, and the limit at $D$ rests on the second-best arm(s) only, which is where the ordering $\mu_1>\mu_2\ge\dots$ enters. Finally the analytic facts about $d$ (continuity, positivity off the diagonal, monotonicity in each argument) must be derived from the exponential family itself.

Formalization scope

Lean represents a model by μ : Fin K → ℝ with 2 ≤ K and every μ a in the mean space deriv F.b '' F.Θ. The paper's arm $1$ is index 0, arm $2$ is index 1. The exponential family is a structure ExpFamily whose parameter set is a nonempty open interval and whose b is twice continuously differentiable with $\ddot b>0$ on $\Theta$. These two conditions are added to the paper's "convex, twice differentiable" and are disclosed: strict convexity is what makes the mean parameterization unique, and openness is what lets alternatives approach the boundary of $\mathrm{Alt}(\boldsymbol\mu)$. The reference measure and normalization are part of the structure but unused here.

The transportation cost is an infimum in EReal, so it is the true infimum of the set of values rather than a default 0. $w^*(\boldsymbol\mu)$ is never defined by choice: "$w$ is optimal" is a predicate, and Theorem 5 characterizes the set of such $w$. The functions $x_a$ are the inverse of $g_a$ on $[0,+\infty[$ and are evaluated only on $[0,d(\mu_1,\mu_2)[$. "Increasing" in Theorem 5 is stated as strictly increasing, as proved in Appendix A.2. Lemmas 3 and 4 and the claim on $g_a$ assume only that arm $1$ is the unique best arm, which is weaker than the paper's standing ordering.

A formalization that replaces $\mathrm{Alt}(\boldsymbol\mu)$ by $\{\lambda_a\ge\lambda_1\}$, assumes the maximizer exists and is unique, or asserts only existence of some $y^*$ without the formula for $w^*$, does not state these results and is ruled out.

A complete development needs: basic calculus of exponential families (the Bregman form of $d$, its continuity and strict positivity off the diagonal, its monotonicity in the second argument), the inverse function of a continuous strictly monotone map on an interval, and compactness of the simplex. The divergence facts are reusable in every bandit mission built on exponential families. Proofs of the milestones, of auxiliary facts about $d$ and $I_\alpha$, and a sorry-free instance of ExpFamily (Bernoulli or unit-variance Gaussian) are welcome.

Selected references

• A. Garivier, E. Kaufmann, Optimal Best Arm Identification with Fixed Confidence, COLT 2016 (JMLR W&CP 49), arXiv:1602.04589v2. https://arxiv.org/abs/1602.04589
• E. Kaufmann, O. Cappé, A. Garivier, On the Complexity of Best-Arm Identification in Multi-Armed Bandit Models, JMLR 17, 2016. https://arxiv.org/abs/1407.4443
• N. K. Vaidhyan, R. Sundaresan, Learning to detect an oddball target, arXiv:1508.05572, 2015. https://arxiv.org/abs/1508.05572
• O. Cappé, A. Garivier, O.-A. Maillard, R. Munos, G. Stoltz, Kullback–Leibler upper confidence bounds for optimal sequential allocation, Annals of Statistics 41(3), 2013. https://arxiv.org/abs/1210.1136

Motivation

Training a statistical model by empirical risk minimization means minimizing an average of $N$ losses over a parameter vector $w\in\mathbb R^n$, where both $N$ and $n$ can be in the millions. Stochastic gradient descent (SGD) is the standard method: each step uses the gradient of a small random batch of losses. It is cheap per step but sensitive to the scaling of the problem. Quasi-Newton methods such as L-BFGS correct the scaling in deterministic optimization, but naive stochastic versions are unstable, because differences of noisy gradients are poor curvature estimates.

Byrd, Hansen, Nocedal and Singer (SIAM J. Optim. 26(2), 2016) proposed the stochastic quasi-Newton (SQN) method. It decouples the two estimates: gradients come from small batches at every step, while curvature pairs are formed only every $L$ steps, from averaged iterates and subsampled Hessian–vector products. The paper's analysis (Section 3) shows that the method keeps the $O(1/k)$ expected suboptimality rate of SGD on strongly convex problems. The same eigenvalue bound was obtained independently by Mokhtari and Ribeiro (JMLR 16, 2015). Bottou, Curtis and Nocedal later gave a general treatment of such preconditioned stochastic methods (SIAM Review 60(2), 2018).

Setting

Let $f_1,\dots,f_N:\mathbb R^n\to\mathbb R$ be twice continuously differentiable losses and

$$F(w)=\frac1N\sum_{i=1}^N f_i(w).$$

For a sample $\mathcal S\subseteq\{1,\dots,N\}$ of size $b$, the minibatch gradient is $\nabla F_{\mathcal S}(w)=\frac1b\sum_{i\in\mathcal S}\nabla f_i(w)$. For a sample $\mathcal S_H$ of size $b_H$, the subsampled Hessian is $\nabla^2F_{\mathcal S_H}(w)=\frac1{b_H}\sum_{i\in\mathcal S_H}\nabla^2 f_i(w)$.

Assumption 1 requires constants $0<\lambda,\Lambda$ with $\lambda I\prec\nabla^2F_{\mathcal S_H}(w)\prec\Lambda I$ for every $w$ and every Hessian sample. It also requires a bound $\gamma^2$ on the second moment of the stochastic gradient. $w^*$ denotes the minimizer of $F$.

Algorithm 2 turns correction pairs $(s_j,y_j)$ into a matrix $H_t$. With $\tilde m=\min\{t,M\}$, it starts from $\frac{s_t^Ty_t}{y_t^Ty_t}I$ and applies the BFGS update

$$H\leftarrow(I-\rho_js_jy_j^T)H(I-\rho_jy_js_j^T)+\rho_js_js_j^T,\qquad\rho_j=\frac1{y_j^Ts_j},$$

for $j=t-\tilde m+1,\dots,t$.

Algorithm 1 (SQN) runs for $k=1,2,\dots$. It draws a gradient sample $\mathcal S_k$ and steps

$$w^{k+1}=w^k-\alpha^kH\nabla F_{\mathcal S_k}(w^k),$$

where $H=I$ for $k\le2L$ and $H=H_t$, $t=\lfloor(k-1)/L\rfloor-1$, afterwards. Every $L$ iterations it forms the block average $\bar w_t$ of the last $L$ iterates and a new pair

$$s_t=\bar w_t-\bar w_{t-1},\qquad y_t=\nabla^2F_{\mathcal S_{H,t}}(\bar w_t)\,s_t .$$

Samples are drawn independently and uniformly among the subsets of their size. The step length is $\alpha^k=\beta/k$.

Formalization targets

Goal: Corollary 3.3, with a corrected constant

There are $0<\mu_1\le\mu_2$, depending only on the problem data, such that every matrix Algorithm 1 applies satisfies $\mu_1I\prec H\prec\mu_2I$. Moreover, for every $\beta>1/(2\mu_1\lambda)$,

$$E[F(w^k)-F(w^*)]\le\frac{Q_c(\beta)}k\qquad(k\ge1),$$ $$Q_c(\beta)=\max\Big\{\frac{\Lambda\mu_2^2\beta^2\gamma^2}{2(2\mu_1\lambda\beta-1)},\ \Lambda\mu_2^2\beta^2\gamma^2,\ F(w^1)-F(w^*)\Big\}.$$

The constants $\mu_1,\mu_2$ are not fixed numerically. The goal asserts a rate of order $1/k$ with an explicit constant in terms of them.

Milestones

• (3.8)–(3.10): the curvature bounds $\lambda\|s\|^2\le y^Ts\le\Lambda\|s\|^2$ and $\lambda\le\|y\|^2/y^Ts\le\Lambda$ for Hessian-product pairs.
• (3.11) and (3.12): the trace bound and Powell's determinant formula for the direct L-BFGS matrices.
• Lemma 3.1: $\mu_1I\prec H_t\prec\mu_2I$ uniformly along every run.
• (3.18): expected descent for the general Newton-like iteration $w^{k+1}=w^k-\alpha^kH_k\nabla f(w^k,\xi^k)$.
• (3.19): $2\lambda[F(w)-F(w^*)]\le\|\nabla F(w)\|^2$.
• (3.22): the recursion $\phi_{k+1}\le(1-2\alpha^k\mu_1\lambda)\phi_k+\frac\Lambda2(\alpha^k\mu_2)^2\gamma^2$.
• Theorem 3.2: the $Q_c(\beta)/k$ rate for the Newton-like iteration.

Significance

The corollary says that curvature information costs nothing in rate. With uniformly bounded preconditioners and the $\beta/k$ schedule, the SQN method converges in expectation at the same order as SGD, which is the order known to be optimal for this class of problems. Lemma 3.1 is the reusable part: it holds for any L-BFGS matrix built from pairs whose curvature is controlled by a bounded Hessian. Theorem 3.2 applies to every stochastic method whose preconditioner is fixed before the sample is drawn and has uniformly bounded spectrum.

The formalization adds three things. First, it states the result correctly. As printed, Theorem 3.2 is false and Assumption 1(3) cannot be satisfied (see Formalization scope), and the mission states and labels the repaired versions. Second, it gives a machine-checked statement of the SQN algorithm itself, which is not currently formalized anywhere. Third, it provides L-BFGS and preconditioned-SGD infrastructure that later missions on stochastic second-order methods can reuse. To our knowledge none of these results has a machine-checked proof.

Difficulty

The natural first idea is to feed the iterates of Algorithm 1 to a standard SGD rate theorem. This fails for two reasons. The preconditioner $H_t$ depends on the past iterates and on independent Hessian samples, so the analysis needs a filtration in which $H_t$ is known before the gradient sample is drawn. Also, the rate proof itself is an induction that breaks in the first iterations, which is exactly where the printed argument goes wrong.

On the linear-algebra side, the difficulty is a lower bound on the smallest eigenvalue of $H_t$ that is uniform over all runs and all $t$. The curvature bounds on each individual pair do not give it directly, because the BFGS updates compound across the memory window. The expectation side needs conditional expectations of vector-valued functions and a descent inequality under a Hessian bound, neither of which Mathlib packages for this setting.

Formalization scope

Vectors live in EuclideanSpace ℝ (Fin n), matrices are Matrix (Fin n) (Fin n) ℝ acting through Matrix.toEuclideanLin, and $A\prec B$ is (B - A).PosDef. Hessians are fderiv ℝ (gradient f) w. Indices $k,t$ start at $1$ as in the paper. In the corollary, $E$ is an exact finite average over sample histories, and "almost surely" means "on every history". Theorem 3.2 uses a general probability space with a filtration. $H_k$ and $w^k$ are $\mathcal F_k$-measurable, the sample $\xi^k$ is $\mathcal F_{k+1}$-measurable, and unbiasedness is a conditional expectation. Integrability of $F(w^k)$ is part of each conclusion, so a junk-zero integral cannot satisfy it.

Two corrections to the paper, each labelled in the item titles and notes:

• Iterate-wise $\gamma$. Assumption 1(3) says $E_\xi\|\nabla f(w,\xi)\|^2\le\gamma^2$ for all $w$. Together with unbiasedness and $\lambda$-strong convexity on $\mathbb R^n$, this forces $\lambda\|w-w^*\|\le\|\nabla F(w)\|\le\gamma$ for every $w$, which is impossible. The mission imposes the bound at the iterates, conditionally on the past, which is how the proof uses it.
• Constant $Q_c(\beta)$. The induction after (3.22) multiplies by $1-2\beta\mu_1\lambda/k$, which is negative for $k<2\beta\mu_1\lambda$. Counterexample: $n=1$, $f_{1,2}(w)=(w\mp1)^2/2$, $H_k=I$, $w^1=0$, $\beta=2$, $\gamma^2=5$. Then $F(w^2)-F(w^*)=2>Q(2)/2=5/3$, and the example survives perturbing the constants so that every strict inequality holds. The middle entry of $Q_c$ repairs it, and $Q_c=Q$ whenever $2\mu_1\lambda\beta\le3/2$.

Smaller conventions:

• The pairs must satisfy $s_t\neq0$, since Algorithm 2 is undefined otherwise.
• Hessian samples have size $b_H\ge1$; the empty sample makes (2.3) a $0/0$.
• The corollary's undefined $\mu_2$ is Lemma 3.1's constant, enlarged together with $\mu_1$ to cover the initial $H=I$ steps.
• The block average of Algorithm 1 is used, not Eq. (2.1).

Trivializing encodings are ruled out: $H_t$ is Algorithm 2 applied to Algorithm 1's own pairs, not an arbitrary bounded matrix, and the second-moment bound is not imposed for all $w$.

Needed infrastructure, all welcome as contributions: the symmetry and spectral bounds of Hessians of $C^2$ functions, trace and determinant identities for BFGS updates, the descent lemma from a Hessian upper bound, conditional-expectation manipulations for adapted iterations, and the reduction of Algorithm 1 with uniform finite sampling to the abstract iteration.

Selected references

• R. H. Byrd, S. L. Hansen, J. Nocedal, Y. Singer, A Stochastic Quasi-Newton Method for Large-Scale Optimization, SIAM J. Optim. 26(2):1008–1031, 2016. https://doi.org/10.1137/140954362
• A. Mokhtari, A. Ribeiro, Global Convergence of Online Limited Memory BFGS, J. Mach. Learn. Res. 16:3151–3181, 2015. https://jmlr.org/papers/v16/mokhtari15a.html
• L. Bottou, F. E. Curtis, J. Nocedal, Optimization Methods for Large-Scale Machine Learning, SIAM Review 60(2):223–311, 2018. https://doi.org/10.1137/16M1080173
• A. Nemirovski, A. Juditsky, G. Lan, A. Shapiro, Robust Stochastic Approximation Approach to Stochastic Programming, SIAM J. Optim. 19(4):1574–1609, 2009. https://doi.org/10.1137/070704277
• M. J. D. Powell, Some global convergence properties of a variable metric algorithm for minimization without exact line searches, in Nonlinear Programming, SIAM-AMS Proc. IX, 1976, pp. 53–72.

Motivation

Statistical learning theory asks when the empirical frequencies of a whole class of events converge to their probabilities uniformly over the class. Vapnik and Chervonenkis answered this question in 1971 (Theory Probab. Appl. 16 (1971) 264–280) by attaching to every class of sets a single combinatorial quantity, the growth function, and bounding the probability of a large uniform deviation in terms of it. For that bound to be useful, the growth function must grow more slowly than an exponential. The first result of the paper, Theorem 1, shows that the growth function of any class is either exactly $2^r$ or bounded by a polynomial. This dichotomy is the reason finite VC dimension (the size of the largest fully shattered sample) became the central complexity measure of learning theory.

Timeline of the combinatorial core:

• 1971–1972. The same polynomial bound appeared in three independent papers: Vapnik and Chervonenkis (this paper; announced in Dokl. Akad. Nauk SSSR 181 (1968)), N. Sauer, On the density of families of sets, J. Combin. Theory Ser. A 13 (1972) 145–147, and S. Shelah, A combinatorial problem; stability and order for models and theories in infinitary languages, Pacific J. Math. 41 (1972) 247–261. The bound $\sum_{k=0}^{n} \binom{r}{k}$ of Lemma 1 below is now called the Sauer–Shelah lemma.
• 1989. Blumer, Ehrenfeucht, Haussler and Warmuth, Learnability and the Vapnik–Chervonenkis dimension, J. ACM 36 (1989) 929–965, made finite VC dimension the characterization of PAC learnability.

Setting

Let $X$ be a set and $S$ a collection of subsets of $X$. A sample of size $r$ is a finite sequence $x_1, \dots, x_r$ of elements of $X$; repetitions are allowed. Each $A \in S$ induces in the sample the subsample of the terms that lie in $A$, which is determined by the set of positions $\{i : x_i \in A\}$.

The index $\Delta^S(x_1, \dots, x_r)$ is the number of different subsamples induced by the sets of $S$, i.e. the number of distinct sets of positions $\{i : x_i \in A\}$ with $A \in S$. It is at most $2^r$. The growth function is

$$m^S(r) = \max_{x_1, \dots, x_r} \Delta^S(x_1, \dots, x_r),$$

the maximum over all samples of size $r$. For the rays $\{y \le a\}$ on the line $m^S(r) = r + 1$; for the open subsets of $[0,1]$, $m^S(r) = 2^r$.

The function $\Phi(n, r)$ on pairs of natural numbers is defined by the recurrence (1) of the paper,

$$\Phi(n, r) = \Phi(n, r-1) + \Phi(n-1, r-1), \qquad \Phi(0, r) = 1, \qquad \Phi(n, 0) = 1 .$$

In the Lean development these are index S x for x : Fin r → X, growthFunction S r, and Phi n r in the namespace VapnikChervonenkis.GrowthFunction.

Formalization targets

Goal: Theorem 1 (p. 267)

For a nonempty class $S$, either $m^S(r) = 2^r$ for every $r$, or, with $n \ge 1$ the first value of $r$ at which $m^S(r) = 2^r$ fails,

$$m^S(r) \le r^n + 1 \qquad \text{for all } r \ge 0 .$$

The exponent $n$ is pinned down by minimality: $m^S(n) \ne 2^n$ and $m^S(r) = 2^r$ for every $r < n$.

Milestones, in the order the proof uses them

1. The index is at most $2^r$ (p. 265): $\Delta^S(x_1, \dots, x_r) \le 2^r$.
2. The closed form of $\Phi$ (p. 266): $\Phi(n, r) = \sum_{k=0}^{n} \binom{r}{k}$ for $r > n$, and $\Phi(n, r) = 2^r$ for $r \le n$.
3. The polynomial bound (p. 266): $\Phi(n, r) \le r^n + 1$ for $n > 0$, $r \ge 0$.
4. Lemma 1 (p. 266): if $1 \le n \le i$ and $\Delta^S(x_1, \dots, x_i) \ge \Phi(n, i)$, some subsample $x_{i_1}, \dots, x_{i_n}$ of size $n$ satisfies $\Delta^S(x_{i_1}, \dots, x_{i_n}) = 2^n$.
5. The first display of the proof of Theorem 1 (p. 268): if $m^S(n) \ne 2^n$, then $\Delta^S(x_1, \dots, x_r) < \Phi(n, r)$ for every sample of size $r > n$.

Significance

Theorem 1 converts the distribution-free bound $\mathbf P\{\pi^{(l)} > \varepsilon\} \le 4 m^S(2l) e^{-\varepsilon^2 l/8}$ of Theorem 2 of the same paper into a convergence statement: whenever the growth function is not identically $2^r$, the right-hand side is a polynomial times a decaying exponential, so relative frequencies converge to probabilities uniformly over $S$. The same dichotomy underlies sample-complexity bounds for PAC learning, covering-number bounds for VC classes, and the notion of VC dimension itself; the exponent $n$ is the VC dimension plus one.

The results are classical and proved. Mathlib contains the Sauer–Shelah lemma for finite set families (Finset.card_shatterer_le_sum_vcDim in Mathlib/Combinatorics/SetFamily/Shatter.lean). The platform has several open formal statements of Sauer's lemma for growth functions over finite point sets (ComputationalLearning.sauer_lemma, FoundationsML.RademacherVC.sauer_lemma, HighDimProb.Chaining.sauer_shelah) and a closed form for Kearns–Vazirani's $\Phi$ (ComputationalLearning.phi_closed_form, the same recurrence). No statement of Theorem 1, and none over the paper's sequence model of samples, is formalized. This mission formalizes the paper's own route: Lemma 1 in the paper's form, the polynomial bound on $\Phi$, and the dichotomy with the minimal exponent. It also provides the growth function over sequences that the companion missions (Theorem 2, and the entropy criterion Theorem 4) are stated with.

Difficulty

The obvious argument has two steps: bound $\Delta^S$ by $\Phi(n, r)$ whenever no subsample of size $n$ is fully split, then bound $\Phi(n, r)$ by $r^n + 1$. The first step is the Sauer–Shelah lemma, and it does not follow from counting alone. A class can induce many subsamples on $r$ points without inducing all $2^n$ on any fixed $n$ of them, and no counting of subsamples one position at a time rules this out. The second step is elementary but must hold uniformly for all $r$, including $r \le n$, where $\Phi(n, r) = 2^r$ and the bound $2^r \le r^n + 1$ uses $r \le n$.

Samples are sequences, not sets. With repeated points, two positions carrying the same point can never be separated, so Lemma 1 must be applied to position sets rather than point sets. Transferring Mathlib's set-family lemma to this setting is a bookkeeping step that does not reduce to a citation.

Formalization scope

• A sample of size $r$ is x : Fin r → X with positions $0, \dots, r-1$; repetitions are allowed. A subsample of size $n$ is x ∘ e with e : Fin n → Fin i strictly increasing.
• index S x counts distinct Finset (Fin r) of positions {i | x i ∈ A} with A ∈ S. Counting point sets A ∩ {x_1, …, x_r} instead would be a different object when points repeat; the growth function over finite sets of points (as in ComputationalLearning_VC) differs from $m^S$ when $X$ has fewer than $r$ elements.
• growthFunction S r is the supremum in ℕ of index S x over all samples; the family is bounded by $2^r$, so it is a maximum. When $X$ is empty and $r \ge 1$ its value is $0$; $m^S(0) = 1$ exactly when $S$ is nonempty.
• Phi is defined by the recurrence (1). The paper introduces $\Phi(n, r)$ as the maximal number of components into which $r$ hyperplanes cut $n$-space; that geometric identity (Example 3) is not part of this mission.
• Hypothesis added to Theorem 1: $S$ nonempty. The paper calls $n$ "a positive constant"; for $S = \emptyset$ every index is $0$, the first violation is at $r = 0$ and $n$ is not positive.
• Corrections of the printed text. (a) The closed form of $\Phi$ is printed with summand $\binom{r}{n}$; it is formalized with $\binom{r}{k}$ (the printed version already fails at $\Phi(1, 2) = 3$). (b) The proof of Theorem 1 ends "for $r > 0$, $\Phi(n, r) < r^n + 1$", which fails at $n = r = 1$; the milestone is the non-strict bound stated on p. 266. The milestone texts are verbatim from the page.
• Milestone 5 states the first display of the proof of Theorem 1 with its hypothesis as printed: $n$ is the first value of $r$ with $m^S(r) \ne 2^r$.
• The goal keeps the minimality of $n$. A version stating $m^S(r) \le r^n + 1$ for an arbitrary $n$ with $m^S(n) \ne 2^n$ would be a different theorem, and a version that drops the first disjunct or allows $n = 0$ would trivialize.

No measure, σ-algebra or probability appears: the class $S$ is an arbitrary collection of subsets of a bare type. Needed infrastructure: basic API for index (monotonicity in the sample, behaviour under restriction to a subsample) and a bridge between samples and Mathlib's set families (Finset.Shatters, Finset.vcDim). Both are reusable by the two companion missions of this paper, and contributions of either are welcome.

Selected references

• V. N. Vapnik and A. Ya. Chervonenkis, On the uniform convergence of relative frequencies of events to their probabilities, Theory of Probability and Its Applications 16(2) (1971) 264–280 (English translation by B. Seckler). https://doi.org/10.1137/1116025
• N. Sauer, On the density of families of sets, Journal of Combinatorial Theory, Series A 13 (1972) 145–147. https://doi.org/10.1016/0097-3165(72)90019-2
• S. Shelah, A combinatorial problem; stability and order for models and theories in infinitary languages, Pacific Journal of Mathematics 41 (1972) 247–261. https://doi.org/10.2140/pjm.1972.41.247
• A. Blumer, A. Ehrenfeucht, D. Haussler and M. K. Warmuth, Learnability and the Vapnik–Chervonenkis dimension, Journal of the ACM 36(4) (1989) 929–965. https://doi.org/10.1145/76359.76371

Motivation

A logistic regression model is fitted on finitely many samples, and the quantity a practitioner cares about is the misclassification risk of the fitted classifier on new data. Its empirical counterpart, the training error, is biased downwards, and classical generalization bounds give it an additive margin that depends on a complexity measure of the model class rather than on the data at hand.

Shafieezadeh-Abadeh, Mohajerin Esfahani and Kuhn (NIPS 2015) take a distributionally robust route. They surround the empirical distribution of the training data by a ball of distributions in the Wasserstein metric and, for a given weight vector, compute the largest and the smallest misclassification probability over that ball. Their Theorem 3 shows that both extremes are optimal values of explicit linear programs. Combined with a measure-concentration result for the empirical distribution in the Wasserstein metric (Fournier and Guillin, PTRF 2015), the two values bracket the true risk with a prescribed confidence. The same Wasserstein-ball construction underlies the data-driven optimization framework of Mohajerin Esfahani and Kuhn (Math. Program. 2018).

Setting

Let $V$ be the feature space $\mathbb R^n$ with an arbitrary norm $\|\cdot\|$, and let labels take the values $y\in\{-1,+1\}$. The feature-label space is $\Xi = V\times\{-1,+1\}$ with points $\xi=(x,y)$. A weight vector $\beta$ acts on features by $x\mapsto\langle\beta,x\rangle$; its dual norm is $\|\beta\|_* = \sup_{\|x\|\le1}\langle\beta,x\rangle$.

Metric (Definition 2). For a weight $\kappa>0$,

$$d\big((x,y),(x',y')\big) = \|x-x'\| + \kappa\,|y-y'|/2 .$$

Changing a label costs $\kappa$; moving a feature costs its norm distance.

Wasserstein distance (Definition 1). For distributions $\mathbb Q,\mathbb P$ on $\Xi$, $W(\mathbb Q,\mathbb P)$ is the infimum of $\int d(\xi,\xi')\,\Pi(d\xi,d\xi')$ over all couplings $\Pi$ of $\mathbb Q$ and $\mathbb P$. The Wasserstein ball of radius $\varepsilon\ge0$ is $\mathbb B_\varepsilon(\mathbb P) = \{\mathbb Q : W(\mathbb Q,\mathbb P)\le\varepsilon\}$.

Data. Training samples $(\hat x_i,\hat y_i)$, $i=1,\dots,N$, define the empirical distribution $\hat{\mathbb P}_N = \frac1N\sum_{i=1}^N\delta_{(\hat x_i,\hat y_i)}$.

Classifier and risk. Logistic regression models $\operatorname{Prob}(y\mid x) = [1+\exp(-y\langle\beta,x\rangle)]^{-1}$ (eq. (1)). The classifier is $f_\beta(x)=+1$ if $\operatorname{Prob}(+1\mid x)>0.5$ and $-1$ otherwise, and its risk under the data-generating distribution $\mathbb P$ is $\mathfrak R(\beta) = \mathbb P[y\ne f_\beta(x)]$.

Worst- and best-case risks.

$$\mathfrak R_{\max}(\beta) = \sup_{\mathbb Q\in\mathbb B_\varepsilon(\hat{\mathbb P}_N)}\mathbb E^{\mathbb Q}\big[\mathbb 1_{\{y\langle\beta,x\rangle\le0\}}\big],\qquad \mathfrak R_{\min}(\beta) = \inf_{\mathbb Q\in\mathbb B_\varepsilon(\hat{\mathbb P}_N)}\mathbb E^{\mathbb Q}\big[\mathbb 1_{\{y\langle\beta,x\rangle<0\}}\big].$$

The worst case counts a nonpositive margin, the best case a strictly negative one.

The linear programs. For data $(\hat x_i,\hat y_i)$, a weight vector $\hat\beta$ and variables $\lambda\in\mathbb R$, $s,r,t\in\mathbb R^N$, program (10a) minimizes $\lambda\varepsilon + \frac1N\sum_i s_i$ subject to, for every $i$,

$$1 - r_i\hat y_i\langle\hat\beta,\hat x_i\rangle\le s_i,\quad 1 + t_i\hat y_i\langle\hat\beta,\hat x_i\rangle - \lambda\kappa\le s_i,\quad r_i\|\hat\beta\|_*\le\lambda,\quad t_i\|\hat\beta\|_*\le\lambda,\quad r_i,t_i,s_i\ge0 .$$

Program (10b) has the same objective and bounds, with the signs of the two margin terms exchanged.

Formalization targets

Goal: Theorem 3 (i)–(ii)

For every $\kappa>0$, $\varepsilon\ge0$, $N\ge1$, all samples and every weight vector $\hat\beta$, both programs attain their minima $v$ and $w$, and

$$\mathfrak R_{\max}(\hat\beta) = v,\qquad \mathfrak R_{\min}(\hat\beta) = 1-w .$$

The identities hold for each fixed $\hat\beta$, so they apply to any $\hat\beta$ computed from the data.

Milestone: Theorem 3(i) alone

$\mathfrak R_{\max}(\hat\beta)$ equals the minimum of (10a).

Milestones: the confidence clauses

If the training samples are i.i.d. from $\mathbb P$ and the radius is such that $\mathbb P^N\{\mathbb P\in\mathbb B_\varepsilon(\hat{\mathbb P}_N)\}\ge1-\eta$, then for any sample-dependent $\hat\beta$

$$\mathbb P^N\{\mathfrak R(\hat\beta)\le\mathfrak R_{\max}(\hat\beta)\}\ge1-\eta,\qquad \mathbb P^N\{\mathfrak R_{\min}(\hat\beta)\le\mathfrak R(\hat\beta)\}\ge1-\eta,$$ $$\mathbb P^N\{\mathfrak R_{\min}(\hat\beta)\le\mathfrak R(\hat\beta)\le\mathfrak R_{\max}(\hat\beta)\}\ge1-2\eta .$$

Significance

The result. Theorem 3 replaces an optimization over an infinite-dimensional set of distributions by a linear program with $3N+1$ variables and $4N$ constraints plus sign constraints. That makes the worst- and best-case misclassification probabilities computable at the scale of the training set, for any norm on the features whose dual norm can be evaluated. With the confidence clauses, the two values are data-driven upper and lower confidence bounds on the out-of-sample risk of the classifier actually deployed, including one fitted on the same data.

Formalizing it. The paper states Theorem 3 without proof in the main text; the argument is deferred to a technical appendix. No part of it is machine-checked. A formal proof needs the evaluation of a worst-case probability of a closed set over a type-1 Wasserstein ball around a discrete distribution, and the analogous best-case probability of an open set. Both are reusable in any Wasserstein-robust treatment of chance constraints or classification error.

Difficulty

The objective $\mathbf 1_{\{y\langle\beta,x\rangle\le0\}}$ is neither continuous nor concave, so the duality theorems for Wasserstein balls stated for continuous or Lipschitz losses do not apply directly. Upper semicontinuity of the indicator of a closed set is what matters, and the strict inequality in $\mathfrak R_{\min}$ has to be handled as the complement of a closed set. The transport cost couples a norm on the features with a discrete label-flip cost, so a sample can reach the misclassification region either by moving its feature to the hyperplane $\langle\hat\beta,x\rangle=0$ or by flipping its label, and the two options interact through the shared budget $\varepsilon$. Distances to the hyperplane are measured in the given norm and produce the dual norm $\|\hat\beta\|_*$. The degenerate weight $\hat\beta=0$ (every point on the hyperplane) must come out correctly without any division by $\|\hat\beta\|_*$.

Formalization scope

The feature space is a finite-dimensional real normed space V with an arbitrary norm, standing for $(\mathbb R^n,\|\cdot\|)$; the Euclidean norm is not assumed. A weight vector is a continuous linear functional V →L[ℝ] ℝ, and $\|\hat\beta\|_*$ is its operator norm, which is exactly the dual norm. Labels are Bool with an explicit embedding $\text{true}\mapsto+1$, $\text{false}\mapsto-1$; the metric of Definition 2 is written literally. The Wasserstein distance is ℝ≥0∞-valued, probabilities and expectations of indicators are measure values in $[0,\infty]$, and suprema and infima range exactly over the probability measures in the ball. "min" in (10a)/(10b) is formalized as attainment (IsLeast) of the objective over the feasible set. Samples are indexed by Fin N with $N\ge1$.

The following choices differ from a literal reading of the page:

• The paper says the risk "can be expressed as" $\mathbb E^{\mathbb P}[\mathbb 1_{\{y\langle\beta,x\rangle\le0\}}]$. This fails on the hyperplane $\langle\beta,x\rangle=0$, where $f_\beta(x)=-1$ is correct for $y=-1$. The mission defines $\mathfrak R(\beta)=\mathbb P[y\ne f_\beta(x)]$ from (1) and includes the true statement $\mathbb E^{\mathbb P}[\mathbb 1_{\{y\langle\beta,x\rangle<0\}}]\le\mathfrak R(\beta)\le\mathbb E^{\mathbb P}[\mathbb 1_{\{y\langle\beta,x\rangle\le0\}}]$ as a helper item.
• The choice $\varepsilon=\varepsilon_N(\eta)$ of (8) and the measure-concentration theorem behind it (Theorem 2) are not formalized. The confidence clauses take their conclusion, $\mathbb P^N\{\mathbb P\in\mathbb B_\varepsilon(\hat{\mathbb P}_N)\}\ge1-\eta$, as a hypothesis, and "with probability $1-\eta$" is read as "with probability at least $1-\eta$". The printed level $1-2\eta$ is kept for the two-sided bound.

Swapping the strict and non-strict inequalities in $\mathfrak R_{\max}$ and $\mathfrak R_{\min}$, restricting the supremum to measures supported on the sample points, or replacing the ball by a set that excludes non-discrete distributions would each change the theorem. None of these is an acceptable reformulation of the goal.

Useful infrastructure: couplings of a discrete measure with an arbitrary one, the distance from a point to a closed half-space in a general norm, and LP-duality arguments for fractional-knapsack-type programs. Proofs of the helper and confidence items, and any reusable lemma about worst-case probabilities of closed sets over Wasserstein balls, are welcome.

Selected references

• S. Shafieezadeh-Abadeh, P. Mohajerin Esfahani, D. Kuhn, Distributionally Robust Logistic Regression, Advances in Neural Information Processing Systems 28 (NIPS 2015). https://papers.nips.cc/paper/2015/hash/cc1aa436277138f61cda703991069eaf-Abstract.html
• N. Fournier, A. Guillin, On the rate of convergence in Wasserstein distance of the empirical measure, Probability Theory and Related Fields 162 (2015). https://doi.org/10.1007/s00440-014-0583-7
• P. Mohajerin Esfahani, D. Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric: performance guarantees and tractable reformulations, Mathematical Programming 171 (2018). https://doi.org/10.1007/s10107-017-1172-1

Motivation

Logistic regression is among the most widely used classification methods in statistics and machine learning. Its maximum-likelihood estimator minimizes the average logloss on the training data and is known to overfit when data are scarce; practitioners respond with ad hoc regularization, typically a norm penalty on the weight vector. Shafieezadeh-Abadeh, Mohajerin Esfahani and Kuhn (NIPS 2015, arXiv:1509.09259) replace the empirical average by a worst case over all distributions within a Wasserstein ball around the empirical distribution. The resulting model has a finite convex reformulation, contains classical and norm-regularized logistic regression as special cases, and comes with out-of-sample guarantees. It is one of the early instances of Wasserstein distributionally robust optimization in learning, building on the duality theory of Mohajerin Esfahani and Kuhn (Math. Program. 2018, arXiv:1505.05116); the regularization interpretation was later extended to general losses by Shafieezadeh-Abadeh, Kuhn and Mohajerin Esfahani (JMLR 2019, arXiv:1710.10016).

Setting

Let $V$ be the feature space $\mathbb R^n$ with an arbitrary norm $\|\cdot\|$, and let $\|\beta\|_* = \sup_{\|x\|\le1}\langle\beta,x\rangle$ be the dual norm of a weight vector $\beta$. Labels are $y\in\{-1,+1\}$, and the feature-label space is $\Xi = V\times\{-1,+1\}$. The logloss of $\beta$ at $(x,y)$ is

$$l_\beta(x,y) = \log\big(1+\exp(-y\langle\beta,x\rangle)\big).$$

For a label weight $\kappa>0$, the metric of Definition 2 on $\Xi$ is

$$d\big((x,y),(x',y')\big) = \|x-x'\| + \kappa\,|y-y'|/2 ,$$

so that changing a label costs $\kappa$. The Wasserstein distance $W(\mathbb Q,\mathbb P)$ between probability distributions on $\Xi$ (Definition 1) is the infimum of $\int d(\xi,\xi')\,\Pi(d\xi,d\xi')$ over all couplings $\Pi$ of $\mathbb Q$ and $\mathbb P$, and $\mathbb B_\varepsilon(\mathbb P) = \{\mathbb Q : W(\mathbb Q,\mathbb P)\le\varepsilon\}$. Given training samples $(\hat x_i,\hat y_i)_{i=1}^N$, the empirical distribution is $\hat{\mathbb P}_N = \frac1N\sum_i\delta_{(\hat x_i,\hat y_i)}$, and the distributionally robust logistic regression problem (6) is

$$\hat J = \inf_\beta\ \sup_{\mathbb Q\in\mathbb B_\varepsilon(\hat{\mathbb P}_N)} \mathbb E^{\mathbb Q}\big[l_\beta(x,y)\big].$$

Program (7) has variables $\beta$, $\lambda\in\mathbb R$, $s\in\mathbb R^N$, objective $\lambda\varepsilon + \frac1N\sum_i s_i$, and constraints $l_\beta(\hat x_i,\hat y_i)\le s_i$, $l_\beta(\hat x_i,-\hat y_i)-\lambda\kappa\le s_i$ for all $i$, and $\|\beta\|_*\le\lambda$.

Formalization targets

Goal: Theorem 1 (tractable reformulation)

For every $\varepsilon\ge0$, $\kappa>0$, $N\ge1$ and every norm on the feature space,

$$\inf_\beta\ \sup_{\mathbb Q\in\mathbb B_\varepsilon(\hat{\mathbb P}_N)}\mathbb E^{\mathbb Q}[l_\beta] \;=\; \inf\Big\{\lambda\varepsilon+\tfrac1N\textstyle\sum_i s_i : (\beta,\lambda,s)\text{ feasible for (7)}\Big\},$$

and for $\varepsilon>0$ the infimum of (7) is attained.

Milestones

1. §3.1 — the feasible set of (7) is convex.
2. §2 — for $\varepsilon=0$ the worst-case expected logloss is the empirical average logloss, so (6) reduces to classical logistic regression (2).
3. Theorem 1 for fixed $\beta$ — $\sup_{\mathbb Q\in\mathbb B_\varepsilon(\hat{\mathbb P}_N)}\mathbb E^{\mathbb Q}[l_\beta]$ equals the attained minimum of (7) over $(\lambda,s)$ with $\beta$ fixed.
4. Remark 2, eq. (9) — at an optimal solution $(\hat\beta,\hat\lambda,\hat s)$,

$$\hat J = \hat\lambda\varepsilon + \mathbb E^{\hat{\mathbb P}_N}[l_{\hat\beta}] + \tfrac1N\textstyle\sum_i\max\{0,\hat y_i\langle\hat\beta,\hat x_i\rangle-\hat\lambda\kappa\}.$$

5. Remark 1 — as $\kappa\to\infty$ the optimal value of (7) converges to $\inf_\beta \varepsilon\|\beta\|_* + \frac1N\sum_i l_\beta(\hat x_i,\hat y_i)$.
6. Theorem 2, implication — if $\mathbb P^N\{\mathbb P\in\mathbb B_\varepsilon(\hat{\mathbb P}_N)\}\ge1-\eta$, then $\mathbb P^N\{\mathbb E^{\mathbb P}[l_{\hat\beta}]\le\hat J\}\ge1-\eta$.

Significance

Theorem 1 turns a minimax problem over an infinite-dimensional family of distributions into a finite convex program whose size grows linearly in $N$; with the $\ell_1$, $\ell_2$ or $\ell_\infty$ norm it is a standard exponential-cone or conic program. Remark 1 explains norm-regularized logistic regression as a distributionally robust model: the regularizer is the dual norm of the transport cost on features, and the regularization weight is the radius of the ambiguity set. Remark 2 exposes an additional term that accounts for label noise and vanishes as label changes become prohibitively expensive. Theorem 2 makes the optimal value $\hat J$ a certificate on the out-of-sample logloss whenever the ball contains the true distribution.

The paper's proofs are in a technical appendix and have not been machine-checked. Mathlib contains no Wasserstein distributionally robust duality. This mission produces a formal statement of the reformulation with an arbitrary norm and a label-dependent cost, together with formal versions of the paper's printed consequences of it (Remarks 1 and 2, the $\varepsilon=0$ reduction, and the implication in Theorem 2).

Difficulty

The worst-case expectation ranges over every Borel probability distribution within transport distance $\varepsilon$ of the empirical distribution, including distributions with unbounded support and distributions that move mass across labels. Exhibiting good distributions in the ball shows only that the robust value is at least the value of (7); the reverse inequality must control every distribution in the ball at once, and nothing in the definition of the ball bounds its elements' supports. The obvious simplification, restricting attention to distributions supported on finitely many points, again yields only a one-sided bound unless the supremum is shown to be approached by such distributions. The label term of the metric couples the two label classes, so results for a pure norm cost on the features do not apply directly, and the dual norm enters through an arbitrary norm rather than the Euclidean one.

Formalization scope

• The feature space is an abstract finite-dimensional real normed space V standing for $(\mathbb R^n,\|\cdot\|)$ with an arbitrary norm; weights are continuous linear functionals V →L[ℝ] ℝ, and $\|\beta\|_*$ is their operator norm, which is exactly the dual norm. Labels are Bool, embedded as $\pm1$; the label $-y$ is Boolean negation. The metric of Definition 2 is written literally.
• The Wasserstein distance is of type 1, valued in $[0,\infty]$, with couplings ranging over all probability measures on $\Xi\times\Xi$ with the two prescribed marginals. The ball consists of probability measures.
• Expectations of the positive logloss are lower Lebesgue integrals in $[0,\infty]$, and the supremum over the ball is taken there; the optimal value of (7) is the infimum of its (nonnegative) objective over the feasible set, also in $[0,\infty]$. A Bochner integral, which vanishes on non-integrable functions, would make the worst case trivially finite and is not used.
• The standing hypotheses are $\kappa>0$, $\varepsilon\ge0$, $N\ge1$.
• Correction. The paper prints "min" in (7) for all $\varepsilon\ge0$. At $\varepsilon=0$ the minimum can fail to be attained ($V=\mathbb R$, $N=1$, $\hat x_1=1$, $\hat y_1=+1$: the value is $0$ but every feasible point has positive objective). The goal states the value identity for $\varepsilon\ge0$ and attainment for $\varepsilon>0$.
• Remark 1 is formalized as convergence of optimal values as $\kappa\to\infty$; a metric with $\kappa=\infty$ is not formalized. Only convexity, not tractability, of (7) is stated. The first claim of Theorem 2 (the radius (8) and the light-tail assumption) is not formalized; the confidence of the ball event is a hypothesis of milestone 6.
• A formalization in which the ball is taken only over distributions supported on the training samples, or in which the label term of the metric is dropped, trivializes the second constraint group of (7) and is ruled out: the ball here contains every Borel probability distribution on $\Xi$ within the prescribed distance.
• Infrastructure needed and reusable beyond this mission: type-1 optimal transport on product spaces with a label component, couplings and their marginals, and elementary properties of the logloss as a function of $\beta$. Contributions of such supporting lemmas as independent theorems are welcome.

Selected references

• S. Shafieezadeh-Abadeh, P. Mohajerin Esfahani, D. Kuhn, Distributionally Robust Logistic Regression, Advances in Neural Information Processing Systems 28 (NIPS 2015). https://arxiv.org/abs/1509.09259
• P. Mohajerin Esfahani, D. Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric: performance guarantees and tractable reformulations, Mathematical Programming 171 (2018). https://arxiv.org/abs/1505.05116
• N. Fournier, A. Guillin, On the rate of convergence in Wasserstein distance of the empirical measure, Probability Theory and Related Fields 162 (2015). https://arxiv.org/abs/1312.2128
• S. Shafieezadeh-Abadeh, D. Kuhn, P. Mohajerin Esfahani, Regularization via Mass Transportation, Journal of Machine Learning Research 20 (2019). https://arxiv.org/abs/1710.10016