Machine Learning

Motivation

A correlated equilibrium (Aumann, 1974) is a joint distribution over the players' strategy profiles from which no player gains by deviating from a recommended strategy. A central question of learning in games is which equilibria repeated play of simple, myopic rules can reach. Foster and Vohra (1997) answered it for calibrated forecasting: if each player forecasts the opponent with a calibrated rule and best-responds to the forecast, the empirical distribution of play approaches the set of correlated equilibria (their Theorem 1). That result has become a basic reference point for no-regret and calibration-based learning in games (Hart and Mas-Colell, 2000).

This mission formalizes the paper's converse. Theorem 1 says calibrated learning ends up in the correlated equilibria; the converse says it can end up at any of them, for almost every game. Together the two results characterize exactly which long-run outcomes calibrated learning with best responses can produce.

Setting

Two players choose strategies from finite sets $S(1)$ with $m$ elements and $S(2)$ with $n$ elements; player $i$ receives payoff $u_i(x,y)\in\mathbb{R}$ and maximizes it. A game $G=(u_1,u_2)$ is a pair of real $m\times n$ matrices, that is, a point of $\mathbb{R}^{2mn}$; a set of games has measure zero if it is Lebesgue-null in $\mathbb{R}^{2mn}$.

A joint distribution $D$ on $S(1)\times S(2)$ is a correlated equilibrium if for every map $\Phi:S(1)\to S(1)$, $\sum_{x,y}D(x,y)u_1(\Phi(x),y)\le\sum_{x,y}D(x,y)u_1(x,y)$, and symmetrically for player 2. $\pi(G)$ is the set of correlated equilibria.

Play is repeated in rounds $t=0,1,2,\dots$. Before each round, player 1 issues a forecast $f_1(t)$, a probability vector over $S(2)$, produced by a deterministic forecasting rule from the history of play so far; player 2 likewise forecasts player 1. For a forecast sequence $f$ and the opponent's plays $z$, let $N(p,t)$ be the number of the first $t$ rounds with forecast $p$, and $\rho(p,j,t)$ the fraction of those rounds in which the opponent played $j$ (zero if $N(p,t)=0$). The forecasts are calibrated if for every $j$

$$\sum_p |\rho(p,j,t)-p_j|\,\frac{N(p,t)}{t}\ \longrightarrow\ 0 \qquad (t\to\infty).$$

Each player then plays $R_i$ of its forecast, where the best-reply function $R_i$ picks a best response to every forecast and does not depend on the round. $D_t(x,y)$ is the fraction of the first $t$ rounds in which $(x,y)$ was played.

$\lambda(G)$, the set of limit points of calibrated forecasts, consists of the $D$ for which some best-reply functions $R_1,R_2$ and some calibrated forecasting rules make $D_t(x,y)\to D(x,y)$ for all $(x,y)$.

Formalization targets

Goal: Theorem 2 (p. 47)

$$\text{for Lebesgue-almost every } G\in\mathbb{R}^{2mn}:\qquad \lambda(G)=\pi(G).$$

Milestones

1. $\lambda(G)\subseteq\pi(G)$ for every game (Theorem 1 restated, p. 46).
2. Every joint distribution $D$ is the limiting empirical distribution of a deterministic play sequence supported on $\{D>0\}$ (p. 47).
3. Along such a sequence the conditional forecasts $p_{1,t}=D(x_t,\cdot)/\sum_yD(x_t,y)$ and $p_{2,t}=D(\cdot,y_t)/\sum_xD(x,y_t)$ are calibrated (p. 47).
4. In a correlated equilibrium each recommended strategy is a best response to its conditional forecast (p. 47).
5. For almost every payoff matrix, each set $M_b(x)$ of forecasts to which $x$ is a best response is either empty or contains a forecast in the open simplex at which $x$ is the unique best response (p. 47).
6. The perturbed forecasts $p_i=(1-1/i)p^*+(1/i)q$ converge to $p^*$ and keep a unique best reply (p. 48).
7. For the $3\times3$ game of p. 48, a correlated equilibrium lies outside $\lambda(G)$, and $\lambda(G)$ is the single point mass on $(C,2)$.

Significance

Theorem 1 by itself leaves open whether calibration selects among correlated equilibria, for instance toward Nash equilibria or toward particular payoffs. Theorem 2 closes that question negatively for generic games: every correlated equilibrium is the genuine limit, not merely an accumulation point, of calibrated play with stationary best replies. As the paper notes, adding the assumption that the limit exists therefore does not refine the equilibrium reached, in contrast with Fudenberg and Kreps's result for asymptotically myopic Bayesian play. The $3\times3$ example shows that the genericity hypothesis cannot be dropped.

The results are proved in the 1997 paper; none is formalized. A complete development produces a reusable layer for repeated two-player games (calibration, empirical distributions, best-reply maps, correlated equilibria), a genericity lemma for best-response regions that is useful beyond this paper, and a machine-checked version of an argument that the paper gives only in outline.

Difficulty

The natural construction takes a correlated equilibrium $D$, a play sequence realizing $D$, and forecasts equal to the conditional distributions of $D$. The forecasts are then calibrated and each played strategy is a best response. What fails is the best-reply function: two strategies $x'\ne x''$ can have the same conditional forecast $p^*$, while a stationary $R_1$ maps $p^*$ to only one strategy. Separating them needs forecasts near $p^*$ at which each is the unique best response, and that exists only when the best-response regions have nonempty relative interior, a property that fails on a null set of games (the $3\times3$ example) and whose genericity must be proved. The perturbed forecasts are no longer exactly equal to the conditional frequencies, so calibration has to be re-established with errors that vanish along the sequence.

Formalization scope

• Strategies are Fin m and Fin n; payoffs are real matrices; players maximize. A game is a point of (Fin m → Fin n → ℝ) × (Fin m → Fin n → ℝ) with Mathlib's volume (Lebesgue measure on $\mathbb{R}^{2mn}$), and "almost every" is ∀ᵐ.
• A correlated equilibrium is the joint-distribution form of p. 44 (a joint distribution with the two deviation inequalities).
• Forecasting rules map finite histories to probability vectors; the play is generated recursively from the rules and the best-reply functions. Best-reply functions are arbitrary stationary selections of a best response at every probability vector; they may not depend on the round, since round-dependent tie-breaking enlarges $\lambda(G)$ (the matching pennies example of p. 46).
• Rounds are $0,\dots,t-1$; $D_0=0$. The calibration sum runs over the forecasts issued so far, which is the paper's sum over all $p$ since the other terms vanish.
• $\lambda(G)$ requires convergence of $D_t$, not a subsequence. Replacing the limit by a limit point, or stating only $\pi(G)\subseteq\lambda(G)$, does not formalize the theorem.
• The page's sentence "Almost every game has the property that all the sets $M_b(x)$ have non-empty interior" is false for dominated strategies ($M_b(x)=\emptyset$ on an open set of games). Milestone 5 states the dichotomy the page's argument proves: empty or with relative interior.
• The page prints the denominator of $p_{2,t}$ as $\sum_{x}D(x_t,y)$; the mission uses $\sum_xD(x,y_t)$.

The theorems are stated from the mission's own definitions of the game, calibration and $\lambda(G)$; no statement is vacuous: at $m=0$ or $n=0$ both sides of the goal are empty, and the $3\times3$ example exercises every definition. Contributions welcome: proofs of the milestones in any order, the genericity lemma (Lebesgue-null sets of linear degeneracies), and the calibration estimates for the perturbed forecasts.

Selected references

• D. P. Foster and R. V. Vohra, Calibrated learning and correlated equilibrium, Games and Economic Behavior 21 (1997), 40–55. https://doi.org/10.1006/game.1997.0595
• R. J. Aumann, Subjectivity and correlation in randomized strategies, Journal of Mathematical Economics 1 (1974), 67–96. https://doi.org/10.1016/0304-4068(74)90037-8
• A. P. Dawid, The well-calibrated Bayesian, Journal of the American Statistical Association 77 (1982), 605–610. https://doi.org/10.1080/01621459.1982.10477856
• D. Fudenberg and D. M. Kreps, Learning mixed equilibria, Games and Economic Behavior 5 (1993), 320–367. https://doi.org/10.1006/game.1993.1021
• S. Hart and A. Mas-Colell, A simple adaptive procedure leading to correlated equilibrium, Econometrica 68 (2000), 1127–1150. https://doi.org/10.1111/1468-0262.00153

Motivation

In supervised binary classification, a hypothesis class is learnable if and only if it has uniform convergence, meaning that empirical risks converge to true risks uniformly over the class. When that holds, empirical risk minimisation (ERM) learns. This equivalence, due to Vapnik and Chervonenkis and extended to real-valued losses by Alon, Ben-David, Cesa-Bianchi and Haussler, is the usual starting point of statistical learning theory.

Vapnik's General Learning Setting is broader. It covers stochastic convex optimisation, clustering and density estimation, and in it the equivalence breaks down. Shalev-Shwartz, Shamir, Srebro and Sridharan (JMLR 11 (2010) 2635–2670) exhibit learnable problems with no uniform convergence, and learnable problems where ERM fails. So neither uniform convergence nor the success of ERM characterises learnability there, and something else has to. This mission formalizes the paper's answer, its Theorem 7: stability.

Timeline:

• 1971–1995: Vapnik and Chervonenkis prove learnability ⇔ uniform convergence for binary classification. Vapnik (1995) introduces the General Learning Setting.
• 2002: Bousquet and Elisseeff show that uniform stability of a learning rule implies generalization.
• 2006: Mukherjee, Niyogi, Poggio and Rifkin show that, in the supervised setting, stability of ERM is necessary and sufficient for learnability.
• 2009–2010: Shalev-Shwartz, Shamir, Srebro and Sridharan (COLT 2009, JMLR 2010) prove that, in the General Learning Setting, learnability is equivalent to the existence of a uniform-RO stable, universally asymptotic empirical risk minimiser (Theorem 7).

Setting

A learning problem consists of a hypothesis class $\mathcal H$ (nonempty), an instance set $\mathcal Z$ with a $\sigma$-algebra, and an objective $f:\mathcal H\times\mathcal Z\to\mathbb R$ with $|f(h;z)|\le B$ for all $h,z$. Given a probability distribution $\mathcal D$ on $\mathcal Z$ and an i.i.d. sample $S=(z_1,\dots,z_m)\sim\mathcal D^m$, the following quantities are defined:

• the risk is $F(h)=\mathbb E_{z\sim\mathcal D}[f(h;z)]$, and $F^*=\inf_{h}F(h)$;
• the empirical risk is $F_S(h)=\frac1m\sum_{i=1}^m f(h;z_i)$, and $F_S(\hat h_S)=\inf_h F_S(h)$ is the minimal empirical risk. Only the value is used; no minimiser need exist.

A learning rule $A$ maps each sample $S$ of each size $m$ to a hypothesis $A(S)$. A rate $\varepsilon(m)$ is a non-increasing sequence tending to $0$. For a rule $A$ the paper defines the following properties:

• $A$ is consistent with rate $\varepsilon_{\rm cons}$ under $\mathcal D$ if $\mathbb E_S[F(A(S))-F^*]\le\varepsilon_{\rm cons}(m)$. It is universally consistent if this holds for every $\mathcal D$ with the same rate. The problem is learnable (Definition 1) if a universally consistent rule exists.
• $A$ is an AERM (asymptotic empirical risk minimiser) with rate $\varepsilon_{\rm erm}$ under $\mathcal D$ if $\mathbb E_S[F_S(A(S))-F_S(\hat h_S)]\le\varepsilon_{\rm erm}(m)$, and universally so if this holds for every $\mathcal D$.
• $A$ generalizes with rate $\varepsilon_{\rm gen}$ under $\mathcal D$ if $\mathbb E_S[|F(A(S))-F_S(A(S))|]\le\varepsilon_{\rm gen}(m)$.
• With $S^{(i)}$ the sample $S$ with $z_i$ replaced by $z_i'$, $A$ is uniform-RO stable with rate $\varepsilon_{\rm stable}$ (Definition 4) if, for all $S$, all replacements $(z_1',\dots,z_m')$ and all $z'\in\mathcal Z$,

$$\frac1m\sum_{i=1}^m\bigl|f(A(S^{(i)});z')-f(A(S);z')\bigr|\le\varepsilon_{\rm stable}(m).$$

Average-RO stability (Definition 5) is the in-expectation analogue, with the replacement point also serving as the test point.

Formalization targets

Goal: Theorem 7

The problem is learnable if and only if there is a learning rule that is uniform-RO stable and universally an AERM. Quantitatively, if $A$ is universally consistent with rate $\varepsilon_{\rm cons}$, then some rule $A'$ is uniform-RO stable and universally AERM with

$$\varepsilon_{\rm stable}(m)=\frac{2B}{\sqrt m},\qquad \varepsilon_{\rm erm}(m)=3\,\varepsilon_{\rm cons}\bigl(\lfloor m^{1/4}\rfloor\bigr)+\frac{8B}{\sqrt m},$$

and conversely, a uniform-RO stable universal AERM is universally consistent with rate $\varepsilon_{\rm stable}(m)+\varepsilon_{\rm erm}(m)$.

Milestones

These follow the order of the paper's proof.

• Sufficiency: Utility Lemma 12 (a bounded sample mean deviates by at most $B/\sqrt m$ in expectation), Lemma 11 (on-average generalization ⇔ average-RO stability), Claim 6 (uniform-RO ⇒ average-RO stability), Lemma 15 (an on-average generalizing AERM is consistent), and Theorem 8 (a stable AERM is consistent with rate $\varepsilon_{\rm stable}+\varepsilon_{\rm erm}$ and generalizes with rate $\varepsilon_{\rm stable}+2\varepsilon_{\rm erm}+2B/\sqrt m$).
• Necessity: Lemma 20 (every rule has a uniform-RO stable, $3B/\sqrt m$-generalizing version with consistency rate $\varepsilon_{\rm cons}(\lfloor\sqrt m\rfloor)$), Lemma 16, the Main Converse Lemma ($\mathbb E|F_S(\hat h_S)-F^*|\le2\varepsilon_{\rm cons}(m')+2B/\sqrt m+2Bm'^2/m$ for $2\le m'\le m/2$), and Lemma 18 (under that bound, a consistent and generalizing rule is an AERM).

Significance

Theorem 7 shows that in the General Learning Setting, stability replaces uniform convergence as the notion that characterises learnability. It also says where to look for a learning rule: ERM may fail, but some AERM always works, and it must be stable. The rates are explicit and polynomial. Downstream, the paper uses Theorem 7 to prove Theorem 23 (randomised rules) and to design a generic learning algorithm (Theorem 25). Mission II of this series (Tikhonov-regularised ERM for stochastic convex optimisation) is a concrete instance of a stable AERM for a problem with no uniform convergence.

The theorem has been proved since 2010 but has not been formalized. The platform has the textbook side of the same authors' framework: Understanding Machine Learning Theorem 13.2, UnderstandingML.stability_identity, the replace-one identity behind Lemma 11, stated for hypotheses in $\mathbb R^d$. The platform does not have learnability in the General Learning Setting, over an arbitrary hypothesis class, or the converse direction. That direction is the new content: learnability forces a stable AERM to exist.

Difficulty

The sufficiency direction is a chain of expectation identities. The necessity direction is harder. A universally consistent rule need not be an AERM, need not generalize and need not be stable (Example 2 of the paper), so it cannot simply be reused. ERM cannot be used either, since it can fail on learnable problems. The Main Converse Lemma is where universal consistency is used in full: the rule's guarantee has to be applied under a distribution other than $\mathcal D$, and a naive argument under $\mathcal D$ alone fails (Example 1: consistency under one distribution does not imply generalization under it). Combining the lemmas into the stated rates requires choosing the auxiliary sample size and tracking every constant, including the regime of small $m$ where Lemma 16's hypothesis $2\le m'\le m/2$ cannot be met.

Formalization scope

Samples are Fin m → Z, the sample law $\mathcal D^m$ is Measure.pi, and $S^{(i)}$ is Function.update S i (S' i). Learning rules have type (m : ℕ) → (Fin m → Z) → H, and every property is asserted for $m\ge1$. The minimal empirical risk and $F^*$ are real infima over the nonempty, bounded-below family, never values at a chosen minimiser. Rates are non-increasing on $m\ge1$ and tend to $0$. $\lfloor m^{1/4}\rfloor$ and $\lfloor\sqrt m\rfloor$ are Nat.sqrt (Nat.sqrt m) and Nat.sqrt m, the paper's $\varepsilon_{\rm cons}(m^{1/4})$ read at an integer sample size. The paper's $B=\sup|f|$ is replaced by any bound $B$ (all rates increase in $B$).

The paper never discusses measurability. This formalization adds one standing assumption, identical across the series: each $f(h;\cdot)$ is measurable, the minimal empirical risk $S\mapsto\inf_hF_S(h)$ is measurable (true for countable $\mathcal H$, for example), and every learning rule, whether assumed or asserted to exist, has $(S,z)\mapsto f(A(S);z)$ jointly measurable. Without this a non-measurable rule would have Bochner integrals equal to $0$, and existence claims such as "some rule is a universal AERM" would be satisfied by junk. Every existential in the goal therefore produces a measurable rule, and learnability is quantified over measurable rules with the rate chosen before the distribution. Uniform-RO stability is pointwise over all samples, replacement vectors and test points; it is never replaced by the in-expectation Definition 5.

No statement is corrected. The proof of the converse in the paper calls $A'$ "$2B/\sqrt m$-generalizing" where Lemma 20 gives $3B/\sqrt m$. The stated $8B/\sqrt m$ absorbs either value, so Theorem 7 is formalized as printed.

The definitions (risks, rules, consistency, AERM, generalization, the two RO-stability notions) are reusable by the other missions of this series and by any stability-based result in the General Learning Setting. Contributions are welcome at every level: proofs of the milestones, the measure-theoretic infrastructure they need (exchangeability of i.i.d. coordinates under Measure.pi, sub-sampling and restriction of product measures, the variance bound for bounded sample means), and the remaining results of Section 5 (Theorems 9 and 10, Lemmas 14 and 17).

Selected references

• S. Shalev-Shwartz, O. Shamir, N. Srebro, K. Sridharan, Learnability, Stability and Uniform Convergence, Journal of Machine Learning Research 11 (2010) 2635–2670. https://jmlr.org/papers/v11/shalev-shwartz10a.html
• V. N. Vapnik, The Nature of Statistical Learning Theory, Springer, 1995. https://doi.org/10.1007/978-1-4757-2440-0
• N. Alon, S. Ben-David, N. Cesa-Bianchi, D. Haussler, Scale-sensitive dimensions, uniform convergence, and learnability, Journal of the ACM 44(4) (1997) 615–631. https://doi.org/10.1145/263867.263927
• O. Bousquet, A. Elisseeff, Stability and Generalization, Journal of Machine Learning Research 2 (2002) 499–526. https://jmlr.org/papers/v2/bousquet02a.html
• S. Mukherjee, P. Niyogi, T. Poggio, R. Rifkin, Learning theory: stability is sufficient for generalization and necessary and sufficient for consistency of empirical risk minimization, Advances in Computational Mathematics 25 (2006) 161–193. https://doi.org/10.1007/s10444-004-7634-z
• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 13. https://doi.org/10.1017/CBO9781107298019

Motivation

Classifiers trained to high standard accuracy can be fooled by small, deliberately chosen perturbations of their inputs, so-called adversarial examples (Szegedy et al., 2014; Goodfellow et al., 2015). Training methods that aim at robustness against perturbations bounded in the $\ell_\infty$ norm reach high robust accuracy on the training set while robust test accuracy stays far lower, a gap much larger than the standard generalization gap (Madry et al., 2018). Schmidt, Santurkar, Tsipras, Talwar and Mądry (arXiv:1804.11285) ask whether this gap is intrinsic: does learning a robust classifier need more data than learning an accurate one?

They answer with two simple data distributions. In a Gaussian model the robust sample complexity is larger than the standard one by a factor of order $\sqrt d$, for every learning algorithm. In a Bernoulli model on the hypercube, linear classifiers suffer the same penalty, but a nonlinear classifier does not. This mission formalizes the second half of that picture: in the Bernoulli model, thresholding the input and then applying the linear classifier learned from one single sample is robust against every $\ell_\infty$ perturbation of size less than $1$.

Setting

Points live in $\mathbb R^d$ with the Euclidean inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|_2$. Labels are $y\in\{\pm1\}$. A binary classifier is any map $f:\mathbb R^d\to\{\pm1\}$, and for $w\in\mathbb R^d$ the linear classifier is $f_w(x)=\operatorname{sgn}(\langle w,x\rangle)$.

The $(\theta^\star,\tau)$-Bernoulli model. Fix a sign vector $\theta^\star\in\{\pm1\}^d$ and a bias $\tau\in(0,\tfrac12]$. A sample $(x,y)$ is drawn by choosing $y$ uniformly in $\{\pm1\}$ and then, independently for each coordinate $i$, setting $x_i=y\theta^\star_i$ with probability $\tfrac12+\tau$ and $x_i=-y\theta^\star_i$ with probability $\tfrac12-\tau$. So $x\in\{\pm1\}^d$, and each coordinate carries a weak signal of strength $2\tau$ about the label.

Errors. The classification error of $f$ is $\mathbb P_{(x,y)}[f(x)\ne y]$. For $\varepsilon\in\mathbb R$ the $\ell_\infty$ ball is $\mathcal B^\varepsilon_\infty(x)=\{x'\in\mathbb R^d:\|x'-x\|_\infty\le\varepsilon\}$, and the $\ell_\infty^\varepsilon$-robust classification error of $f$ is

$$\mathbb P_{(x,y)}\big[\exists\,x'\in\mathcal B^\varepsilon_\infty(x):\ f(x')\ne y\big].$$

The adversary may move $x$ anywhere in the ball, including off the hypercube.

Thresholding. The thresholding map $T:\mathbb R^d\to\mathbb R^d$ is $T(x)_i=+1$ if $x_i\ge0$ and $T(x)_i=-1$ otherwise. The classifier studied is $f_{\hat w}\circ T$, with $\hat w=yx$ computed from one training sample $(x,y)$.

Formalization targets

Goal: Theorem 10 (p. 8)

There is a universal constant $c>0$ such that, whenever $\tau\ge c\,d^{-1/4}$ and $(x,y)$ is one sample of the model with $\hat w=yx$,

$$\mathbb P_{(x,y)}\Big[\exists\,\varepsilon<1:\ \mathrm{RobErr}_\varepsilon\big(f_{\hat w}\circ T\big)>\tfrac1{100}\Big]\ \le\ \exp\!\Big(-\frac{\tau^2d}{2}\Big).$$

The constant $c$ is left existential; only the scaling $\tau\gtrsim d^{-1/4}$ is fixed. The failure probability is the one the paper proves for the same classifier.

Milestones

1. Lemma 24 (p. 31): $\mathbb P\big[\langle z,\theta^\star\rangle\le2\tau d-\sqrt{2d\log(1/\delta)}\big]\le\delta$ for $z=xy$.
2. Lemma 25 (p. 31): for $\hat w=z/\|z\|_2$, $\mathbb P[\langle\hat w,\theta^\star\rangle\le\tau\sqrt d]\le\exp(-\tau^2d/2)$.
3. Lemma 26 (p. 32): for a fixed unit $w$ with $\langle w,2\tau\theta^\star\rangle\ge0$, $\mathbb P[\langle w,z\rangle\le0]\le\exp(-2\tau^2\langle w,\theta^\star\rangle^2)$.
4. Theorem 27 (p. 32): with probability at least $1-\exp(-\tau^2d/2)$, $f_{\hat w}$ has classification error at most $\exp(-2\tau^4d)$.
5. Corollary 28 (p. 33): if $\tau\ge(\log(1/\beta)/(2d))^{1/4}$, then with probability at least $1-\exp(-\tau^2d/2)$, $f_{\hat w}$ has classification error at most $\beta$.
6. Thresholding identity (§2.2, p. 7): $T(\mathcal B^\varepsilon_\infty(x))=\{x\}$ for every $x\in\{\pm1\}^d$ and $0\le\varepsilon<1$.

Significance

Together with the lower bound for linear classifiers in the same model (Theorem 9 of the paper), Theorem 10 shows that robust sample complexity depends on the hypothesis class and on the data distribution, not only on the perturbation size: a fixed nonlinear preprocessing step closes a gap that no linear classifier can close. The paper's Gaussian model shows the opposite behaviour, where every learner pays the $\sqrt d$ penalty, so the two models together separate "robustness is information-theoretically expensive" from "robustness is expensive for a restricted class". The authors also report that an explicit thresholding layer improves robust training on MNIST, which motivates the model.

The result is proved in the paper. To the platform's knowledge it has no machine-checked proof. Formalizing it yields a complete, finite and self-contained robust-learning upper bound, the single-sample standard-generalization bounds of Theorem 27 and Corollary 28 as reusable statements, and a worked instance of one-sided Hoeffding bounds for weighted sums of hypercube coordinates.

Difficulty

The concentration steps are standard, but the natural first approach to the goal fails: a bound on the classification error of the linear classifier $f_{\hat w}$ says nothing about its robust error, and for $\varepsilon$ of order $\tau$ the robust error of every linear classifier is close to $\tfrac12$. The goal concerns the nonlinear classifier $f_{\hat w}\circ T$, whose robustness rests on the data lying exactly on the hypercube and on the adversary's budget being below $1$; neither fact is visible to an argument about linear classifiers. A second difficulty is bookkeeping: the paper uses three forms of the estimator ($yx$, $z/\|z\|_2$, $yx/\|x\|_2$), a training sample and a test sample with the same name, and a failure event that must hold for all $\varepsilon<1$ at once.

Formalization scope

$\mathbb R^d$ is EuclideanSpace ℝ (Fin d). Labels and hypercube coordinates are Bool ($+1\leftrightarrow$ true). Because the model is finite, every probability is a finite sum of the weights $\tfrac12\prod_i(\tfrac12\pm\tau)$; no measure theory is involved. Conventions committed to:

• coordinates of $x$ are independent given $y$ (the paper's "sampling each coordinate", as its proofs use it);
• $0<\tau\le\tfrac12$ in every theorem, since $\tfrac12-\tau$ must be a probability;
• $\operatorname{sgn}(0)$ is taken as $+1$ (a tie is classified $+1$); $T$ sends $0$ to $+1$, as printed;
• the $\ell_\infty$ ball is written coordinatewise, never as the Euclidean ball;
• "with probability at least $1-q$, the error is at most $\beta$" is stated as "the failure event has probability at most $q$";
• the goal's "for any $\varepsilon<1$" is inside the event, one good sample for all $\varepsilon$;
• added hypotheses, each forced by a degenerate case where the printed statement is false: $d\ge1$ in Lemma 24, $\beta>0$ in Corollary 28, $\varepsilon\ge0$ in the thresholding identity.

A formalization that bounds only the standard error of $f_{\hat w}$, drops $T$, uses the Euclidean ball, or lets the estimator see $\theta^\star$ would be a different and easier statement; the goal rules each of these out.

A complete development needs one-sided Hoeffding bounds for weighted sums of independent bounded variables on a finite product space (Mathlib has the measure-theoretic version, ProbabilityTheory.measure_sum_ge_le_of_iIndepFun with hasSubgaussianMGF_of_mem_Icc) and the transfer between the finite-sum encoding and a product measure. Both are reusable beyond this mission. Proofs of any milestone, and a bridge lemma from bprob to Measure.pi, are welcome. The other missions of this series (Gaussian lower bound, Bernoulli lower bound for linear classifiers, Gaussian upper bound) formalize the paper's remaining main results.

Selected references

• L. Schmidt, S. Santurkar, D. Tsipras, K. Talwar, A. Mądry, Adversarially Robust Generalization Requires More Data, NeurIPS 2018; arXiv:1804.11285v2. https://arxiv.org/abs/1804.11285
• A. Madry, A. Makelov, L. Schmidt, D. Tsipras, A. Vladu, Towards Deep Learning Models Resistant to Adversarial Attacks, ICLR 2018. https://arxiv.org/abs/1706.06083
• C. Szegedy et al., Intriguing properties of neural networks, ICLR 2014. https://arxiv.org/abs/1312.6199
• I. Goodfellow, J. Shlens, C. Szegedy, Explaining and Harnessing Adversarial Examples, ICLR 2015. https://arxiv.org/abs/1412.6572
• P. Rigollet, J.-C. Hütter, High Dimensional Statistics, lecture notes, MIT, 2017. https://math.mit.edu/~rigollet/PDFs/RigNotes17.pdf

Motivation

Classifiers trained by standard methods reach high accuracy on image benchmarks and yet change their prediction under perturbations of each pixel that are invisible to a human. Training against such perturbations (adversarial training) improves robustness, but on CIFAR10 and SVHN the robust test accuracy stays far below the robust training accuracy: robust models overfit. Schmidt, Santurkar, Tsipras, Talwar and Mądry (arXiv:1804.11285, 2018) asked whether this gap is a failure of current methods or an information-theoretic fact about the number of samples needed. They introduced two simple data models in which a single sample suffices for standard accuracy and proved that robust accuracy needs many more samples.

This mission formalizes their lower bound for the second model, the Bernoulli model on the hypercube, which was designed to resemble MNIST (whose images are close to binary). In this model the lower bound holds for linear classifiers, and the paper shows separately that a non-linear classifier (thresholding followed by a linear rule) escapes it. The result therefore isolates a concrete way in which the model class, not only the amount of data, governs robust generalization.

Setting

Let $d\ge0$ and $\tau>0$. Points are $x\in\{\pm1\}^d\subset\mathbb R^d$, labels $y\in\{\pm1\}$. For a parameter $\theta^\star\in\{\pm1\}^d$, the $(\theta^\star,\tau)$-Bernoulli model draws $y$ uniformly from $\{\pm1\}$ and then, independently for every coordinate $i$, sets $x_i=y\theta^\star_i$ with probability $\tfrac12+\tau$ and $x_i=-y\theta^\star_i$ with probability $\tfrac12-\tau$ (Definition 7). The two classes are noisy copies of the opposite vertices $\pm\theta^\star$.

The adversary may move a test point anywhere in the $\ell_\infty$ ball

$$\mathcal B^\varepsilon_\infty(x)=\{x'\in\mathbb R^d:\|x'-x\|_\infty\le\varepsilon\},$$

leaving the hypercube. The $\ell_\infty^\varepsilon$-robust classification error of a classifier $f:\mathbb R^d\to\{\pm1\}$ is (Definition 3)

$$\beta(f)=\Pr_{(x,y)}\big[\exists x'\in\mathcal B^\varepsilon_\infty(x):\ f(x')\ne y\big].$$

A linear classifier is $f_w(x)=\operatorname{sgn}\langle w,x\rangle$ for $w\in\mathbb R^d$. A linear-classifier learning algorithm $g_n$ is any function from $n$ labelled samples to a weight vector $w\in\mathbb R^d$.

The lower bound is Bayesian: $\theta^\star$ is drawn uniformly from $\{\pm1\}^d$, the learner receives $n$ independent samples $S$ from the $(\theta^\star,\tau)$-model, outputs $w=g_n(S)$, and is charged the robust error of $f_w$ on a fresh sample, averaged over $\theta^\star$ and $S$. The posterior mean $\mathbb E[\theta^\star_i\mid S]=\Pr[\theta^\star_i=+1\mid S]-\Pr[\theta^\star_i=-1\mid S]$ measures how much the learner can know about coordinate $i$.

Formalization targets

Goal: Theorem 31 (p. 35)

For $0<\tau\le\tfrac14$, $0\le\varepsilon<3\tau$, $0<\gamma<\tfrac12$ and every linear learner $g_n$: if

$$n\le\frac{\varepsilon^2\gamma^2}{5000\,\tau^4\log(4d/\gamma)},$$

then

$$\mathbb E_{\theta^\star,S}\big[\beta(f_{g_n(S)})\big]\ge\tfrac12-\gamma .$$

Milestones

1. Eqs. (4)–(5), p. 33: in one dimension the posterior odds of $\theta$ equal $\prod_k\big(\tfrac{1/2+\tau}{1/2-\tau}\big)^{y_kx_k}$.
2. Lemma 29, p. 33: for $\tau\le\tfrac14$ and $n\le1/\tau^2$, with probability $1-\delta$,

$$\Big|\log\tfrac{\Pr[\theta=+1\mid S]}{\Pr[\theta=-1\mid S]}\Big|\le15\tau\sqrt{2n\log(2/\delta)} .$$

3. Proof of Theorem 31, p. 36: with probability $1-\gamma/2$, $|\mathbb E[\theta^\star_i\mid S]|\le15\tau\sqrt{2n\log(4d/\gamma)}$ for all $i$.
4. §4, p. 10: $\sup_{\|\Delta\|_\infty\le\varepsilon}\langle yw,\Delta\rangle=\varepsilon\|w\|_1$, so $w$ robustly classifies $(x,y)$ iff $\langle yw,x\rangle>\varepsilon\|w\|_1$.
5. Proof of Theorem 31, p. 37: when $\theta^\star$ has independent coordinates with means bounded by $b$ in absolute value, a fresh sample satisfies $\langle w,yx\rangle\le\frac{2\tau b}{\gamma}\|w\|_1$ with probability at least $(1-\gamma)/2$.

The goal keeps the paper's explicit constants ($5000$, $3\tau$, $\log(4d/\gamma)$) because Theorem 31 is itself the explicit form of the paper's asymptotic Theorem 9.

Significance

With $\tau\asymp d^{-1/4}$ a single sample already yields a linear classifier with small standard error (Theorem 8 of the paper), while Theorem 31 shows that for $\varepsilon$ of order $\tau$ every linear learner needs on the order of $\sqrt d/\log d$ samples to get expected robust error below $\tfrac12-\gamma$ against an $\ell_\infty$ adversary (the paper's Theorem 9 states this as $n\le c_2\varepsilon^2\gamma^2 d/\log(d/\gamma)$ for $\tau=c_1d^{-1/4}$). The companion upper bound (Theorem 10) shows that thresholding the input first makes one sample enough for any $\varepsilon<1$. Together these give a rigorous example in which robust generalization is polynomially harder than standard generalization for a model class, and in which a change of model class removes the gap.

The theorem and its proof are published and not in doubt. The platform holds no statement of this lower bound, of Lemma 29, or of the ℓ∞/ℓ1 robustness criterion for linear classifiers (searched 2026-09-26). The mission produces a checked statement of the result with every hypothesis explicit, including the tie convention and the domain of $\varepsilon$ that the printed statement leaves implicit, and a finite, measure-free encoding of a Bayesian learning lower bound that other hypercube models can reuse.

Difficulty

The obvious attempt bounds the robust error of the best classifier the learner could output, but the learner is arbitrary: it may output any $w$, including ones that use the samples in unusual ways. The argument must therefore hold for every function of the samples, which is why $\theta^\star$ is random and why the error is averaged over it; for a fixed $\theta^\star$ the learner $g_n\equiv\theta^\star$ is robust and the statement is false. The technical difficulty is to pass from "the posterior of every coordinate is nearly uniform" (a statement about $d$ separate one-dimensional problems) to a bound on the margin $\langle w,yx\rangle$ relative to $\|w\|_1$ that holds for every $w$ at once, uniformly in how $w$ spreads its weight across coordinates. Concentration of $\langle w,yx\rangle$ is not available for a general $w$ (a single heavy coordinate defeats it), so only a weak, constant-probability tail bound survives, which is why the final error is $\tfrac12-\gamma$ rather than close to $1$.

Formalization scope

Everything is finite. Hypercube points are sign vectors Fin d → Bool, labels are Bool with true ↦ $+1$, and every probability is an explicit finite sum of weights; no measure theory is involved. $\mathbb R^d$ is EuclideanSpace ℝ (Fin d). Committed conventions:

• The coordinates of $x$ are sampled independently (the reading of "sampling each coordinate" that the paper's proofs use).
• $\|\cdot\|_\infty\le\varepsilon$ and $\|w\|_1$ are written coordinatewise; the adversary's ball is the $\ell_\infty$ ball, not the Euclidean one.
• $f_w(x)=+1$ when $\langle w,x\rangle=0$ (the paper's $\operatorname{sgn}(0)$ is not in $\{\pm1\}$).
• The robust error is Definition 3's event $\exists x'\in\mathcal B^\varepsilon_\infty(x),\ f(x')\ne y$, not the margin criterion; the equivalence is milestone 4.
• Added hypotheses: $\varepsilon\ge0$ in the goal (for $\varepsilon<0$ the ball is empty and the printed statement fails at $n=0$), and $\delta>0$ in Lemma 29 (at $\delta=0$ Lean's $\log(2/0)=0$ makes it false). Posteriors are defined by Bayes' rule as ratios of joint weights.

The learner is any function of the samples to $\mathbb R^d$; restricting to a specific learner, fixing $\theta^\star$, letting the learner output an arbitrary classifier (for which the theorem is false), or bounding only the standard error ($\varepsilon=0$) would each trivialize or falsify the target and are excluded. Useful infrastructure: Hoeffding's inequality for sums of independent $\pm1$ variables, Markov's inequality over finite sums, and the ℓ∞/ℓ1 duality on EuclideanSpace. Related platform work: the other three missions of this series (the Gaussian lower bound, the Gaussian robust upper bound, and the Bernoulli thresholding upper bound). Contributions of general lemmas on finite product measures over the hypercube are welcome.

Selected references

• L. Schmidt, S. Santurkar, D. Tsipras, K. Talwar, A. Mądry, Adversarially Robust Generalization Requires More Data, arXiv:1804.11285v2, 2018; NeurIPS 2018. https://arxiv.org/abs/1804.11285
• I. Goodfellow, J. Shlens, C. Szegedy, Explaining and Harnessing Adversarial Examples, ICLR 2015. https://arxiv.org/abs/1412.6572
• A. Mądry, A. Makelov, L. Schmidt, D. Tsipras, A. Vladu, Towards Deep Learning Models Resistant to Adversarial Attacks, ICLR 2018. https://arxiv.org/abs/1706.06083
• S. Boucheron, G. Lugosi, P. Massart, Concentration Inequalities: A Nonasymptotic Theory of Independence, Oxford University Press, 2013. https://doi.org/10.1093/acprof:oso/9780199535255.001.0001

Motivation

Many estimation problems in statistics, signal processing and bioinformatics minimize a composite function $f = g + h$: a smooth convex loss $g$ plus a convex but nonsmooth penalty or constraint $h$, such as the lasso's $\ell_1$ norm or the indicator of a convex set. Proximal Newton-type methods handle such problems by minimizing, at each iterate $x_k$, a model $\hat f_k = \hat g_k + h$ in which $g$ is replaced by its second-order Taylor expansion. Widely used solvers of this kind (glmnet, newGLMNET, QUIC) never solve these model subproblems exactly; they stop an inner iterative solver early by some heuristic. Lee, Sun and Saunders (arXiv:1206.1623v13, 2014) proposed an adaptive stopping rule for the inner solver and proved that it preserves fast local convergence. This mission formalizes that local convergence theory (§3.4 of the paper).

Timeline:

• 1982: Dembo, Eisenstat and Steihaug introduce inexact Newton methods for smooth equations and prove local linear and superlinear convergence under a relative-residual condition with forcing terms $\eta_k$ (doi:10.1137/0719025).
• 1996: Eisenstat and Walker propose self-adjusting forcing terms that avoid oversolving (doi:10.1137/0917003).
• 2012–2014: Lee, Sun and Saunders transfer the relative-residual condition to composite functions, replacing gradients by composite gradient steps, and prove Theorems 3.10 and 3.11.
• 2016: Byrd, Nocedal and Oztoprak analyze inexact proximal Newton methods for $\ell_1$-regularized problems under an additional sufficient-descent condition on the subproblem (doi:10.1007/s10107-015-0941-y).

Setting

Work in $\mathbb R^n$ with the Euclidean inner product. The smooth part $g:\mathbb R^n\to\mathbb R$ is twice continuously differentiable and strongly convex with constant $m>0$: $g(y)\ge g(x)+\nabla g(x)^T(y-x)+\frac m2\|x-y\|^2$ for all $x,y$. Its gradient $\nabla g$ is Lipschitz with constant $L_1$, its Hessian $\nabla^2 g$ is Lipschitz with constant $L_2$, and $\nabla^2 g(x)\preceq MI$ for a constant $M>0$. The nonsmooth part $h$ is proper, closed and convex, and may take the value $+\infty$; it is given by its domain $D$ and its values on $D$. The problem is $\min_x f(x)=g(x)+h(x)$, and $x^\star$ denotes its (unique) optimal solution.

The proximal mapping of $h$ is $\operatorname{prox}_h(v)=\arg\min_y h(y)+\frac12\|y-v\|^2$. The composite gradient step with step length $t>0$ is

$$G_{tf}(x)=\tfrac1t\big(x-\operatorname{prox}_{th}(x-t\nabla g(x))\big),$$

with $G_f=G_{1f}$; it vanishes exactly at minimizers of $f$ and plays the role of the gradient. The step $G_{f/M}$ is the unit step on $f/M=g/M+h/M$. The model at $x_k$ is $\hat f_k=\hat g_k+h$ with $\hat g_k(y)=g(x_k)+\nabla g(x_k)^T(y-x_k)+\frac12(y-x_k)^T\nabla^2 g(x_k)(y-x_k)$.

The inexact proximal Newton method with unit step lengths produces $x_{k+1}=x_k+\Delta x_k$, where the direction $\Delta x_k$ is any point satisfying the adaptive stopping condition

$$\|G_{\hat f_k/M}(x_k+\Delta x_k)\|\le\eta_k\,\|G_{f/M}(x_k)\|\qquad(2.24)$$

for a forcing term $\eta_k\ge0$. The Eisenstat–Walker choice is

$$\eta_k=\min\Big\{\frac m2,\ \frac{\|G_{\hat f_{k-1}/M}(x_k)-G_{f/M}(x_k)\|}{\|G_{f/M}(x_{k-1})\|}\Big\}.\qquad(2.25)$$

Formalization targets

Goal: Theorem 3.10 (p. 17)

1. There are $\bar\eta\in(0,m/2)$, $\delta>0$ and $r\in[0,1)$ such that, whenever $0\le\eta_k\le\bar\eta$ for all $k$ and $\|x_0-x^\star\|<\delta$,

$$\|x_{k+1}-x^\star\|\le r\,\|x_k-x^\star\|\quad\text{for all }k.$$

2. For every forcing sequence with $\eta_k\ge0$, $\eta_k\to0$, there is $\delta>0$ such that every run with $\|x_0-x^\star\|<\delta$ converges to $x^\star$ q-superlinearly: for every $\varepsilon>0$, eventually $\|x_{k+1}-x^\star\|\le\varepsilon\|x_k-x^\star\|$.

Both parts are asserted together. The statement fixes no constant beyond the existence of $\bar\eta$, $\delta$ and $r$.

Milestones

• §2.1, property 3: $G_f(x)=0$ if and only if $x$ minimizes $f$.
• Lemma 2.2: $\|G_f(x)\|\le(L_1+1)\|x-x^\star\|$.
• Lemma 3.8: $\|G_f(x)-G_{\hat f_k}(x)\|\le\frac{L_2}2\|x-x_k\|^2$.
• Lemma 3.9: $(x-y)^T(G_{tf}(x)-G_{tf}(y))\ge\frac m2\|x-y\|^2$ for $0<t\le1/L_1$.
• Theorem 3.11: with the forcing terms (2.25), the method converges q-superlinearly from every start sufficiently close to $x^\star$.

Significance

Theorem 3.10 justifies stopping the inner solver of a proximal Newton method at a relative accuracy that is set by the current optimality measure $\|G_{f/M}(x_k)\|$: a constant small forcing term keeps linear convergence, and forcing terms that decay to zero recover superlinear convergence, with no sufficient-descent condition on the subproblem and for a generic nonsmooth $h$. Theorem 3.11 shows that the self-adjusting choice (2.25) achieves the superlinear regime automatically. Together they are the composite analogue of the inexact Newton theory used in most large-scale smooth solvers.

The results are proved in the paper. No machine-checked proof of any of them is known, and the platform contains no proximal mapping, composite gradient step or inexact Newton condition. A formalization adds a checked proximal-operator toolkit (existence and nonexpansiveness of $\operatorname{prox}$, the optimality characterization of $G_f$, strong monotonicity of $G_{tf}$) and a precise form of the theorem: the paper's proofs mix two scalings of the composite step and cite a lemma where another is meant, so the formal proof settles which constants are valid.

Difficulty

The obvious argument compares the inexact step with the exact proximal Newton step and treats the gap as a perturbation. For composite functions this fails: the exact step is defined by a nonsmooth inclusion, and the stopping condition bounds a residual of the model's composite gradient step, not the distance to the model's minimizer. The link between the two is strong monotonicity of the composite gradient step (Lemma 3.9), which requires controlling the proximal mapping of a general closed convex $h$ jointly with the curvature of $g$; for $h=0$ it is immediate, and for general $h$ it is the central step. A second difficulty is that the threshold on $\eta_k$ is not scale invariant: a threshold below $m/2$ chosen arbitrarily does not give convergence, so the admissible $\bar\eta$ has to come out of the analysis.

Formalization scope

The space is EuclideanSpace ℝ (Fin n). The nonsmooth part is a pair $(D,h)$: $D$ nonempty and convex, $h$ convex on $D$, and the extended function ($h$ on $D$, $+\infty$ off $D$) lower semicontinuous; indicator functions of closed convex sets are included. The proximal mapping is a total function chosen among the minimizers over $D$, which exist uniquely under these hypotheses. $G_{f/M}$, $G_{\hat f_k/M}$ and $G_{tf}$ are functions of the split $(g,D,h)$ and a scalar, never of $f$ alone. The Hessian is the derivative of the gradient map, measured in operator norm. Sequences are indexed from $k=0$; a run requires $x_0\in D$ and $x_k+\Delta x_k\in D$. Rates are stated without quotients.

"$x_0$ sufficiently close to $x^\star$" is an existential radius chosen before the run; assuming $x_k\to x^\star$, letting the radius depend on the run, or reading part 1 as "for every $\bar\eta<m/2$" (which is false: $g(x)=2x^2$, $h=0$, $\eta_k\equiv\frac32$ diverges) are ruled out. The forcing sequence of Theorem 3.10 is fixed in advance; that of Theorem 3.11 depends on the iterates through (2.25), with a free first term $\eta_0\in[0,m/2]$.

A complete development needs existence, uniqueness and firm nonexpansiveness of the proximal mapping of an extended-valued closed convex function, the subgradient characterization of $\operatorname{prox}$, and a second-order Taylor bound for $C^2$ functions with Lipschitz Hessian. These are reusable well beyond this mission. Contributions of any of them, of the milestones, or of alternative proofs of Lemma 3.9 are welcome.

Selected references

• J. D. Lee, Y. Sun, M. A. Saunders, Proximal Newton-type methods for minimizing composite functions, arXiv:1206.1623v13, 2014; SIAM J. Optim. 24(3), 2014. https://arxiv.org/abs/1206.1623
• R. S. Dembo, S. C. Eisenstat, T. Steihaug, Inexact Newton methods, SIAM J. Numer. Anal. 19(2), 1982. https://doi.org/10.1137/0719025
• S. C. Eisenstat, H. F. Walker, Choosing the forcing terms in an inexact Newton method, SIAM J. Sci. Comput. 17(1), 1996. https://doi.org/10.1137/0917003
• R. H. Byrd, J. Nocedal, F. Oztoprak, An inexact successive quadratic approximation method for L-1 regularized optimization, Math. Program. 157, 2016. https://doi.org/10.1007/s10107-015-0941-y

Motivation

Many estimation problems in statistics, machine learning and signal processing minimize a composite function, the sum of a smooth loss and a convex but nonsmooth regularizer or constraint: the lasso and $\ell_1$-regularized logistic regression, the graphical lasso for sparse inverse covariance estimation, and constrained least squares, where the nonsmooth part is the indicator function of a convex set. First-order proximal gradient methods (ISTA, FISTA, SpaRSA) are the standard tools, and their convergence is at best linear. Practical solvers such as glmnet, newGLMNET and QUIC instead minimize a local quadratic model of the smooth part plus the nonsmooth part at every iteration, and in practice they need far fewer iterations.

Lee, Sun and Saunders (arXiv:1206.1623, SIAM J. Optim. 2014) put these methods into one framework, proximal Newton-type methods, and proved that they inherit the local convergence rates of Newton and quasi-Newton methods for smooth problems. This mission formalizes the exact-subproblem half of their analysis, ending with q-superlinear convergence of proximal quasi-Newton methods whose Hessian approximations satisfy the Dennis–Moré criterion.

Timeline. Dennis and Moré (1974) characterized superlinear convergence of quasi-Newton methods for smooth equations and minimization by what is now called the Dennis–Moré condition. Tseng and Yun (2009) analyzed coordinate gradient descent for composite problems with a scaled quadratic model. Byrd, Nocedal and Oztoprak (2013) studied inexact proximal Newton methods for $\ell_1$-regularized problems. Lee, Sun and Saunders (2012–2014) proved quadratic and superlinear local convergence for a generic closed convex $h$.

Setting

The problem is

$$\min_{x\in\mathbb R^n} f(x) := g(x) + h(x). \qquad (1.1)$$

The smooth part $g:\mathbb R^n\to\mathbb R$ is twice continuously differentiable and strongly convex with constant $m>0$, meaning $g(y)\ge g(x)+\nabla g(x)^T(y-x)+\tfrac m2\|x-y\|^2$ for all $x,y$ (Definition 3.2). Its gradient $\nabla g$ and Hessian $\nabla^2 g$ are Lipschitz continuous with constants $L_1$ and $L_2$. The nonsmooth part $h$ is a proper closed convex function that may take the value $+\infty$. Its effective domain $D=\operatorname{dom} h$ is nonempty and convex, and $x^\star$ denotes the optimal solution of (1.1), which is unique by strong convexity.

At an iterate $x_k$ the method chooses a symmetric positive definite matrix $H_k$ and computes the search direction $\Delta x_k$, the minimizer of the model subproblem

$$\Delta x_k=\arg\min_d\ \nabla g(x_k)^Td+\tfrac12 d^TH_kd+h(x_k+d). \qquad (2.9)$$

The predicted decrease is $\lambda_k=\nabla g(x_k)^T\Delta x_k+h(x_k+\Delta x_k)-h(x_k)$. A step length $t$ satisfies the sufficient descent condition (2.19) if $f(x_k+t\Delta x_k)\le f(x_k)+\alpha t\lambda_k$ for a fixed $\alpha\in(0,\tfrac12)$. A backtracking line search with factor $\beta\in(0,1)$ takes $t_k=\beta^{j}$ for the least $j\ge0$ that passes, so the unit step is tried first. The update is $x_{k+1}=x_k+t_k\Delta x_k$ (Algorithm 1). With $H_k=\nabla^2 g(x_k)$ this is the proximal Newton method. With any other choice of $H_k$ it is a proximal quasi-Newton method. The sequence $\{H_k\}$ satisfies the Dennis–Moré criterion if

$$\frac{\|(H_k-\nabla^2 g(x^\star))(x_{k+1}-x_k)\|}{\|x_{k+1}-x_k\|}\to0. \qquad (3.2)$$

Formalization targets

Goal: Theorem 3.7

If $mI\preceq H_k\preceq MI$ for all $k$, with $0<m\le M$, and $\{H_k\}$ satisfies (3.2), then every run of Algorithm 1 from any $x_0\in D$ satisfies

$$x_k\to x^\star,\qquad \|x_{k+1}-x^\star\|=o(\|x_k-x^\star\|).$$

The goal fixes no rate constant. It asserts only the shape of the convergence.

Milestones

In the order the proof uses them:

1. Proposition 2.4: $\lambda\le-\Delta x^TH\Delta x$ and $f(x+t\Delta x)\le f(x)+t\lambda+O(t^2)$.
2. Proposition 2.5: $x$ is optimal if and only if $\Delta x=0$ at $x$.
3. Lemma 2.6: every $t\le\min\{1,(2m/L_1)(1-\alpha)\}$ satisfies (2.19).
4. Theorem 3.1 (global convergence), restated under the assumptions of §3.3: $x_k\to x^\star$.
5. Lemma 3.3: the proximal Newton method eventually accepts the unit step.
6. Theorem 3.4: the proximal Newton method converges q-quadratically, with eventually

$$\|x_{k+1}-x^\star\|\le\frac{L_2}{2m}\|x_k-x^\star\|^2 .$$

7. Lemma 3.5 / A.1: under (3.2) the unit step is eventually accepted.
8. Proposition 3.6: $\|\Delta x_1-\Delta x_2\|\le\sqrt{(1+\bar\theta)/m}\,\|(H_2-H_1)\Delta x_1\|^{1/2}\|\Delta x_1\|^{1/2}$, with $\bar\theta$ depending only on the eigenvalue bounds.

Significance

The result. Theorem 3.7 is the composite counterpart of the Dennis–Moré theorem. It says that the rate of a proximal quasi-Newton method is governed by how well $H_k$ approximates the Hessian of the smooth part along the steps actually taken, whatever the nonsmooth part is. It covers proximal BFGS-type methods for $\ell_1$-regularized and constrained problems, and it explains why solvers built on these methods reach high accuracy in few iterations. Theorem 3.4 gives the corresponding quadratic rate when the exact Hessian is used.

Formalizing it. The results are proved in the paper. None of them has a machine-checked proof: the platform currently has Newton's method only for smooth objectives (Boyd–Vandenberghe's quadratic phase in the mission Convex Optimization V: Newton's Method), and nothing on proximal or composite Newton-type methods. The formalization also settles two defects of the printed text. Theorem 3.1 is false as printed, since it lacks an upper bound on $H_k$: with $g(x)=x^2/2$, $h=0$ and $H_k=2^{k+1}$ the iterates stall at about $0.289\,x_0$. It is therefore stated here under the assumptions of §3.3. Proposition 3.6 uses an undefined constant $m_1$ (read as $m$), and the first-order inequalities in its printed proof contain a typo. The explicit constant $L_2/(2m)$ in Theorem 3.4 is the one the paper's proof derives.

Difficulty

The difficulty is the nonsmooth part. For smooth $g$ the Newton step solves a linear system, and the classical analysis works with that closed form. Here $\Delta x_k$ is defined only as the minimizer of a nonsmooth subproblem, and every estimate on it has to come from the optimality of that minimizer, i.e. from the firm nonexpansiveness of scaled proximal maps in a norm that changes with $H_k$. A natural first idea is to apply the smooth Dennis–Moré argument to $\nabla f$. It fails because $f$ is not differentiable and may be $+\infty$ outside $D$. The superlinear rate also depends on the line search eventually accepting the unit step. That acceptance comes only from a third-order Taylor bound combined with (2.15) and the Dennis–Moré residual, and a line search that may return any admissible step does not give it.

Formalization scope

• Space. The space is EuclideanSpace ℝ (Fin n), and matrices are continuous linear operators. $\nabla g$ is Mathlib's gradient, and $\nabla^2 g$ is fderiv ℝ (gradient g). "Positive definite" includes symmetry, and $mI\preceq H\preceq MI$ is stated through quadratic forms of a symmetric $H$.
• The nonsmooth part. $h$ is encoded by its domain $D$ and its values on $D$: $D$ is nonempty and convex, $h$ is convex on $D$, and the $+\infty$-extension of $h$ is lower semicontinuous. The objective $f$ is extended-valued. Only comparisons are made in EReal, never arithmetic. Replacing $h$ by a real-valued function on all of $\mathbb R^n$ would exclude indicator functions and is not the paper's setting.
• Algorithm. The search direction is a predicate: it minimizes (2.9) over $\{d : x+d\in D\}$. Backtracking is the least-$j$ rule with factor $\beta\in(0,1)$, the convention of Boyd and Vandenberghe, whom the paper cites for its line search. Runs are infinite and indexed from $k=0$, with no stopping test.
• Rates. $o(\cdot)$ and (3.2) are stated without quotients: for every $\varepsilon>0$ the inequality holds eventually.
• Ruling out trivial versions. A line search allowed to return any step satisfying (2.19) would make Theorems 3.4 and 3.7 false. Taking $x^\star$ to be an arbitrary point instead of the minimizer, or letting $\bar\theta$ in Proposition 3.6 depend on the data, would empty the statements. None of these readings is used.
• Infrastructure. A complete development needs: existence and uniqueness of minimizers of strongly convex, lower semicontinuous extended functions; first-order optimality for the subproblem; firm nonexpansiveness of scaled proximal maps in the $H$-norm; and second- and third-order Taylor bounds from Lipschitz derivatives. These pieces are reusable across proximal methods. Contributions of any milestone, of these supporting lemmas, or of the goal directly are welcome.

Selected references

• J. D. Lee, Y. Sun, M. A. Saunders, Proximal Newton-type methods for minimizing composite functions, arXiv:1206.1623v13 (2014); SIAM J. Optim. 24(3), 2014. https://arxiv.org/abs/1206.1623
• J. E. Dennis, J. J. Moré, A characterization of superlinear convergence and its application to quasi-Newton methods, Math. Comp. 28 (1974), 549–560. https://doi.org/10.1090/S0025-5718-1974-0343581-1
• P. Tseng, S. Yun, A coordinate gradient descent method for nonsmooth separable minimization, Math. Program. 117 (2009), 387–423. https://doi.org/10.1007/s10107-007-0170-0
• R. H. Byrd, J. Nocedal, F. Oztoprak, An inexact successive quadratic approximation method for convex L-1 regularized optimization, Math. Program. 157 (2016), 375–396; arXiv:1309.3529. https://arxiv.org/abs/1309.3529
• S. Boyd, L. Vandenberghe, Convex Optimization, Cambridge University Press, 2004. https://web.stanford.edu/~boyd/cvxbook/