Machine Learning

Motivation

Two estimators dominate sparse high-dimensional regression, where the number $M$ of candidate regressors can far exceed the sample size $n$. The Lasso (Tibshirani, 1996) minimises a least-squares criterion plus an $\ell_1$ penalty. The Dantzig selector (Candès and Tao, 2007) minimises the $\ell_1$ norm of the coefficients subject to a bound on the correlation between the residual and the regressors, and is computed by a linear program. They were proposed independently and first analysed under different assumptions: sparsity oracle inequalities for the Lasso (Bunea, Tsybakov and Wegkamp, 2007) and $\ell_2$ bounds for the Dantzig selector under a uniform uncertainty principle (Candès and Tao, 2007). A practitioner choosing between them needs to know whether guarantees for one say anything about the other.

Bickel, Ritov and Tsybakov (arXiv:0801.1095; Ann. Statist. 37(4), 2009, doi:10.1214/08-AOS620) analyse both estimators in parallel under one assumption on the design, the restricted eigenvalue condition. Their main message is that, under sparsity, the two estimators "exhibit similar behavior" (p. 2). Section 5 makes this precise: the prediction losses of the two estimators are close. The result holds in a nonparametric model: the regression function need not be a combination of the regressors. This mission formalizes that comparison, Theorem 5.1 of the paper.

Setting

Let $f_1,\dots,f_M$ be real functions (the dictionary) on a set $\mathcal Z$, and $Z_1,\dots,Z_n\in\mathcal Z$ fixed design points, with $n\ge1$ and $M\ge2$. The design matrix is $X=(f_j(Z_i))\in\mathbb R^{n\times M}$. Observations are $Y_i=f(Z_i)+W_i$, where $f$ is an unknown function and $W_1,\dots,W_n$ are independent $\mathcal N(0,\sigma^2)$ with $\sigma>0$. Write $y=(Y_i)$, $\boldsymbol f=(f(Z_i))$ and $w=(W_i)$, so $y=\boldsymbol f+w$.

The empirical norm of $g$ is $\|g\|_n=(\tfrac1n\sum_i g(Z_i)^2)^{1/2}$. Every column has $\|f_j\|_n\neq0$, and $f_{\max}=\max_j\|f_j\|_n$. For $\beta\in\mathbb R^M$, $f_\beta=\sum_j\beta_jf_j$ has value vector $X\beta$. The support is $J(\beta)=\{j:\beta_j\ne0\}$ and the sparsity is $\mathcal M(\beta)=|J(\beta)|$. For $J\subseteq\{1,\dots,M\}$, $\delta_J$ agrees with $\delta$ on $J$ and vanishes elsewhere.

Fix $r>0$. The Lasso $\hat\beta_L$ is any minimiser of

$$\frac1n\sum_{i=1}^n\big(Y_i-f_\beta(Z_i)\big)^2+2r\sum_{j=1}^M\|f_j\|_n|\beta_j| .$$

With $D=\mathrm{diag}(\|f_1\|_n^2,\dots,\|f_M\|_n^2)$, the Dantzig constraint is $|\tfrac1nD^{-1/2}X^\top(y-X\beta)|_\infty\le r$. The Dantzig selector $\hat\beta_D$ is any vector of smallest $|\beta|_1=\sum_j|\beta_j|$ that satisfies it. The estimators are $\hat f_L=f_{\hat\beta_L}$ and $\hat f_D=f_{\hat\beta_D}$.

Assumption RE$(s,c_0)$ with $1\le s\le M$, $c_0>0$ asks that

$$\kappa(s,c_0)=\min_{|J_0|\le s}\ \min_{\delta\ne0,\ |\delta_{J_0^c}|_1\le c_0|\delta_{J_0}|_1}\ \frac{|X\delta|_2}{\sqrt n\,|\delta_{J_0}|_2}>0 .$$

Throughout, $r=A\sigma\sqrt{\log M/n}$, where $\log$ is the natural logarithm.

Formalization targets

Goal: Theorem 5.1

Assume RE$(s,1)$ with $1\le s\le M$, and let $A>2\sqrt2$. With probability at least $1-M^{1-A^2/8}$, every Lasso solution with $\mathcal M(\hat\beta_L)\le s$ and every Dantzig selector satisfy

$$\Big|\,\|\hat f_D-f\|_n^2-\|\hat f_L-f\|_n^2\,\Big|\le16A^2\,\frac{\mathcal M(\hat\beta_L)\sigma^2}{n}\,\frac{f_{\max}^2}{\kappa^2(s,1)}\,\log M .$$

Milestones

The proof uses one probabilistic event and two one-sided deterministic inequalities.

1. The Lasso satisfies the Dantzig constraint (2.3).
2. The noise event $\mathcal A=\bigcap_j\{2|\tfrac1n\sum_iX_{ij}W_i|\le r\|f_j\|_n\}$ has $\mathbb P(\mathcal A^c)\le M^{1-A^2/8}$ (B.4).
3. On $\mathcal A$, $|\tfrac1nX^\top(\boldsymbol f-X\hat\beta_L)|_\infty\le 3rf_{\max}/2$ (Lemma B.1, (B.2)).
4. The Dantzig error lies in the cone $|\delta_{J_0^c}|_1\le|\delta_{J_0}|_1$ (Lemma B.3, (B.9)).
5. On the larger event $\mathcal B\supseteq\mathcal A$, $|\tfrac1nX^\top(\boldsymbol f-X\hat\beta_D)|_\infty\le 2rf_{\max}$ (Lemma B.3, (B.10)).
6. $\|\hat f_D-f\|_n^2\le\|\hat f_L-f\|_n^2+16f_{\max}^2r^2\mathcal M(\hat\beta_L)/\kappa^2$ on $\mathcal B$ (B.15).
7. $\|\hat f_L-f\|_n^2\le\|\hat f_D-f\|_n^2+9f_{\max}^2r^2\mathcal M(\hat\beta_L)/\kappa^2$ on $\mathcal A$ (B.17).

Further result: Theorem 5.2

Assume $\|f_j\|_n=1$ for all $j$ and RE$(s,5)$. With probability at least $1-M^{1-A^2/8}$, whenever $\mathcal M(\hat\beta_D)\le s$,

$$\|\hat f_L-f\|_n^2\le10\|\hat f_D-f\|_n^2+81A^2\,\frac{\mathcal M(\hat\beta_D)\sigma^2}{n}\,\frac{\log M}{\kappa^2(s,5)} .$$

Significance

The result. Theorem 5.1 bounds the gap between the two prediction losses by the rate $\mathcal M(\hat\beta_L)\sigma^2\log M/n$ of a sparse regression with $\mathcal M(\hat\beta_L)$ parameters. The bound carries a factor $f^2_{\max}/\kappa^2(s,1)$ that measures how ill-conditioned the Gram matrix is on sparse vectors. A prediction bound for one estimator therefore transfers to the other at this cost. The paper uses this transfer in Proposition 6.3, which combines Theorem 5.1 with the Lasso oracle inequality of Section 6 to derive an oracle inequality for the Dantzig selector. The theorem requires no assumption relating $f$ to the dictionary.

Formalizing it. The result has been proved since 2009, and this mission formalizes that proof. None of the objects involved exists on Prove2Me yet: the weighted Lasso, the Dantzig selector and the Gaussian noise events. The Wainwright series on the platform defines a differently normalised Lasso with an unweighted penalty, a single fixed support and a different restricted eigenvalue condition, so it cannot be reused here. A machine-checked proof would also confirm the paper's constants, $16A^2$ and the thresholds $2\sqrt2$ and $M^{1-A^2/8}$, which appear in all later analyses.

Difficulty

Each estimator is defined only implicitly, as the solution of an optimisation problem, and neither need be unique. Comparing their losses directly gives $\pm\tfrac2n\delta^\top X^\top(\boldsymbol f-X\hat\beta)$ plus $\tfrac1n|X\delta|_2^2$ with $\delta=\hat\beta_L-\hat\beta_D$. A crude bound on the cross term, $|\delta|_1\cdot|X^\top(\cdot)|_\infty$, yields an error proportional to $|\delta|_1$. This does not produce the sparse rate unless $|\delta|_1$ is controlled by $|X\delta|_2$. That control needs $\delta$ to lie in the restricted eigenvalue cone at the support of the random, data-dependent vector $\hat\beta_L$. The restricted eigenvalue condition must therefore hold uniformly over supports of size at most $s$; a condition for one fixed support does not suffice. The probabilistic part is a union bound over $M$ Gaussian coordinates, and it must be arranged so that a single event serves every minimiser of both programs.

Formalization scope

The dictionary and the design points enter every statement only through $X$ and $\boldsymbol f$, so the Lean statements take X : Matrix (Fin n) (Fin M) ℝ and f : Fin n → ℝ directly, and $f$ is arbitrary. The noise is a family W : Fin n → Ω → ℝ of measurable, mutually independent random variables with law gaussianReal 0 σ², and $y=f+W(\omega)$. The Lasso and the Dantzig selector are predicates (IsLasso, IsDantzig), and every theorem is stated for every solution. The Dantzig constraint is written coordinatewise as $|\tfrac1n\sum_iX_{ij}(y_i-(X\beta)_i)|\le r\|f_j\|_n$. The Lasso penalty and the Dantzig constraint are weighted by $\|f_j\|_n$, and the Dantzig objective $|\beta|_1$ is unweighted, exactly as in the paper. Theorem 5.1 does not normalise the columns.

RE$(s,c_0)$ is stated through a witness: a real $\kappa>0$ with $\kappa\sqrt n|\delta_{J_0}|_2\le|X\delta|_2$ on the cone, for all $|J_0|\le s$. The paper's $\kappa(s,c_0)$ is attained, so it is the largest witness. Every bound decreases in $\kappa$, so this reading is equivalent to the paper's and avoids a real infimum over an empty set. "With probability at least $p$" becomes the existence of a measurable event $E$ with $\mathbb P(E)\ge p$ on which the conclusion holds for every Lasso solution and every Dantzig selector. The condition $\mathcal M(\hat\beta_L)\le s$ is imposed inside the event, per realisation. The milestones (B.2), (B.10), (B.15) and (B.17) are stated deterministically, on the noise events $\mathcal A$ and $\mathcal B$ as predicates on the noise vector; this is how the proof uses them. (B.4) is stated for every $A>0$, which is stronger than the paper's $A>2\sqrt2$ and still true.

The goal cannot be made vacuous. For $A>2\sqrt2$ the probability bound $1-M^{1-A^2/8}$ is positive. Lasso solutions exist because $r>0$ and every $\|f_j\|_n>0$, and Dantzig selectors exist because the Lasso is feasible. RE$(s,1)$ with $\kappa=1$ holds for $X=\sqrt n\,I$.

A complete development needs:

• subgradient optimality for the weighted Lasso;
• a Gaussian tail bound $\mathbb P(|\eta|\ge t)\le e^{-t^2/2}$ together with the law of a weighted sum of independent Gaussians;
• Cauchy–Schwarz on supports;
• the quadratic bound $bx-x^2\le b^2/4$.

The noise-event lemmas and the Lasso optimality condition can be reused by the companion missions on this paper. Proofs of any milestone are welcome, including proofs that route (B.4) through Mathlib's sub-Gaussian API.

Selected references

• P. J. Bickel, Y. Ritov, A. B. Tsybakov, Simultaneous analysis of Lasso and Dantzig selector, Ann. Statist. 37(4), 1705–1732, 2009. arXiv:0801.1095v3: https://arxiv.org/abs/0801.1095 ; doi:10.1214/08-AOS620
• E. Candès, T. Tao, The Dantzig selector: statistical estimation when p is much larger than n, Ann. Statist. 35(6), 2313–2351, 2007. https://doi.org/10.1214/009053606000001523
• R. Tibshirani, Regression shrinkage and selection via the lasso, J. R. Stat. Soc. B 58(1), 267–288, 1996. https://doi.org/10.1111/j.2517-6161.1996.tb02080.x
• F. Bunea, A. B. Tsybakov, M. H. Wegkamp, Sparsity oracle inequalities for the Lasso, Electron. J. Stat. 1, 169–194, 2007. https://doi.org/10.1214/07-EJS008

Motivation

In stochastic linear optimization under bandit feedback a learner repeatedly chooses a decision $x_t$ from a fixed set $D\subseteq\mathbb R^n$ and observes only the noisy cost of that one decision, whose expectation is a fixed but unknown linear function $\mu^\top x_t$. The model covers online routing, ad and product selection with feature vectors, and any sequential decision problem whose decision set is too large to enumerate but whose expected cost is linear in a known representation. The multi-armed bandit is the special case where $D$ is the set of standard basis vectors.

Dani, Hayes and Kakade (COLT 2008) analysed the algorithm ConfidenceBall₂, a generalization of Auer's LinRel (JMLR 2002), and proved that its regret is $O^*(n\sqrt T)$ with high probability for an arbitrary compact decision set, and that this is optimal up to logarithmic factors. Their confidence-ellipsoid construction became the template for later linear bandit algorithms (OFUL, LinUCB), and the ellipsoid-plus-potential analysis is the standard argument of the field (Lattimore and Szepesvári, Bandit Algorithms, Chapters 19–20).

Timeline: Auer (2002) introduced LinRel for finite decision sets; Dani, Hayes and Kakade (2008) extended it to arbitrary compact sets with the $O^*(n\sqrt T)$ bound and a matching $\Omega(n\sqrt T)$ lower bound; Rusmevichientong and Tsitsiklis (Math. Oper. Res. 2010) studied linearly parameterized bandits with dimension-dependent regret bounds; Abbasi-Yadkori, Pál and Szepesvári (NeurIPS 2011) sharpened the confidence ellipsoids with self-normalized martingale bounds.

Setting

Fix $n\ge1$ and a compact decision set $D\subseteq\mathbb R^n$ whose standard basis $e_1,\dots,e_n$ is a barycentric spanner: each $e_i\in D$ and every $x\in D$ lies in the cube $[-1,1]^n$. The paper's Section 5 adopts these coordinates without loss of generality. An unknown vector $\mu\in\mathbb R^n$ satisfies $|\mu^\top x|\le1$ for $x\in D$, and $x^*\in D$ minimises $\mu^\top x$.

On round $t=1,2,\dots$ the learner plays $x_t\in D$, measurable with respect to the information $\mathcal F_t$ before round $t$, and observes a loss $\ell_t\in[-1,1]$ with $\mathbb E[\ell_t\mid\mathcal F_t]=\mu^\top x_t$. The regret after $T$ rounds is

$$R_T=\sum_{t=1}^T\big(\mu^\top x_t-\mu^\top x^*\big).$$

ConfidenceBall₂$(D,\delta)$ maintains the design matrix $A_t=I+\sum_{\tau<t}x_\tau x_\tau^\top$, the least-squares estimate $\hat\mu_t=A_t^{-1}\sum_{\tau<t}\ell_\tau x_\tau$, the radius

$$\beta_t=\max\Big(128\,n\ln t\ln(t^2/\delta),\ \big(\tfrac83\ln(t^2/\delta)\big)^2\Big),$$

and the confidence ellipsoid $B^2_t=\{\nu:(\nu-\hat\mu_t)^\top A_t(\nu-\hat\mu_t)\le\beta_t\}$. It plays the optimistic decision $x_t\in\operatorname{argmin}_{x\in D}\min_{\nu\in B^2_t}\nu^\top x$. The analysis uses the width $w_t=\sqrt{x_t^\top A_t^{-1}x_t}$, the error $Z_t=(\hat\mu_t-\mu)^\top A_t(\hat\mu_t-\mu)$, and the noise $\eta_t=\ell_t-\mu^\top x_t$.

Formalization targets

Goal: Theorem 2, ConfidenceBall₂ bullet (corrected)

For $0<\delta<1$ with $n\le\beta_1$ and noise $|\eta_t|\le1$,

$$\Pr\Big(\forall T\ge1,\ R_T\le\sqrt{8nT\beta_T\ln(T+1)}\Big)\ge1-\delta.$$

A single event covers every horizon, so the bound is anytime.

Milestones

• Lemma 8. If $\mu\in B^2_t$ then $r_t\le2\min(\sqrt{\beta_t}w_t,1)$.
• Lemma 10. $\det A_{t+1}=\prod_{\tau=1}^t(1+w_\tau^2)$.
• Lemma 9 (corrected). $\sum_{\tau=1}^t\min(w_\tau^2,1)\le2n\ln(t+1)$.
• Theorem 6 (corrected). If $\mu\in B^2_t$ for all $t\le T$, then $\sum_{t\le T}r_t^2\le8n\beta_T\ln(T+1)$.
• Theorem 4 (Freedman). $\Pr(\sum X_i\ge a,\ V\le v)\le\exp(-a^2/(2v+2ab/3))$ for martingale differences bounded above by $b$.
• Lemma 12. $Z_t\le n+2\sum_{\tau<t}\eta_\tau\frac{x_\tau^\top(\hat\mu_\tau-\mu)}{1+w_\tau^2}+\sum_{\tau<t}\eta_\tau^2\frac{w_\tau^2}{1+w_\tau^2}$.
• Lemma 14. $\Pr(\forall t,\ \sum_{\tau<t}M_\tau\le\beta_t/2)\ge1-\delta$.
• Theorem 5 (Confidence). $\Pr(\forall t,\ \mu\in B^2_t)\ge1-\delta$.

Significance

The result gives a regret bound for linear bandits over an arbitrary compact decision set that depends on the dimension $n$ rather than on $|D|$, holds uniformly over horizons, and requires no gap between the best and second-best decision. With the paper's lower bound it shows that the price of bandit feedback, compared with full information, is a factor $\Theta^*(\sqrt n)$. The two components, a confidence theorem for a least-squares ellipsoid under martingale noise and a deterministic potential argument on $\log\det A_t$, are reused in the analysis of most optimistic linear and generalized-linear bandit algorithms.

The theorem has a published proof but, to our knowledge, no machine-checked one. The platform already has the elliptical potential lemma (BanditAlgorithm.elliptical_potential_lemma, Lattimore–Szepesvári Lemma 19.4), the matrix determinant lemma and the Woodbury identity, which cover the linear-algebra layer; the LinUCB regret theorem there (BanditAlgorithm.linear_bandit_linucb_regret_bound) is pathwise given confidence, for a different algorithm, so the probabilistic half is new. Formalization also settles the printed constants, three of which need correction (below).

Difficulty

The deterministic half is linear algebra. The difficulty is the confidence theorem. Hoeffding–Azuma applied to $\sum_\tau M_\tau$ would need a deterministic step bound, and the natural one gives only a $T^{3/4}$ regret. The step sizes of $M_t$ are bounded in terms of the random widths $w_t$, so the argument must control the conditional variances pathwise and apply Freedman's inequality, whose event $\{V\le v\}$ is random. The escape indicator $E_t$, which switches the martingale off after the first failure of confidence, is what makes the variance bound hold on every path, and the induction that turns Lemma 14 into Theorem 5 must be carried out on a single event for all $t$ simultaneously. Freedman's inequality itself is not in Mathlib.

Formalization scope

Vectors are Fin n → ℝ, matrices Matrix (Fin n) (Fin n) ℝ, rounds are indexed $t=1,2,\dots$ in ℕ. The spanner is the standard basis, as in Section 5 of the paper (the algorithm is equivariant under the linear change of coordinates). The probability model is a probability space with a general filtration $(\mathcal F_t)$; $x_t$ is $\mathcal F_t$-measurable and $\ell_t$ is $\mathcal F_{t+1}$-measurable. The argmin is encoded as a joint minimiser over $D\times B^2_t$, which admits every tie-break and is required on every outcome; measurability of $x_t$ is a hypothesis, not derived from the selection. The optimum $x^*$ is a hypothesis ($x^*\in D$, minimising), not an sInf.

Corrections of the printed statements, each labelled in the item's Formalization Note:

1. $\ln(T+1)$ for $\ln T$ in Lemma 9, Theorem 6 and Theorem 2. The printed bounds are false at $T=1$ (with $n=1$, $D=[-1,1]$, $\mu>0$, the tie-break $x_1=1$ gives $R_1=2\mu>0$ against a bound of $0$); the proof of Lemma 9 gives $2\ln\det A_{t+1}\le2n\ln(t+1)$.
2. $n\le\beta_1=(\tfrac83\ln(1/\delta))^2$ is added to Theorems 5 and 2: the proof of Theorem 5 claims $Z_1\le n<\beta_1$, which fails for $\delta$ near $1$. Theorem 6 takes the proof's "$1<\beta_1$" as the hypothesis $\beta_1\ge1$.
3. $|\ell_t-\mu^\top x_t|\le1$ is added to Lemma 14, Theorems 5 and 2: Section 5.2 uses $|\eta_t|\le1$, while the model gives only $|\eta_t|\le2$. It holds when costs lie in $[0,1]$.
4. Theorem 5's "$\delta>0$" is stated with $0<\delta<1$; Lemma 10's index typo ($w_t$ for $w_\tau$) and Theorem 4's $\sum_{i=1}^n$ (for $T$) are corrected.

A regret bound for an arbitrary decision sequence under the assumption $\mu\in B^2_t$ for all $t$ is Theorem 6, not the goal; the goal carries the ConfidenceBall₂ selection rule, the conditional-mean and measurability hypotheses, and $\delta$ as the algorithm's own parameter. The hypotheses are jointly satisfiable, for example by a finite $D$ with a fixed tie-break and i.i.d. costs in $[0,1]$.

Needed infrastructure: Freedman's inequality for a filtration (reusable across all of bandit theory), the potential lemma (available), and measurability of the algorithm's statistics. Contributions of alternative proofs of Theorem 5, for example via self-normalized bounds, are welcome.

Selected references

• V. Dani, T. P. Hayes, S. M. Kakade, Stochastic Linear Optimization under Bandit Feedback, COLT 2008. http://colt2008.cs.helsinki.fi/papers/80-Dani.pdf
• P. Auer, Using Confidence Bounds for Exploitation-Exploration Trade-offs, JMLR 3, 2002. https://www.jmlr.org/papers/v3/auer02a.html
• D. A. Freedman, On Tail Probabilities for Martingales, Annals of Probability 3(1), 1975. https://doi.org/10.1214/aop/1176996452
• B. Awerbuch, R. Kleinberg, Adaptive Routing with End-to-End Feedback, STOC 2004. https://doi.org/10.1145/1007352.1007367
• P. Rusmevichientong, J. N. Tsitsiklis, Linearly Parameterized Bandits, Mathematics of Operations Research 35(2), 2010. https://doi.org/10.1287/moor.1100.0446
• Y. Abbasi-Yadkori, D. Pál, Cs. Szepesvári, Improved Algorithms for Linear Stochastic Bandits, NeurIPS 2011. https://arxiv.org/abs/1102.2670
• T. Lattimore, Cs. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020. https://doi.org/10.1017/9781108571401

Motivation

Matrix completion asks to recover a matrix from a small random subset of its entries. It models collaborative filtering (a ratings table with most entries missing), sensor-network localisation from partial distance data, and system identification. With no structure the task is hopeless, so one assumes the matrix has low rank $r$ and that its information is not concentrated in a few entries (incoherence).

Candès and Recht (Found. Comput. Math., 2009) showed that nuclear-norm minimisation recovers such a matrix from about $n^{6/5} r\log n$ random entries. Candès and Tao (IEEE Trans. Inf. Theory, 2010) lowered this to $n r\,\mathrm{polylog}(n)$. The same paper also asks how few entries any method could possibly use, and answers it with a lower bound, Theorem 1.7: below about $\mu_0 n r\log n$ observed entries, no algorithm can succeed. This mission formalizes that lower bound. The two upper bounds of the same paper are separate missions of this series.

Setting

Work with real $n\times n$ matrices. For a matrix $M$, let $U \subseteq \mathbb{R}^n$ be its column space and $V\subseteq \mathbb{R}^n$ its row space, and let $P_U$, $P_V$ be the orthogonal projections onto them. Let $e_a$ be the $a$-th standard basis vector.

Fix an integer $r$ and a real $\mu_0$. A matrix $M$ has rank at most $r$ and obeys the incoherence property with parameter $\mu_0$ (the paper's (I.18)) if $\operatorname{rank}M \le r$ and

$$\|P_U e_a\|^2 \le \frac{\mu_0 r}{n},\qquad \|P_V e_b\|^2 \le \frac{\mu_0 r}{n}\qquad\text{for all } a,b\in[n].$$

Since $\sum_a \|P_U e_a\|^2 = \dim U$, a matrix of rank exactly $r$ can satisfy this only when $\mu_0\ge 1$; the smallest possible value $\mu_0 = 1$ means the column and row spaces are spread evenly over the coordinates.

Bernoulli sampling. Fix $m \ge 1$ and set $p = m/n^2$. The observed set $\Omega\subseteq[n]\times[n]$ contains each entry independently with probability $p$, so $m$ is the expected number of observed entries. The sampling operator $\mathcal{P}_\Omega$ keeps the entries of a matrix that lie in $\Omega$ and sets the others to $0$. A recovery method sees only $\mathcal{P}_\Omega(M)$.

The sampling conditions are, with the natural logarithm,

$$m \ge n^2\left(1 - e^{-\frac{\mu_0 r}{n}\log\left(\frac{n}{2\delta}\right)}\right) \qquad \text{(I.20)}$$ $$m \ge (1-\epsilon)\,\mu_0 n r\log\left(\frac{n}{2\delta}\right),\qquad \epsilon := \frac12\frac{\mu_0 r}{n}\log\left(\frac{n}{2\delta}\right). \qquad \text{(I.21)}$$

Formalization targets

Goal: Theorem 1.7 (p. 2058)

Fix $1 \le m$, $1 \le r \le n$, $\mu_0\ge 1$ and $0<\delta<1/2$, with $\ell := n/(\mu_0 r)$ an integer. If (I.20) fails, or (I.21) fails, then

$$\mathbb{P}_\Omega\Bigl(\text{there are infinitely many pairs } M\ne M' \text{ of rank} \le r, \text{ incoherent with parameter } \mu_0, \text{ with } \mathcal{P}_\Omega(M)=\mathcal{P}_\Omega(M')\Bigr) \ \ge\ \delta .$$

On that event, the observations cannot tell $M$ from $M'$, so no method can recover every such matrix with probability greater than $1-\delta$. The statement fixes no constant beyond those the paper prints.

Milestones (Section II)

1. For pairwise disjoint sets of entries $S_1,\dots,S_n$ of size $\ell$, $\mathbb{P}(\text{every } S_a \text{ is sampled}) = (1-(1-p)^\ell)^n$.
2. For $n\ge1$, $\pi\in[0,1]$ and $0<\delta<1/2$: $(1-\pi)^n \ge 1-\delta$ implies $\pi \le 2\delta/n$.
3. With $p = m/n^2$ and the theorem's parameters: $(1-p)^\ell \le 2\delta/n$ implies (I.20).
4. $1-e^{-x} > x - x^2/2$ for every $x>0$ (the paper prints $x\ge0$; see Formalization scope).
5. The second part of Theorem 1.7: for the theorem's parameters, (I.20) implies (I.21).

Significance

The result. Theorem 1.7 shows that the sample complexity $n r\,\mathrm{polylog}(n)$ of the paper's upper bounds is close to optimal: about $\mu_0 n r\log n$ entries are necessary, however the matrix is reconstructed. The count exceeds the $2nr - r^2$ degrees of freedom of a rank-$r$ matrix by the factor $\mu_0\log n$. The logarithm is a coupon-collector effect: every row has to be sampled. The factor $\mu_0$ shows that the oversampling grows in proportion to the coherence. The bound is information-theoretic, and it holds even when the rank bound and the coherence are known in advance.

Formalizing it. The theorem and its proof in Section II are published. No machine-checked version is known to exist, and the platform has no lower bound for matrix completion. A formal proof would also check the printed argument, whose steps are compressed. It would yield reusable pieces: a Lean predicate for incoherence of matrices of bounded rank built on Mathlib's orthogonal projections, the independence computation for Bernoulli sampling over disjoint entry sets, and the elementary estimates that turn a success probability into a sampling rate.

Difficulty

The probabilistic and analytic parts are elementary. The difficulty is in building the hard instances as matrices and certifying them. For each observation set one has to exhibit, on an event of probability at least $\delta$, an infinite family of distinct pairs that agree on $\Omega$. Every member must have rank at most $r$ and meet both incoherence bounds, measured through projections onto its column and row spaces, and the pairs must stay distinct across the family. The paper describes the instances only informally. They have to be pinned down so that whatever distinguishes $M$ from $M'$ is really invisible on $\Omega$, while the incoherence bounds still hold for every admissible $\mu_0\ge1$ and $r\le n$. Computing the column space and the projection norms of an explicit matrix in Lean is the main infrastructure cost.

Formalization scope

Matrices are Matrix (Fin n) (Fin n) ℝ (the platform's MatrixCompletion.RealMatrix n n). The observation model is the platform's bernoulliEventProb with rate $m/n^2$, the sum over all $\Omega$ of $p^{|\Omega|}(1-p)^{n^2-|\Omega|}$. The sampling operator is the platform's samplingProjection. Logarithms and exponentials are Real.log, Real.exp. The mission's own definitions are IncoherentRankAtMost r μ₀ M (rank at most $r$, with the projection bounds computed from Mathlib's Submodule.starProjection onto the ranges of $M$ and $M^\top$ in EuclideanSpace ℝ (Fin n)) and SamplingConditionI20, SamplingConditionI21.

The formalization commits to four readings:

• Order of quantifiers. The event is "the set of bad pairs is infinite", evaluated for each $\Omega$, so the pairs may depend on $\Omega$. This is what Section II establishes and what the sentence after the theorem uses. The reading "fixed $M\ne M'$ with $\mathbb{P}(\mathcal{P}_\Omega(M) = \mathcal{P}_\Omega(M'))\ge\delta$" is a different statement and is not the goal.
• Integrality of $\ell$. The hypothesis that $\ell = n/(\mu_0 r)$ is an integer is the paper's own "without loss of generality" of Section II, and it is stated explicitly. It forces $\mu_0 r \le n$.
• "Fix $1\le m, r\le n$" is read as $1\le m$ and $1\le r\le n$. No upper bound on $m$ is imposed, since the failure of (I.20) already gives $m<n^2$.
• Standing assumptions. Section I-H assumes $m\ge 2nr$ and $n$ larger than an absolute constant for the rest of the paper. Those assumptions serve the upper bounds. Theorem 1.7 lists its own ranges, and only those are imposed.

The hypothesis "(I.20) fails or (I.21) fails" covers both parts of the theorem. The last sentence of Section II proves the second part from $1 - e^{-x} > x - x^2/2$, which the paper states "whenever $x \ge 0$". At $x=0$ the two sides are equal, so the strict inequality is false there; milestone 4 states the corrected range $x>0$, which is all the paper uses, since its $x = \frac{\mu_0 r}{n}\log\frac{n}{2\delta}$ is positive.

Trivializing formalizations are ruled out. The set of pairs requires $M\ne M'$, so the diagonal pairs $(M,M)$ do not count. "Infinitely many" is Set.Infinite of a set of pairs, not "at least one". Incoherence uses the theorem's $r$ and the actual column and row spaces, so the class is the paper's. The hypotheses are satisfiable, for example $n=4$, $r=1$, $\mu_0=1$, $\ell=4$, $\delta=0.1$, $m=1$.

Contributions are welcome on every milestone. The Bernoulli independence computation and the incoherence predicate can be reused in the other two missions of this series and in any lower bound for sampling problems.

Selected references

• E. J. Candès and T. Tao, The Power of Convex Relaxation: Near-Optimal Matrix Completion, IEEE Transactions on Information Theory 56(5):2053–2080, 2010. https://doi.org/10.1109/TIT.2010.2044061
• E. J. Candès and B. Recht, Exact Matrix Completion via Convex Optimization, Foundations of Computational Mathematics 9(6):717–772, 2009. https://doi.org/10.1007/s10208-009-9045-5

Motivation

In the predict-then-optimize paradigm a model first predicts the cost vector of a linear optimization problem from contextual features, and the prediction is then fed to an optimization solver that returns a decision. Examples include routing with predicted travel times and portfolio choice with predicted returns. The quality of a prediction is judged by the decision it produces. The Smart Predict-then-Optimize (SPO) loss of Elmachtoub and Grigas (Management Science 2022) measures exactly that: the excess cost of acting on the prediction instead of on the true cost vector.

El Balghiti, Elmachtoub, Grigas and Tewari (arXiv:1905.11488v3) ask when a model with small empirical SPO loss also has small expected SPO loss. The SPO loss is non-convex and discontinuous, so standard Lipschitz-contraction arguments do not apply to it directly. Their Section 4 introduces a margin version of the SPO loss, in the spirit of the margin theory of Koltchinskii and Panchenko (Ann. Statist. 2002) for classification. They show that it is Lipschitz under a geometric condition on the feasible region, and derive a generalization bound in terms of the multivariate Rademacher complexity of the hypothesis class. This mission formalizes that bound.

Setting

Decisions live in $\mathbb R^d$ with a norm $\|\cdot\|$; cost vectors are linear functionals with the dual norm $\|c\|_*=\max_{\|w\|\le1}c^\top w$. The feasible region $S\subseteq\mathbb R^d$ is nonempty, compact and convex, and throughout Section 4 it is not a singleton. An optimization oracle $w^*$ maps each cost vector $c$ to some minimizer $w^*(c)\in\arg\min_{w\in S}c^\top w$. The SPO loss of a prediction $\hat c$ against the realized cost $c$ is

$$\ell_{\rm SPO}(\hat c,c)=c^\top w^*(\hat c)-c^\top w^*(c),$$

and the linear optimization gap is $\omega_S(c)=\max_{w\in S}c^\top w-\min_{w\in S}c^\top w$, with $\omega_S(\mathcal C)=\sup_{c\in\mathcal C}\omega_S(c)$ and $\rho_2(\mathcal C)=\sup_{c\in\mathcal C}\|c\|_2$ for the set $\mathcal C$ of possible true costs.

A cost vector is degenerate if $\min_{w\in S}\hat c^\top w$ has more than one optimal solution; $\mathcal C^\circ$ is the set of degenerate costs. The distance to degeneracy is $\nu_S(\hat c)=\inf_{c\in\mathcal C^\circ}\|c-\hat c\|_*$. The region $S$ has the strength property with parameter $\mu>0$ if

$$\hat c^\top\big(w-w^*(\hat c)\big)\ge\frac{\mu\,\nu_S(\hat c)}{2}\,\|w-w^*(\hat c)\|^2\qquad\text{for all }w\in S\text{ and all }\hat c .$$

For $\gamma>0$ the $\gamma$-margin SPO loss $\ell^\gamma_{\rm SPO}(\hat c,c)$ equals $\ell_{\rm SPO}(\hat c,c)$ when $\nu_S(\hat c)>\gamma$ and $\frac{\nu_S(\hat c)}{\gamma}\ell_{\rm SPO}(\hat c,c)+\big(1-\frac{\nu_S(\hat c)}{\gamma}\big)\omega_S(c)$ otherwise. It dominates the SPO loss.

Data $(x,c)$ are drawn from a distribution $\mathcal D$ on features $\mathcal X$ and costs in $\mathcal C$, and $\mathcal H$ is a class of prediction functions $f:\mathcal X\to\mathbb R^d$. The SPO risk is $R_{\rm SPO}(f)=\mathbb E_{\mathcal D}[\ell_{\rm SPO}(f(x),c)]$ and the empirical margin risk is $\hat R^\gamma_{\rm SPO}(f)=\frac1n\sum_i\ell^\gamma_{\rm SPO}(f(x_i),c_i)$. The multivariate empirical Rademacher complexity is $\hat{\mathfrak R}^n(\mathcal H)=\mathbb E_{\boldsymbol\sigma}\big[\sup_{f\in\mathcal H}\frac1n\sum_i\boldsymbol\sigma_i^\top f(x_i)\big]$ with i.i.d. Rademacher vectors $\boldsymbol\sigma_i\in\{\pm1\}^d$, and $\mathfrak R^n(\mathcal H)$ is its expectation over the sample.

Formalization targets

Goal: Theorem 4, second display (pp. 19–20)

In the $\ell_2$ set-up, under the strength property with $\mu>0$ and for fixed $\gamma>0$, for every $\delta>0$, with probability at least $1-\delta$ over an i.i.d. sample of size $n$, for all $f\in\mathcal H$:

$$R_{\rm SPO}(f)\le\hat R^\gamma_{\rm SPO}(f)+\Big(\frac{2\sqrt2\rho_2(\mathcal C)+2\sqrt2\mu\,\omega_S(\mathcal C)}{\gamma\mu}\Big)\mathfrak R^n(\mathcal H)+\omega_S(\mathcal C)\sqrt{\frac{\log(1/\delta)}{2n}} .$$

Milestones

1. Theorem 3(a): $\|w^*(\hat c_1)-w^*(\hat c_2)\|\le\frac{\|\hat c_1-\hat c_2\|_*}{\mu\min\{\nu_S(\hat c_1),\nu_S(\hat c_2)\}}$.
2. Theorem 3(b): the same Lipschitz-like bound for $\ell_{\rm SPO}(\cdot,c)$, with an extra factor $\|c\|_*$.
3. Theorem 3(c): $\ell^\gamma_{\rm SPO}(\cdot,c)$ is $\frac{\|c\|_*+\mu\,\omega_S(c)}{\gamma\mu}$-Lipschitz for the dual norm.
4. Eq. (7) with $C=\sqrt2$ (Maurer's vector contraction inequality): for $L$-Lipschitz $\Phi_i$ on Euclidean $\mathbb R^d$,

$$\mathbb E_\sigma\Big[\sup_{f\in\mathcal H}\frac1n\sum_i\sigma_i\Phi_i(f(x_i))\Big]\le\sqrt2L\,\hat{\mathfrak R}^n(\mathcal H).$$

5. Theorem 4, first display: for any fixed sample with costs in $\mathcal C$,

$$\hat{\mathfrak R}^n_{\gamma\rm SPO}(\mathcal H)\le\Big(\frac{\sqrt2\rho_2(\mathcal C)+\sqrt2\mu\,\omega_S(\mathcal C)}{\gamma\mu}\Big)\hat{\mathfrak R}^n(\mathcal H).$$

Theorem 3 is stated for a general norm, as in the paper. Eq. (7), Theorem 4 and the goal are Euclidean. The paper's Theorem 5 (p. 20), a version of the goal uniform over $\gamma\in(0,\bar\gamma]$, is not part of this mission.

Significance

The bound replaces the loss-class complexity of the SPO loss, which is controlled only through combinatorial dimensions (Natarajan dimension in the polyhedral case, Section 3 of the paper), by the multivariate Rademacher complexity of $\mathcal H$ itself. For norm-bounded linear hypothesis classes this complexity has mild, even logarithmic, dependence on the dimensions $p$ and $d$ (Section 4.4). The result applies to every feasible region with the strength property. By Section 5 of the paper these include strongly convex sets and polytopes, where $\nu_S$ can also be computed. When most predictions stay far from degeneracy, $\hat R^\gamma_{\rm SPO}\approx\hat R_{\rm SPO}$ and the bound is much sharper than the combinatorial one. It is also a strict generalization of margin bounds for binary classification (Example 7).

The theorem is proved in the paper, which imports two external tools without proof: the Rademacher generalization bound of Bartlett and Mendelson, applied to the margin loss, and Maurer's inequality. To our knowledge none of these results has a machine-checked proof. The mission produces a checked proof of the margin bound and a Lean statement of Maurer's inequality. It also formalizes the strength property and the Lipschitz estimates of Theorem 3, which the companion missions on strongly convex sets and polytopes rely on.

Difficulty

The SPO loss is discontinuous in $\hat c$ at degenerate predictions. The standard route, scalar Ledoux–Talagrand contraction applied to the loss class, therefore fails at the first step. It would fail even for a Lipschitz loss, because it relates the loss class only to a scalar class, and $\mathcal H$ is vector valued. Lipschitz continuity of the margin loss needs the oracle to be stable away from $\mathcal C^\circ$. Convexity and compactness of $S$ alone do not give that: for an $\ell_p$ ball with $2<p<\infty$ the strength property fails for every $\mu>0$ (p. 14). The vector contraction inequality of Maurer (2016) is a nontrivial probabilistic inequality, and its constant $\sqrt2$ must not depend on the dimension $d$. The final concentration step is McDiarmid's inequality for a supremum over a possibly uncountable class, which in a formal proof needs measurability of that supremum.

Formalization scope

The decision space is a finite-dimensional real normed space E. Cost vectors and predictions are continuous linear functionals, StrongDual ℝ E, whose operator norm is the paper's dual norm. In the $\ell_2$ statements E = EuclideanSpace ℝ (Fin d), where the dual norm is Euclidean. Every statement carries the standing assumptions: $S$ nonempty, compact, convex and not a singleton, an arbitrary oracle (no tie-breaking rule), and $\mu>0$, $\gamma>0$. The Lipschitz-like bounds of Theorem 3(a)–(b) are stated multiplied out, because the paper reads $1/0$ as $+\infty$. Expectations over signs are finite averages over sign patterns. $\omega_S(\mathcal C)$ and $\rho_2(\mathcal C)$ are suprema over a nonempty bounded $\mathcal C$ containing the cost almost surely. "With probability at least $1-\delta$" is the statement that the outer $\mathcal D^n$-measure of the failure event is at most $\delta$.

Added hypotheses, all disclosed in the statements: the multivariate Rademacher sums are bounded above (almost surely in the goal) and $\hat{\mathfrak R}^n(\mathcal H)$ is integrable, since otherwise Lean's junk value $0$ would replace an infinite complexity and make the bound false rather than vacuous. Hypotheses $f$ and $\ell_{\rm SPO}(f(x),c)$ measurable, and the uniform deviation and margin Rademacher suprema a.e.-measurable, are also added; the paper is silent on measurability. A singleton $S$ would make $\mathcal C^\circ$ empty and the strength property hold for free; this is excluded explicitly, so the strength property is not vacuous.

A complete development needs the Bartlett–Mendelson symmetrization bound for bounded losses, McDiarmid's inequality, Maurer's inequality, and the Lipschitz and distance-to-degeneracy facts of Section 4.1. Maurer's inequality and the multivariate Rademacher complexity are reusable across vector-valued learning theory. Proofs of any milestone, and of Maurer's inequality in particular, are welcome.

Selected references

• O. El Balghiti, A. N. Elmachtoub, P. Grigas, A. Tewari, Generalization Bounds in the Predict-then-Optimize Framework, Mathematics of Operations Research, 2023; preprint arXiv:1905.11488v3, 2022. https://arxiv.org/abs/1905.11488
• A. N. Elmachtoub, P. Grigas, Smart "Predict, then Optimize", Management Science 68(1), 2022. https://doi.org/10.1287/mnsc.2020.3922
• A. Maurer, A Vector-Contraction Inequality for Rademacher Complexities, Algorithmic Learning Theory (ALT), 2016. https://arxiv.org/abs/1605.00251
• P. L. Bartlett, S. Mendelson, Rademacher and Gaussian Complexities: Risk Bounds and Structural Results, Journal of Machine Learning Research 3, 2002. https://www.jmlr.org/papers/v3/bartlett02a.html
• V. Koltchinskii, D. Panchenko, Empirical Margin Distributions and Bounding the Generalization Error of Combined Classifiers, Annals of Statistics 30(1), 2002. https://doi.org/10.1214/aos/1015362183

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 $P$ over the class, the learner outputs a posterior $Q$, read as the randomized predictor that draws $h \sim Q$, and the price of $Q$ is its Kullback–Leibler divergence from $P$. The PAC-Bayes theorem (Theorem 31.1) says that with probability $1 - \delta$, simultaneously for every posterior, the generalization loss exceeds the training loss by at most $\sqrt{(D(Q\|P) + \ln(m/\delta))/(2(m-1))}$. Its proof is a compact and elegant argument: Markov's inequality for an exponential moment, a change of measure from $Q$ to $P$ 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 $L_S(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

$H$ is a measurable space of hypotheses, $\ell : H \times Z \to [0,1]$ a jointly measurable loss, $D$ a distribution over $Z$, and $P$ a prior probability measure on $H$. For a posterior $Q$, $\ell(Q, z) = \mathbb{E}_{h \sim Q}[\ell(h, z)]$, $L_D(Q) = \mathbb{E}_{h \sim Q}[L_D(h)]$ and $L_S(Q) = \mathbb{E}_{h \sim Q}[L_S(h)]$, and $D(Q\|P) = \mathbb{E}_{h \sim Q}[\ln(dQ/dP)]$ is the Kullback–Leibler divergence, a real number when $Q \ll P$ and the log-density is $Q$-integrable.

Formalization targets

Goal: Theorem 31.1

For $m \ge 2$ and $\delta \in (0,1)$, with probability at least $1 - \delta$ over $S \sim D^m$, every probability measure $Q \ll P$ with finite divergence satisfies

$$L_D(Q) \le L_S(Q) + \sqrt{\frac{D(Q\|P) + \ln(m/\delta)}{2(m-1)}}.$$

Milestones

The identity $\mathbb{E}_{z \sim D}[\ell(Q, z)] = L_D(Q)$ (§31.1); the moment bound $\mathbb{E}_S[e^{2(m-1)\Delta(h)^2}] \le 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 $\mathbb{E}_{h \sim Q}[f(h)] - D(Q\|P) \le \ln\mathbb{E}_{h \sim P}[e^{f(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 - 1$; the claim $\le m$ is nevertheless true, for instance by writing $e^{a\Delta^2} = \mathbb{E}_g[e^{\sqrt{2a}\,g\Delta}]$ for a standard Gaussian $g$ and applying Hoeffding's lemma to the sample mean, which gives $\mathbb{E}_S[e^{2(m-1)\Delta^2}] \le (1 - (m-1)/m)^{-1/2} = \sqrt m$. Theorem 31.1 then follows the book: Markov's inequality on $e^{f(S)}$ with $f(S) = \sup_Q(2(m-1)\mathbb{E}_{h \sim Q}\Delta(h)^2 - D(Q\|P))$, the change of measure (31.2) by Jensen's inequality for $\ln$ applied to the density $dQ/dP$ (the Donsker–Varadhan inequality, which needs $Q \ll P$ and an integrable log-density), the exchange of expectations (31.4) by Fubini, the moment bound, and finally Jensen for $x^2$ in (31.6); formally the supremum over all posteriors is handled by proving the bound for each $Q$ on the event $\{S : \mathbb{E}_{h \sim P}[e^{2(m-1)\Delta(h)^2}] \le m/\delta\}$, whose complement has probability at most $\delta$ by Markov, which sidesteps any measurability question about $f$. Exercise 2 is the theorem with $Q = \delta_h$, for which $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)$ is Mathlib's Radon–Nikodym derivative; the divergence is a Bochner integral, so the theorem quantifies over posteriors $Q \ll P$ whose log-density is $Q$-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 $Q$ violates the bound. The loss is jointly measurable so that $h \mapsto L_D(h)$ and $(S, h) \mapsto L_S(h)$ are measurable and the Gibbs risks are genuine integrals; $m \ge 2$ is forced by the denominator $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.

Motivation

A feedforward neural network is a directed acyclic graph of neurons, each computing a fixed scalar activation of a weighted sum of its inputs; fixing the graph and the activation and letting the weights vary gives a hypothesis class. Chapter 20 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019), studies these classes through the book's three lenses. Approximation: every Boolean function is implemented by a network of depth 2 (Claim 20.1), but only at exponential size (Theorem 20.2), while a sign neuron implements conjunctions and disjunctions (Lemma 20.4), the bridge to Boolean circuits and hence to everything computable in bounded time. Estimation: the VC dimension of the class of sign networks over a graph with $|E|$ edges is $O(|E|\log|E|)$ (Theorem 20.6), so the sample complexity is governed by the number of weights. Optimization: training is NP-hard even for tiny networks, and the practical answer is SGD with the gradient computed by backpropagation, whose correctness the chapter derives from the chain rule.

Setting

A layered graph has layers $V_0, \dots, V_T$, every edge joining $V_{t-1}$ to $V_t$; $V_0$ holds the $n$ inputs and a constant neuron outputting $1$. With weights $w : E \to \mathbb{R}$ and an activation $\sigma$, the outputs are computed layer by layer, $a_{t+1,i} = \sum_{j : (v_{t,j}, v_{t+1,i}) \in E} w_{t,i,j}\,o_{t,j}$ and $o_{t+1,i} = \sigma(a_{t+1,i})$. The class $H_{V,E,\sigma} = \{h_{V,E,\sigma,w} : w : E \to \mathbb{R}\}$ (20.1); for binary classification the output layer is a single neuron and $\sigma$ is the sign function, so $H_{V,E,\operatorname{sign}}$ is a set of $\{\pm1\}$-valued predictors on $\mathbb{R}^n$. The size of the network is $|V|$, its depth $T$. The growth function $\tau_H(m) = \max_{|C| \le m}|H_C|$ extends to classes with any finite codomain (p. 275), and the proof of Theorem 20.6 uses two of its properties, stated as Exercises 3 and 4: the growth function of a product class is at most the product of the growth functions, and likewise for a composition class. For backpropagation the activation is any differentiable $\sigma$ and the loss is $\frac12\|o_T - y\|^2$; the backward pass sets $\delta_T = o_T - y$ and $\delta_t = \delta_{t+1}\operatorname{diag}(\sigma'(a_{t+1}))W_t$.

Formalization targets

Goal: Theorem 20.6

The VC dimension of $H_{V,E,\operatorname{sign}}$ is $O(|E|\log|E|)$. Explicitly, for a layered graph of depth at least $1$ with a single output neuron,

$$\operatorname{VCdim}(H_{V,E,\operatorname{sign}}) \le 2|E|\log_2(16|E|),$$

stated as: every $m \le \operatorname{VCdim}$ satisfies this bound (so the VC dimension is finite).

Milestones

Claim 20.1 (the depth-2 graph with $|V_1| = 2^n + 1$ whose sign class contains every function $\{\pm1\}^n \to \{\pm1\}$); Theorem 20.2 (every sign network implementing all functions $\{0,1\}^n \to \{0,1\}$ has $2^{n/3} \le 2|V|$); Lemma 20.4 (conjunction and disjunction as sign neurons); Exercise 4 (growth function of a composition); the correctness of backpropagation (§20.6: the partial derivative for the edge $(v_{t,j}, v_{t+1,i})$ is $\delta_{t+1,i}\sigma'(a_{t+1,i})o_{t,j}$). Further items: Exercise 3 (growth function of a product) and the intermediate bound $\tau_H(m) \le (em)^{|E|}$ of the proof of Theorem 20.6.

Significance

Theorem 20.6 is the reason networks are learnable at all in the book's sense: by the fundamental theorem, a class with finite VC dimension is agnostic PAC learnable with sample complexity linear in that dimension, and here the dimension is essentially the number of tunable parameters. The proof technique, due to Kakade and Tewari's lecture notes, is a composition-and-product argument on growth functions that applies to any layered class of threshold units and is reusable well beyond this chapter. Theorem 20.2 is the matching negative fact on expressive power, and it is a corollary of the same bound: a class that shatters $2^n$ points needs $\Omega(2^n)$ edges. Backpropagation's correctness is the one theorem about training the chapter can offer, given the hardness results, and it is the algorithm every practitioner runs.

Difficulty

Claim 20.1 and Lemma 20.4 are explicit constructions: the neuron $g_i(x) = \operatorname{sign}(\langle x, u_i\rangle - n + 1)$ detects $x = u_i$ because $\langle x, u_i\rangle \le n - 2$ otherwise, and the output neuron takes the disjunction; formally one must build the weight function and evaluate the forward pass on the $2^n$ inputs. Exercises 3 and 4 are counting: a restricted product is determined by its two restricted factors, and a restricted composition $f_2 \circ f_1$ on $C$ is determined by $f_1|_C$ and $f_2|_{f_1(C)}$, with $|f_1(C)| \le |C|$. Theorem 20.6 then needs: the class of one neuron is the class of homogenous halfspaces on its $d_{t,i}$ incoming coordinates, of VC dimension at most $d_{t,i}$ (Mission VI), Sauer's lemma in the form $\tau(m) \le (em)^{d}$ for every $m \ge 1$ (Mission IV; for $m \le d$ use $2^m \le (em)^m$), the layer class as a product and the network as a composition of layer classes, and finally the arithmetic $2^m \le (em)^{|E|} \Rightarrow m \le 2|E|\log_2(16|E|)$, which replaces the book's appeal to Lemma A.2 (for $m \ge 8|E|$ one has $\ln m \le \frac{m\ln 2}{2|E|}$). Theorem 20.2 follows from the goal with $|E| \le |V|^2$. Backpropagation is a chain-rule computation in a single real variable: the loss as a function of one weight is a composition of finitely many differentiable maps, and the derivative unwinds to the backward recursion; the formal effort is in the induction along layers with the natural-number indexing of the model.

Formalization scope

Layers and neurons are indexed by natural numbers: a LayeredGraph records the depth, the layer widths and, for each $t < T$, the finite set of edges $(v_{t,j}, v_{t+1,i})$ as pairs $(i, j)$ within the layer widths. Weights are functions on all index triples, and only those on edges are used, so the class is the image of all weight functions, as in (20.1). The forward computation netOutput is a recursion on the layer index; netInput is $a_{t+1,i}$. The sign activation returns $\pm1$ with $\operatorname{sign}(0) = -1$, the book's convention elsewhere, and a neuron with no incoming edges outputs $\sigma(0)$ (p. 270). The binary class signNetClass n G is Bool-valued, true iff the output neuron's input is positive, and is stated for graphs of depth at least $1$ (for depth $0$ the edges out of the input layer would be used but not counted in $|E|$). Growth functions with finite codomain are growthY, an sSup over restriction sizes, well defined because the codomains are finite; the Bool case is Mission IV's growth, and VC dimension and shattering are Mission IV's. Theorem 20.6 and Theorem 20.2 are given with explicit constants derived from the proof, since $O(\cdot)$ statements have no formal content; the drafter verified $\max\{m : 2^m \le (em)^{|E|}\} \le 2|E|\log_2(16|E|)$ numerically for $|E|$ up to $3000$ and at $10^4, \dots, 10^7$, and $2^n \le 2|V|^2\log_2(16|V|^2) \le 8|V|^3$. Backpropagation is stated for an arbitrary layered graph (phantom edges have weight $0$, p. 279), any differentiable activation, and one edge at a time as a HasDerivAt of the loss in that weight; $\delta_t$ is defined by recursion on $T - t$. The book's layer indices in (20.3) are shifted by one in the statement.

Not stated: Theorem 20.3 (Turing machines), Theorem 20.5 and Exercise 1 (sigmoid approximation, which needs a convention for outputs in $[-1,1]$ that the chapter leaves open), Theorem 20.7 and Exercise 6 (NP-hardness), Exercise 5 (the $\Omega(|E|^2)$ sigmoid lower bound, which assumes an exact threshold), the sigmoid half of Theorem 20.2, and the SGD pseudocode of §20.6, which is a heuristic without a stated guarantee.

Selected references

• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 20. doi:10.1017/CBO9781107298019
• M. Anthony, P. L. Bartlett, Neural Network Learning: Theoretical Foundations, Cambridge University Press, 1999. doi:10.1017/CBO9780511624216
• D. E. Rumelhart, G. E. Hinton, R. J. Williams, Learning representations by back-propagating errors, Nature 323, 1986. doi:10.1038/323533a0
• I. Parberry, Circuit Complexity and Neural Networks, MIT Press, 1994.
• E. B. Baum, D. Haussler, What size net gives valid generalization?, Neural Computation 1(1), 1989. doi:10.1162/neco.1989.1.1.151