Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Collections

Understanding Machine Learning

Shalev-Shwartz and Ben-David's Understanding Machine Learning: PAC learning, VC dimension, and the fundamental theorem of statistical learning.

23 missions

Missions

21–23 of 23
OpenCompletedAll
🏆Completed
CombinatoricsMachine LearningProbability·Captain: naimengye

Understanding Machine Learning XXIII: Multiclass LearnabilityTextbook

Motivation

Chapter 17 introduced multiclass prediction; Chapter 29 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019), asks the two questions the fundamental theorem answered for binary classes: which classes of multiclass predictors are PAC learnable with respect to the 0–1 loss, and with what sample complexity. Natarajan's dimension generalizes the VC dimension by shattering with two disagreeing label functions, and the multiclass fundamental theorem (Theorem 29.3) bounds the uniform-convergence, agnostic and realizable sample complexities in terms of it, up to logarithmic factors in the number of labels kkk; the only new ingredient in its proof is Natarajan's lemma, the multiclass substitute for Sauer's lemma. The chapter then computes or bounds the Natarajan dimension of the classes that matter, One-versus-All and general reductions to binary classifiers, and linear multiclass predictors (Theorem 29.7). Its last section is a warning: unlike the binary case, not all ERMs are equal, and with infinitely many labels a class can be learnable by one ERM and not by another, so learnability and uniform convergence come apart (Claim 29.9).

Setting

HHH is a class of functions from XXX to a finite label set YYY with ∣Y∣=k|Y| = k∣Y∣=k. C⊆XC \subseteq XC⊆X is shattered by HHH if there are f0,f1:C→Yf_0, f_1 : C \to Yf0​,f1​:C→Y with f0(x)≠f1(x)f_0(x) \ne f_1(x)f0​(x)=f1​(x) everywhere on CCC such that every B⊆CB \subseteq CB⊆C is realized by some h∈Hh \in Hh∈H agreeing with f0f_0f0​ on BBB and with f1f_1f1​ on C∖BC \setminus BC∖B (Definition 29.1); Ndim⁡(H)\operatorname{Ndim}(H)Ndim(H) is the largest size of a shattered set (Definition 29.2). One-versus-All builds T(hˉ)(x)=argmax⁡ihi(x)T(\bar h)(x) = \operatorname{argmax}_i h_i(x)T(hˉ)(x)=argmaxi​hi​(x) from kkk binary classifiers, the smaller label on ties; a general reduction applies a rule r:{0,1}l→[k]r : \{0,1\}^l \to [k]r:{0,1}l→[k] to lll binary classifiers; the linear class HΨH_\PsiHΨ​ predicts argmax⁡i⟨w,Ψ(x,i)⟩\operatorname{argmax}_i\langle w, \Psi(x, i)\rangleargmaxi​⟨w,Ψ(x,i)⟩ for a class-sensitive feature map Ψ:X×[k]→Rd\Psi : X \times [k] \to \mathbb{R}^dΨ:X×[k]→Rd (29.1). The class of §29.4 has labels Pf(X)∪{∗}P_f(X) \cup \{\ast\}Pf​(X)∪{∗}, the finite and cofinite subsets of XXX plus a special label, and hypotheses hA(x)=Ah_A(x) = AhA​(x)=A if x∈Ax \in Ax∈A and ∗\ast∗ otherwise; AgoodA_{good}Agood​ returns h∅h_\emptyseth∅​ on an all-∗\ast∗ sample and AbadA_{bad}Abad​ returns h{x1,…,xm}ch_{\{x_1, \dots, x_m\}^c}h{x1​,…,xm​}c​.

Formalization targets

Goal: Theorem 29.3

There are absolute constants C1,C2>0C_1, C_2 > 0C1​,C2​>0 such that every class H⊆YXH \subseteq Y^XH⊆YX with Ndim⁡(H)=d\operatorname{Ndim}(H) = dNdim(H)=d satisfies

C1d+log⁡(1/δ)ϵ2≤mHUC(ϵ,δ), mH(ϵ,δ)≤C2dlog⁡k+log⁡(1/δ)ϵ2,C1d+log⁡(1/δ)ϵ≤mHreal(ϵ,δ)≤C2dlog⁡(kd/ϵ)+log⁡(1/δ)ϵ,C_1\frac{d + \log(1/\delta)}{\epsilon^2} \le m^{UC}_H(\epsilon,\delta),\ m_H(\epsilon,\delta) \le C_2\frac{d\log k + \log(1/\delta)}{\epsilon^2}, \qquad C_1\frac{d + \log(1/\delta)}{\epsilon} \le m^{\mathrm{real}}_H(\epsilon,\delta) \le C_2\frac{d\log(kd/\epsilon) + \log(1/\delta)}{\epsilon},C1​ϵ2d+log(1/δ)​≤mHUC​(ϵ,δ), mH​(ϵ,δ)≤C2​ϵ2dlogk+log(1/δ)​,C1​ϵd+log(1/δ)​≤mHreal​(ϵ,δ)≤C2​ϵdlog(kd/ϵ)+log(1/δ)​,

the upper bounds by every ERM learner and the lower bounds for small ϵ,δ\epsilon, \deltaϵ,δ and d≥2d \ge 2d≥2, in the format of Mission IV's Theorem 6.8.

Milestones

Lemma 29.4 (Natarajan: ∣H∣≤∣X∣Ndim⁡(H)k2Ndim⁡(H)|H| \le |X|^{\operatorname{Ndim}(H)}k^{2\operatorname{Ndim}(H)}∣H∣≤∣X∣Ndim(H)k2Ndim(H)); Lemma 29.5 (the Natarajan dimension of One-versus-All is O(kdlog⁡(kd))O(kd\log(kd))O(kdlog(kd))); Theorem 29.7 (Ndim⁡(HΨ)≤d\operatorname{Ndim}(H_\Psi) \le dNdim(HΨ​)≤d); Claim 29.9(1) (AgoodA_{good}Agood​ needs 1ϵlog⁡1δ\frac1\epsilon\log\frac1\deltaϵ1​logδ1​ examples); Claim 29.9(2) (AbadA_{bad}Abad​ fails with constant probability on (∣X∣−1)/(6ϵ)(|X|-1)/(6\epsilon)(∣X∣−1)/(6ϵ) examples). Further items: the equality Ndim⁡=VCdim⁡\operatorname{Ndim} = \operatorname{VCdim}Ndim=VCdim for two classes, and Lemma 29.6 for general reductions.

Significance

Theorem 29.3 is the multiclass fundamental theorem of Natarajan (1989) and Ben-David, Cesa-Bianchi, Haussler and Long (1995): finite Natarajan dimension characterizes multiclass learnability, and the sample complexity is linear in it, with the dependence on kkk confined to logarithms. Natarajan's lemma is the combinatorial core, and the dimension bounds of §29.3 are what make the theorem usable: a One-versus-All scheme over a class of VC dimension ddd costs O~(kd)\tilde O(kd)O~(kd), and a linear multiclass predictor costs at most its number of parameters, so the multivector construction of Chapter 17 is learnable with O~(nk/ϵ2)\tilde O(nk/\epsilon^2)O~(nk/ϵ2) examples. Claim 29.9 is a genuine phenomenon of Daniely, Sabato, Ben-David and Shalev-Shwartz (2011): in multiclass classification the choice of ERM matters, and the equivalence "learnable iff uniform convergence" of the binary theory is false, which is why Conjecture 29.10 about good ERMs is open in the form the chapter states it.

Difficulty

The equality with the VC dimension for two labels is a direct comparison of the two shattering definitions. Natarajan's lemma is a Sauer-type induction on ∣X∣|X|∣X∣, in which a shattered set must be produced from two hypotheses that differ at a point; the exercise-level proof of the book becomes a careful double induction formally. Theorem 29.3's upper bounds follow the binary proof of Chapter 28 with Natarajan's lemma in place of Sauer's, hence Massart's lemma and Theorem 26.5 for the agnostic case and the double-sample argument for the realizable case; the lower bounds reduce to the binary ones by embedding a binary class into a multiclass one on a shattered set. These are long formal developments, and the theorem is stated with unspecified constants for that reason. Lemmas 29.5 and 29.6 are counting: a shattered CCC has 2∣C∣≤∣HC∣≤∣(Hbin)C∣k2^{|C|} \le |H_C| \le |(H_{bin})_C|^k2∣C∣≤∣HC​∣≤∣(Hbin​)C​∣k, Sauer's lemma bounds the right side by (∑i≤d(∣C∣i))k\big(\sum_{i \le d}\binom{|C|}{i}\big)^{k}(∑i≤d​(i∣C∣​))k, and the resulting inequality is solved. For Lemma 29.5's printed 3kdlog⁡(kd)3kd\log(kd)3kdlog(kd) this fails only at (k,d)=(2,1),(3,1)(k, d) = (2, 1), (3, 1)(k,d)=(2,1),(3,1). There a shattered set splits by the label pair {f0(x),f1(x)}\{f_0(x), f_1(x)\}{f0​(x),f1​(x)} into parts shattered by {B∖A:A,B∈Hbin}\{B \setminus A : A, B \in H_{bin}\}{B∖A:A,B∈Hbin​} (pairs {0,b}\{0, b\}{0,b}) or by HbinH_{bin}Hbin​ (other pairs). The first class has at most 313131 traces on 555 points. Theorem 29.7 maps a shattered set into Rd\mathbb{R}^dRd by ρ(x)=Ψ(x,f0(x))−Ψ(x,f1(x))\rho(x) = \Psi(x, f_0(x)) - \Psi(x, f_1(x))ρ(x)=Ψ(x,f0​(x))−Ψ(x,f1​(x)), up to sign, and shows the image is shattered by homogeneous halfspaces; the tie-breaking rule decides which sign and which halfspace convention to use. Claim 29.9(1) is the bound (1−ϵ)m≤δ(1-\epsilon)^m \le \delta(1−ϵ)m≤δ; Claim 29.9(2) needs only that at most (d−1)/2(d-1)/2(d−1)/2 of the d−1d-1d−1 light points appear in the sample, an event of probability at least 1/31/31/3 by Markov's inequality when m≤(d−1)/(6ϵ)m \le (d-1)/(6\epsilon)m≤(d−1)/(6ϵ), which exceeds the claimed e−1/6e^{-1}/6e−1/6.

Formalization scope

Labels are an arbitrary finite type, shattering and the Natarajan dimension are stated with witnesses f0,f1f_0, f_1f0​,f1​ defined on all of XXX, and the dimension is a supremum in N∪{∞}\mathbb{N} \cup \{\infty\}N∪{∞}. The multiclass 0–1 loss, the ERM property, agnostic PAC learnability and uniform convergence are Mission I's generic notions; the realizable multiclass PAC property is defined here in the shape of Definition 3.1 with D({h≠f})D(\{h \ne f\})D({h=f}) as the error, since Mission I's binary version is {0,1}\{0,1\}{0,1}-specific. Theorem 29.3 is stated exactly as Mission IV states Theorem 6.8, with existential constants, upper bounds for every ERM learner of a nonempty measurable class with the countable-approximation property (the measurability device of Remark 3.1), and lower bounds for ϵ<ϵ0\epsilon < \epsilon_0ϵ<ϵ0​, δ<δ0\delta < \delta_0δ<δ0​, d≥2d \ge 2d≥2. Argmax predictors, both One-versus-All and HΨH_\PsiHΨ​, break ties towards the smallest label; the book states this rule for One-versus-All, and some fixed rule is necessary for Theorem 29.7, since with arbitrary tie-breaking every function is an argmax predictor of the zero mapping. Lemmas 29.5 and 29.6 are stated per shattered set. Lemma 29.5 keeps the printed 3kdlog⁡(kd)3kd\log(kd)3kdlog(kd), which is true although the book's step ∣(Hbin)C∣≤∣C∣d|(H_{bin})_C| \le |C|^d∣(Hbin​)C​∣≤∣C∣d fails for small ∣C∣|C|∣C∣. Lemma 29.6 uses 2ldlog⁡2(2ld)2ld\log_2(2ld)2ldlog2​(2ld), which the counting supports, because the printed 3ldlog⁡(ld)3ld\log(ld)3ldlog(ld) is false at l=d=1l = d = 1l=d=1. Theorem 29.3's uniform-convergence upper bound is stated for d≥1d \ge 1d≥1. At d=0d = 0d=0 the confidence term log⁡(1/δ)\log(1/\delta)log(1/δ) vanishes as δ→1\delta \to 1δ→1, the bound reaches m=1m = 1m=1, and a single example is not representative. The class of §29.4 has labels Option of the subtype of finite-or-cofinite sets, with the discrete σ-algebra, and the two ERMs are predicates fixing the output on all-∗\ast∗ samples; Claim 29.9(1) is stated for countable XXX with measurable singletons and Claim 29.9(2) for finite XXX of size at least 222, with the proof's own distribution, h∅h_\emptyseth∅​ as target, and every ϵ∈(0,1/2)\epsilon \in (0, 1/2)ϵ∈(0,1/2) in place of the book's unspecified constant aaa.

Not stated: Corollary 29.8 (its lower bound (k−1)(n−1)(k-1)(n-1)(k−1)(n−1) is cited, not proved), Conjecture 29.10, the exercises.

Selected references

  • S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 29. doi:10.1017/CBO9781107298019
  • B. K. Natarajan, On learning sets and functions, Machine Learning 4, 1989. doi:10.1007/BF00114804
  • S. Ben-David, N. Cesa-Bianchi, D. Haussler, P. M. Long, Characterizations of learnability for classes of {0, …, n}-valued functions, Journal of Computer and System Sciences 50(1), 1995. doi:10.1006/jcss.1995.1008
  • D. Haussler, P. M. Long, A generalization of Sauer's lemma, Journal of Combinatorial Theory A 71(2), 1995. doi:10.1016/0097-3165(95)90001-2
  • A. Daniely, S. Sabato, S. Ben-David, S. Shalev-Shwartz, Multiclass learnability and the ERM principle, COLT 2011; Journal of Machine Learning Research 16, 2015.
  • A. Daniely, S. Sabato, S. Shalev-Shwartz, Multiclass learning approaches: a theoretical comparison with implications, NIPS 2012.
15 thms2 active usersReviewed
🏆Completed
CombinatoricsMachine LearningProbability·Captain: naimengye

Understanding Machine Learning XXIV: Compression BoundsTextbook

Motivation

The book has characterized learnability through uniform convergence and through stability; Chapter 30 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019), gives a third sufficient condition, compression: if a learning algorithm's output can be reconstructed from a small subsequence of kkk training examples, then the error on the remaining examples estimates the true error, and the algorithm generalizes with a bound of order klog⁡(m/δ)/mk\log(m/\delta)/mklog(m/δ)/m (Theorem 30.2, Littlestone and Warmuth). The bound is a union bound over the mkm^kmk possible index sequences of a held-out estimate that follows from Bernstein's inequality (Lemma 30.1), and in the consistent case it gives LD≤8klog⁡(m/δ)/mL_D \le 8k\log(m/\delta)/mLD​≤8klog(m/δ)/m (Corollary 30.3). Classes admitting such compression schemes include axis-aligned rectangles (k=2dk = 2dk=2d), homogeneous halfspaces (k=dk = dk=d, through the minimal-norm point of the convex hull and Carathéodory's theorem), separating polynomials by reduction, and any margin-separable data (k≤1/γ2k \le 1/\gamma^2k≤1/γ2, through the Perceptron). Whether every class of finite VC dimension has a compression scheme of size O(d)O(d)O(d) is Warmuth's problem, open when the book was written.

Setting

A sample S=(z1,…,zm)S = (z_1, \dots, z_m)S=(z1​,…,zm​) is drawn i.i.d. from DDD; a selection rule picks (i1,…,ik)∈[m]k(i_1, \dots, i_k) \in [m]^k(i1​,…,ik​)∈[m]k (repetitions allowed), a reconstruction map B:Zk→HB : Z^k \to HB:Zk→H produces A(S)=B(zi1,…,zik)A(S) = B(z_{i_1}, \dots, z_{i_k})A(S)=B(zi1​​,…,zik​​), and VVV is the set of positions not selected, with LVL_VLV​ the average loss over them. The loss takes values in [0,1][0,1][0,1]. A class HHH has a compression scheme of size kkk (Definition 30.4) if for every m≥1m \ge 1m≥1 there are such AAA and BBB with B(SA(S))B(S_{A(S)})B(SA(S)​) correct on every sample labeled by a member of HHH; the unrealizable version (Definition 30.5) asks B(SA(S))B(S_{A(S)})B(SA(S)​) to be an empirical risk minimizer on every sample.

Formalization targets

Goal: Theorem 30.2

For a [0,1][0,1][0,1]-valued loss, k≥1k \ge 1k≥1, m≥2km \ge 2km≥2k, any reconstruction map BBB and any selection rule, with probability at least 1−δ1 - \delta1−δ over S∼DmS \sim D^mS∼Dm,

LD(A(S))≤LV(A(S))+LV(A(S)) 4klog⁡(m/δ)m+8klog⁡(m/δ)m.L_D(A(S)) \le L_V(A(S)) + \sqrt{L_V(A(S))\,\frac{4k\log(m/\delta)}{m}} + \frac{8k\log(m/\delta)}{m}.LD​(A(S))≤LV​(A(S))+LV​(A(S))m4klog(m/δ)​​+m8klog(m/δ)​.

Milestones

Lemma 30.1 (the held-out Bernstein bound); Corollary 30.3 (the consistent case); Lemma 30.6 (realizable schemes give unrealizable schemes); the compression scheme of size 2d2d2d for axis-aligned rectangles (§30.2.1); the separation property of the minimal-norm point of the convex hull (§30.2.2). Further items: the size-ddd scheme for homogeneous halfspaces and the margin scheme of §30.2.4.

Significance

Compression bounds are the cleanest generalization argument in the book: no complexity measure of the class enters, only the number of examples needed to encode the output, and the resulting bound is data-dependent through LVL_VLV​. They explain why support vector machines and the Perceptron generalize in terms of the number of support vectors or updates, and they underlie the sample-compression view of learning that connects to Chapters 9 and 15. Lemma 30.6 shows that compression is robust to label noise in the binary case. The halfspace scheme is a small piece of convex geometry of independent interest, and Warmuth's question about VC classes, settled in the affirmative for finite size by Moran and Yehudayoff after the book appeared, remains open in the form O(d)O(d)O(d).

Difficulty

Lemma 30.1 is Bernstein's inequality for the nnn held-out losses with variance at most LD(hT)L_D(h_T)LD​(hT​), followed by solving the resulting quadratic in LD\sqrt{L_D}LD​​ to move the risk from the right-hand side to LVL_VLV​; the constant 444 comes out of that step (the exact value is about 3.193.193.19). Theorem 30.2 is a union bound over the mkm^kmk index sequences with δ′=mkδ\delta' = m^k\deltaδ′=mkδ, using ∣V∣≥m−k≥m/2|V| \ge m - k \ge m/2∣V∣≥m−k≥m/2 and log⁡(mk/δ′)≤klog⁡(m/δ′)\log(m^k/\delta') \le k\log(m/\delta')log(mk/δ′)≤klog(m/δ′), which needs k≥1k \ge 1k≥1; formally the event for the learner is contained in the union of the events of Lemma 30.1 for each fixed index sequence, so no measurability of the selection rule is needed. Corollary 30.3 is immediate. Lemma 30.6 applies the realizable scheme to the subsample on which an ERM hypothesis is correct. The rectangle scheme is bookkeeping about extremal coordinates. The halfspace scheme needs three facts: the minimal-norm point of the hull separates (a one-line perturbation argument), it lies on a face and hence is a convex combination of ddd sample points (Carathéodory's theorem, in Mathlib, applied to a face), and it is the minimal-norm point of the hull of those ddd points (uniqueness of the projection onto a convex set); the existence of the minimizer uses compactness of the hull. The margin scheme is the Perceptron convergence theorem of Mission VI applied to the batch algorithm, whose output is the sum of the updated examples.

Formalization scope

Samples are Fin m-indexed under Mission I's iidLaw, and probability statements bound the outer measure of the failure event. Lemma 30.1 splits a sample of size k+nk + nk+n into its first kkk and last nnn entries; Theorem 30.2 takes an arbitrary selection rule sel:Zm→[m]k\mathrm{sel} : Z^m \to [m]^ksel:Zm→[m]k and reconstruction map BBB, the held-out set being the positions not in the range of the selection, and requires k≥1k \ge 1k≥1 and m≥1m \ge 1m≥1 in addition to the book's m≥2km \ge 2km≥2k: for k=0k = 0k=0 the bound reads LD≤LVL_D \le L_VLD​≤LV​, which fails, and the book's derivation uses k≥1k \ge 1k≥1 in log⁡(mk/δ′)≤klog⁡(m/δ′)\log(m^k/\delta') \le k\log(m/\delta')log(mk/δ′)≤klog(m/δ′). Compression schemes are defined for every m≥1m \ge 1m≥1, since for m=0m = 0m=0 there is no index to select, with indices allowed to repeat as in [m]k[m]^k[m]k and with BBB's outputs in HHH; the unrealizable version uses Mission XXIII's multiclass 0–1 loss. The halfspace results are stated for strictly separable ±1\pm1±1-labeled samples, yi⟨w⋆,xi⟩>0y_i\langle w^\star, x_i\rangle > 0yi​⟨w⋆,xi​⟩>0, the book's "w.l.o.g. all labels positive" normalization; this avoids the boundary negatives that a realizable sample may contain under the sign⁡(0)\operatorname{sign}(0)sign(0) convention of Mission VI, and it is the setting in which the minimal-norm argument works. The scheme is stated as the existence of ddd indices whose signed examples have a minimal-norm hull point separating the whole sample, which is the content of AAA and BBB without fixing how ties among faces are broken. Rectangles are closed boxes. The margin scheme uses Theorem 9.1's normalization.

Not stated: §30.2.3 (polynomials, a reduction), the bibliographic remarks, and the intermediate Carathéodory step as a separate item.

Selected references

  • S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 30. doi:10.1017/CBO9781107298019
  • N. Littlestone, M. K. Warmuth, Relating data compression and learnability, technical report, University of California, Santa Cruz, 1986.
  • S. Floyd, M. K. Warmuth, Sample compression, learnability, and the Vapnik-Chervonenkis dimension, Machine Learning 21, 1995. doi:10.1007/BF00993593
  • S. Ben-David, A. Litman, Combinatorial variability of Vapnik-Chervonenkis classes with applications to sample compression schemes, Discrete Applied Mathematics 86, 1998. doi:10.1016/S0166-218X(98)00000-6
  • S. Moran, A. Yehudayoff, Sample compression schemes for VC classes, Journal of the ACM 63(3), 2016. doi:10.1145/2890490
10 thms2 active usersReviewed
🏆Completed
Machine LearningProbabilityStatistics·Captain: naimengye

Understanding Machine Learning XXV: PAC-BayesTextbook

Motivation

The MDL and Occam principles of Chapter 7 rank hypotheses by description length and pay for a hypothesis according to its rank. Chapter 31 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019), generalizes this to the PAC-Bayesian approach of McAllester: prior knowledge is a prior distribution PPP over the class, the learner outputs a posterior QQQ, read as the randomized predictor that draws h∼Qh \sim Qh∼Q, and the price of QQQ is its Kullback–Leibler divergence from PPP. The PAC-Bayes theorem (Theorem 31.1) says that with probability 1−δ1 - \delta1−δ, simultaneously for every posterior, the generalization loss exceeds the training loss by at most (D(Q∥P)+ln⁡(m/δ))/(2(m−1))\sqrt{(D(Q\|P) + \ln(m/\delta))/(2(m-1))}(D(Q∥P)+ln(m/δ))/(2(m−1))​. Its proof is a compact and elegant argument: Markov's inequality for an exponential moment, a change of measure from QQQ to PPP by Jensen's inequality, an exchange of expectations that is possible because the prior does not depend on the sample, and a moment bound for the deviation of a single hypothesis. The bound suggests the learning rule of Remark 31.1, minimize LS(Q)L_S(Q)LS​(Q) plus the divergence penalty, which is regularized risk minimization in disguise, and for a finite class with a uniform prior it recovers an Occam-type bound (Exercise 2).

Setting

HHH is a measurable space of hypotheses, ℓ:H×Z→[0,1]\ell : H \times Z \to [0,1]ℓ:H×Z→[0,1] a jointly measurable loss, DDD a distribution over ZZZ, and PPP a prior probability measure on HHH. For a posterior QQQ, ℓ(Q,z)=Eh∼Q[ℓ(h,z)]\ell(Q, z) = \mathbb{E}_{h \sim Q}[\ell(h, z)]ℓ(Q,z)=Eh∼Q​[ℓ(h,z)], LD(Q)=Eh∼Q[LD(h)]L_D(Q) = \mathbb{E}_{h \sim Q}[L_D(h)]LD​(Q)=Eh∼Q​[LD​(h)] and LS(Q)=Eh∼Q[LS(h)]L_S(Q) = \mathbb{E}_{h \sim Q}[L_S(h)]LS​(Q)=Eh∼Q​[LS​(h)], and D(Q∥P)=Eh∼Q[ln⁡(dQ/dP)]D(Q\|P) = \mathbb{E}_{h \sim Q}[\ln(dQ/dP)]D(Q∥P)=Eh∼Q​[ln(dQ/dP)] is the Kullback–Leibler divergence, a real number when Q≪PQ \ll PQ≪P and the log-density is QQQ-integrable.

Formalization targets

Goal: Theorem 31.1

For m≥2m \ge 2m≥2 and δ∈(0,1)\delta \in (0,1)δ∈(0,1), with probability at least 1−δ1 - \delta1−δ over S∼DmS \sim D^mS∼Dm, every probability measure Q≪PQ \ll PQ≪P with finite divergence satisfies

LD(Q)≤LS(Q)+D(Q∥P)+ln⁡(m/δ)2(m−1).L_D(Q) \le L_S(Q) + \sqrt{\frac{D(Q\|P) + \ln(m/\delta)}{2(m-1)}}.LD​(Q)≤LS​(Q)+2(m−1)D(Q∥P)+ln(m/δ)​​.

Milestones

The identity Ez∼D[ℓ(Q,z)]=LD(Q)\mathbb{E}_{z \sim D}[\ell(Q, z)] = L_D(Q)Ez∼D​[ℓ(Q,z)]=LD​(Q) (§31.1); the moment bound ES[e2(m−1)Δ(h)2]≤m\mathbb{E}_S[e^{2(m-1)\Delta(h)^2}] \le mES​[e2(m−1)Δ(h)2]≤m of the proof (p. 417); Exercise 2, the bound for a finite class with the uniform prior.

Significance

PAC-Bayes bounds are among the tightest generalization bounds known in practice, and the reason is visible in Theorem 31.1: the complexity term is not a property of the class but of the posterior actually chosen, measured against a prior, so a learner that stays close to its prior generalizes even in a huge class. The theorem is the ancestor of a large literature (Seeger, Langford, Catoni, Maurer) and of modern nonvacuous bounds for neural networks. Formally it is a pleasant target: the change-of-measure inequality Eh∼Q[f(h)]−D(Q∥P)≤ln⁡Eh∼P[ef(h)]\mathbb{E}_{h \sim Q}[f(h)] - D(Q\|P) \le \ln\mathbb{E}_{h \sim P}[e^{f(h)}]Eh∼Q​[f(h)]−D(Q∥P)≤lnEh∼P​[ef(h)] is the Donsker–Varadhan inequality, of independent value, and the moment bound is a sharp sub-Gaussian fact. On the platform, the mission introduces Gibbs risks and the Kullback–Leibler divergence between measures on a class, ending the book's series with its last learning principle.

Difficulty

The Gibbs risk identity is Fubini for a bounded jointly measurable function. The moment bound is the delicate step: the book derives it from Hoeffding's tail bound through Exercise 1, whose one-sided hypothesis is not enough (a constant negative variable satisfies it with an unbounded moment), and even the two-sided tail integrates only to 2m−12m - 12m−1; the claim ≤m\le m≤m is nevertheless true, for instance by writing eaΔ2=Eg[e2a gΔ]e^{a\Delta^2} = \mathbb{E}_g[e^{\sqrt{2a}\,g\Delta}]eaΔ2=Eg​[e2a​gΔ] for a standard Gaussian ggg and applying Hoeffding's lemma to the sample mean, which gives ES[e2(m−1)Δ2]≤(1−(m−1)/m)−1/2=m\mathbb{E}_S[e^{2(m-1)\Delta^2}] \le (1 - (m-1)/m)^{-1/2} = \sqrt mES​[e2(m−1)Δ2]≤(1−(m−1)/m)−1/2=m​. Theorem 31.1 then follows the book: Markov's inequality on ef(S)e^{f(S)}ef(S) with f(S)=sup⁡Q(2(m−1)Eh∼QΔ(h)2−D(Q∥P))f(S) = \sup_Q(2(m-1)\mathbb{E}_{h \sim Q}\Delta(h)^2 - D(Q\|P))f(S)=supQ​(2(m−1)Eh∼Q​Δ(h)2−D(Q∥P)), the change of measure (31.2) by Jensen's inequality for ln⁡\lnln applied to the density dQ/dPdQ/dPdQ/dP (the Donsker–Varadhan inequality, which needs Q≪PQ \ll PQ≪P and an integrable log-density), the exchange of expectations (31.4) by Fubini, the moment bound, and finally Jensen for x2x^2x2 in (31.6); formally the supremum over all posteriors is handled by proving the bound for each QQQ on the event {S:Eh∼P[e2(m−1)Δ(h)2]≤m/δ}\{S : \mathbb{E}_{h \sim P}[e^{2(m-1)\Delta(h)^2}] \le m/\delta\}{S:Eh∼P​[e2(m−1)Δ(h)2]≤m/δ}, whose complement has probability at most δ\deltaδ by Markov, which sidesteps any measurability question about fff. Exercise 2 is the theorem with Q=δhQ = \delta_hQ=δh​, for which D(Q∥P)=ln⁡∣H∣D(Q\|P) = \ln|H|D(Q∥P)=ln∣H∣.

Formalization scope

The class is an arbitrary measurable space, priors and posteriors are probability measures on it, and Q(h)/P(h)Q(h)/P(h)Q(h)/P(h) is Mathlib's Radon–Nikodym derivative; the divergence is a Bochner integral, so the theorem quantifies over posteriors Q≪PQ \ll PQ≪P whose log-density is QQQ-integrable, exactly the posteriors with a finite divergence, for which the bound has content, and no junk value can make a case false. Posteriors may depend on the sample: the statement bounds the outer measure of the set of samples for which some admissible QQQ violates the bound. The loss is jointly measurable so that h↦LD(h)h \mapsto L_D(h)h↦LD​(h) and (S,h)↦LS(h)(S, h) \mapsto L_S(h)(S,h)↦LS​(h) are measurable and the Gibbs risks are genuine integrals; m≥2m \ge 2m≥2 is forced by the denominator 2(m−1)2(m-1)2(m−1). The moment bound is stated as the claim the proof needs rather than as Exercise 1, whose printed hypothesis is insufficient; the item text records this. Exercise 2 is stated as a simultaneous bound over the finite class, the form in which the theorem delivers it.

Not stated: Remark 31.1 (a learning rule, not a theorem), Exercise 1 as printed, and the second part of Exercise 2.

Selected references

  • S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 31. doi:10.1017/CBO9781107298019
  • D. A. McAllester, Some PAC-Bayesian theorems, Machine Learning 37, 1999. doi:10.1023/A:1007618624809
  • D. A. McAllester, PAC-Bayesian stochastic model selection, Machine Learning 51, 2003. doi:10.1023/A:1021840411064
  • A. Maurer, A note on the PAC Bayesian theorem, arXiv:cs/0411099, 2004.
  • M. Seeger, PAC-Bayesian generalisation error bounds for Gaussian process classification, Journal of Machine Learning Research 3, 2002.
  • J. Langford, J. Shawe-Taylor, PAC-Bayes and margins, NIPS 2002.
6 thms4 active usersReviewed
Previous

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me