Optimization

Motivation

Trained neural networks are increasingly embedded inside optimization models: to verify that a classifier is robust to small input perturbations, to optimize over a learned surrogate of an expensive system, or to choose decisions whose outcome is predicted by a network. When the network uses rectified linear units (ReLU), each neuron $y=\max\{0,\,w\cdot x+b\}$ is piecewise linear, and the whole network can be written exactly as a mixed-integer program (MIP) with one binary variable per neuron. How fast a branch-and-bound solver closes such a model depends on how tight the linear-programming relaxation of each neuron's formulation is.

Anderson, Huchette, Tjandraatmadja and Vielma (arXiv:1811.08359v2, the IPCO 2019 extended abstract) gave a formulation (6) of a single ReLU neuron over a box that uses only the original variables and one binary variable, and is ideal: its LP relaxation has integral extreme points (Proposition 1, p. 6). The price is an exponential family of inequalities (6b), one for every subset $I$ of the support of $w$. The present mission formalizes their Proposition 2: each of these inequalities is facet-defining, so no member of the family can be dropped without weakening the relaxation. A longer journal version of the work, with different numbering, appeared later (arXiv:1811.01988); this mission follows the extended abstract.

Setting

Fix $\eta\in\mathbb N$, a weight vector $w\in\mathbb R^\eta$, a bias $b\in\mathbb R$, and bounds $L,U\in\mathbb R^\eta$ with $L_i<U_i$ for every $i$ (§1.3, p. 4). Write $f(x)=w\cdot x+b$ and $[L,U]=\{x : L\le x\le U\}$. The sign-adjusted bounds are

$$\breve L_i=\begin{cases}L_i & w_i\ge 0\\ U_i & w_i<0\end{cases},\qquad \breve U_i=\begin{cases}U_i & w_i\ge 0\\ L_i & w_i<0\end{cases},$$

so that $M^+(f)=w\cdot\breve U+b$ and $M^-(f)=w\cdot\breve L+b$ are the maximum and minimum of $f$ over $[L,U]$. The support is $\operatorname{supp}(w)=\{i : w_i\neq 0\}$. Strict activity means $M^-(f)<0<M^+(f)$: the neuron is neither always off nor always on over the box. The paper assumes it throughout (§1.3).

Formulation (6) (p. 6) consists of the points $(x,y,z)$ with

$$\begin{aligned} &y\ge w\cdot x+b, &&\text{(6a)}\\ &y\le\sum_{i\in I}w_i\bigl(x_i-\breve L_i(1-z)\bigr)+\Bigl(b+\sum_{i\notin I}w_i\breve U_i\Bigr)z\quad\forall I\subseteq\operatorname{supp}(w), &&\text{(6b)}\\ &(x,y,z)\in[L,U]\times\mathbb R_{\ge0}\times\{0,1\}. &&\text{(6c)} \end{aligned}$$

In Lean, form6 w b L U is this set, and relax6 w b L U is its LP relaxation ($0\le z\le1$ in place of $z\in\{0,1\}$). The right-hand side of (6b) for the subset $I$ is rhs6b w b L U I x z.

An inequality $g\le0$ is facet-defining for a set $P$ when it holds on $P$, its face $F=P\cap\{g=0\}$ is nonempty, and $\dim F=\dim P-1$, the dimension of a set being that of its affine hull. The paper uses this standard notion without defining it.

Formalization targets

Goal: Proposition 2 (p. 6)

Under $L<U$ and strict activity, for every $I\subseteq\operatorname{supp}(w)$, the inequality (6b) for $I$ is facet-defining for

$$P=\operatorname{conv}\{(x,y,z) : (x,y,z)\text{ satisfies (6a)–(6c)}\}.$$

The page states the result as "Each inequality in (6b) is facet-defining", and adds right after the proof line: "We require the assumption of strict activity above, as introduced in Section 1.3."

Milestones (App. A.2, p. 15)

1. For some $\varepsilon>0$, the $\eta+2$ points $p^0=(\breve L,0,0)$, $p^1=(\breve U,f(\breve U),1)$, $\tilde p^i=(\breve L+\varepsilon\sigma_ie^i,0,0)$ for $i\notin I$, and $\tilde p^i=(\breve U-\varepsilon\sigma_ie^i,f(\breve U-\varepsilon\sigma_ie^i),1)$ for $i\in I$ are feasible with respect to (6) and satisfy (6b) for $I$ at equality; here $\sigma_i=\pm1$ is the sign of $w_i$ (with $\sigma_i=1$ when $w_i=0$).
2. For every $\varepsilon>0$ these $\eta+2$ points are affinely independent.

Significance

The result. Proposition 1 shows that (6) is ideal; Proposition 2 shows it cannot be made smaller: removing any single inequality (6b) produces a strictly weaker relaxation. Since the family has $2^{|\operatorname{supp}(w)|}$ members, this is what justifies the paper's practical recommendation to start from the big-$M$ formulation and separate inequalities of (6b) on demand (Proposition 3, p. 7) rather than to search for a smaller ideal description in the same variables. The facet structure also gives the geometric picture the paper describes after Proposition 2: each facet is the convex combination of an $(\eta-|I|)$-dimensional face at $z=0$ and an $|I|$-dimensional face at $z=1$.

Formalizing it. The result is proved in the paper, in a half-page appendix; it has not been machine-checked. The formalization adds two things. First, the proof is written for $w\ge0$ "without loss of generality by appropriately interchanging $+$ and $-$"; the Lean statements are for every sign pattern, including zero weights. Second, the appendix exhibits $\eta+2$ affinely independent points on the face, which bounds the face dimension from below; the statement that the face has dimension exactly one less than the polyhedron also needs the polyhedron to be full-dimensional and the face to lie in a proper hyperplane, steps the extended abstract leaves implicit and a complete proof must supply.

Difficulty

The arithmetic in each step is elementary. The work lies in the bookkeeping: choosing a single $\varepsilon$ that keeps every perturbed point inside the box and on the correct side of $f=0$ (this is exactly where strict activity enters), checking the perturbed points against all $2^{|\operatorname{supp}(w)|}$ inequalities of (6b) and not only the one for $I$, and turning a row-reduction argument on an $(\eta+1)\times(\eta+2)$ matrix into a statement about AffineIndependent and finrank of a vectorSpan in Lean. The natural shortcut, proving only that $\eta+2$ affinely independent tight points exist, is not Proposition 2: it says nothing about the dimension of the polyhedron itself.

Formalization scope

Inputs are Fin η → ℝ (indices $0,\dots,\eta-1$ for the paper's $1,\dots,\eta$); a point $(x,y,z)$ is p : (Fin η → ℝ) × ℝ × ℝ with p.1 = x, p.2.1 = y, p.2.2 = z. $M^\pm(f)$ are given by their closed forms $w\cdot\breve U+b$ and $w\cdot\breve L+b$. In (6b), "$i\notin I$" ranges over all indices outside $I$, zero weights included; $I$ ranges over subsets of $\operatorname{supp}(w)$, as on the page.

Every goal and milestone keeps the standing assumptions of §1.3, $L_i<U_i$ for all $i$ and strict activity, except the affine-independence milestone, which holds without them and is stated without them (a stronger statement). No other hypothesis is added. Strict activity excludes $\eta=0$, so no nonemptiness assumption on the index set is needed.

IsFacetDefining P g is the standard notion: validity, a nonempty face, and $\dim F+1=\dim P$ with dimensions the finrank of the vectorSpan. The equation is written with $+1$ on the left so that no natural-number subtraction can make the empty set or a point a facet. The polyhedron is the convex hull of the points of (6), not the set form6 itself (which is not convex, since $z\in\{0,1\}$); by Proposition 1 it equals the LP relaxation relax6, but the statement does not depend on that.

The shared objects of this paper (the ReLU graph, $\breve L$, $\breve U$, $M^\pm$, support, strict activity, formulation (6), ideality) come from the shared definitions module ReluMIP.Ideal.Setting, common to the companion mission on Proposition 1; this mission's own definitions module adds form6, IsFacetDefining, the sign inward, and the indexed family facetPts of the $\eta+2$ points. The facet notion and the affine-independence argument are reusable for other facet proofs of polyhedra in product spaces. Proofs of the milestones, of the goal, and of the full-dimensionality step are all welcome.

Selected references

• R. Anderson, J. Huchette, C. Tjandraatmadja, J. P. Vielma, Strong mixed-integer programming formulations for trained neural networks, IPCO 2019, LNCS 11480, pp. 27–42; preprint arXiv:1811.08359v2, 2019. https://arxiv.org/abs/1811.08359v2
• R. Anderson, J. Huchette, W. Ma, C. Tjandraatmadja, J. P. Vielma, Strong mixed-integer programming formulations for trained neural networks, Mathematical Programming 183 (2020), 3–39. https://doi.org/10.1007/s10107-020-01474-5
• G. L. Nemhauser, L. A. Wolsey, Integer and Combinatorial Optimization, Wiley, 1988. https://doi.org/10.1002/9781118627372
• M. Conforti, G. Cornuéjols, G. Zambelli, Integer Programming, Springer, 2014. https://doi.org/10.1007/978-3-319-11008-0
• J. P. Vielma, Mixed integer linear programming formulation techniques, SIAM Review 57 (2015), 3–57. https://doi.org/10.1137/130915303

Motivation

Brands that sell consumer goods are held responsible by the public for the labour and safety practices of their suppliers. After the 2013 Rana Plaza collapse in Bangladesh, about 200 clothing brands and retailers signed the Accord on Fire and Building Safety and inspect roughly 1,600 factories jointly; pharmaceutical companies such as Pfizer and GSK audit their suppliers jointly through the Pharmaceutical Supply Chain Initiative (both examples from the paper, pp. 4 and 14). Two features of such supply bases matter for auditing. Competing brands often share a common supplier, so a scandal at that supplier hurts both of them. And brands compete downstream, so a scandal that hurts only a rival can help a brand.

Chen, Qi and Dawande (MSOM 2020; accepted manuscript SSRN 2889889) model two competing buyers with one common and two independent suppliers. Their Proposition 2 shows that, when each buyer audits on his own, competition drives the buyers away from the common supplier: in every equilibrium it is left unaudited. This mission formalizes their Proposition 3. It shows that a coalition that audits jointly, and splits the cost by a Shapley-value rule, does audit the common supplier and is stable. A companion mission (Supplier Centrality … I) covers Proposition 2.

Setting

Two buyers $B_1, B_2$ source from three suppliers: $B_i$ from its independent supplier $S_i$, and both from the common supplier $S_c$. Each supplier is compliant with probability $e\in(0,1)$. A non-compliant supplier that passes an audit of effort $x\in[0,1]$ (probability $1-x$) is exposed in public with probability $r\in(0,1]$. An independent supplier audited with effort $x$ therefore causes damage with probability $\lambda_I(x)=r(1-e)(1-x)$. The three suppliers offend independently.

If buyer $B_i$ has $n_i\in\{0,1,2\}$ exposed suppliers, its demand intercept falls from $\alpha$ to $\alpha-d_M$ (by $d_M>0$ once, however many offend). Each exposed supplier also raises its unit input cost from $w$ to $\hat w\ge w$. The buyers then play a Cournot game with differentiated products (substitution $\beta\in(0,1]$). Buyer $B_1$'s equilibrium profit is $\pi^b_1(n_1,n_2)=(q^*_1)^2$, where

$$q^*_1=\frac{2(A_1-c_1)-\beta(A_2-c_2)}{4-\beta^2},\qquad A_i=\alpha-d_M\mathbf 1\{n_i\ge1\},\quad c_i=(2-n_i)w+n_i\hat w.$$

The aggregate ex post profit is $\pi^b(i\,d_M,j\,d_M)=\pi^b_1(i,j)+\pi^b_2(i,j)$. Auditing a supplier with effort $x$ costs $K\mathbf 1\{x>0\}+\tfrac a2x^2$.

Unilateral auditing. Each buyer audits at most one of his two suppliers. $\Pi^b_i$ is buyer $B_i$'s expected profit net of his own audit costs. An equilibrium is a pair of mutual best responses in which, by the paper's tie-breaking rule, a buyer who audits strictly prefers it to not auditing. The effort $\hat e_I$ of eq. (2) is a buyer's optimal effort on his own supplier when the rival does not audit.

Joint auditing. The coalition chooses efforts $x=(e_{c1},e_{cc},e_{c2})\in[0,1]^3$ on $S_1,S_c,S_2$, auditing at most two suppliers, and pays each audited supplier's cost once. The buyers still compete downstream. With $R^b_i(x)$ the buyers' expected profits excluding audit costs, the coalition's profit is

$$\Pi^b(x)=R^b_1(x)+R^b_2(x)-\sum_{j\in\{1,c,2\}}\Big[K\mathbf 1\{e_{cj}>0\}+\tfrac a2e_{cj}^2\Big].$$

The difference of the buyers' profits is $\Delta\Pi=R^b_1-R^b_2$. The cost shares are $\Gamma_{1,2}=\tfrac12[\text{total cost}\pm\Delta\Pi]$ (eq. (3)). The analysis assumes the scenario

$$\pi^b(0,0)\ge\pi^b(d_M,0)\ge\pi^b(d_M,d_M)\ge\pi^b(2d_M,d_M)\ge\pi^b(2d_M,2d_M).$$

Formalization targets

Goal: Proposition 3

There are thresholds $K^L_c\le K^H_c$ such that, for every $K\ge0$, an optimal joint plan

$$\begin{cases}\text{audits } S_1 \text{ and } S_c,\ \Delta\Pi>0, & K<K^L_c,\\ \text{audits only } S_c,\ \Delta\Pi=0, & K^L_c\le K<K^H_c,\\ \text{audits nothing}, & K\ge K^H_c.\end{cases}$$

The coalition is also stable. At an optimal plan its aggregate profit is at least the buyers' aggregate profit in any unilateral equilibrium. After paying $\Gamma_i$, each buyer earns at least his profit in a symmetric unilateral equilibrium.

Milestones

The coalition's profit as a sum of unilateral profits (proof of Lemma OA9). Lemma OA9: $S_c$ beats one independent supplier, and beats no audit for $K<\hat K$. Lemma OA10: $S_c$ with $S_1$ beats $S_1$ with $S_2$. Lemma OA11: $S_1$ with $S_c$ beats $S_c$ alone for $K<\tilde K$. The fair shares (3). The case analysis with $K^L_c=\min\{\frac{\hat K+\tilde K}2,\tilde K\}$ and $K^H_c=\max\{\frac{\hat K+\tilde K}2,\hat K\}$. Stability.

Significance

The result separates two effects of downstream competition on responsible sourcing. Under unilateral auditing, a buyer gains nothing private from auditing the shared supplier: the reduction in risk accrues equally to his rival. The joint coalition removes this free-riding. The common supplier is audited whenever anything is, and the Shapley-type split (3) charges the buyer who also has his own supplier audited for the competitive advantage this gives him ($\Gamma_1>\Gamma_2$ exactly when $\Delta\Pi>0$). The paper's welfare comparison (Proposition 4) builds on this proposition and on Proposition 2.

The proof in the e-companion argues through four comparisons of candidate plans and short cost-sharing algebra. None of it is machine-checked. A formal proof fixes the model (in particular which costs the coalition pays and what "at most two suppliers" excludes) and checks each comparison. In one place it also corrects the printed claim: the per-firm stability argument is given only for the symmetric unilateral equilibrium, and it does not extend to the asymmetric one (see Formalization scope).

Difficulty

All objects are explicit polynomials in the efforts. The difficulty is in the comparisons. Lemmas OA9 and OA10 compare different audit plans through the scenario ordering of aggregate ex post profits, an assumption on the stage-2 closed form that is not implied by the standing conditions. The obvious attempt, comparing first-order conditions, fails because the coalition's profit is discontinuous at zero effort (the fixed cost) and the feasible set is not convex: "at most two of three" is a union of faces of the cube. The thresholds $\hat K$, $\tilde K$ are differences of maxima, so the case analysis has to handle ties and the boundary $K=K^H_c$ with weak inequalities. Stability needs the unilateral equilibria of Proposition 2, so the full goal reaches into the companion mission's game.

Formalization scope

• Model. Params holds $\alpha,\beta,w,\hat w,d_M,e,r,a$ with $\beta\in[0,1]$, $w\le\hat w$, $d_M>0$, $e\in(0,1)$, $r\in(0,1]$, $a>0$ and the three positivity conditions of p. 8. Every statement adds $\beta>0$ (Sec. 4.3 continues the competing case) and the p. 13 scenario as five inequalities between piAgg values. Their arguments count exposed suppliers: $\pi^b(2d_M,d_M)$ is a label, not a damage of $2d_M$.
• Expected profits are 8-outcome expectations of the closed-form stage-2 profit. The coalition's profit charges each audited supplier once, and the common supplier's damage probability under a joint audit is $r(1-e)(1-e_{cc})$.
• Thresholds $\hat K,\tilde K$ are the maxima at $K=0$ written as sSup over $[0,1]$ and $[0,1]^2$. At $K=0$ the profit is a polynomial, so these suprema are attained.
• "Yields the highest aggregate profit" is read as "some maximizer over the feasible plans has this pattern"; uniqueness is not claimed. $\Delta\Pi$ is evaluated at that maximizer (its mirror image, which audits $S_2$, has $\Delta\Pi<0$).
• Cost shares use the total cost of the plan. For plans with $e_{c2}=0$ they are the printed formulas (3).
• Unilateral benchmark. The equilibrium includes the tie-breaking rule of p. 10, and the interior-effort assumption of p. 10 is encoded as $\hat e_I<1$, with $\hat e_I$ given by eq. (2).
• Stability, corrected. Condition (b) of Sec. 4.3 (each firm earns more) is stated against symmetric unilateral equilibria only, the case the paper's proof treats. Against the asymmetric equilibrium, where one buyer audits with $\hat e_I$ and the other audits nothing, it fails. Take $\alpha=10$, $\beta=1$, $w=1$, $\hat w=3$, $d_M=\tfrac12$, $e=\tfrac1{10}$, $r=1$, $a=50$, $K=0.2$: the coalition optimally audits nothing, yet the auditing buyer earns more unilaterally than half of the coalition's profit. Condition (a) is stated against every equilibrium. "Higher" is stated as $\ge$.
• The goal's thresholds are existential and come before $\forall K$. Choosing $K^L_c=K^H_c$ does not trivialize it, because the three cases must cover every $K\ge0$. The milestone on part (2) fixes the thresholds explicitly.
• The source is the authors' SSRN accepted manuscript. Main-text page numbers equal PDF pages, and e-companion page ec$k$ is PDF page $28+k$.

Contributions welcome: proofs of Lemmas OA9–OA11, which are self-contained polynomial inequalities; existence of maximizers on the non-convex feasible set (upper semicontinuity); and the link to the unilateral equilibria needed for stability.

Selected references

• F. Chen, A. Qi, M. Dawande, Supplier Centrality and Auditing Priority in Socially-Responsible Supply Chains, Manufacturing & Service Operations Management, 2020; accepted manuscript, SSRN 2889889. https://ssrn.com/abstract=2889889
• E. L. Plambeck, T. A. Taylor, Supplier evasion of a buyer's audit: Implications for motivating supplier social and environmental responsibility, Manufacturing & Service Operations Management 18(2):184–197, 2016. https://doi.org/10.1287/msom.2015.0550
• N. Singh, X. Vives, Price and quantity competition in a differentiated duopoly, RAND Journal of Economics 15(4):546–554, 1984. https://doi.org/10.2307/2555525

Motivation

Many large convex problems in signal processing, networking and statistics have a separable objective coupled by linear constraints: $K$ blocks of variables, each with its own nonsmooth regularizer and its own feasible set, tied together by $\sum_k E_kx_k=q$. The alternating direction method of multipliers (ADMM) is the standard tool for such problems when $K=2$. For $K\ge3$ the direct extension of ADMM can diverge, as shown by Chen, He, Ye and Yuan (2016), and convergence guarantees for multi-block variants typically require strong convexity or extra correction steps.

Hong, Chang, Wang, Razaviyayn, Ma and Luo propose the block successive upper-bound minimization method of multipliers (BSUM-M), which updates each primal block by minimizing a local upper bound of the augmented Lagrangian, followed by a dual gradient step, and prove that it converges for any number of blocks without strong convexity of the objective. They also analyse a randomized version, RBSUM-M, in which each iteration updates a single randomly chosen block, primal or dual. Randomized block selection matters when data or computation are distributed and not every block is available at every step. This mission formalizes the randomized half of their main theorem; the cyclic half is a separate mission.

Setting

Let $x=(x_1,\dots,x_K)$ with $x_k\in\mathbb R^{n_k}$, and consider

$$\min_x\ f(x)=g(x)+\sum_{k=1}^K h_k(x_k)\quad\text{s.t.}\quad Ex=\sum_{k=1}^K E_kx_k=q,\quad x_k\in X_k. \tag{1.1}$$

The standing assumptions (Assumption A) are: $g(x)=\ell(Ax)+\langle x,b\rangle$ with $\ell$ strictly convex and continuously differentiable; $h_k(x_k)=\lambda_k\|x_k\|_1+\sum_J w_J\|x_{k,J}\|_2$ with nonnegative weights; each $X_k=\{x_k\mid C_kx_k\le c_k\}$ is a compact polyhedron; the problem is feasible and its primal and dual optimal values are attained.

For $\rho>0$ the augmented Lagrangian and augmented dual function are

$$L(x;y)=f(x)+\langle y,q-Ex\rangle+\frac\rho2\|q-Ex\|^2,\qquad d(y)=\min_{x\in X}L(x;y),$$

and $X(y)$ is the set of minimizers of $L(\cdot;y)$ over $X=\prod_kX_k$. The method works with approximation functions $u_k(v_k;x)$ (Assumption B): $u_k(\cdot;x)$ majorizes $g+\frac\rho2\|E\cdot-q\|^2$ in block $k$, touches it with matching gradient at $x_k$, is strongly convex with modulus $\gamma_k$ and has an $L_k$-Lipschitz gradient.

RBSUM-M. Fix probabilities $p_0,\dots,p_K>0$ summing to 1. At iteration $t\ge1$ draw $k$ with probability $p_k$. If $k=0$, take a dual step $y^{t+1}=y^t+\alpha^t(q-Ex^t)$; otherwise replace block $k$ by

$$x_k^{t+1}=\arg\min_{x_k\in X_k}\ u_k(x_k;x^t)-\langle y^t,E_kx_k\rangle+h_k(x_k),$$

leaving the other blocks and $y$ unchanged. The analysis uses the block steps $\hat x_k^{t+1}$ (the minimizer above, computed for every $k$), the dual step $\hat y^{t+1}=y^t+\alpha^t(q-Ex^t)$, the gaps $\Delta_d^t=d^*-d(y^t)$, $\Delta_p^t=L(x^t;y^t)-d(y^t)$, and the proximal gradient $\tilde\nabla_xL(x;y)=x-\operatorname{prox}_{h+\iota_X}\big(x-\nabla_x(L(x;y)-h(x))\big)$. The error bound with constant $\tau$ is $\operatorname{dist}(x,X(y))\le\tau\|\tilde\nabla_xL(x;y)\|$ for all $y$ and $x\in X$.

Formalization targets

Goal: Theorem 2.1, part 2

Under Assumptions A and B and the error bound, if the stepsizes are either constant and sufficiently small, or satisfy $\sum_t\alpha^t=\infty$, $\alpha^t\to0$, then with probability 1

$$\|Ex^t-q\|\to0,\qquad\|x^t-x^{t+1}\|\to0,\qquad\|x^t-\bar x^t\|\to0,$$

where $\bar x^t$ is the point of $X(\hat y^t)$ nearest to $x^t$, and every limit point of $(x^t,y^t)$ is a primal and dual optimal pair. The threshold for "sufficiently small" is existential and depends only on the problem data, the $u_k$, the error-bound constant and $p$.

Milestones

In the order of the paper: Lemma 2.1 (differentiability of $d$, $\nabla d(y)=q-Ex(y)$, the $1/\rho$-Lipschitz bound); Lemma 2.3(2) (expected decrease of $L$); Lemma 2.4(2) (proximal gradient bounded by the block and dual steps); Lemmas 2.5(2) and 2.6(2) (expected change of the dual and primal gaps); and from the proof of Theorem 2.1, (2.24)–(2.25) (expected change of $\Delta_p+\Delta_d$), (2.28) (constraint violation), (2.29) (the descent estimate with explicit coefficients) and (2.40) (one-step change of $\|E\bar x^t-q\|$).

Significance

The result shows that a randomized, single-block-per-iteration primal-dual method converges almost surely to primal-dual optimal solutions of a multi-block linearly constrained problem, under assumptions that allow a rank-deficient $A$, nonsmooth group-sparse regularizers, and inexact (majorized) block subproblems. The potential function $\Delta_p+\Delta_d$ and the way the error bound converts it into a supermartingale estimate are reused in later analyses of multi-block and randomized ADMM-type methods.

The result is proved in the paper; to our knowledge it has no machine-checked proof. Formalizing it produces a checked convergence proof for a randomized augmented-Lagrangian method, a reusable formal treatment of the augmented dual function of a convex program with compact polyhedral constraints, and a precise record of the conventions under which the published statements hold (see the scope section).

Difficulty

The obvious route is to show that $L(x^t;y^t)$ decreases. It does not: a dual step increases $L$ by $\alpha^t\|q-Ex^t\|^2$, and without strong convexity there is no direct control of the distance to the solution set. The argument has to combine the primal and dual gaps into one potential, bound the residual term $\|Ex^t-E\bar x^{t+1}\|$ through an error bound that holds without strong convexity, and then pass from a conditional-expectation inequality to almost-sure convergence. Under diminishing stepsizes the supermartingale argument only yields $\liminf\|E\bar x^t-q\|=0$, and upgrading this to a limit needs a separate pathwise argument on how fast $\nabla d(\hat y^t)$ can move.

Formalization scope

Blocks are EuclideanSpace ℝ (Fin (n k)) and the full vector lives in PiLp 2, so norms are Euclidean. $\ell$ is real-valued on all of $\mathbb R^p$. The augmented dual function is $d(y)=\min_{x\in X}L(x;y)$ (the page's (1.9) prints an unconstrained minimum of $g$ plus penalty; the constrained reading is the one Lemma 2.1 and (2.19) use). The prox in the proximal gradient includes the constraint set $X$, which is what the proof of Lemma 2.4 needs; the error bound of Lemma 2.2 is a hypothesis of the goal, in its global form on $X$, and is not derived. Lemma 2.2 itself is not part of the mission.

Conditional expectations given $z^t=(x^t,y^t)$ are written as the explicit average $p_0F(x,\hat y)+\sum_kp_kF((\hat x_k,x_{-k}),y)$ over the random index, at every state; this is $\mathbb E[F(z^{t+1})\mid z^t]$ because the index drawn at iteration $t$ is independent of $z^t$. The goal is stated on an arbitrary probability space carrying mutually independent indices with law $p$, for every run from a deterministic start $x^1\in X$, $y^1$. Iterations are indexed from $t=1$ as on the page.

Two printed statements are corrected and labelled in their items: Lemma 2.1 asserts $Ax$ (not each $A_kx_k$) constant over $X(y)$, and Lemma 2.6(2) uses $\alpha^t$ where the page prints $\alpha^r$. Statements are not trivialized: the setting is satisfiable (for instance $K=1$, $g\equiv0$, $h=0$, $E=0$, $X=[-1,1]$, $u(v;x)=(v-x_1)^2/2$), the stepsize threshold precedes the probability space and the run, and the solution sets entering distances are nonempty under Assumption A. A formalization in which the error bound or the gap bounds are assumed in a form that already contains the conclusion would not count.

A complete development needs: Danskin-type differentiability of $d$ and the $1/\rho$-smoothness of the augmented dual; first-order optimality and nonexpansiveness of the prox of $h+\iota_X$; and the Robbins–Siegmund almost-supermartingale convergence theorem in Mathlib's conditional expectation framework, together with a bridge from the explicit index average to condExp. The last two are reusable well beyond this mission. Contributions to any of the milestones, or to these general lemmas, are welcome.

Selected references

• M. Hong, T.-H. Chang, X. Wang, M. Razaviyayn, S. Ma, Z.-Q. Luo, A Block Successive Upper Bound Minimization Method of Multipliers for Linearly Constrained Convex Optimization, arXiv:1401.7079v1, 2014; Mathematics of Operations Research 45(3), 2020. https://arxiv.org/abs/1401.7079, https://doi.org/10.1287/moor.2019.1010
• M. Hong, Z.-Q. Luo, On the linear convergence of the alternating direction method of multipliers, Mathematical Programming 162, 2017. https://doi.org/10.1007/s10107-016-1034-2
• C. Chen, B. He, Y. Ye, X. Yuan, The direct extension of ADMM for multi-block convex minimization problems is not necessarily convergent, Mathematical Programming 155, 2016. https://doi.org/10.1007/s10107-014-0826-5
• H. Robbins, D. Siegmund, A convergence theorem for non negative almost supermartingales and some applications, in Optimizing Methods in Statistics, Academic Press, 1971. https://doi.org/10.1016/B978-0-12-604550-5.50015-8
• M. Razaviyayn, M. Hong, Z.-Q. Luo, A unified convergence analysis of block successive minimization methods for nonsmooth optimization, SIAM Journal on Optimization 23(2), 2013. https://doi.org/10.1137/120891009

Theorem numbers, equation numbers and page numbers in this mission refer to arXiv:1401.7079v1 (printed page = PDF page − 1); the journal version renumbers them.

Why barycenters of histograms matter

A barycenter summarizes several objects by minimizing a weighted sum of distances to them. For probability histograms, ordinary coordinatewise averages depend strongly on how the bins are labeled. Optimal transport instead lets mass move between bins and charges for those moves through a cost matrix. The resulting Wasserstein barycenter can reflect the geometry of the bins: nearby bins can exchange mass at a lower cost than distant ones. Peyré and Cuturi use this construction in their treatment of variational transport problems, including shape interpolation and the representation of a measure as a barycenter of other measures. The finite histogram problem in this mission is the entropically regularized version developed in §9.2 of their textbook.

The computational question is how to connect three ways of describing the same solution: a histogram that is the barycenter, transport matrices coupling it to the inputs, and vectors of dual potentials. Proposition 9.1 on p. 530 identifies the dual potentials behind the scaling factors of the optimal transport matrices. This is the second proposition numbered 9.1 in the chapter; the one on p. 519 concerns derivatives with respect to histograms.

Finite histogram setting

There are $S$ input histograms. Source $s$ has $n_s$ bins and a probability vector $b_s$, while the barycenter has $n$ bins. The real matrix $C_s\in\mathbb R^{n\times n_s}$ gives the cost of transporting a unit of mass from barycenter bin $i$ to input bin $j$. A weight vector $\lambda\in\Sigma_S$ has nonnegative entries summing to one; $\Sigma_k$ denotes the probability simplex on $k$ bins. The unregularized barycenter problem (9.10) minimizes $\sum_s\lambda_s L_{C_s}(a,b_s)$ over $a\in\Sigma_n$, where $L_{C_s}$ is the minimum transport cost with marginals $a$ and $b_s$.

For a regularization parameter $\varepsilon>0$, the entropic transport cost $L^\varepsilon_{C_s}(a,b_s)$ minimizes $\langle C_s,P_s\rangle-\varepsilon H(P_s)$ over nonnegative coupling matrices $P_s$ with row marginal $a$ and column marginal $b_s$. Here $\langle C_s,P_s\rangle=\sum_{i,j}C_{s,ij}P_{s,ij}$ and $H(P_s)=\sum_{i,j}(-P_{s,ij}\log P_{s,ij}+P_{s,ij})$, with $0\log0=0$. The Gibbs kernel is $K_{s,ij}=e^{-C_{s,ij}/\varepsilon}$.

The book also writes the regularized barycenter as a weighted KL projection. Its variables are the matrices $(P_s)_s$; each matrix has column marginal $b_s$, and every matrix has the same row marginal. That shared row marginal is $a$, so the optimization can be expressed without carrying $a$ as a separate variable. The generalized matrix divergence is $\mathrm{KL}(P_s\mid K_s)=\sum_{i,j}[P_{s,ij}\log(P_{s,ij}/K_{s,ij})-P_{s,ij}+K_{s,ij}]$, using the continuous value at $P_{s,ij}=0$. See (9.15)–(9.17) in Peyré and Cuturi.

Formalization targets

The goal is Proposition 9.1 on p. 530. The dual variables are row potentials $f_s\in\mathbb R^n$ and column potentials $g_s\in\mathbb R^{n_s}$. They maximize

$$\sum_s\lambda_s\left[\langle g_s,b_s\rangle-\varepsilon\sum_{i,j}e^{f_{s,i}/\varepsilon}K_{s,ij}e^{g_{s,j}/\varepsilon}\right] \quad\text{subject to}\quad \sum_s\lambda_s f_s=0.$$

The theorem asserts that the primal and dual optima are attained, that every optimal primal family and every optimal dual family satisfy

$$P_{s,ij}=e^{f_{s,i}/\varepsilon}K_{s,ij}e^{g_{s,j}/\varepsilon},$$

and that the dual maximum is the minimum value of the entropic barycenter objective (9.15). The milestone targets are the scalar and matrix versions of the KL conjugate (9.22), followed by the closed form maximizer of one $g_s$ block, corresponding to the update (9.18). These statements retain the source's finite matrix setting and are listed in the order in which their concepts enter the dual formulation.

What the result supplies

The scaling formula turns the optimal couplings into a product of a row factor, a fixed positive kernel, and a column factor. It identifies those factors with exponentials of dual potentials and gives a constrained maximization problem whose value is the entropic barycenter cost. Thus a solver can reason about the couplings, the barycenter marginal, or the potentials while referring to one theorem that connects them. The book uses the same variables to describe the iterative scaling updates on pp. 529–531 and later illustrates barycenters of shapes and surface measures; those applications depend on interpreting the matrix factors correctly. Peyré and Cuturi give the mathematical proposition and its argument. A complete Lean proof of the proposition and its supporting KL identities is the work this mission calls for; the statements here are draft targets rather than machine-checked solutions.

Where the difficulty lies

The potential program is a constrained optimization problem, while the transport problem constrains nonnegative matrices by two kinds of marginals. Equality of their optimum values must preserve the normalization constants in generalized KL. The exponential form alone does not establish that a proposed matrix has the required marginals, nor does a feasible matrix alone identify dual potentials. In addition, the assertion concerns every optimizer: a choice of zero source weight would leave that source's coupling unconstrained by the objective, and a zero target entry would put a logarithmic column update on the boundary. These are substantive edge cases of the formulas, not merely notation.

Formalization scope

Lean uses Fin S, Fin n, and Fin (n_s) for the finite index sets; these are zero based versions of the book's one based indices. Histograms and potentials are real vectors, costs and couplings are real matrices, and the Gibbs kernel is defined entrywise. The theorem requires $S,n,n_s>0$, $\varepsilon>0$, strictly positive weights $\lambda_s$ that sum to one, and strictly positive input histograms $b_s$ that each sum to one. The strict positivity of weights and input entries is an explicit restriction beyond (9.15)–(9.21), needed for a statement about every optimizer and finite logarithmic potentials. Entropy uses $0\log0=0$ on nonnegative couplings. The shared row marginal is constructed by the constraints on the $P_s$; it is not a free histogram unrelated to them.

The definition layer includes finite matrix pairing, entropy, generalized KL, the Gibbs kernel, feasibility, and primal and dual objective functions. The KL conjugate identities and the block optimizer are separate theorem targets so they can be reused in other entropic transport developments. The main theorem asserts primal and dual attainment as well as their relationship; it does not assume strong duality or an optimal scaling as an input. The page has slips in the dimensions of the marginal equations and a missing subscript on $K$ in (9.17); the Lean statements use the dimensions specified by $P_s\in\mathbb R^{n\times n_s}$. The optional cost-gradient Proposition 9.2 on pp. 519–520 and the $f_s$ block update (9.19)–(9.20) lie outside this proposal.

Selected references

• Gabriel Peyré and Marco Cuturi, Computational Optimal Transport, Foundations and Trends in Machine Learning 11(5–6):355–607, 2019. DOI: 10.1561/2200000073.

Motivation

Optimal transport compares two distributions by finding the least expensive way to move mass between them. For finite histograms, the resulting linear program is precise but its optimal coupling can be sparse. In applications where the coupling represents traffic, matching, or a differentiable loss, a sparse plan may be undesirable or expensive to compute repeatedly. Peyré and Cuturi describe how adding an entropy term selects a diffuse coupling and leads to matrix scaling algorithms that can be used on large finite problems (Peyré and Cuturi, 2019, Chapter 4).

The entropic dual gives a second view of the same regularized problem. Its variables are real vectors attached to the two marginal constraints. Unlike the ordinary Kantorovich dual, the objective has no explicit feasibility constraints and is smooth. This permits calculations in the log domain, which the book introduces because direct scaling with exponentials can suffer from numerical overflow or underflow when the regularization parameter is small relative to the costs (Peyré and Cuturi, 2019, §4.4). This mission targets the exact relationship between the regularized minimum, the smooth dual maximum, and the scaling factors.

Setting

Fix positive integers $n,m$. A histogram $a\in\Sigma_n$ is a vector with nonnegative entries summing to one; $b\in\Sigma_m$ is defined similarly. Strict positivity is required for the attained dual maximum and log-domain updates; the primal scaling and Kantorovich-feasibility statements also cover zero-entry histograms. A coupling $P\in U(a,b)$ is an $n\times m$ matrix with nonnegative entries, row sums $a$, and column sums $b$. A real matrix $C$ assigns cost $C_{ij}$ to each transfer from row $i$ to column $j$, and $\langle C,P\rangle=\sum_{i,j}C_{ij}P_{ij}$ is its transport cost.

The book uses the entropy $H(P)=-\sum_{i,j}P_{ij}(\log P_{ij}-1)$, with $0\log0=0$. For $\varepsilon>0$, the regularized cost is $L_C^\varepsilon(a,b)=\min_{P\in U(a,b)}\{\langle C,P\rangle-\varepsilon H(P)\}$. The Gibbs kernel has entries $K_{ij}=\exp(-C_{ij}/\varepsilon)$. Given potentials $f\in\mathbb R^n$ and $g\in\mathbb R^m$, the smooth dual objective is $Q(f,g)=\langle f,a\rangle+\langle g,b\rangle-\varepsilon\sum_{i,j}e^{f_i/\varepsilon}K_{ij}e^{g_j/\varepsilon}$. These are the finite-dimensional objects of (4.1), (4.2), and (4.30) in the source (Peyré and Cuturi, 2019, pp. 425, 428, 448).

Formalization targets

Attained entropic duality

The goal is Proposition 4.4. There are an optimal coupling $P$ and potentials $(f,g)$ at which the dual reaches its maximum, with the common value

$$L_C^\varepsilon(a,b) =\langle C,P\rangle-\varepsilon H(P) =\max_{f',g'} Q(f',g').$$

For every maximizing pair $(f',g')$, the same optimal coupling satisfies

$$P_{ij}=e^{f'_i/\varepsilon}K_{ij}e^{g'_j/\varepsilon}.$$

Thus the dual potentials determine the scaling vectors $u=e^{f'/\varepsilon}$ and $v=e^{g'/\varepsilon}$ in (4.12). The maximum is an attained maximum of a real function, as stated in the book, rather than an unrestricted real infimum or supremum that might take a default value on a bad input (Peyré and Cuturi, 2019, Proposition 4.4).

Supporting results

The milestones follow the source's statements. Proposition 4.3 gives existence, uniqueness, and the Gibbs scaling of the primal optimizer. Remark 4.21 gives the two partial-gradient formulas and the closed log-domain block updates. Proposition 4.5 states that an entropic dual maximizer is a feasible pair of ordinary Kantorovich potentials, so its linear objective is bounded above by the unregularized cost $L_C(a,b)$ (Peyré and Cuturi, 2019, pp. 432, 449, 452–453).

Significance

The equality establishes that the matrix scaling variables and the dual potentials describe the same optimal coupling. It lets a computation based on scaling be interpreted as maximizing a smooth objective, and it gives exact marginal-error expressions through the dual gradients. Feasible Kantorovich potentials obtained at the optimum also provide a lower bound on the ordinary transport cost. These statements explain why log-domain updates represent the same mathematical problem as entropic transport, even when direct exponentiation is numerically fragile (Peyré and Cuturi, 2019, §§4.4–4.5).

The results are established in the textbook; the open work here is their Lean formalization. A completed development would provide reusable finite coupling, entropy, Gibbs-kernel, and smooth-dual interfaces, together with the existence and differentiability results needed to connect them. It would also distinguish a primal optimum, a dual maximum, and a feasible potential without relying on informal convention. The mission does not assert that these textbook results are new, and no machine-checked proof of these exact statements is claimed here.

Difficulty

The unconstrained dual objective has a symmetry: shifting every coordinate of $f$ by one constant and every coordinate of $g$ by its negative leaves the value unchanged. Consequently, the set of maximizers is not bounded in the ordinary product space. Positivity of the marginals matters for attaining a maximum with finite real potentials; if a marginal entry is zero, the corresponding potential can escape toward negative infinity. On the primal side, the entropy formula must be valid at zero entries even though optimality links it to strictly positive exponential scalings. The formal argument must connect these boundary conventions and the finite-dimensional optimization statements without turning the maximum into a junk real supremum (Peyré and Cuturi, 2019, Proposition 4.4 and Remark 4.21).

Formalization scope

The Lean development represents indices by Fin n and Fin m, matrices by Matrix (Fin n) (Fin m) ℝ, and histograms by Mathlib's stdSimplex. Positive dimensions and $\varepsilon>0$ appear throughout. Strictly positive marginal entries are required for the attained dual maximum and log-domain updates; the other statements permit zero entries. The book assumes positive weights for discrete measures in Remark 2.1; the marginal positivity is also required for the attained dual maximum and the logarithmic updates. The cost matrix itself may have arbitrary real entries. Entropy uses Real.negMulLog, which implements $0\log0=0$ on the nonnegative couplings where it is applied.

The primal optimum is a predicate on a coupling and its objective, rather than a chosen matrix. The unregularized $L_C$ is a real infimum used only when simplex marginals make its feasible set nonempty and bounded. The dual objective is a finite sum. Its gradients are stated as one-variable derivatives in each coordinate, and each block update is characterized as the unique maximizer with the other block fixed. The complete development needs Mathlib's finite sums, real exponential and logarithm, calculus, finite-dimensional topology, and optimization facts. Contributions that establish these shared interfaces or the four milestone statements are in scope.

Propositions 4.7 and 4.8 are excluded from this proposal because their printed bounds compare a dual linear objective with $L_C^\varepsilon$ where the accompanying arguments instead support a comparison with the unregularized $L_C$; (4.47) also has a sign discrepancy. The milestone list therefore avoids encoding a false inequality (Peyré and Cuturi, 2019, pp. 453–454).

Selected references

• Gabriel Peyré and Marco Cuturi, Computational Optimal Transport, Foundations and Trends in Machine Learning 11(5–6), 2019, pp. 355–607. DOI: 10.1561/2200000073.

Why optimize over a trained ReLU neuron

A trained feed-forward neural network with ReLU activations, $\mathrm{ReLU}(v)=\max\{0,v\}$, is a piecewise linear function of its input. Many tasks ask for an optimization over such a network with its weights held fixed: verifying that no small perturbation of an image changes its classification, finding adversarial examples, or embedding a learned model of demand or cost inside a decision problem ("predict, then optimize"). The standard way to solve such problems exactly is mixed-integer programming (MIP): each neuron is written as a small set of linear constraints with one binary variable, and the network is the composition of these neuron formulations. How strong each neuron formulation is decides how fast branch-and-bound can close the gap.

The formulation used in the literature up to 2018 is the big-M formulation. It is valid but weak. This mission formalizes the main result of Anderson, Huchette, Tjandraatmadja and Vielma, IPCO 2019 extended abstract (arXiv:1811.08359v2), which gives the strongest possible formulation of a single ReLU neuron that uses the original variables and one binary variable only.

Timeline. Big-M formulations of ReLU networks were used by several groups in 2017–2018 for verification and adversarial analysis (see §1.2 of the paper). Balas's disjunctive programming (1985, 1998) and the multiple choice formulation of piecewise linear functions (Vielma and Nemhauser, Math. Program. 2011) give an ideal formulation of the neuron that needs a copy of the input variables. Anderson et al. (2019) project out that copy and obtain the formulation (6) below; a longer journal version (Math. Program. 2020, with W. Ma) develops the analysis further, including interactions between neurons.

Setting

Fix $\eta\in\mathbb N$, a weight vector $w\in\mathbb R^\eta$, a bias $b\in\mathbb R$, and bounds $L,U\in\mathbb R^\eta$ with $L_i<U_i$ for every $i$. The neuron computes $\mathrm{ReLU}(f(x))$ for the affine function $f(x)=w\cdot x+b$ on the box $[L,U]=\{x: L\le x\le U\}$. Its graph is

$$\operatorname{gr}(\mathrm{ReLU}\circ f;[L,U])=\{(x,\mathrm{ReLU}(f(x))) : L\le x\le U\}.$$

The sign-adjusted bounds are $\breve L_i=L_i$, $\breve U_i=U_i$ when $w_i\ge 0$, and $\breve L_i=U_i$, $\breve U_i=L_i$ when $w_i<0$. Then $M^+(f)=w\cdot\breve U+b$ and $M^-(f)=w\cdot\breve L+b$ are the maximum and minimum of $f$ on $[L,U]$, and $\operatorname{supp}(w)=\{i: w_i\ne 0\}$. Strict activity means $M^-(f)<0<M^+(f)$: the neuron is neither always off nor always on. The paper assumes throughout that $L_i<U_i$ and that strict activity holds.

A set $R$ of points $(x,y,z)$ with $z\in[0,1]$, read together with the constraint $z\in\{0,1\}$, is a formulation of the graph if $(x,y)$ lies on the graph exactly when $(x,y,z)\in R$ for some $z\in\{0,1\}$; $R$ is then its LP relaxation. The formulation is ideal if every extreme point of $R$ has $z\in\{0,1\}$.

The big-M formulation (3) is $y\ge f(x)$, $y\le f(x)-M^-(f)(1-z)$, $y\le M^+(f)z$, $(x,y,z)\in[L,U]\times\mathbb R_{\ge0}\times\{0,1\}$. The formulation of Proposition 1 is

$$\begin{aligned} &y\ge w\cdot x+b &&(6a)\\ &y\le\sum_{i\in I}w_i\bigl(x_i-\breve L_i(1-z)\bigr)+\Bigl(b+\sum_{i\notin I}w_i\breve U_i\Bigr)z\qquad\forall I\subseteq\operatorname{supp}(w) &&(6b)\\ &(x,y,z)\in[L,U]\times\mathbb R_{\ge0}\times\{0,1\}. &&(6c) \end{aligned}$$

Formalization targets

Goal: Proposition 1 (p. 6)

$$\text{(6a)–(6c) is a formulation of }\operatorname{gr}(\mathrm{ReLU}\circ f;[L,U]),\ \text{and every extreme point of its LP relaxation has } z\in\{0,1\}.$$

Milestones (Appendix A.1 and §2.2)

1. The multiple choice formulation (5), with copies $x^0,x^1,y^0,y^1$, has only integral $z$ at extreme points in its lifted space and formulates the graph; projected to $(x,y,z)$, its LP relaxation is the convex hull of its points with $z\in\{0,1\}$ (§2.2, pp. 5–6).
2. Projecting the copies out of the LP relaxation of (5) gives the linear system (7): (6a), (6b), a second exponential family (7c), and the bounds (7d) (App. A.1, p. 14).
3. The family (7c) is implied by the other constraints (App. A.1, pp. 14–15).
4. The LP relaxation of (6) is the convex hull of its points with $z\in\{0,1\}$ (App. A.1, p. 14).

Companion results

• $M^\pm(f)$ are the maximum and minimum of $f$ on $[L,U]$ (§1.3, p. 4).
• Proposition 3 (p. 7): for $(\hat x,\hat y,\hat z)\in[L,U]\times\mathbb R_{\ge0}\times[0,1]$, if some inequality of (6b) is violated, the one for $\hat I=\{i\in\operatorname{supp}(w): w_i\hat x_i<w_i(\breve L_i(1-\hat z)+\breve U_i\hat z)\}$ is the most violated.
• The big-M formulation (3) is a formulation of the graph (p. 4); Examples 1 and 2 (p. 5) show that it is not ideal and that its gap grows like $\tfrac12\gamma\eta$; its inequalities (3b), (3c) are (6b) for $I=\operatorname{supp}(w)$ and $I=\emptyset$ (p. 7).

Significance

Proposition 1 says that the convex hull of the graph, lifted with one binary variable, is described by (6a), (6b) and the bounds, with no auxiliary continuous variables. Optimizing a linear function over the LP relaxation of (6) therefore gives the tightest convex relaxation available for a single neuron, and Proposition 3 gives a separation routine linear in $\eta$, so the exponential family can be added on demand to a big-M model. The paper's experiments (§3, not formalized) report that separating over (6b) solves smaller MNIST verification instances faster than Gurobi's default cut generation by a factor of 7.

The result is proved in the paper; nothing here is open. To our knowledge none of these statements has a machine-checked proof. The work this mission asks for is the formalization of the known proof: an ideality statement for the multiple choice formulation, a Fourier–Motzkin projection carried out for an arbitrary index set with general-sign weights, and the passage from a hull identity to integrality of extreme points.

Difficulty

The formulation half of Proposition 1 is a short case analysis on $z\in\{0,1\}$; the content is ideality. The obvious attempt, characterizing the extreme points of the LP relaxation of (6) directly, is impractical: the polytope is cut out by $2^{|\operatorname{supp}(w)|}$ inequalities, and showing that every point with fractional $z$ is a proper convex combination of feasible points means handling all patterns of tight inequalities of (6b) at once. Ideality of the extended formulation (5) is classical and passes to its projection onto $(x,y,z)$, but that only helps once the projection is known to be exactly the LP relaxation of (6): it has to be computed for an arbitrary index set, and every inequality it produces must be shown to be one of (6a), (6b), the bounds, or implied by them. Weights of both signs must be handled throughout: the page treats negative weights by a change of variables, and a formal development has to carry the sign-adjusted bounds $\breve L,\breve U$ through every step.

Formalization scope

Inputs $x\in\mathbb R^\eta$ are Fin η → ℝ, so indices are 0-based; points $(x,y,z)$ are (Fin η → ℝ) × ℝ × ℝ. A formulation is encoded by its LP relaxation $R$ (with $z\in[0,1]$) and the predicate "$(x,y)\in S$ iff $(x,y,z)\in R$ for some $z\in\{0,1\}$"; ideality is ∀ p ∈ Set.extremePoints ℝ R, p.2.2 = 0 ∨ p.2.2 = 1. $M^\pm(f)$ are defined by their closed forms, and a companion theorem proves that they are the maximum and minimum. In (6b) and (7c), "$i\notin I$" ranges over all indices outside $I$, zero weights included. The system (7) is stated with $\breve L,\breve U$, i.e. after undoing the page's substitution $\tilde x_i=-x_i$; for $w\ge 0$ it is the page's display. The LP relaxation of (5) is represented both in its lifted space and projected to $(x,y,z)$, with the copies quantified existentially in the latter, and constant $b$ is scaled by $1-z$ in (5b) and by $z$ in (5c).

The goal carries both standing assumptions of §1.3 ($L_i<U_i$ and strict activity) and nothing else. Milestones that do not need strict activity omit it, which makes them stronger. Example 2 includes the page's $\gamma=0$ boundary: although its box then violates $L_i<U_i$ when $\eta>0$, the example's three stated claims remain true.

Ideality is a statement about the LP relaxation, not about the set with $z\in\{0,1\}$: applied to the latter it would hold trivially, and a goal stating only that (6) is a formulation would omit the result's content. Both are ruled out by the statement of the goal.

A complete development needs: extreme points and convex hulls of polyhedra in product spaces (Mathlib), the hull of a union of two polytopes as a projection, Fourier–Motzkin elimination over an arbitrary finite index set, and finite-sum manipulations over subsets of $\operatorname{supp}(w)$. The Fourier–Motzkin and disjunctive-hull lemmas are reusable well beyond this mission; contributions of either are welcome, as are proofs of the companion results.

Source: the IPCO 2019 extended abstract, arXiv:1811.08359v2 (28 Feb 2019); all labels and pages refer to that version.

Selected references

• R. Anderson, J. Huchette, C. Tjandraatmadja, J. P. Vielma, Strong mixed-integer programming formulations for trained neural networks, IPCO 2019 (LNCS 11480), extended abstract. arXiv:1811.08359v2
• R. Anderson, J. Huchette, W. Ma, C. Tjandraatmadja, J. P. Vielma, Strong mixed-integer programming formulations for trained neural networks, Mathematical Programming 183 (2020) 3–39. doi:10.1007/s10107-020-01474-5, arXiv:1811.01988
• J. P. Vielma, G. Nemhauser, Modeling disjunctive constraints with a logarithmic number of binary variables and constraints, Mathematical Programming 128 (2011) 49–72. doi:10.1007/s10107-009-0295-4
• E. Balas, Disjunctive programming and a hierarchy of relaxations for discrete optimization problems, SIAM Journal on Algebraic and Discrete Methods 6(3) (1985) 466–486. doi:10.1137/0606047
• E. Balas, Disjunctive programming: properties of the convex hull of feasible points, Discrete Applied Mathematics 89 (1998) 3–44. doi:10.1016/S0166-218X(98)00136-X
• J. P. Vielma, Mixed integer linear programming formulation techniques, SIAM Review 57(1) (2015) 3–57. doi:10.1137/130915303

Motivation

Many problems in signal processing, machine learning and power systems have the form of a convex objective that is a sum of a smooth coupled term and nonsmooth block-separable terms, minimized subject to linear equality constraints that couple $K$ blocks of variables: basis pursuit, demand response control in smart grids, and distributed estimation are the examples of Hong, Chang, Wang, Razaviyayn, Ma, Luo. The alternating direction method of multipliers (ADMM) handles two blocks well, but for $K\ge3$ blocks the directly extended Gauss–Seidel ADMM can diverge (Chen, He, Ye, Yuan, 2016), and convergence proofs for multi-block schemes usually need strong convexity or extra correction steps.

The block successive upper-bound minimization method of multipliers (BSUM-M) is the paper's answer: each block is updated by minimizing a local upper bound of the augmented Lagrangian, which makes the subproblems simple (for instance closed-form proximal steps), and the multiplier is updated by a dual gradient step with a small or diminishing stepsize. The main theorem shows that this scheme converges to primal and dual optimal solutions for any number of blocks without strong convexity, under an error bound.

Setting

The variable is $x=(x_1,\dots,x_K)$, $x_k\in\mathbb R^{n_k}$, with the Euclidean norm $\|x\|^2=\sum_k\|x_k\|^2$. Problem (1.1) is

$$\min_x\ f(x)=g(x)+\sum_{k=1}^K h_k(x_k)\quad\text{s.t.}\quad Ex=\sum_{k=1}^KE_kx_k=q,\quad x_k\in X_k .$$

Under the standing Assumption A, $g(x)=\ell(Ax)+\langle x,b\rangle$ with $\ell$ strictly convex and continuously differentiable and $A$ any matrix; $h_k(x_k)=\lambda_k\|x_k\|_1+\sum_Jw_J\|x_{k,J}\|_2$ is a mixed $\ell_1/\ell_2$ norm with nonnegative weights; each $X_k=\{x_k\mid C_kx_k\le c_k\}$ is a compact polyhedron and $X=\prod_kX_k$; the problem is feasible and the dual optimal value is attained.

For $\rho>0$, the augmented Lagrangian is $L(x;y)=f(x)+\langle y,q-Ex\rangle+\frac\rho2\|q-Ex\|^2$, the augmented dual is $d(y)=\min_{x\in X}L(x;y)$, and $X(y)=\arg\min_{x\in X}L(x;y)$. For $x\in X$, $\bar x$ denotes the point of $X(y)$ nearest to $x$.

Assumption B concerns the approximation functions $u_k(v_k;x)$: each upper-bounds $G(x)=g(x)+\frac\rho2\|Ex-q\|^2$ along block $k$, is tight with matching gradient at $v_k=x_k$, is continuous, strongly convex in $v_k$ with a uniform modulus $\gamma_k>0$, and has an $L_k$-Lipschitz gradient in $v_k$.

BSUM-M (1.12). From $x^1\in X$ and any $y^1$, for $r\ge1$:

$$y^{r+1}=y^r+\alpha^r(q-Ex^r),\qquad x_k^{r+1}=\arg\min_{x_k\in X_k}u_k(x_k;w_k^{r+1})-\langle y^{r+1},E_kx_k\rangle+h_k(x_k),$$

for $k=1,\dots,K$ in order, with the Gauss–Seidel point $w_k^{r+1}=(x_1^{r+1},\dots,x_{k-1}^{r+1},x_k^r,\dots,x_K^r)$.

The proximal gradient is $\tilde\nabla_xL(x;y)=x-\operatorname{prox}(x-\nabla_x(L(x;y)-h(x)))$ with $\operatorname{prox}(z)=\arg\min_{u\in X}h(u)+\frac12\|z-u\|^2$. The error bound asks for $\tau>0$ with $\operatorname{dist}(x,X(y))\le\tau\|\tilde\nabla_xL(x;y)\|$ for all $x\in X$ and all $y$.

Formalization targets

Goal: Theorem 2.1, part 1

Under Assumptions A and B and the error bound, there is $\bar\alpha>0$ such that for stepsizes $\alpha^r>0$ that are either constant with $\alpha^r=\alpha\le\bar\alpha$, or satisfy $\sum_r\alpha^r=\infty$ and $\alpha^r\to0$, every BSUM-M run satisfies

$$\lim_{r\to\infty}\|Ex^r-q\|=0,\qquad\lim_{r\to\infty}\|x^r-x^{r+1}\|=0,\qquad\lim_{r\to\infty}\|x^r-\bar x^r\|=0,$$

and every limit point of $\{(x^r,y^r)\}$ is a primal and dual optimal solution. The threshold $\bar\alpha$ is not specified; no rate is claimed.

Milestones

Lemma 2.3(1) (one sweep decreases $L(\cdot;y^{r+1})$ by $\gamma\|x^r-x^{r+1}\|^2$), Lemma 2.5(1) (dual gap decrease), Lemma 2.6(1) (primal gap bound), Lemma 2.4(1) (the proximal gradient at $x^r$ is $O(\|x^{r+1}-x^r\|)$) and Lemma 2.1 (differentiability of $d$, $\nabla d(y)=q-Ex(y)$, and Lipschitz continuity of $\nabla d$ on superlevel sets).

Significance

The theorem gives a convergent multi-block method of multipliers whose block subproblems may be replaced by any majorizer satisfying Assumption B, such as a linearized proximal step. It covers the cyclic Gauss–Seidel order, where the direct multi-block ADMM can fail, and it does not require strong convexity of $f$ (the matrix $A$ need not have full column rank). The paper's randomized variant (part 2 of the same theorem) is a separate mission.

The result is proved in the paper (the proof of part 1 is described as following the steps written out for part 2). It has not been machine-checked. Formalization adds a verified account of the potential-function argument for a primal-dual method with inexact block updates, and checks three printed statements that need correction (see the scope section): a formal proof settles them.

Difficulty

The obvious approach is to treat BSUM-M as an inexact dual gradient ascent on $d$, but a single Gauss–Seidel sweep does not compute $x(y^{r+1})\in X(y^{r+1})$, so the dual step uses a gradient at the wrong point. Controlling that error requires relating the primal step length to the distance from $X(y)$, which fails without an error bound: $L(\cdot;y)$ is not strongly convex, $X(y)$ need not be a singleton, and the proximal gradient can be small far from $X(y)$. The cyclic order adds a second gap: block $k$ is linearized at $w_k^{r+1}$, not at $x^r$. With a constant stepsize the dual ascent must not outrun the primal descent, which is where the smallness threshold enters.

Formalization scope

Citation basis: the arXiv preprint arXiv:1401.7079v1 (28 Jan 2014); every index refers to that version, not to the revised journal version (Mathematics of Operations Research, 2020).

Representation: blocks are indexed by Fin K with $K\ge1$; the block space is PiLp 2 of Euclidean spaces (the Euclidean norm, not the sup norm). $\ell$ is real valued and $C^1$ on all of $\mathbb R^p$, which specializes the paper's extended-valued $\ell$. $d$, $d^*$ and $f^*$ are real infima and suprema over nonempty compact sets, where they are attained. The algorithm is a predicate on sequences indexed from $r=1$; argmin steps are minimality conditions, the minimizer being unique. The initial point is required to lie in $X$. "Sufficiently small" is an existential threshold quantified before the stepsizes and the run. $\|x^r-\bar x^r\|$ is the distance from $x^r$ to $X(y^r)$. Limit points are cluster points of the joint sequence; boundedness of $\{y^r\}$ is neither assumed nor concluded.

Interpretations and corrections, each labelled in the item's statement:

• the proximity operator in (2.3) includes the constraint set $X$, as the paper's optimality relation (2.14) requires;
• $d(y)$ is $\min_{x\in X}L(x;y)$; (1.9) prints $g(x)$ and an unconstrained minimum;
• (2.17) has $Ex^r$ where its proof (2.19) has $Ex^{r-1}$; the proved inequality is stated;
• (2.12) evaluates the proximal gradient at $y^r$ and is false at $r=1$; it is stated at $y^{r+1}$;
• Lemma 2.1's clause "$A_kx_k$ constant on $X(y)$" fails for non-separable $\ell$; it is stated as "$Ax$ constant".

The error bound is a hypothesis of the goal, as in the paper, and is not derived from Assumption A: the paper's Lemma 2.2 does not hold under Assumption A alone. A formalization that makes the hypotheses unsatisfiable, drops the run's dependence on $y^{r+1}$, or lets $\bar\alpha$ depend on the run is not this theorem. A sanity check that the hypotheses are satisfiable (a one-block instance with a constant run) is part of the drafting record.

Infrastructure needed: proximity operators of convex functions restricted to polyhedra and their nonexpansiveness; Danskin-type differentiability of a parametric minimum over a compact set; smoothness of the augmented dual; elementary convergence lemmas for nonnegative sequences with summable decrements. These pieces are reusable for other augmented Lagrangian and ADMM analyses. Proofs of the milestones are welcome independently of the goal.

Selected references

• M. Hong, T.-H. Chang, X. Wang, M. Razaviyayn, S. Ma, Z.-Q. Luo, A Block Successive Upper Bound Minimization Method of Multipliers for Linearly Constrained Convex Optimization, arXiv:1401.7079v1, 2014; Mathematics of Operations Research 45(3), 2020. https://arxiv.org/abs/1401.7079 , https://doi.org/10.1287/moor.2019.1010
• M. Hong, Z.-Q. Luo, On the linear convergence of the alternating direction method of multipliers, Mathematical Programming 162, 2017. https://doi.org/10.1007/s10107-016-1034-2
• M. Razaviyayn, M. Hong, Z.-Q. Luo, A unified convergence analysis of block successive minimization methods for nonsmooth optimization, SIAM Journal on Optimization 23(2), 2013. https://doi.org/10.1137/120891009
• C. Chen, B. He, Y. Ye, X. Yuan, The direct extension of ADMM for multi-block convex minimization problems is not necessarily convergent, Mathematical Programming 155, 2016. https://doi.org/10.1007/s10107-014-0826-5