Operations Research

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

Large traders who must unwind a position by a deadline face a trade-off between trading fast, which moves prices against them, and trading slowly, which exposes them to price risk. When many traders liquidate at once, each one's execution price also depends on the aggregate selling rate of the others. Fu, Graewe, Horst and Popier (arXiv:1804.04911) model this as a mean field game (MFG) with common noise and a hard liquidation constraint: every position must be zero at the terminal time $T$. Single-player liquidation with this constraint leads to backward equations with singular terminal values (Ankirchner, Jeanblanc and Kruse, SIAM J. Control Optim. 2014; Graewe, Horst and Séré, Stoch. Proc. Appl. 2018). Earlier MFG models of execution (Cardaliaguet and Lehalle, Math. Financ. Econ. 2018; Carmona and Lacker, Ann. Appl. Probab. 2015) allow no liquidation constraint. This mission formalizes the paper's first main result: the constrained game has a unique equilibrium under a weak-interaction condition.

Setting

Fix $T>0$ and a probability space carrying an $m$-dimensional Brownian motion $\widetilde W=(W^0,W)$, where $W^0$ is the one-dimensional common noise, and an initial portfolio $\mathcal X\in L^2$ independent of $\widetilde W$. Let $\mathbb F^0$ be the filtration of $W^0$ and $\mathbb F$ that of $(\mathcal X,W^0,W)$, both augmented by null sets. The cost coefficients are bounded nonnegative $\mathbb F$-progressive processes $\kappa$ (interaction), $\lambda$ (risk aversion) and $\eta$ (temporary impact), with $\lambda,\eta$ bounded away from zero.

A player's trading rate $\xi$ produces the position $X^\xi_t=\mathcal X-\int_0^t\xi_sds$. The admissible strategies are $\mathcal A_{\mathbb F}(\mathcal X)=\{\xi\in L^2_{\mathbb F}:\int_0^T\xi_sds=\mathcal X\}$. Given an $\mathbb F^0$-progressive aggregate rate $\mu$, the cost is

$$J(\mathcal X,\xi;\mu)=\mathbb E\Big[\int_0^T\big(\kappa_sX^\xi_s\mu_s+\eta_s\xi_s^2+\lambda_s(X^\xi_s)^2\big)ds\ \Big|\ \mathcal X\Big],$$

and $V(\mathcal X;\mu)$ is its essential infimum over $\mathcal A_{\mathbb F}(\mathcal X)$. A process $\mu$ solves the MFG (1.7) if some optimal strategy $\xi^*$ given $\mu$ satisfies $\mu_t=\mathbb E[\xi^*_t\mid\mathcal F^0_t]$ for a.e. $t$.

The equilibrium is described by the conditional mean-field FBSDE (2.3):

$$X_t=\mathcal X-\int_0^t\frac{Y_s}{2\eta_s}ds,\quad X_T=0,\quad -dY_t=\Big(\kappa_t\,\mathbb E\Big[\frac{Y_t}{2\eta_t}\Big|\mathcal F^0_t\Big]+2\lambda_tX_t\Big)dt-Z_t\,d\widetilde W_t\ \ \text{on }[0,T).$$

Solutions are sought in weighted spaces: $Y\in\mathcal H_l$ if $\mathbb E\sup_{t\le T}|Y_t/(T-t)^l|^2<\infty$, and $Y\in\mathcal M_l$ if $(T-t)^{-l}|Y_t|$ is essentially bounded. The weak-interaction condition (Assumption 2.3) asks for $\theta>0$ with $\kappa_{\max}/(4\eta_\star)<\theta<4\lambda_\star/\kappa_{\max}$, and $\alpha:=\eta_\star/\|\eta\|\in(0,1]$. The decoupling $Y=AX+B$ uses the solution $A$ of the singular Riccati BSDE $-dA_t=(2\lambda_t-A_t^2/(2\eta_t))dt-Z^A_td\widetilde W_t$, $A_T=+\infty$.

Formalization targets

Goal: Theorem 2.4

Under Assumption 2.3 the FBSDE (2.3) has a unique solution

$$(X,Y,Z)\in\mathcal H_\alpha\times L^2_{\mathbb F}([0,T])\times L^2_{\mathbb F}([0,T-];\mathbb R^m);$$

$\xi^*=Y/(2\eta)$ is optimal, $X$ is the optimal position, $\mu^*_t=\mathbb E[Y_t/(2\eta_t)\mid\mathcal F^0_t]$ is the unique solution of the MFG (1.7), and

$$V(\mathcal X;\mu^*)=\tfrac12A_0\mathcal X^2+\tfrac12B_0\mathcal X+\tfrac12\mathbb E\Big[\int_0^T\kappa_sX^*_s\mu^*_sds\ \Big|\ \mathcal X\Big].$$

Milestones

The milestones follow the paper's proof: Fact 2.2 on the weighted spaces; Lemma A.1, existence and uniqueness of $A$ with the bounds (A.1), and $A\in\mathcal M_{-1}$; the decay estimate (2.9), $\exp(-\int_r^sA_u/(2\eta_u)du)\le((T-s)/(T-r))^\alpha$; Lemma 2.5, an a priori estimate for the decoupled system (2.11) with homotopy parameter $\mathfrak p\in[0,1]$; Lemma 2.6, explicit unique solvability at $\mathfrak p=0$; Lemma 2.7, the continuation step $\mathfrak p\to\mathfrak p+\mathfrak d$; Proposition 2.8, unique solvability of (2.3) with (2.10) and a norm bound; the boundary limit (2.15); and Proposition 2.9, optimality, the equilibrium property and the value formula.

Significance

The theorem gives a complete equilibrium description for constrained liquidation with many players and stochastic, partially common market data: the equilibrium rate is the conditional expectation of the decoupled feedback rate given the common noise, and its value is explicit in terms of the Riccati solution. It is the basis of the paper's other two results, the $O(N^{-1/2})$-Nash property of the equilibrium in the $N$-player game (Theorem 3.3) and the approximation by penalized games (Theorem 4.6), which are separate missions in this series.

The result is proved in the paper; none of it is machine-checked. A formal development would contain the first formal treatment of BSDEs with singular terminal value and of a conditional (common-noise) mean-field FBSDE. Shorter proofs of individual steps, in particular of the a priori estimate and the continuation step, are welcome.

Difficulty

The obvious approach fails at the terminal time. Standard FBSDE theory requires a terminal condition for $Y$; here only $X_T=0$ is known, and $Y_T$ is undetermined. The decoupling coefficient $A$ blows up like $(T-t)^{-1}$, so the driver of the equation for $B$ is singular, and the classical monotonicity method of Hu–Peng and Peng–Wu, applied to $(X,B)$ in unweighted spaces, does not close. The paper works instead with weighted norms that encode the rate at which $X$ and $B$ vanish at $T$, and runs the continuation on the triple $(X,B,Y)$. The mean-field term is a conditional expectation given the common-noise filtration, not an expectation, so it remains random and has to be controlled pathwise in the weighted norms.

Formalization scope

Time is ℝ≥0; processes are real valued and $\widetilde W$ has $m=k+1$ coordinates, coordinate $0$ being $W^0$. The Itô calculus is the published definition Peng1990.SMP.Stochastic (standard Brownian motion, $L^2_{\mathbb F}$, Itô integrals, BSDEs in integrated form). The explicit choices:

• Filtrations are augmented by the measurable null sets, and $\mathbb F$ contains $\sigma(\mathcal X)$.
• $\kappa_{\max},\eta_\star,\lambda_\star,\|\eta\|$ are essential bounds over $dt\otimes d\mathbb P$. Condition (2.4) is written without division, and "$1/\lambda,1/\eta$ bounded" as positive essential lower bounds.
• Assumption 2.3 is a hypothesis of every statement of §2, as the paper's standing assumption. Lemma A.1 (appendix) assumes only what §A assumes: $\lambda,\eta$ progressive, nonnegative and bounded, and $1/\eta$ bounded.
• Backward equations on $[0,T)$ are imposed on every $[0,\tau]$, $\tau<T$. $A_T=\infty$ means $A_t\to+\infty$ as $t\uparrow T$ a.s.
• Weighted norms are computed in $[0,\infty]$, with the weight $(T-t)^{-l}$ in ℝ≥0∞.
• Every conditional expectation $\mathbb E[\cdot\mid\mathcal F^0_t]$ in an equation is evaluated through a progressive version, and its argument is required to be integrable.
• The value is an essential infimum of conditional costs.
• The relation $Y=AX+B$ is part of the solution concept of (2.11): without it, $Y$ is determined only up to an additive $\mathcal F_0$-measurable constant.
• The constant of Proposition 2.8 is uniform over initial portfolios in an $L^2$ ball, for fixed coefficients.
• Fact 2.2's product rule assumes paths of $K_1$ continuous on $[0,T)$, and its claim that $K_T=0$ for $K\in\mathcal M_l$ is not stated. Both printed versions fail under the essential-supremum norm.

The interaction term must stay conditioned on $\mathcal F^0_t$: conditioning on $\mathcal F_t$ makes it $Y_t/(2\eta_t)$ itself and collapses the game. The constraint $X_T=0$ and the admissibility condition $\int_0^T\xi=\mathcal X$ cannot be dropped either. The degenerate instance $\kappa\equiv0$ satisfies all hypotheses but decouples the game.

A complete development needs the following, all reusable beyond this mission: martingale representation for the augmented filtration $\mathbb F$; existence of progressive versions of conditional expectation processes; Doob's inequality on $[0,\tau]$; and linear BSDE solution formulas.

Selected references

• G. Fu, P. Graewe, U. Horst, A. Popier, A Mean Field Game of Optimal Portfolio Liquidation, arXiv:1804.04911v3, 2021; Math. Oper. Res. 46(4), 2021. https://arxiv.org/abs/1804.04911
• S. Ankirchner, M. Jeanblanc, T. Kruse, BSDEs with singular terminal condition and a control problem with constraints, SIAM J. Control Optim. 52(2), 2014. https://doi.org/10.1137/130913411
• P. Graewe, U. Horst, E. Séré, Smooth solutions to portfolio liquidation problems under price-sensitive market impact, Stoch. Proc. Appl. 128(3), 2018. https://doi.org/10.1016/j.spa.2017.07.002
• P. Cardaliaguet, C.-A. Lehalle, Mean field game of controls and an application to trade crowding, Math. Financ. Econ. 12, 2018. https://doi.org/10.1007/s11579-017-0206-z
• R. Carmona, D. Lacker, A probabilistic weak formulation of mean field games and applications, Ann. Appl. Probab. 25(3), 2015. https://doi.org/10.1214/14-AAP1020
• Y. Hu, S. Peng, Solution of forward-backward stochastic differential equations, Probab. Theory Related Fields 103, 1995. https://doi.org/10.1007/BF01204214

Motivation

A trader who must sell a large position within a fixed horizon faces a trade-off: selling fast moves the price against her (temporary price impact), selling slowly exposes her to price risk. Since Almgren and Chriss, this optimal liquidation problem has been studied as a stochastic control problem with a terminal state constraint: the remaining position must be zero at the horizon $T$. When many traders liquidate at the same time, each trader's sales also depress the price that the others receive (permanent price impact), and the problem becomes a game.

Fu, Graewe, Horst and Popier (arXiv:1804.04911v3) study this game in the mean-field limit. Their §2 constructs a mean-field equilibrium through a singular conditional mean-field FBSDE. Their §3, the subject of this mission, justifies the limit: the strategies computed from the mean field game are an approximate Nash equilibrium of the finite game with $N$ traders, with an error of order $1/\sqrt N$. Without such a result, the mean-field equilibrium describes a model nobody plays; with it, the equilibrium is a usable approximation for large but finite markets.

The approximation of $N$-player games by mean field games goes back to Huang, Malhamé and Caines (2006) and Lasry and Lions (2007); Carmona and Delarue (SIAM J. Control Optim. 51, 2013) proved an $\varepsilon_N$-Nash property for a McKean–Vlasov class with state interaction and a rate $N^{-1/(d+4)}$. The present game differs in three respects: players interact through their controls (the average trading rate), there is a common noise observed by all, and each player's state must reach zero at time $T$.

Setting

A single probability space carries a one-dimensional Brownian motion $W^0$ (the common noise, which drives the benchmark price and is observed by every player), for each player $i$ a $k$-dimensional Brownian motion $W^i$ (the private noise), and i.i.d. initial portfolios $\mathcal X^i$ with law $\nu$; all of these are mutually independent. Player $i$ observes $\mathbb F^i$, $\mathcal F^i_t=\sigma(\mathcal X^i,W^0_s,W^i_s,\ s\le t)$, and chooses a trading rate $\xi^i$; her position is $X^i_t=\mathcal X^i-\int_0^t\xi^i_s\,ds$ and must satisfy $X^i_T=0$. Given the profile $\vec\xi=(\xi^1,\dots,\xi^N)$, her conditional cost is

$$J^{N,i}(\vec\xi)=\mathbb E\Big[\int_0^T\Big(\frac{\kappa^i_t}{N}\sum_{j=1}^N\xi^j_tX^i_t+\eta^i_t(\xi^i_t)^2+\lambda^i_t(X^i_t)^2\Big)dt\ \Big|\ \mathcal X^i\Big],$$

where $\kappa^i$ (permanent impact), $\eta^i$ (temporary impact) and $\lambda^i$ (risk aversion) are nonnegative bounded processes. Under Assumption 3.1 they are the same deterministic measurable functionals $\kappa,\eta,\lambda$ of $(t,\mathcal X^i,W^i_{\cdot\wedge t},W^0_{\cdot\wedge t})$ for every player, so the players are statistically identical.

In the mean field game, the average $\frac1N\sum_j\xi^j$ is replaced by a process $\mu$ adapted to the common-noise filtration $\mathbb F^0$, and an equilibrium is a $\mu^*$ with $\mu^*_t=\mathbb E[\xi^*_t\mid\mathcal F^0_t]$ for the representative player's best response $\xi^*$. The paper characterizes it through the FBSDE (2.3),

$$dX_t=-\frac{Y_t}{2\eta_t}dt,\qquad -dY_t=\Big(\kappa_t\,\mathbb E\Big[\frac{Y_t}{2\eta_t}\Big|\mathcal F^0_t\Big]+2\lambda_tX_t\Big)dt-Z_t\,d\widetilde W_t,\qquad X_0=\mathcal X,\ X_T=0,$$

with $\widetilde W=(W^0,W)$; the optimal rate is $\xi^*=Y/(2\eta)$. Player $i$'s mean-field strategy $\xi^{*,i}=Y^i/(2\eta^i)$ comes from the same FBSDE with her own data.

Formalization targets

Goal: Theorem 3.3

For a positive function $M$ with $\psi\le M$, where $\psi(\mathcal X^i)=\mathbb E[\int_0^T|\xi^{*,i}_t|^2dt\mid\mathcal X^i]$, and admissible sets $\mathcal A^i=\{\xi\in\mathcal A_{\mathbb F^i}(\mathcal X^i):\mathbb E[\int_0^T|\xi_t|^2dt\mid\mathcal X^i]\le M(\mathcal X^i)\}$, there is a function $g$, independent of $i$ and $N$, with

$$J^{N,i}(\vec\xi^*)\le J^{N,i}(\xi^i,\xi^{*,-i})+\frac{g(\mathcal X^i)}{\sqrt N}\qquad\text{for all }N\ge1,\ 1\le i\le N,\ \xi^i\in\mathcal A^i .$$

The goal asserts only the shape of the bound, not its constant.

Milestones

1. Lemma 3.2: one measurable map $\Phi$ gives $(X^i,Y^i,\int_0^\cdot Z^i)=\Phi(\mathcal X^i,W^i,W^0)$ for every player, and $\xi^{*,i}=\phi(\mathcal X^i,W^0,W^i)$ (3.1).
2. (3.2): a single $\mu^*$ with $\mu^*_t=\mathbb E[\xi^{*,i}_t\mid\mathcal F^0_t]$ for every $i$.
3. (3.3): $\mathbb E\int_0^T|\xi^{*,i}_t|^2dt\le C$ uniformly in $i$.
4. (3.5): $\mathbb E[\int_0^T(\mu^*_t-\frac1N\sum_j\xi^{*,j}_t)^2dt\mid\mathcal X^i]\le 2(M(\mathcal X^i)+(2N-1)C)/N^2$.
5. The bounds on $I_1$ and $I_2$ (p. 24): the two differences of conditional costs into which the proof splits $J^{N,i}(\xi,\xi^{*,-i})-J^{N,i}(\vec\xi^*)$ are $O(1/\sqrt N)$.

Significance

The result turns the mean-field equilibrium of §2 into a statement about the finite market: when all $N$ traders use their mean-field strategies, a trader who deviates can save at most $g(\mathcal X^i)/\sqrt N$ in conditional expected cost. The error bound depends on the trader's own initial position only through $M(\mathcal X^i)$, and the rate $1/\sqrt N$ is dimension-free, in contrast with the $N^{-1/(d+4)}$ rates of state-interaction games, because the interaction runs through the empirical mean of the controls rather than through an empirical measure.

The paper's proof of Theorem 3.3 is short but rests on several facts it states without proof: the Yamada–Watanabe-type Lemma 3.2 (whose proof is referred to other papers), the identification (3.2) of a common conditional mean, and the moment bound (3.3) attributed to Proposition 2.8. This mission makes each of these a separate machine-checkable statement. As far as we know, none of these results, nor any optimal-liquidation mean field game, has a machine-checked proof.

Difficulty

The estimate (3.5) is a law-of-large-numbers bound for the average of $N$ processes that are not independent: all of them depend on the common noise $W^0$. The obvious argument, expanding the square and using independence, fails as stated; the cross terms vanish only conditionally on $W^0$, and only once one knows that every $\xi^{*,j}$ is the same measurable functional of $(\mathcal X^j,W^0,W^j)$. That is Lemma 3.2, a Yamada–Watanabe-type statement for a singular FBSDE with a conditional mean-field term, which needs strong uniqueness of the FBSDE in the class $\mathcal H_\alpha\times L^2\times L^2([0,T-])$ and is the main technical step. The terminal constraint $X_T=0$ makes the backward component singular at $T$ ($Y$ blows up like $X/(T-t)$), so standard Lipschitz FBSDE theory does not apply. Finally, the deviation $\xi$ is constrained only through a conditional second-moment bound $M$, and the comparison with the mean-field cost uses the optimality of $\xi^{*,i}$ (Proposition 2.9) against $\mu^*$.

Formalization scope

Everything is stated on one probability space carrying all players, with players indexed by $\mathbb N$; the $N$-player game uses players $i<N$ (the paper's $1,\dots,N$, shifted by one). Time is $\mathbb R_{\ge0}$ and the processes are real valued. Choices made explicit:

• Assumption 2.3 for every player is a hypothesis of every theorem: the paper states it "throughout" (p. 8), and the proof of Theorem 3.3 uses Propositions 2.8 and 2.9, which need it. Its constants $\kappa_{\max},\eta_\star,\lambda_\star,\|\eta\|$ are essential bounds over $[0,T]\times\Omega$; "$1/\lambda,1/\eta\in L^\infty$" is a positive essential lower bound.
• The equilibrium processes $(X^i,Y^i,Z^i)$ are hypotheses: solutions of (2.3) for player $i$'s data in the class of Theorem 2.4. $\xi^{*,i}$ is defined as $Y^i/(2\eta^i)$, never through $\phi$.
• Conditioning on $\mathcal X^i=x^i$ is conditioning on $\sigma(\mathcal X^i)$; every conclusion holds almost surely, i.e. for $\nu$-a.e. $x^i$. "$\psi\le M$" is the a.s. inequality of conditional second moments, and $M$ is assumed measurable.
• $g$ is quantified before $N$ and $i$. A statement in which $g$ may depend on $N$ is trivially true and is ruled out.
• Filtrations are augmented by null sets. Each conditional expectation $\mathbb E[\,\cdot\mid\mathcal F^0_t]$ is evaluated through a progressive version of an integrable argument. BSDEs on $[0,T)$ are imposed on every $[0,\tau]$, $\tau<T$.
• Lemma 3.2's path spaces carry the product σ-algebra; its identities hold for each $t$ almost surely.
• The paper's bound on $I_2$ is stated for $|I_2|$, which is what its Cauchy–Schwarz step gives and what the proof needs.

The development reuses the Itô-calculus definitions of Peng1990.SMP.Stochastic (standard Brownian motion, $L^2_{\mathbb F}$, Itô integrals, BSDEs). Contributions useful beyond this mission: conditional independence given a common noise for functionals of independent inputs, a Yamada–Watanabe argument for FBSDEs, and conditional Cauchy–Schwarz bounds for time integrals. Proofs of any milestone, and of the facts from §2 they rely on, are welcome.

Selected references

• G. Fu, P. Graewe, U. Horst, A. Popier, A Mean Field Game of Optimal Portfolio Liquidation, arXiv:1804.04911v3, 2021; Math. Oper. Res. 46(4), 2021. https://arxiv.org/abs/1804.04911
• R. Almgren, N. Chriss, Optimal execution of portfolio transactions, J. Risk 3(2), 2001. https://doi.org/10.21314/JOR.2001.041
• M. Huang, R. P. Malhamé, P. E. Caines, Large population stochastic dynamic games: closed-loop McKean–Vlasov systems and the Nash certainty equivalence principle, Commun. Inf. Syst. 6(3), 2006. https://doi.org/10.4310/CIS.2006.v6.n3.a5
• J.-M. Lasry, P.-L. Lions, Mean field games, Jpn. J. Math. 2, 2007. https://doi.org/10.1007/s11537-007-0657-8
• R. Carmona, F. Delarue, Probabilistic analysis of mean-field games, SIAM J. Control Optim. 51(4), 2013. https://doi.org/10.1137/120883499
• S. Peng, A general stochastic maximum principle for optimal control problems, SIAM J. Control Optim. 28(4), 1990. https://doi.org/10.1137/0328054

Motivation

Brands are routinely held responsible for the labour and environmental practices of their suppliers. A brand that is linked in public to a non-compliant supplier loses consumer willingness to pay, and firms answer this risk by auditing their suppliers. Supply networks are not trees, however: one supplier often serves several competing brands. Chen, Qi and Dawande (SSRN 2889889, Manufacturing & Service Operations Management, 2020) ask how the position of a supplier in such a network, and in particular its centrality (the number of buyers it serves), affects which suppliers get audited when buyers decide on their own, and when they audit jointly.

This mission formalizes the paper's answer for unilateral auditing by competing buyers (Sec. 4.2, Proposition 2). A companion mission treats joint auditing (Proposition 3).

Setting

Two buyers $B_1, B_2$ source from three suppliers: an independent supplier $S_i$ for each buyer $B_i$, and a common supplier $S_c$ that serves both. Each supplier complies with social-responsibility standards with probability $e \in (0,1)$. In stage 1, buyer $B_i$ chooses an auditing effort $e_{ii} \in [0,1]$ on $S_i$ and $e_{ic} \in [0,1]$ on $S_c$, and audits at most one of them: $e_{ii}\,e_{ic} = 0$. Auditing a supplier with effort $x > 0$ costs $K + \tfrac a2 x^2$, with a fixed cost $K \ge 0$ and $a > 0$; effort $0$ means no audit and costs nothing.

A non-compliant supplier that passes the audits is discovered in public with probability $r \in (0,1]$. Hence $S_i$ causes damage to $B_i$ with probability $\lambda_I(e_{ii}) = r(1-e)(1-e_{ii})$, and $S_c$ causes damage to both buyers with probability $\lambda_C(e_{1c},e_{2c}) = r(1-e)(1-e_{1c})(1-e_{2c})$, independently. A buyer with at least one exposed supplier suffers the MWTP damage $d_M > 0$: his demand intercept drops from $\alpha$ to $\alpha - d_M$. Each exposed supplier is then paid $\hat w \ge w$ per unit instead of $w$, so a buyer with $n \in \{0,1,2\}$ exposed suppliers has unit cost $(2-n)w + n\hat w$.

In stage 2 the buyers compete in quantities with inverse demands $p_i = A_i - q_i - \beta q_{i'}$, $\beta \in (0,1]$ (Dixit 1979; Singh and Vives 1984). Its equilibrium profit for $B_1$ is $\pi^b_1(n_1,n_2) = q^*_1(n_1,n_2)^2$, in closed form (Lemma 1). Buyer $B_1$'s ex ante expected profit $\Pi^b_1(e_{11},e_{1c};e_{22},e_{2c})$ is the expectation of $\pi^b_1$ over the eight damage outcomes, minus his audit costs; $\Pi^b_2$ is symmetric. Three conditions on $(\alpha,\beta,w,\hat w,d_M)$ (p. 8) make all stage-2 quantities positive.

An equilibrium is a profile $(s_1,s_2)$, $s_i = (e_{ii},e_{ic})$, in which each buyer's strategy is a best response to the other's, with the tie-breaking rule of p. 10: a buyer who is indifferent between auditing and not auditing does not audit. Two explicit efforts, $e^*_I$ (eq. (1)) and $\hat e_I$ (eq. (2)), are rational functions of the parameters; $\hat e_I$ is a buyer's optimal effort on his independent supplier when the rival audits nobody, and $e^*_I$ is the symmetric solution when both audit their independent suppliers.

Formalization targets

Goal: Proposition 2

Assume $\beta \in (0,1]$ and $\hat e_I < 1$. There exist $K^L_u < K^M_u < K^H_u$ such that for every $K \ge 0$, writing $A = ((e^*_I,0),(e^*_I,0))$, $B_1 = ((\hat e_I,0),(0,0))$, $B_2 = ((0,0),(\hat e_I,0))$, $N = ((0,0),(0,0))$,

$$\mathrm{EqSet}(K) = \begin{cases} \{A\} & K < K^L_u,\\ \{A, B_1, B_2\} & K^L_u \le K < K^M_u,\\ \{B_1, B_2\} & K^M_u \le K < K^H_u,\\ \{N\} & K \ge K^H_u. \end{cases}$$

In every equilibrium the common supplier receives zero effort.

Milestones

Lemma 1 (stage-2 equilibrium), the OA.2 expected-profit display, the best-response function (OA-9) with $e^*_I$ and $\hat e_I$ as its values, the dominance inequality (OA-11), Lemmas OA5 and OA6 (the two kinds of auditing equilibria and their threshold ranges), the monotonicity facts (OA-14)–(OA-15), Lemma OA7 (the order of the thresholds) and Lemma OA8 (no equilibrium audits $S_c$). The thresholds of the milestones are the explicit ones the proof defines in (OA-10), (OA-12), (OA-13).

Significance

The result separates network position from competition. Without downstream competition ($\beta = 0$, Proposition 1) there is a Pareto-dominant equilibrium in which one buyer audits the common supplier. With competition, Proposition 2 shows that the common supplier, the most central and therefore the most consequential source of risk, is never audited: auditing it would also protect the rival, who free-rides. This inefficiency is what motivates the paper's analysis of joint auditing (Proposition 3) and of social welfare (Proposition 4).

The result is proved in the paper, partly by omission: the e-companion leaves the proof of Lemma OA8 and the case $K \ge K^H_u$ to the reader. No machine-checked version exists. A formal proof would give a complete case analysis of a two-stage game with a discontinuous fixed cost, a constrained strategy set and a tie-breaking rule, and would check the paper's closed forms, several of which are printed with small slips.

Difficulty

The first-order conditions alone do not determine the equilibria. The fixed cost makes each buyer's payoff discontinuous at zero effort, so every candidate must be compared with no audit, and the best response is a choice among three regimes (audit $S_i$, audit $S_c$, audit nobody). Uniqueness claims therefore require excluding every profile in the constrained strategy set, including those where a buyer audits the common supplier, for which the paper gives no proof. The threshold comparisons $K^L_u < K^M_u < K^H_u$ rest on monotonicity in the rival's effort, and the expected profit is multilinear in the four efforts (plus the quadratic audit costs), with coefficients that are differences of squared Cournot quantities whose signs depend on the p. 8 conditions.

Formalization scope

All objects live in the namespace SupplierAudit.Competition. The source is the authors' accepted manuscript on SSRN (2889889); main-text printed pages equal PDF pages, and e-companion page ec $k$ is PDF page $28 + k$.

• Parameters. A structure Params carries $\alpha, \beta, w, \hat w, d_M, e, r, a$ and the standing assumptions $\beta \in [0,1]$, $w \le \hat w$, $d_M > 0$, $e \in (0,1)$, $r \in (0,1]$, $a > 0$ and the three conditions of p. 8. The theorems add $\beta > 0$ (competition, Sec. 4.2). $K$ is a separate real argument and the goal quantifies over $K \ge 0$.
• Stage 2. The general linear differentiated Cournot duopoly is its own definition (CournotDuopoly). The model's stage-2 profit is the closed form $q^*_1(n_1,n_2)^2$ for all $(n_1,n_2)$; Lemma 1 states that it is the game's unique equilibrium.
• Expected profit. $\Pi^b_1$ is the eight-outcome expectation; $\Pi^b_2$ is $\Pi^b_1$ with the roles exchanged. The grouped display of OA.2 is a milestone.
• Strategies and equilibrium. Strategies are pairs in $[0,1]^2$ with product zero. Equilibria include the strict-improvement tie-breaking rule of p. 10; without it the goal is false at $K = K^M_u$ and $K = K^H_u$.
• Interior efforts. The paper assumes equilibrium efforts lie in $(0,1)$ (p. 10; sufficient conditions in OA.1 are not given in closed form). This is encoded as the single hypothesis $\hat e_I < 1$ on the explicit formula (2), never as a hypothesis on an unknown equilibrium variable.
• Thresholds. The goal states the thresholds existentially, as printed, with their order as part of the conclusion; the milestones use the explicit (OA-10), (OA-12), (OA-13). $e^*_I$, $\hat e_I$ and $e^*_{11}(\cdot)$ are the printed formulas, not argmaxes.
• Printed slips, corrected. In (OA-11) the second prefactor should be $\beta(\hat w - w)$; only the strict inequality is stated. The printed derivative of $e^*_{11}$ in the proof of Lemma OA7 lacks a factor $1/a$; only monotonicity is stated.

A formalization in which equilibrium is plain Nash, efforts range over all of $\mathbb R$, a buyer may audit both suppliers, or "interior" is a hypothesis on the equilibrium efforts themselves would state a different (and in places false or vacuous) theorem; these are ruled out by the definitions above. Proofs of any milestone are welcome, as is reusable infrastructure for linear Cournot duopolies and for finite expectations over independent Bernoulli events.

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). https://ssrn.com/abstract=2889889
• A. Dixit, A Model of Duopoly Suggesting a Theory of Entry Barriers, Bell Journal of Economics 10(1), 1979. https://doi.org/10.2307/3003317
• N. Singh, X. Vives, Price and Quantity Competition in a Differentiated Duopoly, RAND Journal of Economics 15(4), 1984. https://doi.org/10.2307/2555525
• 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), 2016. https://doi.org/10.1287/msom.2015.0550

Motivation

Best-subset selection with ridge shrinkage, $\min_\beta \tfrac12\|y-X\beta\|_2^2+\lambda_0\|\beta\|_0+\lambda_2\|\beta\|_2^2$, is a mixed-integer program that statisticians want to solve to certified optimality at the scale of modern data ($p$ up to $10^7$ features). Hazimeh, Mazumder and Saab (arXiv:2004.06152, Mathematical Programming 2022) built a branch-and-bound solver, L0BnB, whose node relaxations are solved in the primal space by active-set coordinate descent instead of by an interior-point method. Branch-and-bound prunes a node only with a valid dual bound, a certified lower bound on the node's relaxation value. A primal method returns an approximate minimizer, not such a bound, so the solver must turn an inexact primal point into a dual feasible point and needs to know how much is lost in doing so. This mission formalizes the paper's answer, its main theorem (Theorem 3).

Setting

Data are $X\in\mathbb R^{n\times p}$ with columns $X_1,\dots,X_p$, $y\in\mathbb R^n$, and parameters $\lambda_0,\lambda_2,M>0$. The reverse Huber penalty is $\mathcal B(t)=|t|$ for $|t|\le1$ and $(t^2+1)/2$ for $|t|\ge1$. The penalty $\psi(b)$ equals $\psi_1(b)=2\lambda_0\mathcal B(b\sqrt{\lambda_2/\lambda_0})$ if $\sqrt{\lambda_0/\lambda_2}\le M$ and $\psi_2(b)=(\lambda_0/M+\lambda_2M)|b|$ otherwise. The reduced relaxation (5) is

$$\min_{\beta\in\mathbb R^p}\ F(\beta)=\tfrac12\|y-X\beta\|_2^2+\sum_{i}\psi(\beta_i)\quad\text{s.t.}\quad \|\beta\|_\infty\le M .$$

Throughout, the columns of $X$ and $y$ have unit $\ell_2$ norm (the standing assumption of Section 3 of the paper).

Algorithm 2 (active-set coordinate descent) returns a point $\hat\beta$ in the box such that the set

$$V=\{i\notin\operatorname{Supp}(\hat\beta):\ 0\ne\operatorname*{arg\,min}_{|t|\le M}F(\hat\beta_1,\dots,t,\dots,\hat\beta_p)\}$$

is empty: no coordinate outside the support wants to move. Write $\hat r=y-X\hat\beta$, $k=\|\hat\beta\|_0$, and let $\beta^*$ be an optimal solution of (5) with $r^*=y-X\beta^*$. The primal gap is $\epsilon=\|X(\beta^*-\hat\beta)\|_2$.

The two duals of (5) (Theorem 2 of the paper) are, with $v(\alpha,\gamma_i)=[(\alpha^\top X_i-\gamma_i)^2/(4\lambda_2)-\lambda_0]_++M|\gamma_i|$,

$$h_1(\alpha,\gamma)=-\tfrac12\|\alpha\|_2^2-\alpha^\top y-\textstyle\sum_i v(\alpha,\gamma_i),\qquad h_2(\rho,\mu)=-\tfrac12\|\rho\|_2^2-\rho^\top y-M\|\mu\|_1,$$

the latter under $|\rho^\top X_i|-\mu_i\le\lambda_0/M+\lambda_2M$. The dual variables built from $\beta^*$ are $\alpha^*=\rho^*=-r^*$, $\gamma^*_i=\mathbb 1_{[|\beta^*_i|=M]}(\alpha^{*\top}X_i-2M\lambda_2\operatorname{sign}(\alpha^{*\top}X_i))$ and $\mu^*_i=\mathbb 1_{[|\beta^*_i|=M]}(|\rho^{*\top}X_i|-\lambda_0/M-\lambda_2M)$. The dual points built from $\hat\beta$ are $\hat\alpha=\hat\rho=-\hat r$, with $\hat\gamma$ a maximizer of $h_1(\hat\alpha,\cdot)$ (25) and $\hat\mu$ a maximizer of $h_2(\hat\rho,\cdot)$ under the constraints (27).

Formalization targets

Goal: Theorem 3 with the proof's constants

If $\sqrt{\lambda_0/\lambda_2}\le M$, with $c_i=(2\lambda_2)^{-1}$ when $|\beta^*_i|<M$ and $c_i=M$ when $|\beta^*_i|=M$,

$$h_1(\hat\alpha,\hat\gamma)\ \ge\ h_1(\alpha^*,\gamma^*)-2\epsilon-\tfrac12\epsilon^2-\sum_{i\in\operatorname{Supp}(\hat\beta)}\big(c_i\epsilon+(4\lambda_2)^{-1}\epsilon^2\big).\qquad(55)$$

If $\sqrt{\lambda_0/\lambda_2}>M$,

$$h_2(\hat\rho,\hat\mu)\ \ge\ h_2(\rho^*,\mu^*)-\epsilon(2+Mk)-\tfrac12\epsilon^2.\qquad(59)$$

The paper states these as $-kO(\epsilon)-kO(\epsilon^2)$ (29) and $-kO(\epsilon)-O(\epsilon^2)$ (30); the goal states the expressions its proof establishes.

Milestones

In the order the proof uses them: the closed-form coordinate updates (14) and (15); Proposition 3, $V=\{i\notin\operatorname{Supp}(\hat\beta): |\langle\hat r,X_i\rangle|>c(\lambda_0,\lambda_2,M)\}$; the bound $\|\alpha^*\|_2\le1$; Lemma 2, which bounds $v(\hat\alpha,\hat\gamma_i)$ coordinate by coordinate and makes it vanish off the support; inequality (53); the closed form (28) of $\hat\mu$; the optimality conditions (58); the bound (57) $|\hat\mu_i|\le\epsilon+|\mu^*_i|$ on the support; and inequality (56).

Significance

The result. In both regimes the loss of the dual bound is controlled by the primal gap times the sparsity $k$ of the iterate, with constants depending only on $M$ and $\lambda_2$; the number of features $p$ does not enter. Since L0BnB seeks solutions with $k\ll p$, the cheap dual bound obtained from an inexact primal solution is nearly as good as the exact one, which is what allows pruning without an interior-point solve at every node. The paper notes that with plain coordinate descent in place of Algorithm 2 the same argument gives $p$ in place of $k$.

Formalizing it. The result is proved in the paper; it has no machine-checked proof. The mission produces a checked version of the main theorem with explicit constants, a formal model of what "output of an active-set method" means for the analysis, and reusable closed forms for the boxed soft-thresholding updates of an $\ell_1$- or reverse-Huber-penalized box-constrained least squares problem.

Difficulty

The bound is not a consequence of weak duality alone: weak duality says only that each dual value is below the primal optimum, and says nothing about how far the constructed dual point is from the dual optimum. The obvious estimate, a Lipschitz bound on $h_1$ or $h_2$ summed over all coordinates, gives a loss proportional to $p$. Getting $k$ instead requires showing that the dual contribution of every coordinate outside $\operatorname{Supp}(\hat\beta)$ vanishes exactly, which uses the emptiness of $V$ through Proposition 3 and the closed forms (14)–(15) of one-dimensional nonsmooth box-constrained problems. On the support, the loss must be bounded using the structure of $\gamma^*$ and $\mu^*$ at coordinates where $\beta^*$ hits the box, which is where $c_i=M$ and (58) enter.

Formalization scope

Indices are Fin p; norms are explicit sums; $\operatorname{sign}$ is Real.sign with $\operatorname{sign}(0)=0$; $[a]_+$ is max a 0. The unit norms of the columns of $X$ and of $y$ are hypotheses, never built into the definitions, and each theorem assumes only the ones it uses. $\beta^*$ is any point of the box minimizing $F$ over the box. The output of Algorithm 2 is modelled by its two properties used in the paper: $\|\hat\beta\|_\infty\le M$ and $V=\emptyset$ ("$0\ne\arg\min$" encoded as "$0$ is not a minimizer"); the iterations are not formalized. $\hat\gamma$ and $\hat\mu$ are arbitrary maximizers satisfying (25) and (27). The dual variables (23)–(24) are defined by their formulas; their optimality (Theorem 2, a separate mission) is neither assumed nor needed, and the goal is an inequality between explicit numbers.

Instantiations of $O(\cdot)$. (29) is stated as (55): $kO(\epsilon)+kO(\epsilon^2)$ becomes $2\epsilon+\tfrac12\epsilon^2+\sum_{i\in\operatorname{Supp}(\hat\beta)}(c_i\epsilon+(4\lambda_2)^{-1}\epsilon^2)$ with $c_i\in\{(2\lambda_2)^{-1},M\}$ decided by $\beta^*$. (30) is stated as (59): $kO(\epsilon)+O(\epsilon^2)$ becomes $\epsilon(2+Mk)+\tfrac12\epsilon^2$. The proof's final rearrangement of (29), which counts $|\hat\beta_i|$ instead of $|\beta^*_i|$, is not used.

A formalization that takes $\hat\beta=\beta^*$, $\hat\gamma=\gamma^*$ or $\hat\mu=\mu^*$, that drops the hypothesis $V=\emptyset$, or that replaces the constants by an existential "$\exists C$" would be trivial or a different statement; the goal quantifies over every optimal $\beta^*$, every box-feasible $\hat\beta$ with $V=\emptyset$ and every maximizer $\hat\gamma$, $\hat\mu$, with the explicit constants above.

Needed infrastructure: one-dimensional convex minimization on an interval with piecewise penalties, Cauchy–Schwarz for finite sums, and first-order optimality conditions for box-constrained composite problems. Proofs of any milestone are welcome independently.

Selected references

• H. Hazimeh, R. Mazumder, A. Saab, Sparse Regression at Scale: Branch-and-Bound rooted in First-Order Optimization, arXiv:2004.06152v2, 2021; Mathematical Programming 196 (2022). https://arxiv.org/abs/2004.06152
• P. Tseng, Convergence of a block coordinate descent method for nondifferentiable minimization, J. Optim. Theory Appl. 109 (2001). https://doi.org/10.1023/A:1017501703105
• J. Friedman, T. Hastie, R. Tibshirani, Regularization paths for generalized linear models via coordinate descent, J. Stat. Softw. 33 (2010). https://doi.org/10.18637/jss.v033.i01

Motivation

Second order dynamical systems with vanishing damping are continuous-time models of accelerated first-order methods. The system $\ddot x + \frac{\alpha}{t}\dot x + \nabla g(x) = 0$ is the continuous limit of Nesterov's accelerated gradient method (Su, Boyd, Candès 2016), and its trajectories converge weakly to a minimizer of a convex $g$ when $\alpha>3$ (Attouch, Chbani, Peypouquet, Redont 2018). Two modifications of this system have been studied separately. A Hessian-driven damping term $\beta\nabla^2 g(x)\dot x$ damps oscillations and keeps the fast rates (Attouch, Peypouquet, Redont 2016). A Tikhonov regularization term $\epsilon(t)x$ with $\epsilon(t)\to0$ selects one minimizer, the one of minimum norm, and can turn weak convergence into strong convergence (Attouch, Chbani, Riahi 2018).

Boţ, Csetnek and László (arXiv:1911.12845v2, Math. Program. 2021) study the system with both terms. Their results split into two regimes according to how fast $\epsilon$ decays. This mission covers the slow-decay regime of §4.1, where $\int^{+\infty}\epsilon(t)/t\,dt=+\infty$ and the trajectory approaches the minimum-norm minimizer in a weighted average sense.

Timeline. 2016: Su, Boyd and Candès derive the continuous model of Nesterov's method. 2016: Attouch, Peypouquet and Redont add Hessian-driven damping ($\alpha\ge3$, $\beta>0$) and prove fast rates and weak convergence. 2018: Attouch, Chbani and Riahi add Tikhonov regularization without Hessian damping and prove, among other results, strong ergodic convergence to the minimum-norm minimizer when $\int\epsilon(t)/t\,dt=+\infty$. 2020: Boţ, Csetnek and László combine both terms and extend that ergodic result (their Theorem 4.2).

Setting

Let $\mathcal H$ be a real Hilbert space, $t_0>0$, $\alpha>0$, $\beta\ge0$, and $u_0,v_0\in\mathcal H$. The data satisfy the paper's General assumption:

• $g:\mathcal H\to\mathbb R$ is convex and twice Fréchet differentiable, its gradient $\nabla g$ is Lipschitz continuous on bounded sets, and $\operatorname{argmin} g\neq\emptyset$;
• $\epsilon:[t_0,+\infty)\to[0,+\infty)$ is nonincreasing, of class $C^1$, and $\lim_{t\to+\infty}\epsilon(t)=0$.

A global $C^2$-solution of system (5) is a twice continuously differentiable $x:[t_0,+\infty)\to\mathcal H$ with

$$\ddot x(t)+\frac{\alpha}{t}\dot x(t)+\beta\nabla^2 g(x(t))\dot x(t)+\nabla g(x(t))+\epsilon(t)x(t)=0\quad(t\ge t_0),\qquad x(t_0)=u_0,\ \dot x(t_0)=v_0 .$$

The set $\operatorname{argmin} g$ is nonempty, closed and convex, so it has a unique element of minimum norm, the minimum-norm minimizer $x^*=\operatorname{argmin}\{\|x\|:x\in\operatorname{argmin} g\}$. For $\epsilon>0$ the Tikhonov approximation curve is

$$x_\epsilon=\operatorname*{argmin}_{x\in\mathcal H}\Big(g(x)+\frac{\epsilon}{2}\|x\|^2\Big),$$

the unique minimizer of a strongly convex function. Finally, $h_{x^*}(t)=\tfrac12\|x(t)-x^*\|^2$ measures the distance of the trajectory to $x^*$, with derivative $\dot h_{x^*}(t)=\langle\dot x(t),x(t)-x^*\rangle$.

Formalization targets

Goal: Theorem 4.2 (p. 18)

If $\int_{t_0}^{+\infty}\frac{\epsilon(t)}{t}\,dt=+\infty$ and $\alpha>0$, then every global $C^2$-solution satisfies

$$\lim_{t\to+\infty}\frac{1}{\int_{t_0}^{t}\frac{\epsilon(s)}{s}\,ds}\int_{t_0}^{t}\frac{\epsilon(s)}{s}\|x(s)-x^*\|^2\,ds=0 \qquad\text{and}\qquad \liminf_{t\to+\infty}\|x(t)-x^*\|=0 .$$

No rate and no constant is asserted, so the goal does not depend on any particular choice of $\epsilon$.

Milestones

1. Lemma 4.1 (p. 16): for $\alpha>0$, $\beta\ge0$, the velocity is bounded, $\frac1t\|\dot x(t)\|^2\in L^1([t_0,+\infty))$, and $\sup_{t\ge t_0}\frac1t|\dot h_{x^*}(t)|<+\infty$ for every $x^*\in\operatorname{argmin} g$.
2. §4, p. 18: $\|x_\epsilon\|\le\|x^*\|$ for every $\epsilon>0$.
3. §4, p. 18: $\lim_{\epsilon\to0^+}x_\epsilon=x^*$ (stated in the paper as well known).
4. (46) (p. 20): under the hypotheses of Theorem 4.2 there is $C>0$ with

$$\int_{t_0}^{t}\frac{\epsilon(s)}{s}\Big(h_{x^*}(s)-\frac12\big(\|x^*\|^2-\|x_{\epsilon(s)}\|^2\big)\Big)ds\le C\quad\text{for every }t\ge t_0 .$$

Significance

The result shows that slow Tikhonov regularization still selects the minimum-norm minimizer when Hessian damping is added: the weighted time average of $\|x(t)-x^*\|^2$ tends to zero and the trajectory comes arbitrarily close to $x^*$ infinitely often. The hypothesis is only $\alpha>0$, well below the threshold $\alpha\ge3$ that the paper needs for its fast rates, and no growth condition on $\epsilon$ beyond the divergence of $\int\epsilon(t)/t\,dt$ is imposed. It complements Theorem 4.4 of the same paper (a separate mission), which reaches full strong convergence under fast decay, $\int\epsilon(t)/t\,dt<+\infty$, plus further conditions.

On the formal side, the theorem and its milestones are proved in the paper and in the cited literature, but none of them has a machine-checked proof. The work splits into an energy estimate for a nonautonomous second order ODE in a Hilbert space (Lemma 4.1), two facts about the Tikhonov curve that underlie the whole theory of Tikhonov regularization of convex problems (milestones 2 and 3), an integrated differential inequality (46), and a l'Hospital-type averaging step. The Tikhonov-curve facts are reusable for any formal treatment of viscosity selection and minimum-norm solutions.

Difficulty

The obvious attempt, a Lyapunov function that decreases along the trajectory and controls $\|x(t)-x^*\|$, fails because $x^*$ is not a stationary point of the perturbed system: $\nabla g(x^*)+\epsilon(t)x^*=\epsilon(t)x^*\neq0$ in general. The distance to $x^*$ therefore need not decrease, and pointwise convergence is not available under the slow-decay hypothesis alone. The comparison point has to move along the Tikhonov curve $x_{\epsilon(t)}$, whose convergence to $x^*$ comes without a rate. The available bound controls only a weighted integral of $h_{x^*}$ corrected by $\|x^*\|^2-\|x_{\epsilon(s)}\|^2$, so the passage from (46) to the goal needs both $x_{\epsilon(t)}\to x^*$ and the divergence of the weight. In the formal setting the Tikhonov-curve limit is itself a nontrivial weak-compactness argument in a Hilbert space, which the paper does not spell out.

Formalization scope

• $\mathcal H$ is a real Hilbert space (InnerProductSpace ℝ H, CompleteSpace H). $\nabla g$ is gradient g, and $\nabla^2 g(x)v$ is the Fréchet derivative of gradient g at $x$ applied to $v$. "Twice Fréchet differentiable" means $g$ and $\nabla g$ are differentiable; Lipschitz continuity on bounded sets is stated on every closed ball around the origin.
• Trajectories are maps $\mathbb R\to\mathcal H$ with explicit velocity and acceleration maps; derivatives are taken within $[t_0,+\infty)$ (one-sided at $t_0$), the acceleration is continuous there, and values before $t_0$ are irrelevant. The same holds for $\epsilon$ and its derivative.
• Every theorem is stated for every global $C^2$-solution of (5). Existence and uniqueness of the solution is Theorem 2.1 of the paper, a milestone of the first mission of this series, so the hypothesis is not vacuous. The paper's standing $\alpha\ge3$ is replaced by each statement's own hypothesis $\alpha>0$.
• The minimum-norm minimizer and the Tikhonov points are predicates on a candidate point; where the curve $\epsilon\mapsto x_\epsilon$ is needed, a selection that minimizes $g+\frac\epsilon2\|\cdot\|^2$ for every $\epsilon>0$ is a hypothesis.
• $\int_{t_0}^{+\infty}\epsilon(t)/t\,dt=+\infty$ is stated as divergence of $T\mapsto\int_{t_0}^T\epsilon(t)/t\,dt$, never as an equation for a Bochner integral, which would take the value $0$ on a non-integrable function. Likewise, $\liminf\|x(t)-x^*\|=0$ is stated as "for every $\delta>0$, $\|x(t)-x^*\|<\delta$ for arbitrarily large $t$", not through Filter.liminf, whose value on an unbounded function is a default. $\sup<+\infty$ is boundedness from above of the image of $[t_0,+\infty)$, and $L^1$ membership is integrability on $[t_0,+\infty)$.
• Definitions needed: argmin, the minimum-norm minimizer, Tikhonov points, the General assumption, the solution predicate for (5), and $h_{x^*}$, $\dot h_{x^*}$. These duplicate objects of the other two missions of the series, which are drafted independently.
• Contributions welcome: proofs of the Tikhonov-curve facts in Mathlib generality, the energy estimate of Lemma 4.1, a continuous l'Hospital/Cesàro lemma for weighted averages, and the goal itself.

Selected references

• R.I. Boţ, E.R. Csetnek, S.C. László, Tikhonov regularization of a second order dynamical system with Hessian driven damping, Mathematical Programming, 2021, https://doi.org/10.1007/s10107-020-01528-8 (cited from arXiv:1911.12845v2). https://arxiv.org/abs/1911.12845
• H. Attouch, Z. Chbani, H. Riahi, Combining fast inertial dynamics for convex optimization with Tikhonov regularization, Journal of Mathematical Analysis and Applications 457(2), 1065–1094, 2018. https://arxiv.org/abs/1602.01973
• H. Attouch, J. Peypouquet, P. Redont, Fast convex optimization via inertial dynamics with Hessian driven damping, Journal of Differential Equations 261(10), 5734–5783, 2016. https://arxiv.org/abs/1601.07113
• H. Attouch, Z. Chbani, J. Peypouquet, P. Redont, Fast convergence of inertial dynamics and algorithms with asymptotic vanishing viscosity, Mathematical Programming 168, 123–175, 2018. https://arxiv.org/abs/1507.04782
• W. Su, S. Boyd, E.J. Candès, A differential equation for modeling Nesterov's accelerated gradient method: theory and insights, Journal of Machine Learning Research 17(153), 1–43, 2016. https://arxiv.org/abs/1503.01243