All missions

Why closed-form ADMM updates for ℓ1 problems

Many estimation problems in statistics, machine learning and signal processing minimize a smooth loss plus a nonsmooth ℓ1-type regularizer: the lasso, basis pursuit, least absolute deviations, Huber fitting, the group lasso, and ℓ1-penalized maximum likelihood for Gaussian graphical models. Chapter 6 of Boyd, Parikh, Chu, Peleato and Eckstein, Distributed Optimization and Statistical Learning via the Alternating Direction Method of Multipliers (Found. Trends Mach. Learn. 3(1), 2011), shows that the alternating direction method of multipliers (ADMM) splits each of these problems into a step that touches only the loss and a step that touches only the regularizer, and that each step has a closed form. The practical value of ADMM on these problems rests entirely on those closed forms: an iteration is one cached linear solve, one projection, or one thresholding.

The capstone is sparse inverse covariance selection (§6.5), the ℓ1-penalized Gaussian maximum-likelihood problem of Banerjee, El Ghaoui and d'Aspremont (2008), also solved by the graphical lasso of Friedman, Hastie and Tibshirani (2008). Its ADMM X-update minimizes a log-determinant objective over positive definite matrices, and the book shows that it is solved exactly by one symmetric eigenvalue decomposition.

Setting

All vectors are real and $\|\cdot\|_2$ is the Euclidean norm. For $\kappa\in\mathbb R$ the soft thresholding operator is $S_\kappa(a)=a-\kappa$ if $a>\kappa$, $0$ if $|a|\le\kappa$, and $a+\kappa$ if $a<-\kappa$, applied componentwise to vectors and entrywise to matrices. The vector soft thresholding operator on $\mathbb R^m$ is $\mathcal S_\kappa(a)=(1-\kappa/\|a\|_2)_+a$, with $\mathcal S_\kappa(0)=0$. The Huber penalty is $g^{\mathrm{hub}}(a)=a^2/2$ for $|a|\le1$ and $|a|-1/2$ for $|a|>1$, summed over components for vectors.

In scaled-form ADMM for minimizing $f(x)+g(z)$ subject to $Ax+Bz=c$, with penalty $\rho>0$ and scaled dual variable $u$, the updates are

$$x^{k+1}=\operatorname*{argmin}_x\bigl(f(x)+\tfrac\rho2\|Ax+Bz^k-c+u^k\|_2^2\bigr),\quad z^{k+1}=\operatorname*{argmin}_z\bigl(g(z)+\tfrac\rho2\|Ax^{k+1}+Bz-c+u^k\|_2^2\bigr),$$

followed by $u^{k+1}=u^k+Ax^{k+1}+Bz^{k+1}-c$. "The update is given by formula $F$" means $F$ is the unique minimizer of the corresponding subproblem.

For sparse inverse covariance selection, $S\in\mathbb R^{n\times n}$ is symmetric (the empirical covariance), $\lambda>0$ is the regularization weight, $\|M\|_F^2=\sum_{ij}M_{ij}^2$, $\|M\|_1=\sum_{ij}|M_{ij}|$, and $\mathbb S^n_{++}$ is the set of symmetric positive definite matrices, the domain of $\log\det$. ADMM alternates

$$X^{k+1}=\operatorname*{argmin}_{X\in\mathbb S^n_{++}}\Bigl(\operatorname{Tr}(SX)-\log\det X+\tfrac\rho2\|X-Z^k+U^k\|_F^2\Bigr),\qquad Z^{k+1}=\operatorname*{argmin}_Z\Bigl(\lambda\|Z\|_1+\tfrac\rho2\|X^{k+1}-Z+U^k\|_F^2\Bigr),$$

and $U^{k+1}=U^k+X^{k+1}-Z^{k+1}$.

Formalization targets

Goal: the X-update in closed form (§6.5, p. 47)

Let $S$ and $Z-U$ be symmetric, $\rho>0$, and $\rho(Z-U)-S=Q\,\mathrm{diag}(\mu_1,\dots,\mu_n)\,Q^T$ with $Q^TQ=QQ^T=I$. Then

$$X=Q\,\mathrm{diag}\Bigl(\frac{\mu_i+\sqrt{\mu_i^2+4\rho}}{2\rho}\Bigr)Q^T$$

is positive definite and is the unique minimizer of $\operatorname{Tr}(SX')-\log\det X'+\frac\rho2\|X'-Z+U\|_F^2$ over $X'\in\mathbb S^n_{++}$.

Milestones

1. Scalar root (p. 47): for $\rho>0$, $t=(\mu+\sqrt{\mu^2+4\rho})/(2\rho)$ is positive and $\rho t-1/t=\mu$.
2. Equation (6.5) (p. 47): the matrix $X$ above is positive definite and $\rho X-X^{-1}=\rho(Z-U)-S$.
3. First-order condition (p. 47): a positive definite $X$ minimizes the X-objective over $\mathbb S^n_{++}$ if and only if $S-X^{-1}+\rho(X-Z+U)=0$.
4. Z-update (p. 47): $Z_{ij}=S_{\lambda/\rho}(X_{ij}+U_{ij})$ is the unique minimizer of $\lambda\|Z\|_1+\frac\rho2\|X-Z+U\|_F^2$.
5. Huber z-update (§6.1.1, p. 40): with $v=Ax-b+u$, $z=\frac{\rho}{1+\rho}v+\frac1{1+\rho}S_{1+1/\rho}(v)$ minimizes $g^{\mathrm{hub}}(z)+\frac\rho2\|Ax-z-b+u\|_2^2$.
6. Basis pursuit (§6.2, p. 41): if $AA^T$ is invertible, $(I-A^T(AA^T)^{-1}A)(z-u)+A^T(AA^T)^{-1}b$ is the projection of $z-u$ onto $\{x\mid Ax=b\}$.
7. Lasso (§6.4, p. 43): $(A^TA+\rho I)^{-1}(A^Tb+\rho(z-u))$ minimizes $\frac12\|Ax-b\|_2^2+\frac\rho2\|x-z+u\|_2^2$, and $S_{\lambda/\rho}(x+u)$ minimizes $\lambda\|z\|_1+\frac\rho2\|x-z+u\|_2^2$.
8. Group lasso (§6.4.2, p. 45): blockwise $\mathcal S_{\lambda/\rho}(x_i+u_i)$ minimizes $\lambda\sum_i\|z_i\|_2+\frac\rho2\sum_i\|x_i-z_i+u_i\|_2^2$.

Significance

The closed forms are what make ADMM competitive on these problems. For the lasso the x-update is a ridge regression whose factorization is computed once; for basis pursuit it is a cached projection; the ℓ1 step is a componentwise threshold. For covariance selection the X-update costs one eigenvalue decomposition, and the book (p. 46) cites Scheinberg, Ma and Goldfarb (2010) as showing that ADMM outperforms state-of-the-art methods on this problem. The goal also yields that $X^{k+1}$ is always positive definite, so the iterates remain in the domain of $\log\det$ without a line search.

All statements here are classical and their proofs are elementary convex analysis and linear algebra. A search of the platform found no machine-checked version of any of them. Formalizing them produces verified proximity operators (soft thresholding, vector soft thresholding, Huber, projection onto an affine set) and a verified matrix-function argument for $\log\det$ that later missions on ADMM, proximal methods and Gaussian graphical models can import.

Difficulty

The vector updates reduce to separable one-dimensional problems or to a normal equation, and the difficulty there is bookkeeping: uniqueness, the case $a=0$ of vector soft thresholding, and the three regimes of the Huber prox.

The goal is harder. The book's argument says that $X$ satisfies the gradient equation "and thus minimizes the X-minimization objective". Checking the equation is algebra; the claim to be proved is minimality over the open cone $\mathbb S^n_{++}$, which needs the convexity (indeed strict convexity, for uniqueness) of $-\log\det$ on positive definite matrices and the identification of its gradient with $-X^{-1}$ along symmetric directions. Mathlib has determinants and positive definiteness; a usable convexity statement for $\log\det$ on $\mathbb S^n_{++}$ is not among the platform's published results. Showing that $X$ satisfies (6.5) alone does not establish the goal.

Formalization scope

• Carriers. Vectors are EuclideanSpace ℝ (Fin n), matrices Matrix (Fin m) (Fin n) ℝ acting by Matrix.toEuclideanLin. The Frobenius norm and the entrywise ℓ1 norm are written as explicit sums, not through Mathlib's matrix norm instances. The vector ℓ1 norm is the platform definition HighDimStat.SparseLinear.l1Norm.
• Updates as unique minimizers. Each update is stated as: the book's formula is the unique minimizer of the subproblem (IsUniqueMinimizerOn). Iterates are not defined; the subproblem's data ($z^k$, $u^k$, $x^{k+1}$) are arbitrary.
• Domain of log det. The X-objective is minimized over Matrix.PosDef only. Singular or indefinite matrices are never competitors, so Real.log of a nonpositive determinant plays no role.
• Explicit hypotheses. $S$ and $Z-U$ are assumed symmetric in the goal and the first-order condition; $S$ need not be positive semidefinite. $\rho>0$ everywhere. Basis pursuit assumes $\det(AA^T)\ne0$, which the book uses without stating. The book's $\lambda>0$ is relaxed to $\lambda\ge0$ in the thresholding statements, which contain the book's case.
• Eigendecomposition. The goal holds for every orthogonal $Q$ and real $\mu$ with $\rho(Z-U)-S=Q\,\mathrm{diag}(\mu)Q^T$, not for one decomposition chosen by Mathlib.
• Names. The book uses $\lambda$ for both the regularization weight and the eigenvalues; Lean calls them lam and μ.
• Typo. The book prints $u^k$ in the group-lasso block update; the block $u_i^k$ is stated.
• Ruled out. A goal that only asserts that $X$ satisfies (6.5), or that minimizes over a set extended by Real.log of nonpositive determinants, is not the book's claim; the goal states unique minimality over $\mathbb S^n_{++}$.
• Not stated. Least absolute deviations and the generalized lasso updates (same pattern as milestones 5 and 7), the overlapping group lasso, and the two-step termination claim for Huber fitting on p. 40 (whose formula $x^{\mathrm{ls}}=(A^TA)^{-1}b$ is misprinted).

Contributions welcome: convexity and strict convexity of $-\log\det$ on $\mathbb S^n_{++}$ and its derivative; a general "prox of a separable function is componentwise" lemma; and the projection onto an affine set.

Selected references

• S. Boyd, N. Parikh, E. Chu, B. Peleato, J. Eckstein, Distributed Optimization and Statistical Learning via the Alternating Direction Method of Multipliers, Foundations and Trends in Machine Learning 3(1), 2011, pp. 1–122. https://doi.org/10.1561/2200000016
• O. Banerjee, L. El Ghaoui, A. d'Aspremont, Model Selection Through Sparse Maximum Likelihood Estimation for Multivariate Gaussian or Binary Data, Journal of Machine Learning Research 9, 2008, pp. 485–516. https://jmlr.org/papers/v9/banerjee08a.html
• J. Friedman, T. Hastie, R. Tibshirani, Sparse Inverse Covariance Estimation with the Graphical Lasso, Biostatistics 9(3), 2008, pp. 432–441. https://doi.org/10.1093/biostatistics/kxm045
• K. Scheinberg, S. Ma, D. Goldfarb, Sparse Inverse Covariance Selection via Alternating Linearization Methods, Advances in Neural Information Processing Systems 23, 2010 (reference [148] of the book).
• R. Tibshirani, Regression Shrinkage and Selection via the Lasso, Journal of the Royal Statistical Society B 58(1), 1996, pp. 267–288. https://doi.org/10.1111/j.2517-6161.1996.tb02080.x
• M. Yuan, Y. Lin, Model Selection and Estimation in Regression with Grouped Variables, Journal of the Royal Statistical Society B 68(1), 2006, pp. 49–67. https://doi.org/10.1111/j.1467-9868.2005.00532.x

Motivation

The cutting stock problem asks how to cut standard stock rolls of length $L$ into pieces of demanded lengths $l_1,\dots,l_m$ so that the demands are met at least cost. Gilmore and Gomory solved its linear programming relaxation by column generation (Part I, Opns. Res. 9 (1961)): every cutting pattern is a column, and the column to bring into the basis is found by solving an integer knapsack problem whose objective is given by the current dual prices. In Part II (Opns. Res. 11 (1963)) they replaced the dynamic-programming knapsack solver of Part I by a lexicographic enumeration with a bound test, the Knapsack Method, and reported it to be about five times as fast as dynamic programming on their problem set (p. 866). The method is an early enumeration-with-bounds (branch-and-bound type) procedure for the integer knapsack, and the same pricing problem remains the inner loop of column generation for cutting stock, bin packing and their many variants.

Setting

There are $m$ demanded lengths $l_1,\dots,l_m>0$ with linear programming prices $b_1,\dots,b_m\ge0$, and $k$ standard stock lengths $L_1,\dots,L_k$ with costs $c_1,\dots,c_k$. A column for $L_j$ is a vector $(\alpha)_m=(a_1,\dots,a_m)$ of nonnegative integers with $\sum_i l_ia_i\le L_j$. The knapsack problem (1) for $L_j$ is

$$\bar M_j=\max\Big\{\sum_{i=1}^m b_ia_i : a_i\in\mathbb Z_{\ge0},\ \sum_{i=1}^m l_ia_i\le L_j\Big\},$$

and the quantity to compute is $M_j=\max(c_j,\bar M_j)$: a column improves the linear program exactly when $\bar M_j>c_j$.

For a prefix $(\alpha)_s=(a_1,\dots,a_s)$ write $\lambda\cdot(\alpha)_s=\sum_{i\le s}l_ia_i$ and $\beta\cdot(\alpha)_s=\sum_{i\le s}b_ia_i$. Step (1) sorts the data, $b_1/l_1\ge\dots\ge b_m/l_m$ and $L_1>\dots>L_k$, and appends a slack item $a_{m+1}$ with $b_{m+1}=0$, $l_{m+1}=1$. The method then generates vectors in decreasing lexicographic order:

• Steps (2) and (7) fill the coefficients after a prefix greedily, $a_i=[(L-\text{used})/l_i]$, for $L=L_1$ at the start and $L=L_t$ later.
• Step (3) records $\beta\cdot(\alpha)_m$ as the new $M_j$ for each $j\ge t$ with $L_j\ge\lambda\cdot(\alpha)_m$ and $\beta\cdot(\alpha)_m>M_j$.
• Step (4) finds the last nonzero coefficient $a_s$.
• Step (5) lowers $a_s$ by one and looks for the smallest $j$ with $L_j\ge\lambda\cdot(\alpha)_s$ and $(L_j-\lambda\cdot(\alpha)_s)b_{s+1}>(M_j-\beta\cdot(\alpha)_s)l_{s+1}$. This is the bound obtained by relaxing the integrality of $a_{s+1}$.
• Step (6) backs up to the previous nonzero coefficient when no such $j$ exists, and stops when there is none.

In Lean the method is a transition system Step on states (a, s, t, M, phase). Reachable means reachable from the start state of Step (2).

Formalization targets

Goal: the method terminates and computes $M_1$

Under Step (1)'s ordering, with $l_i>0$ and $b_i\ge0$:

$$\text{every run is finite},\quad \text{a non-final state has a successor},\quad M_1^{\text{final}}=\max\big(c_1,\bar M_1\big),$$

and at the end every $M_j$ is $c_j$ or the price of a column for $L_j$, with $c_j\le M_j$. With one stock length ($k=1$) this is the paper's correctness claim in full: the method solves the knapsack problem (1).

Milestones

1. Steps (2)/(7): the greedy completion is the lexicographically largest extension of a prefix that fits the capacity.
2. Step (4): the lexicographic predecessor of a fitting vector extends $(\alpha^1)_s$.
3. The relaxation bound $\beta\cdot(\alpha')_m\le\beta\cdot(\alpha)_s+b_{s+1}(L-\lambda\cdot(\alpha)_s)/l_{s+1}$ for every fitting extension.
4. After the inequality of Step (5)'s test fails, no vector between $(\alpha)_s$ and the successor of Step (6) improves $M$.
5. The vectors tested in Step (3) strictly decrease lexicographically.
6. The invariant on entry to Step (3).
7. Identical prices: among lengths with equal prices only the shortest is needed (p. 869).

Significance

The goal certifies the pricing oracle of the Gilmore–Gomory column-generation method: the knapsack solver it calls returns the true optimum. The pricing step is exact only if that holds, and so is the conclusion "no improving column exists, the LP is solved". Milestones 1–4 are reusable on their own. They are the textbook ingredients of lexicographic and depth-first branch-and-bound for the integer knapsack: the greedy completion, the density-ordered LP bound, and the pruning rule.

The paper's argument is a short paragraph, "clear from the order in which the $m$-vectors are generated". Writing it out shows that the claim is false for several stock lengths as the steps are printed. With $m=1$, $l_1=b_1=1$, $L=(5,2)$ and $c=(0,0)$, the method tests $(5)$. The test of Step (5) at $(4)$ then fails for $j=2$ only because $4>L_2$, Step (6) stops, and the run ends with $M_2=0$ while the column $(2)$ has price 2. This mission therefore states what the printed algorithm does achieve. The result is the full claim for $k=1$ and for the longest stock length in general. A sorry-free Lean proof of the counterexample run accompanies the mission. No part of the method or its correctness has been formalized before, as far as a search of the platform shows.

Difficulty

The method skips large parts of the lexicographic order in three ways:

• Step (7) jumps to the greedy completion for $L_t$ rather than $L_1$.
• Step (6) jumps past every smaller value of $a_s$ once one test fails.
• Step (3) updates only $j\ge t$.

Each skip has to be justified by a bound that holds for every vector skipped, and the justifications interact. A skipped vector may fit a longer stock length but not $L_t$, and the bound for $L_1$ must cover exactly those vectors. The invariant that survives all three moves is not the naive "every vector above the current one has been examined": the vectors are not examined, only bounded. Termination needs the lexicographic decrease together with finiteness of the fitting vectors, and progress needs the reachability invariants $1\le s\le m$ and $a_s\ne0$ that make Step (5) meaningful.

Formalization scope

• Items are Fin m from 0. The paper's level $s$ is a natural number, and the prefix $(\alpha)_s$ is the coordinates with index < s. Stock lengths are Fin k, and $L_1$ is index 0. The slack item enters only through $b_{s+1}$ and $l_{s+1}$ at $s=m$. The lexicographic order is Mathlib's Pi.Lex, and $[x]$ is Nat.floor.

• $M_j=\max(c_j,\bar M_j)$ is the predicate IsKnapsackMax, never a real supremum, which would be 0 on an empty set. The algorithm's output is never defined as the maximum. The goal includes termination and progress, so its correctness clause is not vacuous. Every invariant is stated for reachable states only.

• The goal adds two disclosed hypotheses:

  • $l_i>0$: demanded lengths.
  • $b_i\ge0$: with a negative price the method is wrong, and the paper applies it to cutting-stock prices, which are nonnegative.

  Step (1) is a hypothesis on the data, not a step.

• The goal also makes these corrections:

  • The claim is narrowed. For every $j$ it states $c_j\le M_j$ and attainment, and the upper bound for $L_1$ only (see Significance).
  • The lexicographic order is repaired. The page's definition misses vectors that differ in their first coefficient.
  • Step (7) reads λ·(α)_m. The page's "satisfies $L_t\ge\lambda\cdot(\alpha)_s$" is read as $\lambda\cdot(\alpha)_m$.
  • Step (4) gets a stopping case. On the zero vector, where the page has no case, the method stops.
  • Milestone 4 is stated for the failed inequality, not for a failed test, because the failed test is what makes the page's successor claim false.

• Not formalized:

  • Step (3′), the variant computing $\max_j(M_j-c_j)$.
  • The record of patterns.
  • The dynamic-programming recursion and the timing estimates.

Contributions welcome: proofs of the milestones, and a corrected multi-length variant of the method with a proof that it computes every $M_j$.

Selected references

• P. C. Gilmore, R. E. Gomory, A linear programming approach to the cutting stock problem—Part II, Operations Research 11(6) (1963), 863–888. https://doi.org/10.1287/opre.11.6.863
• P. C. Gilmore, R. E. Gomory, A linear programming approach to the cutting-stock problem, Operations Research 9(6) (1961), 849–859. https://doi.org/10.1287/opre.9.6.849
• G. B. Dantzig, Discrete-variable extremum problems, Operations Research 5(2) (1957), 266–288. https://doi.org/10.1287/opre.5.2.266

Why consensus and sharing

Many large optimization problems arising in statistics, machine learning, signal processing and resource allocation have an objective that is a sum of terms, each depending on data held by a different processor, or a coupling term that depends on the sum of the agents' decisions. Chapter 7 of Boyd, Parikh, Chu, Peleato and Eckstein's monograph on the alternating direction method of multipliers (ADMM) (Found. Trends Mach. Learn. 3(1), 2011) introduces two templates that turn such problems into distributed algorithms: consensus and sharing. Nearly every distributed application in the rest of the monograph (distributed lasso, distributed logistic regression, splitting across examples and across features in Chapter 8) is an instance of one of the two. Consensus problems in the context of ADMM go back to Bertsekas and Tsitsiklis (Parallel and Distributed Computation, 1989).

The value of the templates lies in a handful of exact algebraic facts about the ADMM subproblems: the global update is an average, the dual variables average to zero, and the sharing update, which looks like a problem in $Nn$ variables, is really a problem in $n$ variables. These facts are what this mission formalizes.

Setting

There are $N\ge1$ agents. Vectors live in $\mathbb R^n$ with the Euclidean inner product, and an overline denotes an average over agents, $\bar v=\frac1N\sum_{i=1}^N v_i$. Each local cost $f_i$ and the shared cost $g$ are functions into $\mathbb R\cup\{+\infty\}$. The penalty parameter is $\rho>0$.

Global variable consensus (§7.1) is the problem

$$\text{minimize }\sum_{i=1}^N f_i(x_i)\quad\text{subject to } x_i-z=0,\ i=1,\dots,N,$$

with local variables $x_i\in\mathbb R^n$ and a global variable $z$. ADMM alternates a parallel $x_i$-update, an averaging $z$-update and a dual update of the multipliers $y_i$. With a regularizer $g(z)$ added (7.2), the $z$-update (7.4) becomes a minimization involving $g$.

General form consensus (§7.2) lets local variable $x_i\in\mathbb R^{n_i}$ copy only some entries of $z$: entry $j$ of $x_i$ corresponds to entry $z_{\mathcal G(i,j)}$, and $\tilde z_i\in\mathbb R^{n_i}$ is defined by $(\tilde z_i)_j=z_{\mathcal G(i,j)}$. The number of local entries copying $z_g$ is $k_g$.

Sharing (§7.3) is the problem

$$\text{minimize }\sum_{i=1}^N f_i(x_i)+g\Big(\sum_{i=1}^N x_i\Big),\tag{7.11}$$

written for ADMM with copies $z_i$ of the $x_i$ (7.12). In scaled form, with $a_i=u_i^k+x_i^{k+1}$, its $z$-update is

$$(z_1^{k+1},\dots,z_N^{k+1})\in\operatorname*{argmin}_{z_1,\dots,z_N}\ g\Big(\sum_{i=1}^N z_i\Big)+(\rho/2)\sum_{i=1}^N\|z_i-a_i\|_2^2,$$

followed by $u_i^{k+1}=u_i^k+x_i^{k+1}-z_i^{k+1}$.

Formalization targets

Goal: the sharing $z$-update reduction (§7.3, p. 57)

For every $a_1,\dots,a_N$: $(z_1,\dots,z_N)$ solves the $Nn$-variable $z$-update iff $\bar z$ solves

$$\operatorname*{minimize}_{\bar z\in\mathbb R^n}\ g(N\bar z)+(\rho/2)\sum_{i=1}^N\|\bar z-\bar a\|_2^2$$

and

$$z_i=a_i+\bar z-\bar a\quad (7.13);$$

and along every run of sharing ADMM,

$$u_i^{k+1}=\bar u^k+\bar x^{k+1}-\bar z^{k+1}\quad(7.14),$$

so all scaled dual variables agree after one step.

Milestones

• §7.1: the consensus $z$-update is $z^{k+1}=\bar x^{k+1}+(1/\rho)\bar y^k$; then $\bar y^{k+1}=0$, $z^k=\bar x^k$ and the simplified iteration.
• (7.4), §7.1.1: with a regularizer, the $z$-update is averaging followed by a proximal step with weight $N\rho$; the soft-threshold ($g=\lambda\|\cdot\|_1$) and positive-part ($g$ the indicator of $\mathbb R^n_+$) examples.
• §7.2: the general form $z$-update is local averaging, and the dual entries attached to each global index sum to zero after the first iteration.
• (7.13): with $\bar z$ fixed, $z_i=a_i+\bar z-\bar a$ is the unique minimizer.

Significance

The reduction is what makes sharing ADMM scale: the central step needs only the averages $\bar x^{k+1}$, $\bar u^k$ and one $n$-dimensional proximal problem, regardless of the number of agents, and the dual state collapses to a single vector. The same reduction underlies exchange ADMM (§7.3.2) and the splitting-across-features algorithms of §8.3. The consensus facts explain why the fusion center only averages and why the dual variables can be dropped from its update.

All results of the chapter are proved, informally, in the monograph; they are elementary. To our knowledge none has a machine-checked proof. The mission produces checked statements of the update formulas that later chapters of the series and distributed-optimization developments can cite instead of re-deriving.

Difficulty

The statements are exact identities between minimizer sets of nonsmooth problems in which $g$ may be any extended-real-valued function: there is no first-order condition to use, so each step must be argued by comparing objective values, and the iff requires producing, for an arbitrary competitor, a competitor of the reduced problem with no larger value. The index bookkeeping is the other half: averages of sums of sequences indexed by agents and by iterations, the off-by-one in "after the first iteration", and in §7.2 sums over the fibres $\{(i,j):\mathcal G(i,j)=g\}$ of an index map between local vectors of different dimensions.

Formalization scope

• Vectors are EuclideanSpace ℝ (Fin n); agents are indexed by Fin N, so the book's $i=1,\dots,N$ is Lean's $i-1$; components are 0-based as well.
• An extended-real-valued function is encoded by its effective domain (a set) and its finite values; every minimization is over the domain. Convexity is not assumed: none of the stated identities needs it, so the statements are slightly more general than the chapter's standing assumption that each $f_i$ is convex.
• Iterates are hypotheses: a run is any sequence satisfying the update rules (argmin properties, not chosen minimizers). The consensus run uses the averaging formula exactly as printed on p. 49; the general form and sharing runs use the argmin form printed on pp. 55–56.
• Explicit hypotheses that the book leaves implicit: $N\ge1$, $\rho>0$, $\lambda>0$ (named lam), $k_g\ge1$ for every global index $g$ in §7.2, and the index ranges $k\ge1$ for $\bar y^{k}=0$ and $k\ge2$ for $z^k=\bar x^k$ (the starting $y^0$ is arbitrary).
• Corrected misprints: p. 52 prints $\bar x^{k+1}-(1/\rho)\bar y^k$ in the soft-threshold and positive-part examples, while the proximal form gives $\bar x^{k+1}+(1/\rho)\bar y^k$; p. 55 prints $\sum_{i=1}^m$ for $\sum_{i=1}^N$; p. 57 writes $u\in\mathbf R^m$ for a vector of $\mathbb R^n$.
• The goal is about minimizers of the $Nn$-variable $z$-subproblem, not the algebraic identity (7.13) alone, and (7.14) is derived for every run rather than built into a single-dual-variable definition; either shortcut would make the goal trivial.
• Not included: the consensus residual norms (p. 51), the duality discussion of §7.3.1 and exchange ADMM (§7.3.2). Contributions formalizing them on top of these definitions are welcome.

Selected references

• S. Boyd, N. Parikh, E. Chu, B. Peleato, J. Eckstein, Distributed Optimization and Statistical Learning via the Alternating Direction Method of Multipliers, Foundations and Trends in Machine Learning 3(1), 1–122, 2011. https://doi.org/10.1561/2200000016
• D. P. Bertsekas, J. N. Tsitsiklis, Parallel and Distributed Computation: Numerical Methods, Prentice Hall, 1989. https://web.mit.edu/dimitrib/www/pdc.html

Motivation

In two-stage optimization under uncertainty, a first-stage decision $x$ is taken before the data are known, and a second-stage decision $y$ is taken after a scenario $\omega$ is revealed. The fully adaptive formulation lets $y$ depend on $\omega$ and minimizes the worst-case cost. It is the natural model of recourse, but it optimizes over policies, one decision per scenario, and is computationally hard in general. The static robust formulation fixes one $y$ in advance that must be feasible in every scenario. It is a single deterministic mixed integer program and is the standard tractable surrogate (Ben-Tal, Goryashko, Guslitzer, Nemirovski 2004; Bertsimas & Sim 2004).

The question is how much is lost by the surrogate. Bertsimas and Goyal (2010) bound the gap by $2$ against the stochastic problem and by $4$ against the adaptive problem when the uncertainty set is symmetric. Their §5.3 identifies a case with no gap at all: when the uncertainty set is a hypercube (a box), the static robust optimum equals the adaptive optimum, and this holds even when the constraint matrices themselves are uncertain. Box uncertainty is the simplest and most common uncertainty model in practice (interval data on every coefficient), so the result says that for it, adaptivity buys nothing.

This mission formalizes that theorem, Theorem 5.4, together with Theorem 2.4, which shows that under right-hand-side uncertainty the robust problem is a single deterministic problem with the coordinatewise worst right-hand side.

Setting

Fix dimensions $m,n_1,n_2$ and sets $I_1,I_2$ of integer coordinates. The decision domains are

$$D_{I}=\{x\in\mathbb R^n : x\ge0,\ x_i\in\mathbb Z\ \text{for } i\in I\},$$

which is $\mathbb R_+^{n-p}\times\mathbb Z_+^{p}$ up to relabelling coordinates, $p=|I|$.

A scenario set $\Omega$ is given. In scenario $\omega$ the data are a constraint matrix $A(\omega)\in\mathbb R^{m\times n_1}$, a recourse matrix $B(\omega)\in\mathbb R^{m\times n_2}$, a right-hand side $b(\omega)\in\mathbb R^m$ and a second-stage cost $d(\omega)\in\mathbb R^{n_2}_+$. The first-stage cost $c\in\mathbb R^{n_1}_+$ is fixed.

• The adaptive problem $\Pi_{\mathrm{Adapt}}(A,B,b,d)$ (5.6) chooses $x\in D_{I_1}$ and $y(\omega)\in D_{I_2}$ for every $\omega$ with $A(\omega)x+B(\omega)y(\omega)\ge b(\omega)$ for all $\omega$, and has value

$$z_{\mathrm{Adapt}}=\inf\ c^Tx+\sup_{\omega\in\Omega}d(\omega)^Ty(\omega).$$

• The robust problem $\Pi_{\mathrm{Rob}}(A,B,b,d)$ (5.7) chooses one $x\in D_{I_1}$, $y\in D_{I_2}$ with $A(\omega)x+B(\omega)y\ge b(\omega)$ for all $\omega$, and has value

$$z_{\mathrm{Rob}}=\inf\ c^Tx+\sup_{\omega\in\Omega}d(\omega)^Ty.$$

The uncertainty set is $\mathcal U=\{(A(\omega),B(\omega),b(\omega),d(\omega)) : \omega\in\Omega\}$, a subset of $\mathbb R^N$ with $N=mn_1+mn_2+m+n_2$. Following Definition 1.1, $\mathcal U$ is a hypercube if $\mathcal U=[l_1,u_1]\times\cdots\times[l_N,u_N]$ for some $l_i\le u_i$.

For Theorem 2.4, $A$, $B$ and $d$ are fixed and only $b(\omega)\in\mathbb R^m_+$ varies; $\Pi_{\mathrm{Rob}}(b)$ (1.2) is the robust problem above, and $\Pi$ is the deterministic problem with right-hand side $b^h_j=\max_\omega b_j(\omega)$.

Formalization targets

Goal: Theorem 5.4 (p. 31)

If $\mathcal U$ is a hypercube, then

$$z_{\mathrm{Rob}}(A,B,b,d)=z_{\mathrm{Adapt}}(A,B,b,d).$$

The integer coordinates $I_1,I_2$ are arbitrary, and nothing is assumed about the signs of $A$, $B$, $b$.

Milestones

1. Theorem 2.4 (p. 17). Under right-hand-side uncertainty, $(x,y)$ is feasible for $\Pi_{\mathrm{Rob}}(b)$ if and only if $Ax+By\ge b^h$; hence $z_{\mathrm{Rob}}(b)=z(\Pi)$.
2. p. 31 display. $z_{\mathrm{Adapt}}(A,B,b,d)\le z_{\mathrm{Rob}}(A,B,b,d)$ for every uncertainty set.
3. Eqs. (5.8)–(5.10). If $\mathcal U$ is a hypercube, some scenario $\bar\omega$ has $A(\bar\omega)$, $B(\bar\omega)$ entrywise minimal and $b(\bar\omega)$, $d(\bar\omega)$ entrywise maximal over $\Omega$.
4. Eqs. (5.11)–(5.13). For such $\bar\omega$, if $(x,y(\cdot))$ is adaptive feasible, then $(x,y(\bar\omega))$ is robust feasible.
5. Eq. (5.14). For such $\bar\omega$, the robust worst-case cost of $(x,y(\bar\omega))$ is at most the adaptive worst-case cost of $(x,y(\cdot))$.

Significance

The result. Theorem 5.4 says that for interval uncertainty on every coefficient, the static robust program, whose size does not grow with the number of scenarios, solves the adaptive problem exactly. Combined with Theorem 2.4 for right-hand-side uncertainty, the adaptive problem collapses to one deterministic mixed integer program with worst-case data. It marks the boundary case of the paper's adaptability-gap bounds: the gap is at most $4$ for symmetric sets, and exactly $1$ for boxes.

Formalizing it. The result is proved in the paper; to our knowledge it has no machine-checked proof. The mission produces a Lean model of two-stage robust and adaptive mixed integer programs with uncertain constraint matrices, with values as extended-real infima, which other formalizations of adjustable robust optimization can build on.

Difficulty

The mathematics is elementary; the care is in the statement. The step that fails for a general uncertainty set is the existence of a single worst scenario $\bar\omega$ that is simultaneously entrywise smallest in $A$, $B$ and entrywise largest in $b$, $d$. For a set that is only contained in a box, the box's worst corner need not be realized. With two scenarios $b=(1,0)$ and $b=(0,1)$, $B=I$, $d=(1,1)$, the adaptive value is $1$ and the robust value is $2$. A formalization therefore has to state the hypercube hypothesis as an equality of sets. A second point is the arithmetic of extended reals: the paper argues from optimal solutions, which need not exist, so the inequalities must be transported through infima over feasible sets that may be empty and through suprema that may be infinite.

Formalization scope

• Decisions are vectors Fin n → ℝ; matrices are Matrix (Fin m) (Fin n) ℝ; constraints use Mathlib's componentwise order and mulVec.
• Mixed-integer domains are "nonnegative, integer on a designated coordinate set $I$", the paper's $\mathbb R_+^{n-p}\times\mathbb Z_+^p$ up to relabelling.
• Optimal values are EReal infima over the feasible set, $+\infty$ when infeasible; worst-case costs are EReal suprema over $\Omega$. No optimal solution is assumed.
• A scenario datum is a structure with the four blocks $(A,B,b,d)$; the box and the hypercube predicate are written entrywise on these blocks, which is Definition 1.1 in $\mathbb R^N$.
• The hypercube hypothesis is IsHypercube (uncertaintySet A B b d), i.e. the realized data are exactly a box. Assuming only that the data lie inside a box would make the statement false (example above); assuming fixed $A$, $B$ would state Corollary 5.1 instead of Theorem 5.4.
• Typos corrected in the Lean: (5.6)–(5.7) print $\mathbb Z^{n_2}_+$ for the second-stage integer block, read as $\mathbb Z^{p_2}_+$; §5.3's opening sentence names $\Pi_{\mathrm{Adapt}}(b,d)$ twice where the first is $\Pi_{\mathrm{Rob}}(b,d)$.
• In Theorem 2.4 the paper's $\max_\omega b_j(\omega)$ is a real supremum under the hypothesis that the right-hand sides are bounded above, and the second stage is continuous ($p_2=0$), as in the problem $\Pi$ on the page.

Contributions welcome: proofs of the milestones and of the goal, and lemmas on monotonicity of mulVec for nonnegative vectors and on EReal infima over feasible sets, which are reusable across the other missions of this series.

Selected references

• D. Bertsimas, V. Goyal, On the power of robust solutions in two-stage stochastic and adaptive optimization problems, Mathematics of Operations Research 35(2), 2010. https://doi.org/10.1287/moor.1090.0440 (cited from the authors' manuscript, MIT DSpace).
• A. Ben-Tal, A. Goryashko, E. Guslitzer, A. Nemirovski, Adjustable robust solutions of uncertain linear programs, Mathematical Programming 99, 2004. https://doi.org/10.1007/s10107-003-0454-y
• D. Bertsimas, M. Sim, The price of robustness, Operations Research 52(1), 2004. https://doi.org/10.1287/opre.1030.0065

Motivation

In just-in-time scheduling each job has a preferred time, and finishing it early is as undesirable as finishing it late. Garey, Tarjan and Wilfong (Math. Oper. Res. 13 (1988), 330–348) study the one-processor version in which task $T_i$ has a length $l_i \ge 0$ and a preferred starting time $a_i \ge 0$, and the discrepancy of a task started at time $s_i$ is $|s_i - a_i|$. The penalty is symmetric: earliness and tardiness cost the same. The paper shows that minimizing the total discrepancy is NP-complete, gives an $O(N \log N)$ algorithm for a fixed task order, and, in §3, gives an efficient algorithm for minimizing the maximum discrepancy $\max_i |s_i - a_i|$: a linear-time test for a given bound $\gamma$ after an $O(N \log N)$ sort, combined with a search over $\gamma$.

This mission formalizes the structural core of §3: the normal-form theorems (Theorem 4, Corollaries 1 and 2) on which the paper's algorithm for maximum discrepancy is built. The two companion missions of the series cover the NP-completeness result (THEOREM 1) and the fixed-order algorithm (THEOREMS 2 and 3).

Setting

Fix a bound $\gamma \ge 0$. A schedule has maximum discrepancy at most $\gamma$ exactly when every task starts no earlier than its release time $r_i = \max\{0, a_i - \gamma\}$ and finishes no later than its deadline $d_i = a_i + l_i + \gamma$ (p. 342). These release times and deadlines are in special form: with $\alpha = 2\gamma$, for every task

$$d_i - r_i = l_i + \alpha \quad\text{or}\quad \big(r_i = 0 \text{ and } d_i < l_i + \alpha\big).$$

From here on the data are arbitrary reals $l_i \ge 0$, $r_i \ge 0$, $d_i$ in special form for some $\alpha \ge 0$.

A schedule is an execution order $\sigma$ ($\sigma(p)$ is the task in position $p$) with starting times $s_i$, such that a task finishes no later than any later-positioned task starts: $s_{\sigma(p)} + l_{\sigma(p)} \le s_{\sigma(q)}$ for $p < q$. It is feasible if $r_i \le s_i$ and $s_i + l_i \le d_i$ for every $i$. Its makespan is $\max_i (s_i + l_i)$, and it is optimum if it is feasible and no feasible schedule has a smaller makespan.

Let $T_N$ be a task of largest deadline. A schedule has the release time property if every task executed after $T_N$ has release time strictly later than the starting time of $T_N$. When the tasks are indexed with $d_1 \le \dots \le d_N$, a schedule is in standard form with split index $j$, $0 \le j \le N-1$, if it begins with an optimum schedule of $T_1, \dots, T_j$, followed by $T_N$ started at the maximum of $r_N$ and the completion time of that first part, followed by $T_{j+1}, \dots, T_{N-1}$ in this order without idle time.

Formalization targets

Goal: Corollary 2 (p. 344)

$$\exists\ \text{a feasible schedule} \;\Longrightarrow\; \exists\ \text{an optimum schedule that is in standard form and has the release time property.}$$

Milestones

1. Theorem 4 (pp. 342–343): if a feasible schedule exists, some optimum schedule has the release time property with respect to any task of largest deadline.
2. The deadline split (proof of Corollary 1, p. 344): in every feasible schedule with the release time property, a task $T_i \neq T_N$ precedes $T_N$ if and only if $d_i \le s_N + \alpha$.
3. Corollary 1 (p. 344): some optimum schedule executes before $T_N$ exactly the tasks of deadline at most $\beta$, for some $\beta \ge 0$.
4. Release before finish (p. 344): every task executed after $T_N$ has $r_i \le s_N + l_N$.
5. Normalization after $T_N$ (p. 344): an optimum schedule with the release time property can be changed, without moving $T_N$ later and without touching the tasks before it, so that there is no idle time from the start of $T_N$ on and the later tasks run in deadline order.

Two companion items state the reformulation of the maximum-discrepancy bound as release times and deadlines, and the special form with $\alpha = 2\gamma$.

Significance

Corollary 2 reduces the search for an optimum schedule of $T_1, \dots, T_n$ to $n$ candidates, one per split index, each assembled from an optimum schedule of a shorter prefix. This is the dynamic program of §3.2, which the paper implements in $O(N)$ time after an $O(N \log N)$ sort; combined with a search over $\gamma$ it minimizes the maximum discrepancy. Without the special form, deciding whether one processor can meet arbitrary release times and deadlines is NP-complete (reference [4] of the paper, Garey and Johnson 1979), so the normal form is what separates the tractable case from the general one.

The results are proved in the paper; no machine-checked proof of them is known on Prove2Me. A formal proof of Corollary 2 would certify the correctness of the split-index recursion and, together with the companions, of the reduction from maximum discrepancy to this release-time/deadline problem.

Difficulty

The obvious argument fails in Theorem 4. Exchanging a straggler (a task after $T_N$ released no later than $T_N$ starts) with $T_N$ shifts the tasks between them, and for general release times and deadlines those tasks can become infeasible. The paper's argument uses the special form at every step: a task released after $T_N$ starts has $r_i > 0$, hence $d_i - r_i = l_i + \alpha$ exactly, and this equality is what bounds how far tasks may move. It also needs an extremal choice of the optimum schedule (fewest tasks after $T_N$, then fewest tasks between $T_N$ and the first straggler), which requires showing that optimum schedules exist over the reals. The passage to standard form then combines this with an earliest-deadline exchange for the tasks after $T_N$ and the replacement of the first part by an optimum sub-schedule without losing feasibility of the later tasks.

Formalization scope

Tasks are indexed by Fin N (0-based: the paper's $T_1, \dots, T_N$ are $0, \dots, N-1$; the paper's $T_N$ in Corollary 2 is the index $N-1$). All data are real. A schedule is a permutation σ : Fin N ≃ Fin N with starting times s : Fin N → ℝ; "executed before/after" refers to σ, not to a comparison of starting times, because zero-length tasks may share a starting time. Execution intervals meet at most at endpoints. The makespan is a supremum over Fin N; "optimum" quantifies over all feasible schedules, not only standard-form ones.

The standing hypotheses on every structural item are $\alpha \ge 0$, $r_i \ge 0$, $l_i \ge 0$ (from $\gamma \ge 0$, the $\max\{0, \cdot\}$ in $r_i$, and nonnegative lengths); since $s_i \ge r_i$, start times are nonnegative, as the paper assumes throughout. The special form is a hypothesis of every structural item and cannot be dropped. The paper's dummy task $T_0$ ($r_0 = d_0 = l_0 = 0$) is not a task; an empty first part completes at time $0$. Corollary 1's "the set of all tasks with deadline $\beta$ or less" is read as excluding $T_N$, the only reading under which it is true. The page's "(which can be assumed optimum)" is part of the standard form. The deadline-split and release-before-finish milestones are stated for every feasible schedule, as their arguments allow.

A trivializing formalization is excluded: the standard form pins $T_N$'s start to $\max(r_N, C)$ and the later tasks to consecutive positions in index order, so the goal is not Corollary 1 restated with an unconstrained split.

Running times ($O(N \log N)$, $O(N)$) and the algorithm of §3.2 are out of scope. The development needs only finite permutations, finite suprema and the exchange arguments of §3.1; the existence of an optimum schedule (minimum makespan over finitely many orders, earliest-start schedules) is reusable for other single-machine problems with release times and deadlines. Proofs of any milestone, and a sorry-free proof of the existence of optimum schedules, are welcome.

Selected references

• M. R. Garey, R. E. Tarjan, G. T. Wilfong, One-Processor Scheduling with Symmetric Earliness and Tardiness Penalties, Mathematics of Operations Research 13(2):330–348, 1988. https://doi.org/10.1287/moor.13.2.330
• M. R. Garey, D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman, 1979 (reference [4] of the paper, cited on p. 342 for the NP-completeness of one-processor scheduling with release times and deadlines). ISBN 0-7167-1045-5