Machine Learning

Motivation

Most generalization guarantees in statistical learning theory bound the gap between training error and expected error through a complexity measure of the hypothesis class: VC dimension, Rademacher complexity, covering numbers. Such bounds are sufficient conditions, and they say little about why a particular algorithm, run on a particular data stream, does or does not generalize. Xu and Mannor (Mach Learn 86 (2012) 391–423) proposed algorithmic robustness as an alternative: an algorithm is robust if a test sample "close to" a training sample incurs a loss close to that training sample's loss. Their first results show that robustness implies generalization (Theorem 1 of the paper, the subject of the first mission in this series).

Section 8 of the paper asks the converse question: is some form of robustness also necessary? The answer is Theorem 8. For a learning method trained on a fixed, growing sequence of samples, generalization is equivalent to a weaker property, weak robustness. The authors present this as evidence that robustness is "an essential property of successful learning", and contrast it with the characterization of learnability by stability (Remark 5 of the paper, citing Shalev-Shwartz et al. 2009; journal version JMLR 11 (2010)): learnability is uniform over all distributions, whereas the generalization studied here is for one distribution and one training sequence.

Setting

Let $\mathcal Z$ be a measurable space of samples, drawn from an unknown probability measure $\mu$. Let $\mathcal H$ be a set of hypotheses and $l : \mathcal H \times \mathcal Z \to \mathbb R$ a loss with $0 \le l(h, z) \le M$ for all $h, z$ (the paper's standing assumption, Sect. 1.1).

• The expected loss of $h$ is $\mathcal L(h) = \mathbb E_{z \sim \mu}\, l(h, z)$ (expectedLoss).
• The average loss of $h$ on an $n$-sample set $\mathbf t(n) = (t_1, \dots, t_n)$ is $L(h, \mathbf t(n)) = \frac1n \sum_{i=1}^n l(h, t_i)$ (avgLoss).
• A learning method $\mathcal A = \{\mathcal A^n\}_{n \in \mathbb N}$ is a sequence of maps $\mathcal A^n : \mathcal Z^n \to \mathcal H$; $\mathcal A_{\mathbf s(n)}$ is the hypothesis learned from $\mathbf s(n)$.
• A training sequence $\mathbf s^* = (s^*_1, s^*_2, \dots)$ is fixed and deterministic, and $\mathbf s^*(n)$ denotes its first $n$ elements (firstN).
• A test sample $\mathbf t(n)$ consists of $n$ i.i.d. draws from $\mu$; $\Pr$ always refers to $\mathbf t(n) \sim \mu^n$.

The method generalizes w.r.t. $\mathbf s^*$ (Definition 8) if

$$\lim_{n\to\infty} \big| \mathcal L(\mathcal A_{\mathbf s^*(n)}) - L(\mathcal A_{\mathbf s^*(n)}, \mathbf s^*(n)) \big| = 0.$$

It is weakly robust w.r.t. $\mathbf s^*$ (Definition 9) if there are sets $\mathcal D_n \subseteq \mathcal Z^n$ with $\Pr(\mathbf t(n) \in \mathcal D_n) \to 1$ and

$$\lim_{n\to\infty} \Big\{ \max_{\hat{\mathbf s}(n) \in \mathcal D_n} \big| L(\mathcal A_{\mathbf s^*(n)}, \hat{\mathbf s}(n)) - L(\mathcal A_{\mathbf s^*(n)}, \mathbf s^*(n)) \big| \Big\} = 0. \qquad (6)$$

A set $\mathcal D_n$ can be read as a family of perturbed copies of the training set that carries almost all of the probability of the test sample.

Formalization targets

Goal: Theorem 8 (p. 409)

$$\mathcal A \text{ generalizes w.r.t. } \mathbf s^* \iff \mathcal A \text{ is weakly robust w.r.t. } \mathbf s^*,$$

for every probability measure $\mu$, every loss measurable in $z$ with values in $[0, M]$, every learning method $\mathcal A$ and every training sequence $\mathbf s^*$.

Milestones

1. First equality of the proof (p. 410). For $n \ge 1$ and every $h$, $\mathbb E_{\mathbf t(n)} L(h, \mathbf t(n)) = \mathcal L(h)$.
2. Sufficiency display (p. 410). If $\Pr(\mathbf t(n) \notin \mathcal D) \le \delta$ and $|L(h, \hat{\mathbf s}) - L(h, \mathbf s)| \le \epsilon$ on $\mathcal D$, then

$$\big|\mathcal L(h) - L(h, \mathbf s)\big| \le \delta M + \epsilon.$$

3. Lemma 2 (p. 410). If $\mathcal A$ is not weakly robust w.r.t. $\mathbf s^*$, there are $\epsilon^*, \delta^* > 0$ with

$$\Pr\big(|L(\mathcal A_{\mathbf s^*(n)}, \mathbf t(n)) - L(\mathcal A_{\mathbf s^*(n)}, \mathbf s^*(n))| \ge \epsilon^*\big) \ge \delta^* \quad\text{for infinitely many } n. \qquad (8)$$

4. Eq. (9) (p. 411). $L(\mathcal A_{\mathbf s^*(n)}, \mathbf t(n)) - \mathcal L(\mathcal A_{\mathbf s^*(n)}) \to 0$ in probability.

Milestones 1–2 give the sufficiency direction; milestones 3–4 give necessity.

Significance

Theorem 8 is a characterization, not a bound. The sufficiency half says a quantitative robustness property yields generalization. The necessity half says every method that generalizes along a sequence is weakly robust along it, so no generalization argument can avoid something of this shape. The paper remarks that $(K, \epsilon)$-robustness for every $\epsilon$ implies weak robustness, which places Theorem 1's condition inside this characterization. Corollary 6, the almost-sure version (generalization with probability 1 iff almost-sure weak robustness), follows from Theorem 8 applied sequence by sequence.

The result is proved in the paper; no machine-checked proof of it is known. This mission contributes a formal statement of Definitions 8 and 9 in Lean, the two directions of the proof as reusable finite-$n$ and asymptotic lemmas, and a place to formalize the bounded-loss law of large numbers for a hypothesis that changes with $n$ (Eq. (9)), which Mathlib states for a fixed random variable.

Difficulty

The sufficiency direction is a direct estimate once the expectation of the average test loss is identified with the expected loss; the formal work is in handling the product measure $\mu^n$ and a set $\mathcal D_n$ that need not be measurable.

The necessity direction is where care is needed. Eq. (9) is not the weak law of large numbers for a fixed function: the hypothesis $\mathcal A_{\mathbf s^*(n)}$ changes with $n$, so the concentration must be uniform in the hypothesis, which holds only because the loss is uniformly bounded. Lemma 2 negates a statement with an existential over sequences of sets and a limit; the naive reading "for each $\epsilon, \delta$ some $\mathcal D_n$ works eventually" does not by itself produce a single sequence $\mathcal D_n$ satisfying (6) with one limit.

Formalization scope

• $\mathcal Z$ is a type with a MeasurableSpace, $\mu$ a Measure with IsProbabilityMeasure, $\mathcal H$ an arbitrary type. The learning method is A : (n : ℕ) → (Fin n → Z) → H, the training sequence sStar : ℕ → Z, and $\mathbf t(n) \sim$ Measure.pi (fun _ : Fin n => μ). Indices start at $0$.
• The loss bound $0 \le l \le M$ is a hypothesis of every theorem. Measurability of $l(h, \cdot)$ is added; the paper explicitly ignores measurability. Expectations are Bochner integrals, well defined here because the loss is bounded and measurable.
• Probabilities and their limits live in $[0, \infty]$ (ℝ≥0∞). The sets $\mathcal D_n$ need not be measurable; their probability is the outer measure. "For infinitely many $n$" is ∃ᶠ n in atTop.
• Eq. (6) is encoded without a supremum: weak robustness asks for sets $D_n$ and reals $\eta_n \to 0$ with $|L(\mathcal A_{\mathbf s^*(n)}, \hat{\mathbf s}) - L(\mathcal A_{\mathbf s^*(n)}, \mathbf s^*(n))| \le \eta_n$ for all $n$ and all $\hat{\mathbf s} \in D_n$. This avoids Lean's junk value $\sup \emptyset = 0$; since $\Pr(\mathbf t(n) \in D_n) \to 1$ forces $D_n$ to be nonempty for all large $n$, the bound form is equivalent to the paper's reading.
• Only part 1 of Definitions 8 and 9 is formalized. Corollary 6 is out of scope.
• The goal is not trivial in either direction: a constant method on a one-point space satisfies both sides, and a constant method whose hypothesis has training average $1$ and expected loss $1/2$ along a fixed sequence fails both, so neither side is vacuous or always true.
• Needed infrastructure: integrals over Measure.pi of coordinate functions, a Chebyshev or Hoeffding bound for averages of bounded i.i.d. variables uniform over a family of functions, and a diagonal-sequence construction. The uniform concentration lemma is reusable beyond this mission. Proofs of the milestones, and alternative routes to Eq. (9), are welcome.

Selected references

• Huan Xu, Shie Mannor, Robustness and Generalization, Machine Learning 86 (2012) 391–423. https://doi.org/10.1007/s10994-011-5268-1
• Shai Shalev-Shwartz, Ohad Shamir, Nathan Srebro, Karthik Sridharan, Learnability, Stability and Uniform Convergence, Journal of Machine Learning Research 11 (2010) 2635–2670. https://www.jmlr.org/papers/v11/shalev-shwartz10a.html
• Wassily Hoeffding, Probability Inequalities for Sums of Bounded Random Variables, Journal of the American Statistical Association 58 (1963) 13–30. https://doi.org/10.1080/01621459.1963.10500830

Why algorithmic robustness

A learning algorithm maps a training set to a hypothesis. It generalizes when the loss it incurs on the training set is close to its expected loss on fresh data. The classical way to certify this bounds the complexity of the whole hypothesis class the algorithm may output, through its VC dimension, covering numbers or Rademacher complexity. A second approach, algorithmic stability (Bousquet and Elisseeff 2002), looks instead at how the output changes when one training point is replaced.

Huan Xu and Shie Mannor proposed a third notion, algorithmic robustness. An algorithm is robust if the sample space can be cut into finitely many cells such that a test point falling in the same cell as a training point incurs nearly the same loss as that training point. The notion came out of their earlier analyses of support vector machines and the Lasso as robust optimization problems (Xu, Caramanis and Mannor 2009). The conference version appeared at COLT 2010, and the journal version, which this mission follows, is Xu and Mannor, Machine Learning 86 (2012) 391–423.

Robustness is a property of the algorithm and not of its hypothesis class, so it applies to algorithms whose class has infinite VC dimension. The paper's main result for i.i.d. data is Theorem 1 (p. 396). This mission formalizes Theorem 1 together with the steps of its proof.

Setting

Throughout, $\mathcal Z$ is a measurable space of samples and $\mathcal H$ is an arbitrary set of hypotheses. A loss $l : \mathcal H \times \mathcal Z \to \mathbb R$ satisfies $0 \le l(h,z) \le M$ for a constant $M$. A training set is $\mathbf s = (s_1, \dots, s_n) \in \mathcal Z^n$, and a learning algorithm is a map $\mathcal A : \mathcal Z^n \to \mathcal H$, written $\mathbf s \mapsto \mathcal A_{\mathbf s}$.

For a probability measure $\mu$ on $\mathcal Z$, the expected error and the training error of the learned hypothesis are

$$\mathcal L(\mathcal A_{\mathbf s}) = \mathbb E_{z\sim\mu}\, l(\mathcal A_{\mathbf s}, z), \qquad l_{\mathrm{emp}}(\mathcal A_{\mathbf s}) = \frac1n \sum_{i=1}^n l(\mathcal A_{\mathbf s}, s_i).$$

Definition 2 (p. 396). For $K \in \mathbb N$ and $\epsilon(\cdot) : \mathcal Z^n \to \mathbb R$, the algorithm $\mathcal A$ is $(K, \epsilon(\cdot))$-robust if $\mathcal Z$ can be partitioned into $K$ disjoint sets $C_1, \dots, C_K$ such that for every $\mathbf s \in \mathcal Z^n$,

$$\forall s \in \mathbf s,\ \forall z \in \mathcal Z,\ \forall i:\quad s, z \in C_i \implies |l(\mathcal A_{\mathbf s}, s) - l(\mathcal A_{\mathbf s}, z)| \le \epsilon(\mathbf s).$$

The partition is chosen once, before the training set. Only the tolerance $\epsilon(\mathbf s)$ may depend on $\mathbf s$.

For a partition $C_1,\dots,C_K$, the cell count $|N_i|$ is the number of training points in $C_i$. The Lean development uses expectedLoss, empiricalLoss, cellCount and IsRobust in the namespace XuMannorRobust.Standard.

Formalization targets

Goal: Theorem 1 (p. 396)

Let $\mathcal A$ be $(K,\epsilon(\cdot))$-robust and let $\mathbf s$ consist of $n \ge 1$ i.i.d. draws from $\mu$. Then for every $\delta > 0$, with probability at least $1-\delta$,

$$|\mathcal L(\mathcal A_{\mathbf s}) - l_{\mathrm{emp}}(\mathcal A_{\mathbf s})| \le \epsilon(\mathbf s) + M\sqrt{\frac{2K\ln 2 + 2\ln(1/\delta)}{n}}.$$

The constants are the paper's and are kept as printed. $K$, $\epsilon(\cdot)$, $M$, $n$, $\delta$, $\mu$ and the algorithm are all universally quantified.

Milestones (proof of Theorem 1, pp. 396–397)

1. Bretagnolle–Huber–Carol inequality for the multinomial vector of cell counts. For every $\lambda \ge 0$,

$$\Pr\Big\{\sum_{i=1}^K \Big|\frac{|N_i|}{n} - \mu(C_i)\Big| \ge \lambda\Big\} \le 2^K \exp\Big(\frac{-n\lambda^2}{2}\Big).$$

2. Eq. (3). With probability at least $1-\delta$,

$$\sum_{i=1}^K \Big|\frac{|N_i|}{n} - \mu(C_i)\Big| \le \sqrt{\frac{2K\ln 2 + 2\ln(1/\delta)}{n}}.$$

3. Eq. (4). For a partition witnessing robustness and for every training set $\mathbf s$, deterministically,

$$|\mathcal L(\mathcal A_{\mathbf s}) - l_{\mathrm{emp}}(\mathcal A_{\mathbf s})| \le \epsilon(\mathbf s) + M\sum_{i=1}^K \Big|\frac{|N_i|}{n} - \mu(C_i)\Big|.$$

Significance

Theorem 1 is the base result of the robustness framework. The later results of the same paper are extensions of it:

• Corollary 1: an adaptive number of cells;
• Corollaries 2 and 3: covering-number instances;
• Theorem 4: a pseudo-robust version;
• the Markovian case.

Its complexity term depends only on the number of cells $K$, not on any capacity measure of $\mathcal H$. This is why it gives bounds for algorithms such as support vector machines, Lasso, feed-forward networks and principal component analysis (Sect. 6 of the paper). For those, $K$ is a covering number of the sample space. Section 8 of the paper shows that a weak form of robustness is also necessary for generalization.

Theorem 1 is a published result with a short proof. What a formalization adds:

• a machine-checked statement of the robustness notion, pinning down which quantifier comes first;
• a formal proof of the multinomial concentration step, which the paper takes from van der Vaart and Wellner rather than proving;
• a reusable interface for the covering-number examples.

A search of the platform (2026-09-26) found no formal statement of Theorem 1, Definition 2, or the Bretagnolle–Huber–Carol inequality for multinomial vectors. Hoeffding's inequality is already available there in proved form.

Difficulty

The deterministic step, Eq. (4), splits the expected loss over the cells. It then compares the loss within each cell with the loss at the training points in that cell. This needs integration over a partition and some care with cells of $\mu$-measure zero, where the conditional expectation in the paper's chain is undefined.

The main obstacle is the probabilistic step. The quantity $\sum_i ||N_i|/n - \mu(C_i)|$ is an $\ell_1$ deviation of a multinomial vector. A coordinate-wise Hoeffding bound followed by a union bound over the $K$ coordinates gives a bound whose deviation level grows linearly in $K$. That is not $2^K e^{-n\lambda^2/2}$, and it does not give the constant $\sqrt{2K\ln 2}$ of Theorem 1. The difficulty is to obtain the exact exponential rate $2^K e^{-n\lambda^2/2}$ for the $\ell_1$ deviation as a whole, with no loss in the constant.

Formalization scope

Samples are a type Z with a MeasurableSpace, training sets are Fin n → Z, the algorithm is a function (Fin n → Z) → H, and the loss is H → Z → ℝ. The partition is a family C : Fin K → Set Z that is pairwise disjoint, measurable, and covers Z. Empty cells are allowed, as in the paper. The i.i.d. sample law is Measure.pi (fun _ => μ) with μ a probability measure, and $\mu(C_i)$ enters as a real number.

"With probability at least $1-\delta$" is encoded as an upper bound $\delta$ on the outer measure, under $\mu^n$, of the set of training sets where the inequality fails. This needs no measurability of $\mathbf s \mapsto \mathcal A_{\mathbf s}$.

The paper ignores measurability. The formalization restores it: every $l(h,\cdot)$ is measurable and every cell is a measurable set. Together with $0 \le l \le M$ this makes the expected error a genuine expectation.

The theorems assume $n \ge 1$. The Bretagnolle–Huber–Carol step assumes $\lambda \ge 0$, because the printed inequality is false for $\lambda < 0$. No upper bound on $\delta$ is imposed: for $\delta > 2^K$ the radicand is negative, the square root evaluates to $0$, and the statements remain true.

Two trivializing readings of Definition 2 are ruled out:

• The partition may not depend on the training set. In IsRobust the existential over the partition precedes the universal over training sets. If the order were swapped, every algorithm with a $\{0,1\}$-valued loss would be $(2,0)$-robust, since it could take the two level sets of its own learned loss as cells. Theorem 1 would then fail for a memorizing classifier.
• The tolerance may not depend on the test point, and the condition is required for every $z \in \mathcal Z$, not only for $z$ equal to a training point.

Beyond the paper's text, a complete development needs the integral over a finite measurable partition, a Hoeffding bound for indicator averages, and a union bound over the subsets of Fin K. The multinomial concentration inequality is reusable beyond this mission, in histogram estimators, discretization arguments and the covering-number examples of the paper. Contributions are welcome at every level: proofs of the milestones, and alternative proofs of the Bretagnolle–Huber–Carol step (for instance via the method of types).

Selected references

• H. Xu and S. Mannor, Robustness and Generalization, Machine Learning 86 (2012) 391–423. https://doi.org/10.1007/s10994-011-5268-1
• A. W. van der Vaart and J. A. Wellner, Weak Convergence and Empirical Processes, Springer, 1996 (Proposition A.6.6). https://doi.org/10.1007/978-1-4757-2545-2
• O. Bousquet and A. Elisseeff, Stability and Generalization, Journal of Machine Learning Research 2 (2002) 499–526. https://www.jmlr.org/papers/v2/bousquet02a.html
• H. Xu, C. Caramanis and S. Mannor, Robustness and Regularization of Support Vector Machines, Journal of Machine Learning Research 10 (2009) 1485–1510. https://www.jmlr.org/papers/v10/xu09b.html
• W. Hoeffding, Probability Inequalities for Sums of Bounded Random Variables, Journal of the American Statistical Association 58 (1963) 13–30. https://doi.org/10.1080/01621459.1963.10500830

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