Optimization

Motivation

Bin packing asks for the fewest unit-capacity bins that hold a given list of item sizes. It is one of the first problems studied through the worst-case analysis of approximation algorithms, and it models storage allocation, paging and file placement on tracks, as well as cutting-stock problems in operations research. Deciding the optimum exactly is NP-hard, so the practical question is how badly simple rules can do. The two simplest on-line rules, First-Fit and Best-Fit, are still the baseline against which every later bin-packing heuristic is measured.

Timeline:

• 1972. Garey, Graham and Ullman announce that First-Fit uses at most about $1.7$ times the optimal number of bins (Proc. 4th ACM STOC, 1972); Johnson's thesis (MIT, 1973) develops the analysis.
• 1974. Johnson, Demers, Ullman, Garey and Graham prove $FF(L)\le 1.7L^*+2$ and $BF(L)\le 1.7L^*+2$ for every list, and give lists with $FF(L)=BF(L)>1.7L^*-8$ for every optimum $L^*=k$, so the asymptotic worst-case ratio of both rules is exactly $\tfrac{17}{10}$ (SIAM J. Comput. 3(4)). This paper is the source of the mission.
• 1976–2014. The additive constant is lowered: Garey, Graham, Johnson and Yao (1976) show $FF(L)\le\lceil 1.7L^*\rceil$, and Dósa and Sgall prove the tight bound $FF(L)\le\lfloor 1.7L^*\rfloor$ (STACS 2013) and the same bound for Best-Fit (ICALP 2014).

Setting

A list is a finite sequence $L=(a_1,a_2,\dots,a_n)$ of real numbers in $(0,1]$; values may repeat. A bin has capacity $1$, and its level is the sum of the numbers in it. The optimum $L^*$ is the minimum number of bins into which the elements of $L$ can be placed so that no bin contains numbers whose sum exceeds $1$.

Both rules place $a_1,\dots,a_n$ in this order into bins $B_1,B_2,\dots$, each initially at level $0$, and never move an element once placed.

1. First-Fit (FF) places $a_i$ into the bin $B_j$ of least index whose level $\beta$ satisfies $\beta\le 1-a_i$.
2. Best-Fit (BF) places $a_i$ into a bin whose level $\beta$ satisfies $\beta\le 1-a_i$ and is as large as possible, taking the least index among ties.

$FF(L)$ and $BF(L)$ are the numbers of nonempty bins at the end. The worst-case ratio at optimum $k$ is

$$R_{FF}(k)=\sup\Bigl\{\frac{FF(L)}{L^*}:L^*=k\Bigr\},\qquad R_{BF}(k)=\sup\Bigl\{\frac{BF(L)}{L^*}:L^*=k\Bigr\}.$$

The analysis also uses a weighting function $W:[0,1]\to[0,1]$, piecewise linear with $W(\alpha)=\tfrac65\alpha$ on $[0,\tfrac16]$, $\tfrac95\alpha-\tfrac1{10}$ on $(\tfrac16,\tfrac13]$, $\tfrac65\alpha+\tfrac1{10}$ on $(\tfrac13,\tfrac12]$ and $1$ on $(\tfrac12,1]$, and the coarseness of a bin of a completed packing: the largest $1-\operatorname{level}(B')$ over the bins $B'$ of smaller index, and $0$ for the first bin.

Formalization targets

Goal: the asymptotic ratio (Corollary of Section 2, p. 306)

$$\lim_{k\to\infty}R_{FF}(k)=1.7\qquad\text{and}\qquad\lim_{k\to\infty}R_{BF}(k)=1.7.$$

The goal fixes only the asymptotic ratio and leaves the additive constants free, so it is the statement that survives the later improvements of the constants.

Milestones, in the order the proof uses them

• Claim 2.2.1 (p. 304): a bin with total size at most $1$ has $\sum_i W(b_i)\le\tfrac{17}{10}$.
• Claim 2.2.2 (p. 305): in an FF or BF packing, every element placed into a bin before the bin was more than half full exceeds the bin's coarseness.
• Claim 2.2.3 (p. 305): a bin of coarseness $\alpha<\tfrac12$ whose level exceeds $1-\alpha$ has weight at least $1$.
• Claim 2.2.4 (p. 306): a bin of coarseness $\alpha<\tfrac12$ with weight $1-\beta$, $\beta>0$, either holds a single element at most $\tfrac12$ or has level at most $1-\alpha-\tfrac59\beta$.
• Theorem 2.2 (p. 304): $FF(L)\le 1.7L^*+2$ and $BF(L)\le 1.7L^*+2$ for every list.
• Theorem 2.1 (p. 301): for every $k\ge1$ there is a list with $L^*=k$ and $FF(L)=BF(L)>1.7L^*-8$.

A companion item, not a milestone, records the explicit list of Fig. 3 (p. 307) with $L^*=10$ and $FF(L)=BF(L)=17$.

Significance

The result fixes the worst-case behaviour of the two simplest bin-packing heuristics: neither ever uses more than about $70\%$ more bins than an optimal packing, and both can be forced to. The weighting-function technique introduced for this bound became the standard method for analysing bin-packing heuristics, including First-Fit Decreasing, Harmonic-type algorithms and on-line lower bounds, and the constant $\tfrac{17}{10}$ is the reference point for later on-line algorithms.

The theorem is proved, and its constants have since been sharpened. No machine-checked proof of any of these results is known. This mission produces a Lean model of on-line bin packing (the optimum, the First-Fit and Best-Fit runs with their placement history, and the worst-case ratio) that the other missions of this paper and later bin-packing formalizations can reuse. It also produces formal proofs of the weighting-function bounds, of the $1.7L^*+2$ upper bound and of the lower-bound construction.

Difficulty

The first idea, charging each bin its level, gives only $FF(L)\le 2L^*+1$: at most one bin is at most half full. The ratio $\tfrac{17}{10}$ comes from bins that are more than half full but far from full, and a bound on the total size of the elements cannot see them. No property of the final packing alone suffices: the bins that are far from full can only be controlled through the order in which the rule opened and filled them, so the argument depends on the dynamics of the run. On the lower-bound side, the natural periodic list (sizes near $\tfrac16,\tfrac13,\tfrac12$, p. 301) gives only the ratio $\tfrac53$; reaching $\tfrac{17}{10}$ needs a list on which both rules waste space in every medium bin, for every $k$, while $L^*$ is still known exactly.

Formalization scope

A list is L : List ℝ with the hypothesis IsList L (every element in $(0,1]$), and every statement assumes it. $L^*$ is optBins L, the least b : ℕ for which some assignment Fin L.length → Fin b has every bin sum at most $1$. A run is a fold over the list that keeps only the nonempty bins, in index order, each with its contents in placement order. A new bin is opened at the end exactly when no nonempty bin fits, which is the paper's "least $j$" over infinitely many initially empty bins, since elements are positive. The fit test is the non-strict $\beta+a_i\le1$, and Best-Fit breaks ties by least index. The placement history (the bin chosen for each element and that bin's level just before) is read off the run on the prefix of the list. Indices are $0$-based. Coarseness is computed in the completed packing. $W$ is a function ℝ → ℝ and is only ever applied to elements of $(0,1]$. $R_{FF}(k)$ and $R_{BF}(k)$ are suprema in the extended nonnegative reals $[0,\infty]$, and the limit is taken there.

A real-valued supremum would be $0$ on an empty or unbounded family, and the limit statement would then say nothing about the algorithms. The extended-real supremum rules this trivialization out. Every claim is stated for the concrete First-Fit run and the concrete Best-Fit run, not for an abstract rule with the properties used in the proof.

Claim 2.2.4 is printed with alternative (i) "$m=1$ and $b_1<\tfrac12$", which is false: First-Fit on $(0.6,0.5)$ gives a counterexample. The mission states it with $b_1\le\tfrac12$, which is what the paper's proof establishes and what the main proof uses. The milestone text keeps the printed version.

The model definitions are reusable for any on-line bin-packing rule, since the run is parameterized by the choice rule. Contributions welcome: proofs of the milestones, general lemmas about the runs (levels stay at most $1$, at most one bin is at most half full, the history determines the final packing), and the computation of $L^*$ for the explicit lists of Theorem 2.1 and Fig. 3.

Selected references

• D. S. Johnson, A. Demers, J. D. Ullman, M. R. Garey, R. L. Graham, Worst-Case Performance Bounds for Simple One-Dimensional Packing Algorithms, SIAM Journal on Computing 3(4):299–325, 1974. https://doi.org/10.1137/0203025
• M. R. Garey, R. L. Graham, J. D. Ullman, Worst-case analysis of memory allocation algorithms, Proc. 4th ACM STOC, 1972.
• D. S. Johnson, Near-Optimal Bin Packing Algorithms, PhD thesis, MIT, 1973.
• M. R. Garey, R. L. Graham, D. S. Johnson, A. C. Yao, Resource constrained scheduling as generalized bin packing, J. Combinatorial Theory Ser. A 21, 1976.
• G. Dósa, J. Sgall, First Fit bin packing: A tight analysis, STACS 2013, LIPIcs 20:538–549. https://doi.org/10.4230/LIPIcs.STACS.2013.538
• G. Dósa, J. Sgall, Optimal analysis of Best Fit bin packing, ICALP 2014, LNCS 8572.

Motivation

Minimizing the average completion time of jobs that arrive over time is one of the basic objectives of machine scheduling: it measures how long, on average, a job waits in the system. On a single machine with release dates and no preemption (written $1|r_j|\sum C_j$), the problem is strongly NP-hard, so research has focused on approximation algorithms whose guarantees are stated against every feasible schedule.

The standard route runs through the preemptive relaxation. When jobs may be interrupted and resumed, the shortest-remaining-processing-time rule (SRPT) produces an optimal schedule, and its value is a lower bound for every nonpreemptive schedule. The question is how to turn that preemptive schedule into a nonpreemptive one without losing too much.

Timeline:

• 1995, Phillips, Stein and Wein (WADS 1995, pp. 86–97): order the jobs by their SRPT completion times and schedule them nonpreemptively in that order. This gives a 2-approximation. Later 2-approximations are by Hoogeveen and Vestjens (IPCO 1996), Stougie (1995), and Goemans (SODA 1997). Hoogeveen and Vestjens also showed that deterministic on-line algorithms cannot beat 2.
• 2001, Chekuri, Motwani, Natarajan and Stein (SIAM J. Comput. 31(1)): order by $\alpha$-points instead of completion times, choose $\alpha$ at random, and take the best $\alpha$ off-line. This gives the $e/(e-1)\approx1.58$ bound for Best-$\alpha$ that is the goal of this mission, and an optimal randomized on-line algorithm.
• 1999, Afrati et al. (FOCS 1999): a polynomial-time approximation scheme for $1|r_j|\sum w_jC_j$. This settled the approximability of the problem, but the resulting algorithms are far from simple.

Setting

An instance has $n$ jobs $J_0,\dots,J_{n-1}$. Job $J_j$ has a processing time $p_j>0$, a release date $r_j\ge0$, and, where the objective is weighted, a weight $w_j>0$. There is one machine.

A nonpreemptive schedule assigns each job a start time $S_j\ge r_j$ such that the intervals $[S_j,S_j+p_j)$ are pairwise disjoint. Its completion times are $C_j=S_j+p_j$.

A preemptive schedule $P$ specifies, for each time $t$, which job runs at $t$, if any. Job $J_j$ runs only at times $t\ge\max(0,r_j)$, receives exactly $p_j$ units of processing in total, and finishes by some finite time. Its completion time $C^P_j$ is the first time by which all of $J_j$ has been processed. For $\alpha\in(0,1]$, its $\alpha$-point $C^P_j(\alpha)$ is the first time by which $\alpha p_j$ units have been processed.

For a job $J_i$, $T_i$ denotes the idle time of $P$ before $C^P_i$. $x_{ij}$ denotes the fraction of $J_j$ processed before $C^P_i$. The paper writes $S^P_i(\beta)$ for the set of jobs with $x_{ij}=\beta$, and also for their total processing time.

One-machine list scheduling in a given order runs the jobs nonpreemptively in that order. Each job starts at the later of its release date and the completion of the previous job in the list. An $\alpha$-schedule is list scheduling in nondecreasing order of the $\alpha$-points $C^P_j(\alpha)$. $C^\alpha_j$ denotes the completion times of an $\alpha$-schedule.

Random-$\alpha$ draws $\alpha$ from a distribution on $(0,1]$ and outputs the $\alpha$-schedule. Best-$\alpha$ outputs the $\alpha$-schedule of smallest total completion time $\min_\alpha\sum_j C^\alpha_j$.

Formalization targets

Goal: Corollary 2.7

Let $P$ be optimal among preemptive schedules for $\sum_j C_j$. Then there is $\alpha\in(0,1]$ such that every $\alpha$-schedule derived from $P$ satisfies

$$\sum_j C^\alpha_j\;\le\;\frac{e}{e-1}\sum_j C_j\qquad\text{for every feasible nonpreemptive schedule } (C_j)_j .$$

Since Best-$\alpha$ returns a schedule no worse than this $\alpha$-schedule, Best-$\alpha$ is an $e/(e-1)$-approximation.

Milestones

1. The calculus behind the constant. For $f(\alpha)=e^\alpha/(e-1)$ and every $\beta\in(0,1]$,

$$\int_0^\beta\frac{1+\alpha-\beta}{\beta}f(\alpha)\,d\alpha=\frac1{e-1}.$$

2. Lemma 2.2: $C^P_i=T_i+\sum_{0<\beta\le1}\beta S^P_i(\beta)$.
3. Lemma 2.3: $C^\alpha_i\le T_i+(1+\alpha)\sum_{\beta\ge\alpha}S^P_i(\beta)+\sum_{\beta<\alpha}\beta S^P_i(\beta)$.
4. Lemma 2.5: if $\alpha$ has density $f$ on $(0,1]$, then $E[C^\alpha_i]\le(1+\delta)C^P_i$ with $\delta=\max_{0<\beta\le1}\int_0^\beta\frac{1+\alpha-\beta}{\beta}f(\alpha)\,d\alpha$.
5. Theorem 2.6, for the weighted objective with $P$ optimal among preemptive schedules: the expected approximation ratio of Random-$\alpha$ is at most $2$ for uniform $\alpha$, at most $1.8$ for $\alpha=1$ w.p. $3/5$ and $\alpha=1/2$ w.p. $2/5$, and at most $e/(e-1)$ for the density $e^\alpha/(e-1)$.

Companion statements, not milestones:

• the upper bound of Theorem 2.1, $\sum_jC^\alpha_j\le(1+1/\alpha)\sum_jC^P_j$;
• the existence of an optimal preemptive schedule.

Significance

The $e/(e-1)$ bound shows that conversion from the preemptive relaxation can beat the factor 2 of the natural ordering. It does so by exploiting that no single instance is bad for many values of $\alpha$ at once. The $\alpha$-point technique was also used with LP relaxations, for example by Goemans (SODA 1997) and by Schulz and Skutella. The randomized version is an optimal randomized on-line algorithm for $1|r_j|\sum C_j$. Lemma 2.3 is a statement about any preemptive schedule, so it applies wherever a good preemptive or fractional schedule is available.

All results of the mission are proved in the paper, except that the proof of Theorem 2.6, part 2 is omitted there. No machine-checked proof of them is known. A complete development would give a verified model of preemptive one-machine schedules, $\alpha$-points and list scheduling, together with the averaging argument over $\alpha$. These are reusable for the later results of the same paper and for the $\alpha$-point literature.

Difficulty

The obvious argument bounds each job's $\alpha$-schedule completion time directly against its preemptive completion time. That argument loses a factor $1+1/\alpha$ (Theorem 2.1), which is at least 2 for every fixed $\alpha$. The improvement needs Lemma 2.3. There the charge to each job depends on how much of it was done by $C^P_i$ relative to $\alpha$, and the idle time $T_i$ is not inflated at all. Proving Lemma 2.3 requires reasoning about a preemptive schedule as a measure on time, and about how moving pieces of jobs changes completion times. A proof that treats the preemptive schedule as a finite list of pieces must first show that nothing is lost by this discretization.

The averaging step needs the expectation over $\alpha$ to be an honest integral. The map $\alpha\mapsto C^\alpha_i$ must be shown integrable, which requires a fixed rule for ties between equal $\alpha$-points.

Formalization scope

• Model. Jobs are Fin n, time is real, $p_j>0$ and $r_j\ge0$. The paper admits $p_j=0$ only in its tightness instances.
  • A preemptive schedule is a function $\sigma:\mathbb R\to$ Option (Fin n) (none = idle). Each job's run set is measurable, lies in $[\max(0,r_j),\infty)$, is bounded above, and has Lebesgue measure $p_j$.
  • Completion times and $\alpha$-points are infima of nonempty sets that are bounded below.
  • $T_i$ is the measure of the idle set in $[0,C^P_i)$.
  • The paper's sums over $\beta$ are sums over jobs, weighted by the fraction $x_{ij}$.
• List scheduling is strict: jobs never overtake the list order, and the machine is free from time $0$.
  • Lemma 2.3, Theorem 2.1, Theorem 2.6.2 and the goal hold for every tie-break among equal $\alpha$-points.
  • The expectations (Lemma 2.5, Theorem 2.6.1 and 2.6.3) use the tie-break by job index. They assert integrability as part of the conclusion.
• Optimality. "Approximation ratio $c$" is stated as an inequality against every feasible nonpreemptive schedule, never against an infimum.
  • The optimality of $P$ among preemptive schedules is the paper's standing assumption for its upper bounds (p. 151). It appears as a hypothesis of Theorem 2.6 and of the goal.
  • The lemmas hold for arbitrary $P$ and do not carry it.
  • An existence statement shows the hypothesis can be met.
• Lemma 2.5's $\delta$ is replaced by any upper bound of the integrals over $\beta\in(0,1]$. This is equivalent, and it avoids assuming that the maximum is attained.
• Not stated:
  • the running time $O(n^2)$ of Best-$\alpha$ and the optimality of SRPT;
  • the tightness parts of Theorem 2.1 and Corollary 2.4, and the lower bounds of Theorem 2.9, which use zero-length jobs;
  • the on-line Theorem 2.8, which needs a model of on-line algorithms.
• Trivializing formalization ruled out. Dropping the optimality of $P$ from the goal would turn it into a statement about arbitrary preemptive schedules, which is Lemma 2.5, not Corollary 2.7. Comparing against $\sum_jC^P_j$ instead of every nonpreemptive schedule would likewise remove the content of the corollary.

Contributions are welcome at every level. The calculus milestone and Lemma 2.2 are good first targets.

Selected references

• C. Chekuri, R. Motwani, B. Natarajan, C. Stein, Approximation Techniques for Average Completion Time Scheduling, SIAM J. Comput. 31(1):146–166, 2001. https://doi.org/10.1137/S0097539797327180
• C. Phillips, C. Stein, J. Wein, Scheduling jobs that arrive over time, Proc. 4th Workshop on Algorithms and Data Structures (WADS), 1995, pp. 86–97 (reference [25] of the paper; no link verified).
• J. A. Hoogeveen, A. P. A. Vestjens, Optimal on-line algorithms for single-machine scheduling, Proc. 5th IPCO, 1996, pp. 404–414 (reference [21]; no link verified).
• M. X. Goemans, Improved approximation algorithms for scheduling with release dates, Proc. 8th ACM-SIAM SODA, 1997, pp. 591–598 (reference [12]; no link verified).
• F. Afrati et al., Approximation schemes for minimizing average weighted completion time with release dates, Proc. 40th FOCS, 1999 (reference [2]; no link verified).

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 uncapacitated facility location (UFL) problem is one of the basic models of location theory and operations research: a firm chooses which warehouses, plants or servers to open, paying a fixed cost for each open site and a service cost for every client according to its distance to the nearest open site. It is also a standard test case for approximation algorithms.

Local search is the simplest of these and the one most used in practice: start from any set of open facilities and repeatedly add, drop or exchange one facility while this lowers the cost. The question is how bad a solution can be when no such move helps. Arya, Garg, Khandekar, Meyerson, Munagala and Pandit (SIAM J. Comput. 33(3), 2004) answered it for UFL with an exact constant.

Timeline. Korupolu, Plaxton and Rajaraman (SODA 1998, J. Algorithms 2000) analysed local search with add, drop and swap moves and proved a locality gap of at most 5; their analysis contains the service cost bound restated here as Lemma 4.1. Charikar and Guha (FOCS 1999) proved a locality gap of 3 for a different local search, in which one facility is added and any number are dropped. Arya et al. (STOC 2001; journal version 2004) proved that the add/drop/swap neighbourhood itself has locality gap at most 3, and gave an instance showing that 3 cannot be improved (§4.3).

Setting

A metric instance consists of a finite set $C$ of clients, a finite set $F$ of facilities, and a distance $d$ on $C \cup F$ that is nonnegative, symmetric and satisfies the triangle inequality. The cost of serving client $j$ by facility $i$ is $c_{ji} = d(j,i)$; the distance $c_{ii'}$ between two facilities is also available. Each facility $i \in F$ has an opening cost $f_i \ge 0$.

A solution is a nonempty set $S \subseteq F$ of open facilities. Every client is served by its nearest open facility, so

$$\mathrm{cost}_f(S) = \sum_{i \in S} f_i, \qquad \mathrm{cost}_s(S) = \sum_{j \in C} \min_{i \in S} c_{ji}, \qquad \mathrm{cost}(S) = \mathrm{cost}_f(S) + \mathrm{cost}_s(S).$$

The neighbourhood of $S$ is the set of solutions reachable by adding one facility, dropping one facility, or swapping one open facility for another:

$$\mathcal B(S) = \{S + \{s'\}\} \cup \{S - \{s\} \mid s \in S\} \cup \{S - \{s\} + \{s'\} \mid s \in S\}.$$

$S$ is locally optimum if $\mathrm{cost}(S) \le \mathrm{cost}(S')$ for every $S' \in \mathcal B(S)$. The locality gap is the supremum, over all instances, of the ratio between the cost of a worst local optimum and the cost of a global optimum.

The proofs use the following notation, which appears in the milestones but not in the goal. Fix a second solution $O$ and nearest-facility assignments $\sigma_S : C \to S$, $\sigma_O : C \to O$; write $S_j = c_{j\sigma_S(j)}$, $O_j = c_{j\sigma_O(j)}$, $N_S(s) = \sigma_S^{-1}(s)$, $N_O(o) = \sigma_O^{-1}(o)$ and $N^o_s = N_O(o) \cap N_S(s)$. A facility $s \in S$ captures $o \in O$ if $|N^o_s| > \tfrac12 |N_O(o)|$; $s$ is good if it captures no facility of $O$ and bad otherwise. The proof of the facility cost bound uses a permutation $\pi$ of the clients that maps each $N_O(o)$ onto itself, moves every client of a non-capturing block $N^o_s$ out of that block (Property 3.1), and fixes every client of a capturing block that it would map into the same block.

Formalization targets

Goal: Theorem 4.3

$$\mathrm{cost}(S) \le 3 \cdot \mathrm{cost}(O) \quad \text{for every locally optimum } S \text{ and every solution } O.$$

This is the locality gap bound of Theorem 4.3 (p. 557) in its strongest printed form: $O$ is any solution, not only an optimal one.

Milestones

1. Lemma 4.1 (service cost), p. 554: $\mathrm{cost}_s(S) \le \mathrm{cost}_f(O) + \mathrm{cost}_s(O)$.
2. The refined mapping $\pi$ of the proof of Lemma 4.2, p. 555: such a permutation exists for any two assignments.
3. Inequality (5), p. 555: the drop move for a good facility $s$,

$$-f_s + \sum_{j \in N_S(s),\ \pi(j) \neq j} (O_j + O_{\pi(j)} + S_{\pi(j)} - S_j) + 2 \sum_{j \in N_S(s),\ \pi(j) = j} O_j \ge 0.$$

4. Inequality (6), pp. 555–556: the swap of a bad facility $s$ with the facility $o$ it captures that is nearest to it.
5. Inequality (8), p. 556: for a bad facility $s$ capturing the set $P \subseteq O$, the analogue of (5) with $\sum_{o' \in P} f_{o'} - f_s$ in place of $-f_s$.
6. Lemma 4.2 (facility cost), p. 555: $\mathrm{cost}_f(S) \le \mathrm{cost}_f(O) + 2 \cdot \mathrm{cost}_s(O)$.

A companion item, not a milestone, states the bound in the proof of Theorem 4.4 with $\alpha = \sqrt2$: a local optimum of the instance with facility costs $\sqrt2 f_i$ costs at most $(1+\sqrt2)\,\mathrm{cost}(O)$ in the original instance.

Significance

The result. Theorem 4.3 shows that the simplest local search for metric UFL is within a factor 3 of optimal at every local optimum, with no LP and no rounding, and the tight example of §4.3 shows the analysis cannot be improved for this neighbourhood. Because Lemmas 4.1 and 4.2 hold against every solution $O$, scaling the facility costs before running local search trades the two bounds against each other and gives the $1 + \sqrt2 + \epsilon$ guarantee of Theorem 4.4. The same capture-and-reassign technique is used for k-median (§3) and capacitated facility location (§5).

Formalizing it. The theorem is proved on paper; no machine-checked proof of it or of any locality gap bound for facility location is known to this mission. A formal development would check the reassignment arguments, which are stated case by case in the paper, and would produce reusable Lean infrastructure for metric facility location instances, nearest-facility costs and neighbourhood-based local optimality.

Difficulty

The service cost bound is routine; the facility cost bound is where the work lies. The natural first idea, closing a facility $s \in S$ and sending each of its clients to the facility of $S$ nearest to that client's optimal facility, fails when $s$ serves most of the clients of some $o \in O$: the nearest facility of $S$ to $o$ may be $s$ itself, so the client has nowhere to go. The proof separates good facilities, which can be dropped, from bad ones, which must be swapped with a captured facility, and pays for the clients that cannot be moved through the distance between $s$ and its nearest captured facility. The combinatorial core is the construction of a permutation within each $N_O(o)$ that avoids every non-capturing block and has fixed points only where they are unavoidable.

Formalization scope

Clients and facilities are finite types Cl and Fa. The distance is a real-valued function on Cl ⊕ Fa that is nonnegative, symmetric and satisfies the triangle inequality; $d(x,x) = 0$ is not assumed, since the paper neither states nor uses it. Opening costs are a function f : Fa → ℝ with 0 ≤ f i, and demands are unit, as in the paper.

Solutions are nonempty Finsets. The service cost is $\sum_j \min_{i \in S} c_{ji}$ (Finset.inf') and is defined only for nonempty sets, so no junk value for $\emptyset$ enters. Accordingly the drop move is considered only when a facility remains open; with at least one client, $\emptyset$ cannot serve anyone and is not a solution. Local optimality is required for all moves of $\mathcal B(S)$: every added facility, every dropped facility and every swap, not only the moves used in the proof. The goal is stated as the multiplied-out inequality $\mathrm{cost}(S) \le 3\,\mathrm{cost}(O)$ for every nonempty $O$, never as a ratio, since $\mathrm{cost}(O)$ may be $0$.

In the milestones, the nearest-facility assignments $\sigma_S$, $\sigma_O$ are arbitrary among the nearest ones (ties broken arbitrarily), and the family of bijections $\pi : N_O(o) \to N_O(o)$ is a single permutation of the clients with $\sigma_O \circ \pi = \sigma_O$. Inequality (5) assumes at least one client, which the paper assumes implicitly: with no clients and $S = \{s\}$ it would read $-f_s \ge 0$. The goal and Lemma 4.2 need no such assumption.

A statement that assumes local optimality only for the moves the proof uses, that fixes $O$ to be a global optimum defined by hypotheses, or that allows the empty set a zero service cost would be a different theorem; none of these is used.

Needed infrastructure: sums over nearest-facility assignments and their fibers $N_O(o)$, the permutation $\pi$, and bookkeeping of the three kinds of moves. The instance, cost and local optimality definitions are reusable for other local search analyses of metric location problems. Proofs of any milestone are welcome, as are alternative proofs of the goal.

Selected references

• V. Arya, N. Garg, R. Khandekar, A. Meyerson, K. Munagala, V. Pandit, Local Search Heuristics for k-Median and Facility Location Problems, SIAM J. Comput. 33(3):544–562, 2004. https://doi.org/10.1137/S0097539702416402
• M. R. Korupolu, C. G. Plaxton, R. Rajaraman, Analysis of a Local Search Heuristic for Facility Location Problems, J. Algorithms 37(1):146–188, 2000. https://doi.org/10.1006/jagm.2000.1100
• M. Charikar, S. Guha, Improved Combinatorial Algorithms for the Facility Location and k-Median Problems, FOCS 1999, 378–388. https://doi.org/10.1109/SFFCS.1999.814609

Motivation

Bilinear programs, which minimize an objective containing a term $x^\top y$ over constraints on $x$ and $y$, model pooling and blending in petroleum refining, location–allocation, certain dynamic production problems and many other applications (Konno 1971, surveyed in Al-Khayyal and Falk 1983, p. 274). The term $x^\top y$ is not convex, so such problems can have local minima that are not global. For example, $\min\{xy : -1 \le x \le 2,\ -2 \le y \le 3\}$ has local solutions at $(-1, 3)$ and $(2, -2)$. When $x$ and $y$ are constrained separately, a solution lies at an extreme point of the feasible region, and vertex-enumeration and cutting-plane methods apply. When the constraints couple $x$ and $y$, this property is lost.

Al-Khayyal and Falk (Math. Oper. Res. 8(2), 1983) gave a branch-and-bound algorithm for this jointly constrained case. It lower-bounds the objective on each box by the convex envelope of the bilinear term, and they proved that it converges to a global solution. The closed form of that envelope, found independently by McCormick (1976) and now called the McCormick envelope, underlies the bilinear relaxations of modern global solvers.

Timeline:

• 1969, Falk and Soland: a branch-and-bound scheme for separable nonconvex programs using convex envelopes, the pattern this algorithm follows.
• 1976, McCormick: convex underestimators of factorable functions, including the envelope of $xy$ on a rectangle.
• 1983, Al-Khayyal and Falk: the envelope of $xy$ over a rectangle (Theorem 2), the branch-and-bound algorithm for jointly constrained biconvex programs, and a proof of its convergence.

Setting

Fix $n \ge 1$ and a box $\Omega = \{(x,y) \in \mathbb{R}^n \times \mathbb{R}^n : l \le x \le L,\ m \le y \le M\}$ with coordinate rectangles $\Omega_i = [l_i, L_i] \times [m_i, M_i]$. Problem $\mathcal P$ is

$$\min\ \varphi(x,y) = f(x) + x^\top y + g(y) \quad \text{subject to } (x,y) \in S \cap \Omega,$$

with $f$, $g$ convex (and continuous) on their boxes, $S$ closed and convex, and $S \cap \Omega \neq \emptyset$. Its optimal value is $v^*$.

The convex envelope $\mathrm{Vex}_B\, h$ of a function $h$ over a set $B$ is the pointwise supremum of all convex functions that underestimate $h$ on $B$. For a box $B$, the node function $\psi^B(x,y) = f(x) + \mathrm{Vex}_B\, x^\top y + g(y)$ is convex and lies below $\varphi$ on $B$. The subproblem at node $B$, minimizing $\psi^B$ over $S \cap B$, is a convex program.

A run of the algorithm is a sequence of stages. Stage $0$ has the single open node $\Omega$. At stage $k$ the Best Bound Rule selects an open node $B_k$ whose subproblem value is least, and the stage point $(x^k, y^k)$ is its subproblem solution. The best lower bound is $v_b^k = \psi^{B_k}(x^k, y^k)$ and the best upper bound is $V_b^k = \min_{l \le k} \varphi(x^l, y^l)$. The selected node is then split. The algorithm picks the coordinate $I$ with the largest gap $x^k_i y^k_i - \mathrm{Vex}_{(B_k)_i}\, x_i y_i$ and replaces the rectangle $(B_k)_I$ by the four subrectangles cut out by the point $(x^k_I, y^k_I)$ (Figure 1 of the paper). All other rectangles are kept. The stage function $\psi^k$ assigns to each point of $\Omega$ the least node value $\psi^B$ among the open boxes containing it.

Formalization targets

Goal: convergence to a global solution

For every run,

$$\text{every accumulation point } (\bar x, \bar y) \text{ of } (x^k, y^k) \text{ solves } \mathcal P, \qquad \lim_k v_b^k = v^* = \lim_k V_b^k .$$

Milestones

In attack order:

• Theorem 2: $\mathrm{Vex}_\Omega\, xy = \max\{mx + ly - lm,\ Mx + Ly - LM\}$ on a rectangle.
• Theorem 3: the envelope is exact on the rectangle's boundary.
• The Corollary, in two parts:
  • separability, $\mathrm{Vex}_\Omega\, x^\top y = \sum_i \mathrm{Vex}_{\Omega_i}\, x_i y_i$;
  • exactness at points whose every coordinate pair lies on $\partial\Omega_i$.
• Along runs: $\psi^k \le \psi^{k+1} \le \varphi$ on $\Omega$.
• The bound chain $v_b^1 \le v_b^2 \le \cdots \le v^* \le \cdots \le V_b^2 \le V_b^1$.
• Termination when $v_b^k = V_b^k$.
• The gradient bound $\gamma_i$.
• The equicontinuity estimate $\|z - w\| < \varepsilon/(n\gamma) \Rightarrow |\mathrm{Vex}_B\, x^\top y(z) - \mathrm{Vex}_B\, x^\top y(w)| < \varepsilon$ within every sub-box $B$.
• The limit identity: along a convergent subsequence of stage points, $v_b^{k_t} \to \varphi(\bar x, \bar y)$.

Theorem 4 of the paper, on the envelope of $\sum f_i(x_i) + x^\top y + \sum g_i(y_i)$ with concave $f_i, g_i$, is included as a further target.

Significance

The convergence theorem certifies that the algorithm computes the global optimum of a nonconvex problem. It is not a local search. Its ingredients carry over to spatial branch-and-bound in general: envelopes that are exact on the boundary of their box, a subdivision at the relaxation's solution, and best-bound selection. Theorem 2 and its separable extension are the building block of McCormick relaxations, used for bilinear terms throughout global optimization.

As far as is known, none of these results is formalized. The mission produces a formal model of a spatial branch-and-bound procedure with rectangular subdivision at the relaxation solution, together with the convex-envelope facts it rests on. The paper's convergence proof is informal and, as printed, passes through two claims that do not hold (see Formalization scope). A machine-checked proof of the convergence theorem would settle the result on firm ground.

Difficulty

The algorithm splits at the relaxation's solution, not at the midpoint, so the boxes of a run need not shrink to points. The usual "exhaustive subdivision" argument, in which the diameters of nested boxes tend to zero, does not apply. What makes the gap close is Theorem 3: after a split, the split point sits on the boundary of the new rectangles in the split coordinate, where the envelope is exact. That exactness has to be carried from the selected points to their accumulation points, across coordinates that may be split finitely or infinitely often. The obvious route through a continuous limit of the stage functions is not available, because the stage functions are not continuous in general.

Formalization scope

Vectors are Fin n → ℝ, points are pairs in (Fin n → ℝ) × (Fin n → ℝ), and boxes are four bound vectors, degenerate boxes allowed. The convex envelope is the paper's definition, the real supremum of values of convex minorants, and is used only at points of convex boxes. The McCormick closed form is Theorem 2, a target, and is not built into any definition. A run is a predicate on four sequences: open nodes as a multiset of boxes, selected node, branching index, stage point. Stages are numbered from $0$ and runs are infinite: the stopping test is ignored, so a run stopped by the paper is a prefix of one. The optional pruning of p. 278 is omitted, and ties are arbitrary. The optimal value enters through IsMinOn, not through an infimum. The Euclidean distance on $\mathbb{R}^{2n}$ is written out explicitly.

Hypotheses and corrections relative to the page:

• Continuity of $f$ and $g$ on their boxes is added; the paper uses it without stating it. $n > 0$ is assumed. The box form of convexity (p. 276) is used.
• Corollary, second clause (p. 276): "for all $(x,y) \in \partial\Omega$" is false for $n \ge 2$ (take $\Omega_1 = \Omega_2 = [0,2]^2$, $x = y = (0,1)$). It is stated for points with every $(x_i, y_i) \in \partial\Omega_i$.
• Well-definedness of the stage function (p. 277) is false from stage 3 on. Two open boxes can share a point at which their node functions differ, and the stage function then jumps. It is not a target. The stage function takes the minimum over the open boxes containing a point, and the continuity asserted on p. 279 is not formalized. The piecewise convexity asserted there is formalized as convexity of each open node function on its box.
• Equicontinuity (p. 282): the display $|H_i^{kj}(x_i,y_i) - H_i^{kj}(u_i,v_i)| \le |x_i y_i - u_i v_i|$ is false, and so is equicontinuity of the stage functions on all of $\Omega$. The estimate is stated within each sub-box, with the paper's $\delta = \varepsilon/(n\gamma)$.

Two trivializations are excluded. The goal is not a statement about an arbitrary sequence of boxes and points whose gap tends to zero: it quantifies over runs of the algorithm as defined, and a separate well-posedness item, run_exists, asserts that runs exist for every instance. Theorem 2 is about the supremum of convex minorants, not about a function defined by the closed form.

Reusable beyond this mission: the convex envelope and its bilinear closed form, and the box-splitting model. Contributions welcome: proofs of the envelope theorems, a proof of run_exists, and a convergence proof that avoids the false intermediate claims.

Selected references

• F. A. Al-Khayyal and J. E. Falk, Jointly Constrained Biconvex Programming, Mathematics of Operations Research 8(2):273–286, 1983. https://doi.org/10.1287/moor.8.2.273
• J. E. Falk and R. M. Soland, An Algorithm for Separable Nonconvex Programming Problems, Management Science 15(9):550–569, 1969. https://doi.org/10.1287/mnsc.15.9.550
• G. P. McCormick, Computability of Global Solutions to Factorable Nonconvex Programs: Part I — Convex Underestimating Problems, Mathematical Programming 10:147–175, 1976. https://doi.org/10.1007/BF01580665
• H. Konno, Bilinear Programming: Part II. Applications of Bilinear Programming, Technical Report 71-10, Operations Research House, Stanford University, 1971 (reference [10] of Al-Khayyal and Falk; no online copy known). https://doi.org/10.1287/moor.8.2.273

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