Machine Learning

Motivation

Chapter 3 of The Principles of Deep Learning Theory by D. A. Roberts and S. Yaida (arXiv:2106.10165) is the book's first complete example of its effective-theory method. For deep linear networks at initialization, the two- and four-point correlators of the network outputs can be computed exactly at any width and depth. The resulting formulas exhibit, in the simplest setting, the phenomena that organize the rest of the book: criticality of the weight variance $C_W=1$, non-Gaussianity that grows with depth, and the depth-to-width ratio $\ell/n$ as the parameter controlling deviations from the infinite-width limit. This mission formalizes §§3.1–3.3. It is the second mission in a series formalizing the book (namespace DeepLearningTheory).

Setting

A deep linear network with widths $n_0, n_1, n_2, \dots$ (all positive) and zero biases maps an input $x\in\mathbb{R}^{n_0}$ to preactivations

$$z^{(0)}_i = x_i,\qquad z^{(\ell+1)}_i = \sum_{j=1}^{n_\ell} W^{(\ell+1)}_{ij}\, z^{(\ell)}_j \quad (i=1,\dots,n_{\ell+1}),$$

(eqs. 3.1–3.2 with $b^{(\ell)}=0$). At initialization all weights $W^{(\ell)}_{ij}$ are independent centered Gaussians with $\mathbb{E}[W^{(\ell)}_{i_1j_1}W^{(\ell)}_{i_2j_2}] = \delta_{i_1i_2}\delta_{j_1j_2}\, C_W/n_{\ell-1}$ (eq. 3.4), with a layer-independent $C_W\ge0$. For inputs $x_{\alpha_1}, x_{\alpha_2}$ let $G^{(0)}_{\alpha_1\alpha_2} = \frac1{n_0}\sum_j x_{j;\alpha_1}x_{j;\alpha_2}$ (eq. 3.9).

Formalization targets

Goal: the exact four-point correlator (eqs. 3.21, 3.25)

For every layer $\ell\ge1$, a single input $x$, and neurons $i_1,\dots,i_4$,

$$\mathbb{E}\big[z^{(\ell)}_{i_1}z^{(\ell)}_{i_2}z^{(\ell)}_{i_3}z^{(\ell)}_{i_4}\big] = (\delta_{i_1i_2}\delta_{i_3i_4}+\delta_{i_1i_3}\delta_{i_2i_4}+\delta_{i_1i_4}\delta_{i_2i_3})\; C_W^{2\ell}\Big[\prod_{\ell'=1}^{\ell-1}\Big(1+\frac{2}{n_{\ell'}}\Big)\Big]\big(G^{(0)}\big)^2 .$$

Milestones

1. Eq. (3.6) — the mean preactivation vanishes.
2. Eq. (3.10) — first-layer two-point correlator $\mathbb{E}[z^{(1)}_{i_1;\alpha_1}z^{(1)}_{i_2;\alpha_2}] = \delta_{i_1i_2}C_W G^{(0)}_{\alpha_1\alpha_2}$.
3. Eqs. (3.12), (3.15) — two-point correlator in layer $\ell$: $\delta_{i_1i_2}C_W^{\ell}G^{(0)}_{\alpha_1\alpha_2}$.
4. Eq. (3.18) — first-layer four-point correlator.
5. Eq. (3.20) — the layer-to-layer recursion for the four-point correlator.
6. Eqs. (3.21)–(3.24) — the recursion $G_4^{(\ell+1)} = C_W^2(1+2/n_\ell)G_4^{(\ell)}$ for the coefficient of the Wick tensor structure.
7. Eq. (3.30) — the connected four-point correlator between two distinct neurons, $G_4^{(\ell)} - (G_2^{(\ell)})^2$.

Significance

The closed forms show that a deep linear network is exactly Gaussian only in the strict infinite-width limit: at criticality $C_W=1$ the connected four-point correlator (3.29)–(3.30) is $\big[\prod(1+2/n_{\ell'})-1\big](G^{(0)})^2 \approx \frac{2(\ell-1)}{n}(G^{(0)})^2$ for equal widths $n$, the first appearance of the depth-to-width ratio as the book's emergent scale. The same recursive method is reused for nonlinear networks in Chapters 4–5. The results are exact computations in the book; this mission formalizes them.

Difficulty

Each correlator is an expectation of a polynomial in exponentially many Gaussian weights. The book's recursion uses that the layer-$(\ell+1)$ weights are independent of the layer-$\ell$ preactivations, followed by Wick contraction of the two or four new weights. In Lean this requires independence of a weight family from a measurable function of the earlier layers, integrability of products of Gaussian polynomials, and careful handling of the Kronecker-delta bookkeeping in the sums (3.23).

Formalization scope

• Widths are n : ℕ → ℕ with n 0 the input dimension; neural indices are $0,\dots,n_\ell-1$. Weights are a random field W : Ω → ℕ → ℕ → ℕ → ℝ on a probability space, only entries $W^{(\ell)}_{ij}$ with $\ell\ge1$, $i<n_\ell$, $j<n_{\ell-1}$ are used.
• IsLinearNetInit P n CW W states mutual independence of all these weights and that each has law gaussianReal 0 (CW / n (ℓ-1)).
• linearPreact n (W ω) x ℓ i is $z^{(\ell)}_i(x)$; inputKernel (n 0) x₁ x₂ is $G^{(0)}_{\alpha_1\alpha_2}$; kron and wickDelta4 are the Kronecker delta and the three-term tensor structure.
• Widths are assumed positive where the source's formulas require it (division by $n_\ell$, nonempty hidden layers). Every hypothesis is satisfiable by a product of independent Gaussians.

Selected references

• D. A. Roberts, S. Yaida (with B. Hanin), The Principles of Deep Learning Theory, Cambridge University Press, 2022, Chapter 3. arXiv:2106.10165
• B. Hanin, M. Nica, Products of many large random matrices and gradients in deep neural networks, Commun. Math. Phys. 376 (2020). arXiv:1812.05994

Motivation

Chapter 4 of The Principles of Deep Learning Theory by D. A. Roberts and S. Yaida (arXiv:2106.10165) begins the analysis of general multilayer perceptrons (MLPs) with a nonlinear activation function $\sigma$ at initialization. The first layer is exactly Gaussian; the second layer is the first place where non-Gaussianity appears, as a connected four-point correlator suppressed by $1/n_1$ and governed by the four-point vertex $V^{(2)}$. This mission formalizes §§4.1–4.2, which are exact at any width. It is the third mission in a series formalizing the book (namespace DeepLearningTheory) and reuses the definitions of Mission II (Deep Linear Networks at Initialization).

Setting

An MLP with widths $n_0,n_1,n_2,\dots$ and activation $\sigma:\mathbb{R}\to\mathbb{R}$ maps inputs $x_\alpha\in\mathbb{R}^{n_0}$ to preactivations

$$z^{(1)}_{i;\alpha}=b^{(1)}_i+\sum_{j=1}^{n_0}W^{(1)}_{ij}x_{j;\alpha},\qquad z^{(\ell+1)}_{i;\alpha}=b^{(\ell+1)}_i+\sum_{j=1}^{n_\ell}W^{(\ell+1)}_{ij}\,\sigma\big(z^{(\ell)}_{j;\alpha}\big)$$

(eqs. 4.2, 4.30). At initialization all biases and weights are independent centered Gaussians with $\mathbb{E}[b^{(\ell)}_ib^{(\ell)}_j]=\delta_{ij}C_b^{(\ell)}$ and $\mathbb{E}[W^{(\ell)}_{i_1j_1}W^{(\ell)}_{i_2j_2}]=\delta_{i_1i_2}\delta_{j_1j_2}C_W^{(\ell)}/n_{\ell-1}$ (eqs. 4.3–4.4). The first-layer metric is $G^{(1)}_{\alpha_1\alpha_2}=C_b^{(1)}+C_W^{(1)}\frac1{n_0}\sum_jx_{j;\alpha_1}x_{j;\alpha_2}$ (eq. 4.8), and $\langle F(z_{\alpha_1},\dots,z_{\alpha_m})\rangle_{g}$ denotes the expectation over a centered Gaussian vector $(z_\alpha)$ with covariance $g$ (eq. 4.25), with $\sigma_\alpha\equiv\sigma(z_\alpha)$.

Formalization targets

Goal: second-layer connected four-point correlator (eq. 4.43)

$$\mathbb{E}\big[z^{(2)}_{i_1;\alpha_1}z^{(2)}_{i_2;\alpha_2}z^{(2)}_{i_3;\alpha_3}z^{(2)}_{i_4;\alpha_4}\big]\Big|_{\text{connected}}=\frac{1}{n_1}\Big[\delta_{i_1i_2}\delta_{i_3i_4}V^{(2)}_{(\alpha_1\alpha_2)(\alpha_3\alpha_4)}+\delta_{i_1i_3}\delta_{i_2i_4}V^{(2)}_{(\alpha_1\alpha_3)(\alpha_2\alpha_4)}+\delta_{i_1i_4}\delta_{i_2i_3}V^{(2)}_{(\alpha_1\alpha_4)(\alpha_2\alpha_3)}\Big]$$

with the four-point vertex $V^{(2)}_{(\alpha_1\alpha_2)(\alpha_3\alpha_4)}=\big(C_W^{(2)}\big)^2\big[\langle\sigma_{\alpha_1}\sigma_{\alpha_2}\sigma_{\alpha_3}\sigma_{\alpha_4}\rangle_{G^{(1)}}-\langle\sigma_{\alpha_1}\sigma_{\alpha_2}\rangle_{G^{(1)}}\langle\sigma_{\alpha_3}\sigma_{\alpha_4}\rangle_{G^{(1)}}\big]$ (eq. 4.40).

Milestones

1. Eq. (4.6) — first-layer mean vanishes.
2. Eqs. (4.7)–(4.8) — first-layer two-point correlator $\delta_{i_1i_2}G^{(1)}_{\alpha_1\alpha_2}$.
3. Eq. (4.9) — first-layer four-point correlator is the Wick value.
4. Eq. (4.23) — the first-layer preactivations are exactly Gaussian with covariance $\delta_{i_1i_2}G^{(1)}_{\alpha_1\alpha_2}$.
5. Eqs. (4.27), (4.28), (4.29) — activation correlators in the first layer as Gaussian expectations.
6. Eq. (4.40) — two-point correlator of the second-layer metric fluctuation.
7. Eq. (4.41) — second-layer two-point correlator.

Significance

These identities are the base case of the book's recursion (Chapter 4.3 onward) for the kernel and four-point vertex in deeper layers, and they show concretely that a finite-width network is not a Gaussian process: the $1/n_1$ connected correlator is generically nonzero for nonlinear $\sigma$. The results are exact computations in the book; this mission formalizes them.

Difficulty

The second layer is a Gaussian conditional on the first layer, with a random covariance (the stochastic metric, eq. 4.36). Turning this into unconditional correlators requires conditioning on the first-layer preactivations, independence of different first-layer neurons, and the identification of first-layer activation correlators with Gaussian expectations over the metric $G^{(1)}$, which may be degenerate (e.g. repeated inputs). Integrability of $\sigma$ against Gaussians must be controlled.

Formalization scope

• Definitions from Mission II are reused: kron, inputKernel, WeightIndex. New definitions: mlpPreact ($z^{(\ell)}_i(x)$), IsMLPInit (independent Gaussian biases and weights with layer-dependent $C_b^{(\ell)},C_W^{(\ell)}$), firstLayerMetric ($G^{(1)}$ on finitely many inputs), gaussAvg ($\langle\cdot\rangle_g$, via Mathlib's multivariateGaussian, which handles singular positive-semidefinite $g$), and HasPolyGrowth.
• Statements about activations assume $\sigma$ measurable with polynomial growth, the standing convention guaranteeing that all Gaussian averages are finite; this covers ReLU, tanh, sigmoid, GELU, SWISH and the perceptron step function.
• The sample set is Fin D (for the specific statements, $D=2$ or $4$ inputs, possibly repeated). $n_1>0$ is assumed where the formulas divide by $n_1$.

Selected references

• D. A. Roberts, S. Yaida (with B. Hanin), The Principles of Deep Learning Theory, Cambridge University Press, 2022, Chapter 4. arXiv:2106.10165
• R. M. Neal, Bayesian Learning for Neural Networks, Springer, 1996. doi:10.1007/978-1-4612-0745-0

Motivation

Chapter 13 showed that convex-Lipschitz-bounded and convex-smooth-bounded problems are learnable by regularized loss minimization; Chapter 14 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019) shows how to learn them with the simplest possible algorithm. Gradient descent moves against the gradient with a fixed step size and outputs the average of its iterates; its analysis (Lemma 14.1) is a single telescoping identity that bounds $\sum_t \langle w^{(t)} - w^\star, v_t\rangle$ for any sequence of directions $v_t$, and this generality is the whole point. It gives the rate $B\rho/\sqrt T$ for convex Lipschitz functions (Corollary 14.2), extends to nondifferentiable functions through subgradients (Definition 14.4, Lemmas 14.3 and 14.7), and, because it never used that the directions were gradients, extends to stochastic gradient descent, in which each direction is random with a subgradient as its conditional expectation (Theorem 14.8). Applied to the risk $L_D(w)$ with a fresh example at each step, SGD is a learning algorithm whose sample complexity is the iteration count: $B^2\rho^2/\epsilon^2$ examples for convex-Lipschitz-bounded problems (Corollary 14.12) and $12B^2\beta/\epsilon^2$ for convex-smooth-bounded ones (Theorem 14.13, Corollary 14.14). A projected, decreasing-step variant for strongly convex objectives has rate $(\rho^2/(2\lambda T))(1 + \log T)$ (Theorem 14.11).

Setting

Hypotheses are vectors in $\mathbb{R}^d$; convex, Lipschitz and smooth losses, convex-Lipschitz-bounded and convex-smooth-bounded problems, and strong convexity are those of Mission IX. A vector $v$ is a subgradient of $f$ at $w$ if $f(u) \ge f(w) + \langle u - w, v\rangle$ for all $u$. The iterates of an update rule $w^{(1)} = 0$, $w^{(t+1)} = w^{(t)} - \eta v_t$ are indexed from $0$, and the output after $T$ steps is $\bar w = \frac1T\sum_{t < T} w^{(t)}$. The randomness of SGD is modelled as the chapter uses it in §14.5: a sample $z_0, \dots, z_{T-1}$ drawn i.i.d. from $D$ and an oracle $g$ with $v_t = g(w^{(t)}, z_t)$, where $g$ is a stochastic subgradient oracle for $f$ if $\mathbb{E}_{z \sim D}\, g(w, z) \in \partial f(w)$ for every $w$. This is the book's condition $\mathbb{E}[v_t \mid w^{(t)}] \in \partial f(w^{(t)})$ in the case where the direction depends on the past only through $w^{(t)}$ and on fresh randomness, which is what every application in the book does; the expectation $\mathbb{E}[f(\bar w)]$ is then an integral over $D^T$. For learning, $g(w, z)$ is a subgradient of $\ell(\cdot, z)$ at $w$, so that $\mathbb{E}_z g(w,z)$ is a subgradient of $L_D$ at $w$ (14.13). The projection of $w$ onto a convex set $H$ is a nearest point of $H$, and the strongly convex variant projects after each step with step size $1/(\lambda t)$.

Formalization targets

Goal: Theorem 14.8

For a convex $f$, $B, \rho > 0$, a measurable oracle $g$ with $\mathbb{E}_z g(w, z) \in \partial f(w)$ and $\|g(w, z)\| \le \rho$, any $w^\star$ with $\|w^\star\| \le B$, $T \ge 1$ and $\eta = B/(\rho\sqrt T)$: $\mathbb{E}[f(\bar w)] - f(w^\star) \le B\rho/\sqrt T$; and for every $\epsilon > 0$, $T \ge B^2\rho^2/\epsilon^2$ gives $\mathbb{E}[f(\bar w)] - f(w^\star) \le \epsilon$.

Milestones

Lemma 14.1. For any directions, $\sum_{t<T}\langle w^{(t)} - w^\star, v_t\rangle \le \|w^\star\|^2/(2\eta) + (\eta/2)\sum_{t<T}\|v_t\|^2$; with $\|v_t\| \le \rho$, $\|w^\star\| \le B$ and $\eta = B/(\rho\sqrt T)$ the average is at most $B\rho/\sqrt T$.

Corollary 14.2. Subgradient descent on a convex $\rho$-Lipschitz $f$ with $\eta = B/(\rho\sqrt T)$ has $f(\bar w) - f(w^\star) \le B\rho/\sqrt T$ for every $\|w^\star\| \le B$, and $T \ge B^2\rho^2/\epsilon^2$ gives $\epsilon$.

Lemma 14.7. A convex $f$ on $\mathbb{R}^d$ is $\rho$-Lipschitz iff all its subgradients have norm at most $\rho$.

Lemma 14.9. For the projection $v$ of $w$ onto a convex $H$ and $u \in H$, $\|w - u\|^2 \ge \|v - u\|^2$.

Theorem 14.11. For $\lambda$-strongly convex $f$, a closed convex $H$, an oracle with $\mathbb{E}_z\|g(w,z)\|^2 \le \rho^2$ and any $w^\star \in H$, the projected variant with $\eta_t = 1/(\lambda t)$ has $\mathbb{E}[f(\bar w)] - f(w^\star) \le (\rho^2/(2\lambda T))(1 + \log T)$.

Corollary 14.12. SGD on the risk of a convex-Lipschitz-bounded problem with $T \ge B^2\rho^2/\epsilon^2$ examples has $\mathbb{E}[L_D(\bar w)] \le L_D(w) + \epsilon$ for every $w \in H$.

Theorem 14.13. For convex, $\beta$-smooth, nonnegative losses and $\eta\beta < 1$, SGD with gradient directions has $\mathbb{E}[L_D(\bar w)] \le \frac{1}{1-\eta\beta}(L_D(w^\star) + \|w^\star\|^2/(2\eta T))$.

Corollary 14.14. For a convex-smooth-bounded problem with $\ell(0,z) \le 1$ and any $\epsilon > 0$, SGD with $\eta = 1/(\beta(1 + 3/\epsilon))$ and $T \ge 12B^2\beta/\epsilon^2$ has $\mathbb{E}[L_D(\bar w)] \le L_D(w) + \epsilon$ for every $w \in H$.

Further items: Lemma 14.3, Claims 14.5, 14.6 and 14.10, and the hinge-loss subgradient of Example 14.2.

Significance

SGD is the algorithm behind most of modern machine learning, and Theorem 14.8 is its basic guarantee: dimension-free, independent of the form of $f$ beyond convexity, and with a sample complexity matching the regularization bound of Chapter 13 up to a constant. Lemma 14.1 isolates the deterministic identity that makes both gradient descent and its stochastic version work, and Lemma 14.7 is the bridge between the Lipschitz assumption of Chapter 12 and the bounded directions the analysis needs. The learning corollaries make the point that runs through Part II of the book: for convex problems, optimization and learning are the same activity, and one pass over the data suffices.

Nothing here is machine-checked. The chapter's statements are essentially correct, and the formalization records the reading choices rather than corrections: the i.i.d.-oracle model of the randomness, the subgradient form of gradient descent, the bound at every point of the ball rather than at a minimizer, and, in Corollary 14.14, the assumptions $\epsilon \le 1$ and $0 \in H$ under which the derivation from Theorem 14.13 goes through.

Difficulty

Lemma 14.1 is a completed square and a telescoping sum and is the intended entry point; the $B\rho/\sqrt T$ clause is the substitution of $\eta$. Corollary 14.2 is Lemma 14.1 with Jensen's inequality for the average and the subgradient inequality at each iterate, plus Lemma 14.7 to bound the directions. The subgradient facts need convex analysis: Lemma 14.3 in the direction "convex implies subgradients exist" is the supporting hyperplane theorem on $\mathbb{R}^d$, which Mathlib does not offer directly; Claim 14.5 uses the first-order characterization of convexity for differentiable functions; Lemma 14.7's "Lipschitz implies bounded subgradients" is the book's one-line argument along $u = w + \epsilon v/\|v\|$. Theorem 14.8 is Lemma 14.1 plus the conditioning argument of the book, which in the i.i.d.-oracle model is Fubini on the product $D^T$: the iterate $w^{(t)}$ is a measurable function of $z_0, \dots, z_{t-1}$, and integrating $\langle w^{(t)} - w^\star, g(w^{(t)}, z_t)\rangle$ over $z_t$ first gives $\langle w^{(t)} - w^\star, \mathbb{E}_z g(w^{(t)}, z)\rangle \ge f(w^{(t)}) - f(w^\star)$. Theorem 14.11 adds the projection lemma, the strong-convexity inequality of Claim 14.10, the telescoping of $\frac{\lambda t}{2}(a_t - a_{t+1}) - \frac\lambda2 a_t$ and the harmonic sum $\sum_{t \le T} 1/t \le 1 + \log T$; the second-moment hypothesis makes $\mathbb{E}\|w^{(t)} - w^\star\|^2$ finite inductively. Corollary 14.12 is Theorem 14.8 for $f = L_D$ with the oracle of (14.13), which requires exchanging a subgradient inequality with the integral over $z$. Theorem 14.13 replaces the Lipschitz bound by self-boundedness, $\|\nabla\ell\|^2 \le 2\beta\ell$, and rearranges; Corollary 14.14 is its arithmetic under the added assumptions. In all expectation statements the measurability of the iterates in the sample, from the measurability of the oracle, is a routine but necessary lemma.

Formalization scope

Iterates are defined by structural recursion, so no argmin is chosen; the sample-driven SGD stops after $T$ updates; the projection onto $H$ is a chosen nearest point, unique for closed convex $H$. Bounds are stated for every $w^\star$ in the ball (or in $H$) rather than for a minimizer, which is what the proofs give and is stronger. The oracle bound $\|g(w,z)\| \le \rho$ is required surely (the book: with probability $1$); the almost-sure version is a routine extension. The second-moment hypothesis of Theorem 14.11 is a lower Lebesgue integral, so that a non-integrable oracle cannot satisfy it vacuously. The learning corollaries assume a measurable loss, nonnegative and bounded at the origin, so that the risks are genuine integrals, and a measurable selector of subgradients. Variable step sizes (§14.4.2), other averaging schemes (§14.4.3), SGD for regularized loss minimization (§14.5.3) and the exercises are not stated.

Trivializing readings are excluded: the expectations are over the product law of the examples with measurable integrands, the subgradient conditions are pointwise inequalities, and the iteration counts are the book's. Welcome contributions: Lemma 14.1 as a reusable telescoping lemma, the measurability of the SGD iterates, and the Fubini step that turns an oracle condition into the inequality (14.10).

Selected references

• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 14. doi:10.1017/CBO9781107298019
• H. Robbins, S. Monro, A stochastic approximation method, Annals of Mathematical Statistics 22(3), 1951. doi:10.1214/aoms/1177729586
• M. Zinkevich, Online convex programming and generalized infinitesimal gradient ascent, Proceedings of ICML, 2003.
• A. Nemirovski, A. Juditsky, G. Lan, A. Shapiro, Robust stochastic approximation approach to stochastic programming, SIAM Journal on Optimization 19(4), 2009. doi:10.1137/070704277
• S. Shalev-Shwartz, Online learning and online convex optimization, Foundations and Trends in Machine Learning 4(2), 2012. doi:10.1561/2200000018

Motivation

Chapters 12 and 13 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019) leave binary classification for the general framework in which a hypothesis is a vector $w \in \mathbb{R}^d$ and the loss $\ell(w, z)$ is a convex function of $w$. Convexity makes the ERM problem tractable (Lemma 12.11), but Examples 12.8 and 12.9 show that convexity, even with a bounded class, does not by itself make a problem learnable: one-dimensional linear regression with the squared loss defeats every learner. The chapter therefore isolates two families, the convex-Lipschitz-bounded and the convex-smooth-bounded problems (Definitions 12.12 and 12.13), and Chapter 13 proves that both are learnable, not by ERM but by Regularized Loss Minimization with Tikhonov regularization, $A(S) \in \operatorname{argmin}_w L_S(w) + \lambda\|w\|^2$. The proof goes through a new idea: stability. Theorem 13.2 expresses the expected overfitting $\mathbb{E}[L_D(A(S)) - L_S(A(S))]$ exactly as the expected effect of replacing one training example, strong convexity of the regularized objective bounds that effect (Lemma 13.5, Corollaries 13.6 and 13.7), and balancing the regularization against the fit gives oracle inequalities (Corollaries 13.8 and 13.10) and sample-complexity guarantees (Corollaries 13.9 and 13.11), with ridge regression as the worked example (Theorem 13.1).

Setting

Hypotheses are vectors in $\mathbb{R}^d$ with the Euclidean norm, as in Mission VI; risk, empirical risk, the product law of a sample and agnostic PAC learnability are those of Mission I. A problem is convex when $H$ is convex and every $\ell(\cdot, z)$ is convex; it is convex-Lipschitz-bounded with parameters $\rho, B$ when moreover $\|w\| \le B$ on $H$ and every $\ell(\cdot, z)$ is $\rho$-Lipschitz on $\mathbb{R}^d$, and convex-smooth-bounded with parameters $\beta, B$ when every $\ell(\cdot, z)$ is nonnegative and differentiable with a $\beta$-Lipschitz gradient. Lipschitzness and smoothness are required on all of $\mathbb{R}^d$ because the RLM rule is unconstrained and its outputs need not lie in $H$. The RLM rule is a relation: $w$ is an output on $S$ if it minimizes $L_S(w) + \lambda\|w\|^2$ over $\mathbb{R}^d$, and a learner implements the rule if all its outputs are minimizers. For the losses of the chapter the minimizer exists and is unique. Given $S = (z_1, \dots, z_m)$ and a further example $z'$, $S^{(i)}$ is $S$ with $z_i$ replaced by $z'$; a learner is on-average-replace-one-stable with rate $\epsilon(m)$ if $\mathbb{E}_{(S,z') \sim D^{m+1},\, i \sim U(m)}[\ell(A(S^{(i)}), z_i) - \ell(A(S), z_i)] \le \epsilon(m)$ for every distribution. Strong convexity is Mathlib's StrongConvexOn, which is Definition 13.4 verbatim.

Expectations over samples are integrals against product laws. For them to be genuine, the theorems about arbitrary learners assume a jointly measurable loss bounded by a constant and a measurable learner, and the theorems about RLM assume a jointly measurable, nonnegative loss bounded at the origin and a measurable learner; for RLM the latter is automatic, since the minimizer is unique.

Formalization targets

Goal: Corollary 13.9

For a convex-Lipschitz-bounded problem with parameters $\rho, B > 0$ and the RLM learner with $\lambda(m) = \sqrt{2\rho^2/(B^2 m)}$: for every distribution, every $m \ge 1$ and every $w \in H$, $\mathbb{E}_S[L_D(A(S))] \le L_D(w) + \rho B\sqrt{8/m}$; hence for every $\epsilon > 0$ and $m \ge 8\rho^2B^2/\epsilon^2$, $\mathbb{E}_S[L_D(A(S))] \le L_D(w) + \epsilon$.

Milestones

Examples 12.8–12.9. Linear regression on $\mathbb{R}$ with the squared loss is not agnostic PAC learnable, over $H = \mathbb{R}$ or over $H = [-1, 1]$.

Theorem 13.2. For any measurable learner and $m \ge 1$, $\mathbb{E}_S[L_D(A(S)) - L_S(A(S))]$ equals the replace-one expectation of (13.6).

Lemma 13.5. $\lambda\|w\|^2$ is $2\lambda$-strongly convex; a strongly convex function plus a convex one is strongly convex; at a minimizer $u$ of a $\lambda$-strongly convex $f$, $f(w) - f(u) \ge \frac\lambda2\|w - u\|^2$.

Corollary 13.6. For a convex $\rho$-Lipschitz loss and $\lambda > 0$, RLM satisfies $\ell(A(S^{(i)}), z_i) - \ell(A(S), z_i) \le 2\rho^2/(\lambda m)$ for every $S, z', i$, is stable with that rate, and has $\mathbb{E}_S[L_D(A(S)) - L_S(A(S))] \le 2\rho^2/(\lambda m)$.

Corollary 13.7. For a convex, nonnegative, $\beta$-smooth loss and $\lambda \ge 2\beta/m$, the replace-one expectation is at most $(48\beta/(\lambda m))\,\mathbb{E}[L_S(A(S))]$, and at most $48\beta C/(\lambda m)$ if $\ell(0, z) \le C$.

Corollary 13.8. $\mathbb{E}_S[L_D(A(S))] \le L_D(w^*) + \lambda\|w^*\|^2 + 2\rho^2/(\lambda m)$ for every $w^*$.

Corollary 13.10. $\mathbb{E}_S[L_D(A(S))] \le (1 + 48\beta/(\lambda m))\,\mathbb{E}_S[L_S(A(S))] \le (1 + 48\beta/(\lambda m))(L_D(w^*) + \lambda\|w^*\|^2)$.

Corollary 13.11. A convex-smooth-bounded problem with $\ell(0, z) \le 1$ is learned by RLM with $\lambda = \epsilon/(3B^2)$ once $m \ge 150\beta B^2/\epsilon^2$.

Theorem 13.1. Ridge regression on the unit ball with labels in $[-1, 1]$, $\lambda = \epsilon/(3B^2)$ and $m \ge 150 B^2/\epsilon^2$ has $\mathbb{E}_S[L_D(A(S))] \le \min_{\|w\| \le B} L_D(w) + \epsilon$.

Further items: Lemma 12.11, the hinge loss as a convex surrogate of the 0–1 loss, the stability-implies-no-overfitting remark of §13.2, and the ridge regression system (13.4)–(13.5).

Significance

Stability is the third route to learnability in the book after uniform convergence and nonuniform learnability, and the only one that applies to convex-Lipschitz-bounded problems in general, for which uniform convergence can fail (the book's Exercise 13.2). The chain from strong convexity through replace-one stability to oracle inequalities is the template for the analysis of every regularized learner, and Theorem 13.2 is an exact identity, not a bound. Ridge regression, support vector machines (Chapter 15) and the regularized algorithms of later chapters are all instances.

Nothing here is machine-checked. The sample sizes of Corollary 13.11 and Theorem 13.1 are the book's $150$. Chaining Corollary 13.10 as printed would need $216$, but the derivation of Corollary 13.7 actually gives the stability rate $20\beta/(\lambda m)$, with which $90$ suffices.

Difficulty

Lemma 12.11 and the hinge surrogate are direct. Lemma 13.5 is elementary but part (3) needs the limit $\alpha \to 0$ of the strong-convexity inequality at a minimizer. Examples 12.8–12.9 require constructing the two finitely supported distributions of the book and computing the risk of a fixed output on each; the probability that all $m$ examples are of the second type is at least $0.99$ under both, and the deterministic learner's output on that sample decides which distribution defeats it. Theorem 13.2 is the exchangeability argument of the book: $\mathbb{E}[\ell(A(S), z')] = \mathbb{E}[\ell(A(S^{(i)}), z_i)]$ because swapping $z_i$ and $z'$ preserves the product law; the formal work is the measure-preserving transposition on $Z^{m+1}$ and the integrability of the functions involved. Corollaries 13.6 and 13.7 follow the book's pointwise derivation from (13.7) to (13.11) and (13.12) to (13.14), where the smooth case uses the self-boundedness $\|\nabla\ell\|^2 \le 2\beta\ell$ of nonnegative smooth functions and the inequality $(a + b)^2 \le 3(a^2 + b^2)$; passing to expectations then uses Theorem 13.2 and, for the smooth case, the symmetry $\mathbb{E}[\ell(A(S^{(i)}), z')] = \mathbb{E}[\ell(A(S), z_i)]$. Corollaries 13.8 to 13.11 are the arithmetic of the book once (13.16), $\mathbb{E}[L_S(A(S))] \le L_D(w^*) + \lambda\|w^*\|^2$, is in hand, with the corrected constant for 13.11. The ridge system is the gradient condition for a strongly convex quadratic, and Theorem 13.1 is Corollary 13.11 applied to $\frac12(\langle w, x\rangle - y)^2$, which is $\|x\|^2$-smooth with $\ell(0, z) = y^2/2 \le 1/2$ on the support. In every expectation statement the measurability of $S \mapsto A(S)$ for the RLM rule, which the theorems take as a hypothesis, is provable from uniqueness of the minimizer and is worth a lemma.

Formalization scope

Losses are real-valued functions of a vector and an example; Lipschitz and smoothness conditions are global on $\mathbb{R}^d$. The RLM rule is a minimizer relation with the regularization parameter as an explicit argument, and Corollary 13.9's learner uses a parameter depending on $m$. Stability quantifies over $m \ge 1$ and averages over the replaced index. Expectation statements carry measurability hypotheses that make every integral genuine, and the theorems about arbitrary learners assume a bounded loss. The minimum over $H$ is stated as "for every $w \in H$", so no minimizer is needed. Definitions 12.1–12.9 and Claims 12.4–12.9 (general convex analysis) are not restated, nor are Examples 12.10–12.11, the discussion of §12.3 beyond the surrogate property, Remark 13.1, and Exercises 12.1–12.4 and 13.1–13.2.

Trivializing readings are excluded: the nonlearnability examples are stated as negations of the framework's learnability, the stability identity is an equality with both sides genuine integrals, and the constants of the oracle inequalities are the book's. Welcome contributions: the transposition invariance of product laws behind Theorem 13.2, the bound $\|A(S)\|^2 \le L_S(0)/\lambda$ for RLM outputs, the measurability of the RLM minimizer, and the self-boundedness inequality (12.6).

Selected references

• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapters 12 and 13. doi:10.1017/CBO9781107298019
• O. Bousquet, A. Elisseeff, Stability and generalization, Journal of Machine Learning Research 2, 2002.
• S. Shalev-Shwartz, O. Shamir, N. Srebro, K. Sridharan, Learnability, stability and uniform convergence, Journal of Machine Learning Research 11, 2010.
• A. N. Tikhonov, On the stability of inverse problems, Doklady Akademii Nauk SSSR 39(5), 1943.
• S. Boyd, L. Vandenberghe, Convex Optimization, Cambridge University Press, 2004. doi:10.1017/CBO9780511804441

From conditional motion to a marginal probability path

Flow matching models a changing probability distribution using a time-dependent velocity field. A conditional model specifies a density and a velocity separately for each conditioning point. The mathematical question is whether those conditional descriptions determine a velocity for the mixture distribution. This mission concerns the continuity-equation formulation of Theorem 1 of Lipman, Chen, Ben-Hamu, Nickel, and Le, Flow Matching for Generative Modeling (ICLR 2023). The source is arXiv:2210.02747v2, Section 3.1 and Appendix A.

Densities, velocities, and probability flux

Fix a natural number $d$ and let $E=\mathbb R^d$. The conditioning distribution $Q$ is a Borel probability measure on $E$. At time $t$, position $x$, and conditioning point $z$, write $\rho(t,x,z)$ for the conditional density and $v(t,x,z)\in E$ for the conditional velocity. The variable $x$ is integrated against Lebesgue measure; $z$ is integrated against $Q$. These roles remain distinct even though both variables take values in the same space.

The conditional flux is $F(t,x,z)=\rho(t,x,z)v(t,x,z)$. The marginal density, marginal flux, and marginal velocity are defined by

$$p(t,x)=\int_E\rho(t,x,z)\,dQ(z),\qquad J(t,x)=\int_E F(t,x,z)\,dQ(z),\qquad u(t,x)=p(t,x)^{-1}J(t,x).$$

These definitions express equations (6) and (8) using a probability measure rather than a data-density function. This representation also allows discrete conditioning distributions. Every conditional density is strictly positive and normalized on $0\leq t\leq1$, jointly measurable in $(x,z)$, and integrable in $z$ at each fixed $(t,x)$.

The divergence of a differentiable vector field is the sum of the diagonal entries of its derivative. A density and velocity satisfy the classical continuity equation when their flux is spatially differentiable and the density has time derivative equal to minus that divergence.

Formalization targets

The goal asserts that $p(t,\cdot)$ is a positive probability density for every $t\in[0,1]$ and that

$$\partial_t p(t,x)+\operatorname{div}_x\bigl(p(t,x)u(t,x)\bigr)=0\qquad(0<t<1,\ x\in E).$$

The hypotheses require the conditional continuity equation for $Q$-almost every conditioning point, at each interior time and spatial point. They also specify a sufficient local domination package for differentiation under the integral. This is an explicit classical interpretation of the regularity qualification in the proof of Theorem 1.

Four supporting targets isolate the mathematical assertions used by this formulation: the probability-density property of equation (6); time differentiation under the conditioning integral; spatial divergence under the conditioning integral; and the velocity/flux identity corresponding to equation (8). The source contains these equations and operations rather than separately numbered supporting lemmas, so the milestone titles identify the relevant equation or proof passage.

What completing the formalization provides

The deliverable is a checked interface for passing from a measurable family of conditional continuity equations to the continuity equation of its mixture. It records which variables are differentiated, which measure is used for averaging, where positivity is needed, and which assumptions justify each analytic operation. The time and spatial differentiation lemmas are stated for general measures and integrands, making them reusable outside this particular probability model.

The mathematical result is already proved in the cited paper. The uploaded theorem items are open formalization targets, with explicit proof placeholders. Successful local compilation checks their types and imports; it does not establish their conclusions. The definition module contains no proof placeholders.

Analytic obligations

Pointwise differentiability of every conditional function does not by itself justify differentiating an integral over the conditioning variable. The regularity predicates therefore require a neighborhood independent of that variable, an integrable bound for the derivative norm throughout that neighborhood, and almost-everywhere measurability of the integrand and derivative. Time and space receive separate predicates because their derivatives take values in different spaces.

There is also a distinction between density normalization in $x$ and integrability in $z$ at a fixed position. The formal assumptions record both. A probability measure on the conditioning space does not make every measurable function integrable. These conditions prevent the totalized Bochner integral from silently supplying a default value where an intended integral fails to exist.

Formalization scope

Space is represented by Fin d → ℝ, with its standard finite-product Borel structure and Lebesgue measure. Its norm is the standard product norm used by mathlib. All finite dimensions, including dimension zero, are included. Time-dependent functions are defined on all real times, while density assumptions apply on the closed unit interval and derivative conclusions apply on its interior. No endpoint time derivative is asserted.

The regularity package is one sufficient realization of the source's Leibniz-rule assumption, not a claim to the weakest possible hypotheses. Conditional continuity equations may hold almost everywhere in the conditioning variable; their exceptional sets may depend on the fixed time and position. Spatial differentiability of the marginal flux is part of the conclusion, so the equation cannot be satisfied merely through the default value of an undefined derivative.

The target is the PDE formulation. It does not assert existence of a global ODE flow, uniqueness of transported measures, or equality with a flow pushforward. Those require a separate transport development. It also asserts no endpoint approximation to a data distribution and no theorem about optimization, neural networks, or Gaussian paths. No marginal continuity equation or differentiation–integration interchange is assumed as an input.

Required infrastructure consists of Bochner integration, finite-dimensional differentiation, finite sums of derivative coordinates, and product-measure integration. Contributions may prove the supporting targets or the goal directly while preserving their statements and the distinction between classical PDE and flow-transport claims.

Selected references

• Yaron Lipman, Ricky T. Q. Chen, Heli Ben-Hamu, Maximilian Nickel, and Matt Le. Flow Matching for Generative Modeling. ICLR 2023. arXiv:2210.02747v2, Section 2, Section 3.1, Theorem 1, equations (6), (8), and (26), and Appendix A's proof of Theorem 1.
• mathlib contributors. ParametricIntegral.lean, revision 0df444a360eaa60ab8c11dca51a86af692955474. Differentiation under the integral.

Motivation

Boosting answers a question raised by Kearns and Valiant: can a learner that is only slightly better than random guessing be turned into one that is arbitrarily accurate? Chapter 10 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019) defines γ-weak learnability (Definition 10.1), the PAC requirement with the accuracy $\epsilon$ replaced by the fixed value $1/2 - \gamma$, and presents AdaBoost, the algorithm of Freund and Schapire that, given weak hypotheses, reweights the training set round by round and outputs a weighted majority vote. The chapter's main result (Theorem 10.2) is that the training error of AdaBoost's output decreases as $e^{-2\gamma^2 T}$ in the number of rounds. Since the output is a halfspace over the predictions of $T$ base hypotheses, the chapter then bounds the VC-dimension of that class (Lemma 10.3), so that the number of rounds becomes a knob for the bias–complexity tradeoff. Example 10.1 shows a concrete weak learner, ERM over decision stumps for the class of 3-piece classifiers on the line, and the chapter remarks that, statistically, weak learnability is no easier than strong learnability: a class of infinite VC-dimension is not weakly learnable either.

Setting

The framework is that of Missions I and IV: binary classification over a domain $X$ with the 0–1 loss, distributions $D$ over $X$ with a labeling function $f$, learners as functions of the sample, the VC-dimension, and ERM. Labels and hypotheses are Boolean, with $\pm 1$ values obtained through $\operatorname{sgn}(\text{true}) = 1$, $\operatorname{sgn}(\text{false}) = -1$, and $\operatorname{sign}(z)$ is true exactly when $z > 0$. A γ-weak learner for $H$ with the function $m_H : (0,1) \to \mathbb{N}$ returns, for every $\delta$, every $D$ and every measurable $f$ realizable by $H$, a hypothesis with $L_{(D,f)}(h) \le 1/2 - \gamma$ with probability at least $1 - \delta$ once $m \ge m_H(\delta)$; the failure event is bounded in outer measure as in Definition 3.1.

AdaBoost is formalized as a deterministic function of the sample $S = (x_1, y_1), \dots, (x_m, y_m)$ and of the sequence of weak hypotheses $h_0, h_1, \dots$ that the weak learner returned. The distributions are defined by recursion: $D^{(0)}$ is uniform, $\epsilon_t = \sum_i D^{(t)}_i \mathbb{1}[h_t(x_i) \ne y_i]$, $w_t = \frac12 \log(1/\epsilon_t - 1)$, and $D^{(t+1)}_i \propto D^{(t)}_i \exp(-w_t y_i h_t(x_i))$; the output after $T$ rounds is $x \mapsto \operatorname{sign}(\sum_{t < T} w_t h_t(x))$. Rounds are indexed from $0$, so $D^{(0)}$ is the book's $D^{(1)}$. The class $L(B, T)$ of Equation (10.4) consists of the functions $x \mapsto \operatorname{sign}(\sum_{t=1}^T w_t h_t(x))$ with $h_t \in B$. Decision stumps over $\mathbb{R}$ are the threshold functions $x \mapsto [\theta < x]$ and their negations $x \mapsto [x \le \theta]$; a 3-piece classifier is $b$ outside $[\theta_1, \theta_2]$ and $-b$ inside, with $\theta_1 < \theta_2$.

Formalization targets

Goal: Theorem 10.2

If $\gamma > 0$ and every round $t < T$ has $0 < \epsilon_t \le 1/2 - \gamma$, then the empirical 0–1 risk of AdaBoost's output after $T$ rounds is at most $\exp(-2\gamma^2 T)$.

Milestones

§10.1. A class of infinite VC-dimension is not γ-weak-learnable for any $\gamma > 0$ (domain with measurable singletons, measurable hypotheses).

Example 10.1. There is one sample-size function with which every ERM learner over the decision stumps is a $1/12$-weak learner for the 3-piece classifiers.

Exercise 10.3. For a nonempty sample and $\epsilon_t \in (0,1)$, the error of $h_t$ under $D^{(t+1)}$ is exactly $1/2$.

Lemma 10.3. If $T \ge 3$ and $\mathrm{VCdim}(B) = d \ge 3$, then $\mathrm{VCdim}(L(B,T)) \le T(d+1)(3\log(T(d+1)) + 2)$.

Further item: Exercise 10.4 (1), $\mathrm{VCdim}(B) \le \mathrm{VCdim}(L(B,T))$ for $T \ge 1$.

Significance

Theorem 10.2 is the reason AdaBoost works and the template for every analysis of boosting: a potential function, here $\frac1m \sum_i e^{-y_i f_t(x_i)}$, bounds the 0–1 training error and contracts by the factor $2\sqrt{\epsilon_{t}(1-\epsilon_{t})} \le \sqrt{1 - 4\gamma^2}$ at every round. Lemma 10.3 supplies the other half of the picture, an estimation-error bound growing only like $T \cdot \mathrm{VCdim}(B)$ up to logarithms, so that Theorem 6.8 turns the pair into a generalization guarantee for boosting. The remark of §10.1 places weak learning in the statistical landscape of Part I: the VC-dimension characterizes it too, and the gain of boosting is computational.

Nothing here is machine-checked. Two points where the book's text needs care are built into the statements. The weight $w_t$ is undefined when $\epsilon_t = 0$, and the algorithm's normalization then divides $0$ by $0$; in Lean the logarithm of a negative number is $0$, so with $\epsilon_t = 0$ the formal algorithm would ignore a perfect weak hypothesis and the bound could fail. The theorems therefore assume $\epsilon_t > 0$, which is the case in which the book's formulas are defined. And the book's derivation of "infinite VC-dimension implies not weakly learnable" from the lower bound of Theorem 6.8 at $\epsilon = 1/2 - \gamma$ uses that bound outside the range in which Chapter 28 proves it; the statement itself is true, by the $km$-point form of the No-Free-Lunch argument (Exercise 5.3 of Mission III) and Lemma B.1.

Difficulty

Exercise 10.4 (1) is a one-line embedding of $B$ into $L(B, T)$ with the weights $(1, 0, \dots, 0)$ and is the entry point. Exercise 10.3 is the computation of the book: after the update, the weight of the mistakes of $h_t$ is $e^{w_t}\epsilon_t$ and the weight of the correct examples is $e^{-w_t}(1 - \epsilon_t)$, and with $e^{w_t} = \sqrt{(1-\epsilon_t)/\epsilon_t}$ these are equal. Theorem 10.2 needs, by induction on the round, the closed form $D^{(t)}_i = e^{-y_i f_{t}(x_i)}/\sum_j e^{-y_j f_{t}(x_j)}$ of the distribution, the pointwise bound $\mathbb{1}[\operatorname{sign}(f(x)) \ne y] \le e^{-y f(x)}$ for the sign convention used, the telescoping product (10.2), the identity $Z_{t+1}/Z_t = 2\sqrt{\epsilon_t(1-\epsilon_t)}$, the monotonicity of $a(1-a)$ on $[0, 1/2]$ and $1 - a \le e^{-a}$. Lemma 10.3 counts dichotomies: Sauer's lemma bounds the restrictions of $B$ to a shattered set by $(em/d)^d$, choosing $T$ of them gives $(em/d)^{dT}$, the halfspaces of $\mathbb{R}^T$ contribute $(em/T)^T$ by Theorem 9.2, and the inequality $2^m \le m^{(d+1)T}$ is solved with Lemma A.1; the finite-VC lower bound $m \le d + 1$ handles small $m$, and the numeric slack of the book's chain must be checked. Example 10.1 combines a geometric observation, that one of the three regions of a 3-piece classifier has mass at most $1/3$ and a stump agrees with the other two, with the agnostic guarantee for ERM over the stumps from Theorem 6.7, applied with accuracy $1/12$; the best stump may only approach error $1/3$ because constant functions are not stumps, and the slack absorbs this. The §10.1 remark is the argument sketched above.

Formalization scope

AdaBoost is a function of the sample and of the returned weak hypotheses; the weak learner's randomness and its failure probability (Remark 10.2) are not modelled, and Theorem 10.2 is the deterministic statement the book proves. Rounds are indexed from $0$. The output uses $\operatorname{sign}(0) =$ negative, consistently with Mission VI. The class $L(B,T)$ is a set of functions, so Lemma 10.3 is a statement about the VC-dimension of Mission IV, with the bound taken in $\mathbb{N} \cup \{\infty\}$ through the integer part of the real right-hand side and the natural logarithm. Decision stumps are closed under negation, as the book's $\operatorname{sign}(x - \theta)\cdot b$; constant functions are not stumps. The efficient ERM for decision stumps (§10.1.1), the face-recognition features (§10.4), Exercises 10.1, 10.2, 10.4 (2)–(3) and 10.5 are not stated. The claims of §10.3 that piecewise-constant classifiers with $T$ pieces lie in $L(\text{stumps}, T)$ and that this class shatters $T+1$ points depend on treating $\operatorname{sign}(x - (-\infty))$ as a stump and on the sign convention; with real thresholds, $L(\text{stumps}, 2)$ does not shatter three points under either convention, so these claims are not stated.

Trivializing readings are excluded: the weak-error hypotheses are strict where the book's formulas require it, the VC bounds are in $\mathbb{N} \cup \{\infty\}$, and the weak-learner guarantee quantifies over all distributions and all realizable labelings. Welcome contributions: the closed form of $D^{(t)}$, the contraction identity for $Z_{t+1}/Z_t$, and the dichotomy count behind Lemma 10.3.

Selected references

• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 10. doi:10.1017/CBO9781107298019
• Y. Freund, R. E. Schapire, A decision-theoretic generalization of on-line learning and an application to boosting, Journal of Computer and System Sciences 55(1), 1997. doi:10.1006/jcss.1997.1504
• R. E. Schapire, The strength of weak learnability, Machine Learning 5(2), 1990. doi:10.1007/BF00116037
• M. Kearns, L. Valiant, Cryptographic limitations on learning Boolean formulae and finite automata, Journal of the ACM 41(1), 1994. doi:10.1145/174644.174647
• R. E. Schapire, Y. Freund, Boosting: Foundations and Algorithms, MIT Press, 2012.

Motivation

Part II of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019) turns from the theory of learnability to hypothesis classes that can actually be learned by algorithms, and it starts with the family that almost every practical method is built on: linear predictors. Chapter 9 introduces the affine functions $L_d$ and the three classes obtained by composing them with a link: halfspaces for classification, linear regression for real-valued prediction, and logistic regression in between. For each class it gives an ERM algorithm and the guarantee that goes with it. For halfspaces in the separable case the algorithm is Rosenblatt's Perceptron, and the guarantee is the classical mistake bound (Theorem 9.1): the number of updates is at most $(RB)^2$, where $R$ bounds the data and $B$ is the norm of the smallest vector separating it with margin one. The chapter then computes the VC-dimension of halfspaces (Theorems 9.2 and 9.3), which by the fundamental theorem of Mission IV makes them learnable, derives the Least Squares normal equations for regression, and observes that the logistic loss is convex, the property later chapters exploit.

Setting

Vectors live in $\mathbb{R}^d$ with its Euclidean inner product and norm. The affine functions are $h_{w,b}(x) = \langle w, x\rangle + b$, homogenous when $b = 0$; a halfspace hypothesis is $x \mapsto \operatorname{sign}(\langle w, x\rangle + b)$, formalized as a Boolean predictor that is true exactly when $\langle w, x\rangle + b > 0$ (the book leaves $\operatorname{sign}(0)$ unspecified; the VC computations do not depend on the convention). A sample $(x_1, y_1), \dots, (x_m, y_m)$ with labels $y_i \in \{\pm 1\}$ is separable if some $w$ has $y_i\langle w, x_i\rangle > 0$ for all $i$; the constants of Theorem 9.1 are $B = \inf\{\|w\| : \forall i,\ y_i\langle w, x_i\rangle \ge 1\}$ and $R = \max_i \|x_i\|$. The Batch Perceptron starts at $w^{(0)} = 0$ and, while some example has $y_i\langle w^{(t)}, x_i\rangle \le 0$, adds $y_i x_i$; since the algorithm may pick any mistaken example, a run is any sequence of updates obeying this rule, and the theorem is stated for all runs. For regression the loss is $(h(x) - y)^2$ and the Least Squares system is $Aw = b$ with $A = \sum_i x_i x_i^\top$, written as the linear map $w \mapsto \sum_i \langle x_i, w\rangle x_i$, and $b = \sum_i y_i x_i$. The logistic function is $\varphi_{sig}(z) = 1/(1 + e^{-z})$ and the logistic loss is $\log(1 + \exp(-y\langle w, x\rangle))$. The learning-theoretic notions (ERM, PAC and agnostic PAC learnability, VC-dimension) are those of Missions I and IV.

Formalization targets

Goal: Theorem 9.1 (Perceptron convergence)

For a separable sample with labels in $\{\pm 1\}$, every run of the Batch Perceptron of $T$ iterations satisfies $T \le (RB)^2$, and some run of at most $(RB)^2$ iterations ends with $y_i\langle w^{(T)}, x_i\rangle > 0$ for every $i$.

Milestones

Equation (9.1). A sample is separable if and only if some $w$ satisfies $y_i\langle w, x_i\rangle \ge 1$ for all $i$.

Theorem 9.2. The VC-dimension of the homogenous halfspaces in $\mathbb{R}^d$ is $d$.

Theorem 9.3. The VC-dimension of the halfspaces in $\mathbb{R}^d$ is $d+1$.

Least Squares (9.6). The system $Aw = b$ always has a solution, and $w$ solves it if and only if $h_w$ is an ERM hypothesis for the squared loss over the homogenous linear predictors.

Further items: Exercise 9.3, the tightness of Theorem 9.1 (for every $m$ a sample with $R \le 1$, $(BR)^2 \le m$ and a run of exactly $m$ updates); the learnability of halfspaces by ERM, a consequence of Theorem 9.3 and the fundamental theorem; Exercise 9.2, $A$ is invertible iff the $x_i$ span $\mathbb{R}^d$; and the convexity of the logistic loss in $w$.

Significance

The Perceptron bound is one of the oldest results of learning theory (Novikoff 1962) and the model for every mistake bound in the online-learning chapters: it is independent of the dimension and of the number of examples, depending only on the geometry of the data through $R$ and $B$. Theorems 9.2 and 9.3 are the first VC-dimension computations of a class used in practice and give, through Theorem 6.8, the sample complexity $\Theta((d + \log(1/\delta))/\epsilon)$ of learning halfspaces. The normal equations are the algorithmic content of linear regression, and the convexity of the logistic loss is why logistic regression is tractable in the nonseparable case, where ERM for halfspaces with the 0–1 loss is hard.

Nothing here is machine-checked in this form. Mathlib has the inner-product geometry, the Cauchy–Schwarz inequality, linear algebra of finite-dimensional spaces and convexity of compositions, but neither the Perceptron nor the VC-dimension of halfspaces.

Difficulty

Equation (9.1) is a rescaling and the intended entry point. The convexity of the logistic loss is the composition of the convex function $\log(1 + e^{-t})$ with the linear map $w \mapsto y\langle w, x\rangle$. Exercise 9.2 is the identification of the kernel of $\sum_i \langle x_i, \cdot\rangle x_i$ with the orthogonal complement of the span. The normal equations require showing that a convex quadratic is minimized exactly where its gradient vanishes, and that $b$ lies in the range of $A$, which is the span of the $x_i$. Theorem 9.1 is the book's proof: by induction on the run, $\langle w^*, w^{(T)}\rangle \ge T$ and $\|w^{(T)}\|^2 \le TR^2$ for any feasible $w^*$, then Cauchy–Schwarz, and finally the passage from a feasible $w^*$ to the infimum $B$; the existence clause follows because a run can be extended as long as the stopping condition fails and all runs are bounded. Theorem 9.2 is the linear-dependence argument of the book, with a case analysis on the signs of the coefficients and on which side is nonempty, and the shattering of the standard basis; Theorem 9.3 lifts it to $\mathbb{R}^{d+1}$ by appending a constant coordinate. The learnability of halfspaces is Theorem 6.7 applied to a class that must be shown measurable, nonempty, of finite VC-dimension and pointwise separable; the last needs rational approximations $(w_n, b_n)$ in which the offset moves below $b$ more slowly than $w_n$ approaches $w$, so that boundary points keep their label.

Formalization scope

Halfspaces are Boolean predictors with $\operatorname{sign}(0)$ negative; the classes are sets of functions, so the VC-dimension is that of Mission IV. The Perceptron is a relation on sequences, not a program: this captures the algorithm's freedom to choose any mistaken example and makes the bound apply to all implementations. $B$ is an infimum, which is attained (the feasible set is closed and the norm is coercive), but the theorem does not need attainment. $R$ is a real supremum over the finite index set, equal to $0$ for the empty sample, where every run has length $0$. The Least Squares statement is about the homogenous class and the sample $i \mapsto (x_i, y_i)$, with ERM in the sense of Mission I; the bias term is handled by the book's reduction, appending a constant coordinate, and is not formalized separately. The learnability item states qualitative learnability and the ERM guarantee with an unspecified sample-complexity function; the quantitative rate is Theorem 6.8 of Mission IV. Linear programming (§9.1.1), the pseudo-inverse (§9.2.1), polynomial regression (§9.2.2), Exercises 9.1 and 9.4–9.6 are not stated.

Trivializing readings are excluded: labels are constrained to $\pm 1$, runs must start at $0$ and update only on mistakes, the VC equalities are in $\mathbb{N} \cup \{\infty\}$, and the ERM equivalence is a biconditional. Welcome contributions: the two Perceptron invariants as separate lemmas, the shattering of the standard basis, and the pointwise separability of halfspaces.

Selected references

• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 9. doi:10.1017/CBO9781107298019
• F. Rosenblatt, The perceptron: a probabilistic model for information storage and organization in the brain, Psychological Review 65(6), 1958. doi:10.1037/h0042519
• A. B. J. Novikoff, On convergence proofs on perceptrons, Proceedings of the Symposium on the Mathematical Theory of Automata 12, 1962.
• S. Agmon, The relaxation method for linear inequalities, Canadian Journal of Mathematics 6, 1954. doi:10.4153/CJM-1954-037-2
• S. Ben-David, H. U. Simon, Efficient learning of linear perceptrons, Advances in Neural Information Processing Systems 13, 2001.