Operations Research

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

In an optimal stopping problem the value function $V$ and the gain function $G$ agree on the stopping set $D=\{V=G\}$, and $V>G$ on the continuation set $C$. The smooth fit principle says that, at the boundary $\partial C$ between them, $V$ meets $G$ with matching first derivatives. Smooth fit is one of the boundary conditions in the free-boundary problems that characterise optimal stopping boundaries. It is behind the integral equations for the early-exercise boundary of the American put and for many problems in sequential analysis and finance (Peskir & Shiryaev, 2006). On a finite horizon the value depends on the remaining time, and continuity of the time derivative $\partial_tV$ across $\partial C$ is the step that justifies the local time-space calculus applied to $V$ (Peskir, 2005).

Before De Angelis & Peskir (2020) such continuity results were proved problem by problem, or under sign conditions that the main examples do not satisfy: $G=0$ on the stopping set and $H<0$ globally, which fails for the American put. Their paper gives two general results. Theorem 8 covers the space derivative, and Theorem 15, the subject of this mission, covers the time derivative on a finite horizon. Both are stated for a strong Markov process realised as a stochastic flow, and both rest on probabilistic regularity of the boundary.

Setting

Fix a horizon $T>0$ and $d=m+1\ge1$. The process is the time-space process $X^{t,x}_s=(t+s,X^x_s)$. Its first coordinate is time, and $(X^x_s)_{s\ge0,\,x\in\mathbb R^{d-1}}$ is a stochastic flow on a probability space $(\Omega,\mathcal F,P)$ with a right-continuous filtration $(\mathcal F_s)$, adapted to it, with $X^x_0=x$. Its paths are right-continuous with left limits, it is left-continuous over stopping times, and it is strong Markov. The flow is continuous in the space variable if, outside one null set, $x\mapsto X^x_s(\omega)$ is continuous for every $s$.

Given continuous functions $\lambda\ge0$, $G$ and $H$ of $(t,x)$, write $\Lambda^{t,x}_s=\int_0^s\lambda(t+u,X^x_u)\,du$. The value function is

$$V(t,x)=\sup_{0\le\tau\le T-t}\mathsf E\Big[e^{-\Lambda^{t,x}_\tau}G(t+\tau,X^x_\tau)+\int_0^\tau e^{-\Lambda^{t,x}_s}H(t+s,X^x_s)\,ds\Big]$$

over stopping times $\tau$ bounded by the remaining time $T-t$. The sets are $C=\{V>G\}$ and $D=\{V=G\}$ inside $[0,T]\times\mathbb R^{d-1}$, and $\partial C=D\cap\overline C$. The problem is well posed if the expected payoffs are integrable and the first entry time $\tau_D$ into $D$ is optimal.

The first hitting time of a set $A$ is $\sigma^{t,x}_A=\inf\{s\in(0,T-t]:X^{t,x}_s\in A\}$. A point $z$ is probabilistically regular for $A$ if $P(\sigma^z_A=0)=1$. The generator $\mathbb L_X$ (2.14) acts in the space variable, with diffusion matrix $\sigma_{ij}$, drift $\mu_i$, killing rate $\lambda$ and jump measure $\nu$. Its coefficient formula is tied to the flow by the right derivative at zero of the killed spatial semigroup applied to $G(t,\cdot)$. The function $\tilde H=G_t+\mathbb L_XG+H$ appears in the hypotheses.

Formalization targets

Goal: Theorem 15, global form (p. 20)

Assume well-posedness, (5.9) ($V$ continuous on $[0,T]\times\mathbb R^{d-1}$ and $C^1$ on $C$), (5.10) ($G\in C^{1,2}$) and (5.11) (Lipschitz continuity of $\tilde H$ and $\lambda$ in $t$, uniformly in $x$), and a continuous flow. Assume the local conditions (5.12)–(5.13) and probabilistic regularity for $D^\circ$ at every $z\in\partial C$. Then

$$\partial_tV\ \text{exists and is continuous on }[0,T]\times\mathbb R^{d-1}.$$

Milestones

1. (5.17): along every sequence $(t_n,x_n)\in C$ with $(t_n,x_n)\to z$, $\displaystyle\liminf_{n}V_t(t_n,x_n)\ge G_t(z)$.
2. (5.20): along the same sequences, $\displaystyle\limsup_{n}V_t(t_n,x_n)\le G_t(z)$.
3. Theorem 15, (5.14): at a single regular $z\in\partial C$,

$$\partial_tV(z)=\partial_tG(z)\quad\text{and}\quad\lim_{C\ni(t,x)\to z}\partial_tV(t,x)=\partial_tG(z).$$

Significance

The result. Theorem 15 turns a probabilistic property of the boundary, which can be checked through sample-path arguments, into the analytic smooth-fit condition in time. Continuity of $\partial_tV$ across $\partial C$ is the hypothesis that the change-of-variable formula with local time on curves and surfaces requires. That formula yields the free-boundary integral equations for optimal stopping boundaries. The theorem needs no sign condition on $G$ or $H$ and no strong Feller property. The time-space process is never strong Feller, which is exactly why the earlier strong Feller route to boundary regularity does not apply here.

Formalizing it. The result is proved in the paper; nothing here is open mathematics. As far as is known no part of it has been machine-checked. Mathlib has stopping times and conditional expectation, but no stochastic flows, no generators of jump diffusions and no optimal stopping in continuous time. A complete development formalizes the proof on pp. 20–23 together with the upper semicontinuity of hitting times of open sets (Lemma 4 and Corollary 6 of the paper, posed in the companion mission on the space derivative).

Difficulty

The infinite-horizon argument (Theorem 13, via Theorem 8) perturbs the starting point and reuses the optimal stopping time of the unperturbed problem. On a finite horizon this fails in the time variable. Shifting the start from $t_n$ to $t_n+\varepsilon_n$ shortens the remaining horizon, so the stopping time optimal for $V(t_n,x_n)$ is no longer admissible for $V(t_n+\varepsilon_n,x_n)$. A first-order comparison of payoffs therefore cannot be used. The proof truncates the stopping time and controls the truncated part, which is the role of the identity (5.12) and of the window $[T-t-\varepsilon,T-t]$ in (5.13). The convergence $\tau_n\to0$ of the optimal stopping times has to come from regularity of $z$ for the interior $D^\circ$ and continuity of the flow, not from the strong Feller property.

Formalization scope

• Space $\mathbb R^{d-1}$ is EuclideanSpace ℝ (Fin m) with $d=m+1$. Time is ℝ≥0. Points of the time-space domain are pairs in ℝ × EuclideanSpace ℝ (Fin m), and $[0,T]\times\mathbb R^{d-1}$ is Set.Icc 0 T ×ˢ univ.
• $P_x$ and $\mathsf E_x$ are $P$ and $\mathsf E$ of the flow started at $x$. All stopping times are for one common right-continuous filtration and are finite valued. Admissible times for $(t,x)$ satisfy $\tau\le T-t$.
• Hitting and entry times take values in $[0,\infty]$ (WithTop ℝ≥0) with $\inf\emptyset=\infty$, and are capped by the horizon.
• Expectations are Bochner integrals. Well-posedness carries integrability of every admissible payoff and optimality of a stopping time equal to $\tau_D$ almost surely, so $V$ is attained and is not a junk supremum.
• $\partial C:=D\cap\overline C$. "$C\ni(t,x)\to z$" is the filter $\mathcal N_C(z)$, and $\partial_tV$ is the derivative of $s\mapsto V(s,x)$ within $[0,T]$. The pointwise clause "continuous at $z$" means convergence along $C$; the global clause is ContinuousOn on $[0,T]\times\mathbb R^{d-1}$.
• (5.13) is an integrable majorant valid simultaneously for all points of the window. The ball $b(z,\varepsilon)$ is the max-metric ball, which is equivalent because $\varepsilon$ is existential. (5.12) includes integrability of both sides.
• $D^\circ$ is the interior in $\mathbb R\times\mathbb R^{d-1}$. No point with $t=T$ is probabilistically regular, so the global hypothesis requires $\overline C$ to avoid $t=T$. This is the paper's scope, not an addition.
• The model is not specialized: any $d\ge1$, general $\lambda$, jumps allowed, càdlàg paths, unbounded $G$, $H$ and $V$. A formalization that takes $\Lambda\equiv0$, $d=1$, continuous paths, or the strong Feller property is a different theorem.

Contributions welcome: the hitting-time lemmas (upper semicontinuity of $\sigma_{D^\circ}$ under a continuous flow), dominated-convergence lemmas for the truncated stopping times, and the two halves (5.17) and (5.20).

Selected references

• T. De Angelis, G. Peskir, Global C¹ regularity of the value function in optimal stopping problems, Ann. Appl. Probab. 30(3), 2020. Preprint arXiv:1812.04564v2. https://arxiv.org/abs/1812.04564v2
• G. Peskir, A. Shiryaev, Optimal Stopping and Free-Boundary Problems, Birkhäuser, 2006. https://doi.org/10.1007/978-3-7643-7390-0
• G. Peskir, A change-of-variable formula with local time on curves, J. Theoret. Probab. 18, 2005. https://doi.org/10.1007/s10959-005-3517-6
• R. M. Blumenthal, R. K. Getoor, Markov Processes and Potential Theory, Academic Press, 1968.

Why boundary regularity matters

An optimal stopping rule chooses when to end a stochastic process in order to collect a terminal reward, possibly after earning or paying a running reward. The resulting value function often solves a free-boundary problem: the state space splits into a region where stopping is optimal and one where continuing is better. Smoothness inside either region does not by itself say what happens where the regions meet. This mission concerns the global first spatial derivative of that value function at the optimal stopping boundary.

De Angelis and Peskir proved that a probabilistic condition on the boundary, together with regularity of the process as a spatial flow and explicit integrability bounds, gives continuous differentiability of the value function across the boundary. Their result applies to standard Markov processes with right-continuous paths and left limits, including jump processes; it is not restricted to diffusions or to a constant discount rate. The source is De Angelis and Peskir, arXiv:1812.04564v2, Theorem 8.

The stopping problem and its boundary

Let $d\ge1$, let $E=\mathbb R^d$, and let $X_t^x$ be a stochastic flow: the same probability space carries a path starting from every state $x\in E$. Time is nonnegative. One right-continuous filtration makes every path adapted and is used for every stopping rule. The process is strong Markov, has right-continuous paths with left limits, is left continuous over stopping times, and starts from $X_0^x=x$. Expectations and probabilities written $E_x$ and $P_x$ in the paper are the expectation and probability of the flow $X^x$ under one measure $P$.

The continuous data are a nonnegative discount rate $\lambda:E\to[0,\infty)$, a terminal reward $G:E\to\mathbb R$, and a running reward $H:E\to\mathbb R$. The discount accumulated along the path from $x$ is $\Lambda_t^x=\int_0^t\lambda(X_s^x)\,ds$. For every finite-valued stopping time $\tau$ of the common filtration, define

$$J(x,\tau)=E\!\left[e^{-\Lambda_\tau^x}G(X_\tau^x)+\int_0^\tau e^{-\Lambda_t^x}H(X_t^x)\,dt\right], \qquad V(x)=\sup_\tau J(x,\tau).$$

This is the infinite-horizon problem (2.1). It is well posed here when all admissible payoffs are integrable and the first entry time into the stopping set is an almost surely finite optimal stopping time. These conditions ensure that $V$ is a real, attained supremum rather than a default value of Lean's real supremum or integral. Define the stopping set $D=\{x:V(x)=G(x)\}$, the continuation set $C=\{x:V(x)>G(x)\}$, and the boundary relevant to the theorem as $D\cap\overline C$. For a state set $A$, the first entry time is $\tau_A^x=\inf\{t\ge0:X_t^x\in A\}$ and the first strictly positive hitting time is $\sigma_A^x=\inf\{t>0:X_t^x\in A\}$. Both may be infinite.

A boundary point $z$ is probabilistically regular for $A$ if $P_z(\sigma_A=0)=1$. It is Green regular for $A$ when $P_x(\tau_A\ge\varepsilon)\to0$ as $x\to z$ through $C$, for every $\varepsilon>0$. The paper obtains Green regularity by either strong Feller continuity with probabilistic regularity for $D$, or spatial continuity of the flow with probabilistic regularity for $D^\circ$. Lemma 1 and Corollaries 2–3 give the first route; Lemma 4 and Corollaries 5–6 give the second. All six statements use an arbitrary closed $D$, as in Section 3 of the source. Source: §§2–3, pp. 3–11.

Formalization targets

The milestone results first establish the two boundary regularity routes. In particular, approaching $z$ through $C$, the first route gives $\tau_D^{x_n}\to0$ in probability; the second gives $\tau_{D^\circ}^{x_n}\to0$ and $\tau_D^{x_n}\to0$ almost surely. Equations (4.16) and (4.19) then bound, respectively, the lower and upper limits of each coordinate derivative $\partial_iV(x_n)$ by $\partial_iG(z)$. The pointwise part of Theorem 8 concludes

$$D V(z)=D G(z),\qquad \lim_{C\ni x\to z}D V(x)=D G(z).$$

The mission goal is the final sentence of Theorem 8. If the theorem's local hypotheses hold at every $z\in D\cap\overline C$, then

$$V\in C^1(\mathbb R^d).$$

The hypotheses include the discounted generator representation (2.14) from the problem setup, continuity and interior $C^1$ regularity of $V$, global $C^1$ regularity of $G$, one positive Lipschitz constant for both $H$ and $\lambda$, a $C^1$ spatial flow, the four local bounds (4.4)–(4.7) with one radius at each boundary point, and one of the two probabilistic regularity alternatives. The goal retains all dimensions $d\ge1$, all nonnegative continuous discount rates, and the source's full class of standard Markov flows. Source: §2.5 and Theorem 8, pp. 7, 11–12.

What the result gives

The conclusion identifies the derivative of the value function on both sides of the stopping boundary. It strengthens a derivative match along a single direction or a chosen sequence into continuous differentiability on the whole state space. This is relevant to free-boundary formulations of optimal stopping, where interior regularity can be available from a Dirichlet or Poisson problem while boundary regularity remains the missing step. The authors describe that distinction in their discussion of smooth fit and global differentiability. Source: §2.5, p. 8.

The mathematical theorem is proved in the 2020 paper. In this mission, the definitions and statements compile as Lean declarations, while the theorem proofs remain to be formalized. A complete development would supply reusable arguments about hitting times, semicontinuity of hitting probabilities, stochastic flows, and limits of derivatives near a stopping boundary. Those components would also support the paper's finite-horizon spatial and temporal results.

The central difficulty

The value is a supremum over stopping rules. Differentiating the reward for a fixed stopping time does not automatically differentiate that supremum, because the optimal time depends on the initial state. Near the boundary, even continuity of the value does not control the duration of the optimal rule from neighboring states. The paper's probabilistic regularity conditions address that duration, while (4.4)–(4.7) provide the integrability needed to pass to derivative limits. A direct appeal to interior differentiability leaves the boundary itself untreated. Source: §§3–4.1, pp. 9–15.

Formalization scope

The state space is EuclideanSpace ℝ (Fin d) with $d\ge1$; Fin d indices are the paper's coordinates $1,\ldots,d$ shifted by one. Balls are open Euclidean balls. Time is $\mathbb R_{\ge0}$, and the entry and hitting times live in $\mathbb R_{\ge0}\cup\{+\infty\}$ so an unattained hit has its intended value. The flow is the process; no separate family of measures $P_x$ is introduced. One common filtration is used for all initial states and is right-continuous. Its finite stopping times are the full admissible class, not only hitting times.

The value uses Bochner expectations and real Lebesgue time integrals. Well-posedness records integrability for every admissible payoff and optimality and almost sure finiteness of $\tau_D^x$. The generator clause acts on smooth functions in the domain of the discounted transition semigroup; it retains the paper's diffusion, drift, killing, and jump terms. The boundary is $D\cap\overline C$, and approach through continuation points is expressed by the within-set neighborhood filter. Pointwise continuous differentiability means a Fréchet derivative at $z$ equal to $D G(z)$ and convergence of $D V$ along $C$; the goal uses global ContDiff. The local bounds retain all independently indexed starting states and coordinates. Their uncountable suprema are represented by integrable common majorants, with timewise measurable envelopes for the suprema inside time integrals. This convention excludes default integral values from nonmeasurable or nonintegrable expressions.

A formalization restricted to Brownian motion, one dimension, zero or constant discount, continuous paths, bounded rewards, or only one boundary regularity branch would state a different theorem. Contributions toward measurable hitting-time events, the two Section 3 regularity chains, the envelope bounds, and the derivative comparison are welcome.

Selected references

• De Angelis, T., and Peskir, G., Global C¹ Regularity of the Value Function in Optimal Stopping Problems, Annals of Applied Probability 30(3), 2020. arXiv:1812.04564v2; DOI:10.1214/19-AAP1517.

Motivation

Optimal portfolio liquidation asks how a trader should unwind a position of $\mathcal X$ shares over a horizon $[0,T]$ when trading moves prices. Since Almgren and Chriss (2001) the standard model charges a quadratic cost $\eta_t\xi_t^2$ for trading at rate $\xi_t$ (temporary impact) and a risk penalty $\lambda_tX_t^2$ on the open position, and imposes the liquidation constraint $X_T=0$. When many traders liquidate at once, each one's costs also depend on the others' aggregate trading rate $\mu_t$ through a permanent impact term $\kappa_t\mu_tX_t$. Fu, Graewe, Horst and Popier (arXiv:1804.04911) model this as a mean field game (MFG) with common noise and prove that, under a weak-interaction condition, the game has a unique equilibrium.

The liquidation constraint makes the problem singular: the value function blows up at $T$, and the equilibrium is described by a forward-backward system whose decoupling field $A$ satisfies a Riccati BSDE with terminal value $A_T=+\infty$. A natural question is whether the constraint can be replaced by a finite penalty $nX_T^2$ on the unliquidated position, a non-singular problem of the type studied in the MFG literature, and whether the penalized equilibria approach the constrained one as $n\to\infty$. Section 4 of the paper answers this at the level of values. In the single-agent case, singular terminal conditions of this type were studied by Ankirchner, Jeanblanc and Kruse (SIAM J. Control Optim., 2014) and Graewe, Horst and Séré (Stochastic Process. Appl., 2018), references [3] and [28] of the paper.

Setting

Fix $T>0$, an $m$-dimensional Brownian motion $\widetilde W=(W^0,W)$ whose first coordinate $W^0$ is common noise, and an initial position $\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,\widetilde W)$, both augmented. The coefficients $\kappa,\lambda,\eta$ are bounded, nonnegative, $\mathbb F$-progressive processes, with $\lambda$ and $\eta$ bounded below by positive constants. Write $\kappa_{\max}$, $\eta_\star$, $\lambda_\star$ for the essential supremum of $\kappa$ and the essential infima of $\eta$ and $\lambda$, $\|\eta\|$ for the essential supremum of $|\eta|$, and $\alpha=\eta_\star/\|\eta\|\in(0,1]$. Assumption 2.3 adds the weak-interaction condition: some $\theta>0$ satisfies $\kappa_{\max}<4\eta_\star\theta$ and $\theta\kappa_{\max}<4\lambda_\star$.

Given an aggregate rate $\mu$, a trading rate $\xi\in L^2_{\mathbb F}$ yields the position $X^\xi_t=\mathcal X-\int_0^t\xi_s\,ds$. The constrained problem minimizes

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

over $\xi$ with $\int_0^T\xi_s\,ds=\mathcal X$; its value is $V(\mathcal X;\mu)$. The penalized problem (4.1) drops the constraint and minimizes

$$J^n(\xi;\mu)=\mathbb E\Big[\int_0^T\big(\kappa_t\mu_tX^\xi_t+\eta_t\xi_t^2+\lambda_t(X^\xi_t)^2\big)dt+n(X^\xi_T)^2\,\Big|\,\mathcal X\Big]$$

over all $\xi\in L^2_{\mathbb F}$, with value $V^n(\mathcal X;\mu)$. An equilibrium is a fixed point $\mu_t=\mathbb E[\xi^*_t|\mathcal F^0_t]$.

The constrained equilibrium is given by the FBSDE (2.3), $dX_t=-\frac{Y_t}{2\eta_t}dt$, $-dY_t=\big(\kappa_t\mathbb E[\frac{Y_t}{2\eta_t}|\mathcal F^0_t]+2\lambda_tX_t\big)dt-Z_t\,d\widetilde W_t$, $X_0=\mathcal X$, $X_T=0$, decoupled as $Y=AX+B$ where

$$-dA_t=\Big(2\lambda_t-\frac{A_t^2}{2\eta_t}\Big)dt-Z^A_t\,d\widetilde W_t,\qquad A_T=+\infty .$$

The penalized equilibria are given by the FBSDE (4.2) with $Y^n_T=2nX^n_T$, decoupled by $A^n$, the solution of the same Riccati BSDE with $A^n_T=2n$. The solutions live in weighted spaces: $\mathcal H_l$ with norm $\big(\mathbb E\sup_t|Y_t/(T-t)^l|^2\big)^{1/2}$, and the penalized analogue $\mathcal H^n_l$ with weight $(T-t+\eta_\star/n)^{-l}$. Assumption 4.1 requires a constant $C$ with $\exp\big(-\int_r^s\frac{A_u}{2\eta_u}du\big)\le C\frac{T-s}{T-r}$ for all $0\le r\le s<T$, almost surely.

Formalization targets

Goal: Theorem 4.6

Under Assumptions 2.3 and 4.1, with $\mu^*=\mathbb E[Y/(2\eta)|\mathcal F^0]$ the constrained equilibrium and $\mu^n=\mathbb E[Y^n/(2\eta)|\mathcal F^0]$ the penalized ones,

$$\lim_{n\to\infty}\mathbb E\big|V^n(\mathcal X;\mu^n)-V(\mathcal X;\mu^*)\big|=0 .$$

Milestones

1. Lemma 4.2 (first condition). If $\eta$ is deterministic, Assumption 4.1 holds.
2. Lemma A.3. $A^n$ exists uniquely, $A^n_t\ge\big(\frac1{2n}+\mathbb E[\int_t^T\frac{ds}{2\eta_s}|\mathcal F_t]\big)^{-1}$, $A^n\uparrow A$, and $\|A^n\|_{\mathcal M_{-1}}+\|A^n\|_{\mathcal M^n_{-1}}\le\mathfrak C$ uniformly in $n$.
3. Theorem 4.3. The FBSDE (4.4), with parameter $\mathfrak p\in[0,1]$ and data $f\in L^2$, has a unique solution in $\mathcal H^n_\alpha\times\mathcal H^n_\gamma\times S^2\times L^2\times L^2$.
4. Lemma 4.4. $\|X^n\|_{n,\alpha}+\|B^n\|_{n,\gamma}+\mathbb E\int_0^T|Y^n_t|^2dt\le\overline{\mathfrak C}$ uniformly in $n$.
5. (4.8). Under Assumption 4.1 the constrained equilibrium position satisfies $\|X^*\|_1<\infty$.
6. Lemma 4.5. $(X^n,B^n,Y^n)\to(X,B,Y)$ in $L^2(dt\otimes d\mathbb P)$.

Significance

The result is a consistency statement between two models of liquidation. Penalized models are what a numerical scheme or a standard MFG solver can handle, since their FBSDEs have finite terminal data. Theorem 4.6 says that equilibrium values computed with a large penalty approximate the value of the hard-constrained game, and Lemma 4.5 says the same for positions and trading rates. Without it, a penalized model would be an unrelated object rather than an approximation of the constrained one.

The result is proved in the paper; it is not formalized anywhere. A machine-checked development would need, beyond the paper, the theory of quadratic BSDEs with finite and singular terminal values, conditional mean-field FBSDEs with common noise, and conditional essential infima of control problems. The milestones isolate reusable pieces: the monotone approximation of a singular Riccati BSDE (Lemma A.3) and uniform estimates in $n$-dependent weighted spaces (Lemma 4.4).

Difficulty

The obvious argument compares the two problems control by control: the constrained optimizer is admissible for the penalized problem, so $V^n\le V$ up to the change of $\mu$. The reverse inequality is where it fails. The penalized optimizer leaves a residual position $X^n_T\neq0$, and its cost has to be compared with the singular one, whose weight $(T-t)^{-1}$ explodes at $T$. Controlling this requires estimates uniform in $n$ in spaces whose weights $(T-t+\eta_\star/n)^{-l}$ degenerate as $n\to\infty$, and the bare exponent $\alpha=\eta_\star/\|\eta\|<1$ of the constrained problem is not enough to make the boundary terms vanish. Assumption 4.1, which upgrades the state to $\mathcal H_1$, is what closes the gap. In addition, the aggregate rate $\mu^n$ changes with $n$, so both the controls and the cost functional move at once.

Formalization scope

Time is $\mathbb R_{\ge0}$; processes are real-valued functions of $(t,\omega)$; $W$ is the $m=k+1$-dimensional $\widetilde W$ with coordinate $0$ the common noise. Stochastic integrals and BSDEs come from the published definition Peng1990.SMP.Stochastic. BSDEs on $[0,T)$ are imposed on every $[0,\tau]$, $\tau<T$; $A_T=+\infty$ is $\lim_{t\uparrow T}A_t=+\infty$ a.s. Conditional expectations inside drivers are $\mathbb F^0$-progressive versions of integrable processes. Weighted norms are computed in $[0,\infty]$. The explicit readings are:

• $\kappa_{\max},\eta_\star,\lambda_\star,\|\eta\|$ are essential bounds over $dt\otimes d\mathbb P$; (2.4) is stated without division; "$1/\lambda,1/\eta\in L^\infty$" is a positive essential lower bound.
• Assumption 2.3 is a hypothesis of every statement, including Lemma A.3 (the appendix assumes only its boundedness part).
• Assumption 4.1 holds almost surely with the constant chosen before $\omega$ (as restated on p. 32).
• The penalty index is an integer $n\ge1$; constants in Lemma A.3 and Lemma 4.4 are chosen before $n$.
• The class of $A^n$ is $S^2\times L^2$ on $[0,T]$ (not printed in Lemma A.3).
• The penalized control set is $L^2_{\mathbb F}$, with no terminal constraint.
• Values are conditional essential infima given $\sigma(\mathcal X)$.
• The equilibria $\mu^n,\mu^*$ of Theorem 4.6 are defined through the FBSDE solutions, as in the proof; uniqueness of penalized equilibria is not claimed.
• The solution of Proposition 2.8 includes the relation $Y=AX+B$ on $[0,T)$; "Theorem 2.8" on pp. 25–29 means Proposition 2.8.
• $L^1$ convergence means $\int|V^n-V|\,d\mathbb P\to0$, not convergence of expectations.

A trivializing formalization would quantify over all solutions of the penalized MFG (claiming a uniqueness the paper does not state) or define $V$ by a pointwise infimum over all controls (which is $-\infty$ or junk); both are ruled out above. Contributions toward BSDE comparison principles and quadratic BSDE well-posedness on this stochastic-integral layer are welcome and reusable.

Selected references

• G. Fu, P. Graewe, U. Horst, A. Popier, A Mean Field Game of Optimal Portfolio Liquidation, Math. Oper. Res. 46(4), 2021; preprint arXiv:1804.04911v3. https://arxiv.org/abs/1804.04911
• R. Almgren, N. Chriss, Optimal execution of portfolio transactions, Journal of Risk 3, 2001. https://doi.org/10.21314/JOR.2001.041
• S. Ankirchner, M. Jeanblanc, T. Kruse, BSDEs with singular terminal condition and a control problem with constraints, SIAM J. Control Optim. 52(2):893–913, 2014 (reference [3] of the paper).
• P. Graewe, U. Horst, E. Séré, Smooth solutions to portfolio liquidation problems under price-sensitive market impact, Stochastic Process. Appl. 128(3):979–1006, 2018 (reference [28] of the paper).
• S. Peng, A general stochastic maximum principle for optimal control problems, SIAM J. Control Optim. 28(4), 1990. https://doi.org/10.1137/0328054

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