Motivation

A proper coloring of a graph assigns colors to its vertices so that adjacent vertices get different colors; the least number of colors that suffices is the chromatic number $\chi(G)$. The clique number $\omega(G)$ is the size of a largest set of pairwise adjacent vertices, and $\chi(G)\ge\omega(G)$ always. A class of graphs is $\chi$-bounded if $\chi$ is bounded by a function of $\omega$ on the class. Abstract triangle-free graphs ($\omega\le2$) of arbitrarily large chromatic number have been known since Zykov (1949) and Mycielski (1955), so the question is which geometric classes are $\chi$-bounded.

For geometric intersection graphs (one vertex per set, an edge for each intersecting pair) the history is as follows.

• 1960: Asplund and Grünbaum prove that families of axis-aligned rectangles in the plane are $\chi$-bounded.
• 1965: Burling constructs triangle-free families of axis-aligned boxes in $\mathbb R^3$ with arbitrarily large chromatic number.
• 1970s: Erdős asks whether families of line segments in the plane are $\chi$-bounded (Brass–Moser–Pach, Research Problems in Discrete Geometry, §9.6, Problem 2; Gyárfás 1987, Problem 1.9).
• 2000–2014: positive special cases. McGuinness (2000) obtains bounds for triangle-free families; Suk (2014) improves them, proving that families of segments meeting a common line, and families of unit-length segments, are $\chi$-bounded.
• 2014: Pawlik, Kozik, Krawczyk, Lasoń, Micek, Trotter and Walczak answer Erdős's question negatively (arXiv:1209.1595).

The same construction disproves Scott's conjecture (1997) that graphs excluding induced subdivisions of a fixed graph are $\chi$-bounded, as first observed by Fox and Pach.

Setting

Points of the plane are pairs $(x,y)\in\mathbb R\times\mathbb R$. A line segment is a closed set $\operatorname{seg}(u,v)=\{(1-t)u+tv: 0\le t\le1\}$ with two distinct endpoints $u\neq v$. A family of segments $\mathcal S=(\sigma_i)_{i<N}$ is a finite indexed list of pairwise distinct segments. Its intersection graph has vertex set $\{0,\dots,N-1\}$, and $i\neq j$ are adjacent exactly when $\sigma_i\cap\sigma_j\neq\emptyset$. The family is triangle-free if no three of its segments pairwise intersect, and $\chi(\mathcal S)$ is the chromatic number of its intersection graph.

The milestones use the paper's auxiliary notions. An axis-aligned rectangle is $R=[a,c]\times[b,d]$, with $x\in[a,c]$ and $y\in[b,d]$. For a family $\mathcal S$ inside the open interior of $R$, a probe for $(\mathcal S,R)$ is a rectangle $P=[a',c]\times[b',d']$ sharing the right edge line of $R$ such that (i) $a<a'<c$ and $b<b'<d'<d$; (ii) no segment meets the left edge of $P$; (iii) no segment has an endpoint in the closed rectangle $P$; (iv) the segments meeting $P$ are pairwise disjoint. The diagonal $D_P$ runs from the bottom-left corner $(a',b')$ to the top-right corner $(c,d')$ of $P$. The sequences $s_k,p_k$ are given by $s_1=p_1=1$, $s_{k+1}=(p_k+1)s_k+p_k^2$ and $p_{k+1}=2p_k^2$.

Formalization targets

Goal: Theorem 1 (p. 2)

For every integer $k\ge1$ there is a finite family $\mathcal S$ of distinct line segments in the plane with triangle-free intersection graph and

$$\chi(\mathcal S)>k .$$

The goal fixes no size for $\mathcal S$ and no particular construction.

Milestones

1. Base case of Lemma 2 (p. 3): one segment and one probe in any rectangle of positive area.
2. Diagonal claim (p. 3): for a probe $Q$ of a family inside the interior of $R$, a segment meets $D_Q$ if and only if it meets $Q$.
3. Color-count dichotomy (p. 4): for a proper coloring of an intersection graph and two index sets $X$, $Y$ each seeing at least $k$ colors, if the color sets differ then $X\cup Y$ sees at least $k+1$ colors; if they agree, a member adjacent to all of $Y$ gets a new color, and $X$ together with it sees at least $k+1$ colors.
4. Induction step (pp. 3–4): Lemma 2 at $k$ for every rectangle gives Lemma 2 at $k+1$ for every rectangle.
5. Lemma 2 (p. 3): for $k\ge1$ and a rectangle $R$ of positive area there are a triangle-free family $\mathcal S_k$ of exactly $s_k$ segments in the interior of $R$ and $p_k$ pairwise disjoint probes for $(\mathcal S_k,R)$ such that every proper coloring of $\mathcal S_k$ uses at least $k$ colors on the segments meeting some probe.
6. The family $\tilde{\mathcal S}_k$ (p. 4): adding the diagonals of all probes to a family with the conclusion of Lemma 2 gives a triangle-free family with $\chi>k$.

Significance

Theorem 1 shows that segment intersection graphs are not $\chi$-bounded, and it settles negatively the question for every class containing them: intersection graphs of curves crossing at most once (Kratochvíl–Nešetřil), McGuinness's class of arcwise connected sets with connected pairwise intersections, and string graphs in general. Through the Fox–Pach observation it refutes Scott's conjecture on induced subdivisions, a purely graph-theoretic statement. The counts in Lemma 2 give $|\tilde{\mathcal S}_k|=s_k+p_k$, so the maximum chromatic number of a triangle-free family of $n$ segments is $\Omega(\log\log n)$ (§4 of the paper). The family $\tilde{\mathcal S}_k$ has the same intersection graph as Burling's boxes.

The theorem is proved on paper; to the best of current knowledge no machine-checked proof exists. The mission produces a Lean 4 statement of the result about actual segments in $\mathbb R^2$, a reusable definition of intersection graphs of plane sets, and the paper's probe machinery stated precisely enough to support a full formal proof.

Difficulty

Abstract triangle-free graphs with large chromatic number are easy to build, but almost none of them are intersection graphs of segments, and the standard constructions (Mycielski, Zykov, shift graphs) do not come with a geometric realization. The difficulty is geometric: the construction has to place every new segment so that it meets exactly a prescribed independent set of old segments and nothing else, at every level of a doubly exponential nesting, while keeping finitely many rectangles disjoint and segment endpoints out of them. In a formal development the burden falls on the planar facts the paper treats as evident in one line each: which edges of a rectangle a segment can cross, when two segments must cross, and why the probe conditions survive when families are nested inside one another.

Formalization scope

• The plane is ℝ × ℝ (first coordinate $x$, second $y$), and segments are Mathlib's closed segment ℝ u v. A family is e : Fin N → (ℝ × ℝ) × (ℝ × ℝ) (endpoint pairs) with seg (e i) the $i$-th segment. "A family of line segments" is read as non-degenerate ((e i).1 ≠ (e i).2) and pairwise distinct (Function.Injective (fun i => seg (e i))).
• interGraph F : SimpleGraph ι is the intersection graph of an indexed family of plane sets: i ≠ j ∧ (F i ∩ F j).Nonempty. Triangle-free is CliqueFree 3; $\chi$ is Mathlib's chromaticNumber : ℕ∞, and the goal states the literal $(k:\mathbb N_\infty)<\chi$.
• Rectangles keep the page's letter order, Rect = ⟨a, c, b, d⟩ for $[a,c]\times[b,d]$, with positive area as a separate hypothesis. A probe is stored as $(a',b',d')$ and is the closed rectangle $[a',c]\times[b',d']$; the interior of $R$ is open.
• sSeq k, pSeq k are $s_k,p_k$, 1-based; every statement assumes $k\ge1$ (the value at $0$ is junk).
• Proper colorings take values in an arbitrary type, and "uses at least $k$ colors on the segments meeting $P$" is $k\le$ ncard of the image of those segments.
• The diagonal claim and the $\tilde{\mathcal S}_k$ milestone are stated for any data with the relevant properties, not only for the paper's construction; the hypotheses are exactly those the page's sentences use.
• The goal is about the intersection graph of the segments the existential provides. A statement about an abstract triangle-free graph with $\chi>k$ is a different, much weaker theorem (already available via Mycielski's construction) and does not count.

Needed infrastructure: elementary planar geometry of segments and axis-aligned rectangles (membership, edges, crossing of two segments via the intermediate value theorem), affine images of segment families, and finite coloring counts. The segment and intersection-graph definitions are reusable for other questions on geometric intersection graphs. Contributions are welcome on any milestone, in particular a complete proof of the diagonal claim and of the induction step.

Selected references

• A. Pawlik, J. Kozik, T. Krawczyk, M. Lasoń, P. Micek, W. T. Trotter, B. Walczak, Triangle-free intersection graphs of line segments with large chromatic number, J. Combin. Theory Ser. B 105 (2014) 6–10; preprint arXiv:1209.1595v5 (2014). https://arxiv.org/abs/1209.1595
• A. Pawlik, J. Kozik, T. Krawczyk, M. Lasoń, P. Micek, W. T. Trotter, B. Walczak, Triangle-free geometric intersection graphs with large chromatic number, Discrete Comput. Geom. 50(3) (2013) 714–726. https://arxiv.org/abs/1212.2058
• J. P. Burling, On coloring problems of families of prototypes, PhD thesis, University of Colorado, Boulder, 1965.
• E. Asplund, B. Grünbaum, On a colouring problem, Math. Scand. 8 (1960) 181–188.
• P. Brass, W. Moser, J. Pach, Research Problems in Discrete Geometry, Springer, 2005.
• A. Gyárfás, Problems from the world surrounding perfect graphs, Zastos. Mat. 19 (1987) 413–441.
• A. Suk, Coloring intersection graphs of x-monotone curves in the plane, Combinatorica 34(4) (2014) 487–505.
• A. D. Scott, Induced trees in graphs of large chromatic number, J. Graph Theory 24(4) (1997) 297–311.
• J. Mycielski, Sur le coloriage des graphes, Colloq. Math. 3 (1955) 161–162.

Why saddle points matter for nonconvex learning

Training a model in machine learning usually means minimizing a nonconvex function $f:\mathbb R^d\to\mathbb R$ with first-order methods. Finding a global minimum of a general nonconvex function is NP-hard, so the classical guarantee for gradient descent (GD), $x_{t+1}=x_t-\eta\nabla f(x_t)$, is weaker: with step size $\eta=1/\ell$ it reaches a point with $\|\nabla f(x)\|\le\varepsilon$ within $\ell(f(x_0)-f^\star)/\varepsilon^2$ iterations, independently of the dimension (Nesterov, 1998). Such a point can be a saddle point. For many learning problems (matrix sensing and completion, phase retrieval, dictionary learning, tensor decomposition), every approximate second-order stationary point is an approximate global minimum, so an algorithm that avoids saddle points solves the problem.

Jin, Netrapalli, Ge, Kakade and Jordan (arXiv:1902.04811, J. ACM 2021) show that simple perturbed versions of GD and SGD find approximate second-order stationary points in essentially the number of iterations GD needs for first-order stationarity, up to polylogarithmic factors in the dimension. Their §5 gives a short, self-contained proof for a variant of perturbed GD (Algorithm 4). That proof is the subject of this mission.

Timeline:

• 2015: Ge, Huang, Jin and Yuan show that noisy SGD escapes strict saddle points in polynomial time.
• 2017: Jin, Ge, Netrapalli, Kakade and Jordan (ICML) prove that perturbed GD finds an $\varepsilon$-second-order stationary point in $\tilde O(\ell\Delta_f/\varepsilon^2)$ iterations, with a geometric argument on the "stuck region".
• 2019: arXiv:1902.04811 extends this to SGD and simplifies the deterministic proof through the improve or localize lemma (Lemma 21). §5 of that paper is formalized here.

Setting

Let $f:\mathbb R^d\to\mathbb R$, $d\ge1$, with gradient $\nabla f$ and Hessian $\nabla^2 f$; $\|\cdot\|$ is the Euclidean norm on vectors and the spectral norm on matrices. Assumption A: $f$ is $\ell$-gradient Lipschitz, $\|\nabla f(x_1)-\nabla f(x_2)\|\le\ell\|x_1-x_2\|$, and $\rho$-Hessian Lipschitz, $\|\nabla^2f(x_1)-\nabla^2f(x_2)\|\le\rho\|x_1-x_2\|$. A point $x$ is an $\varepsilon$-second-order stationary point ($\varepsilon$-SOSP) if

$$\|\nabla f(x)\|\le\varepsilon\qquad\text{and}\qquad\nabla^2 f(x)\succeq-\sqrt{\rho\varepsilon}\,I .$$

Write $f^\star=\inf f$ and $\Delta_f=f(x_0)-f^\star$.

Algorithm 4 (Perturbed GD, Variant). With step size $\eta$, radius $r$, time interval $\mathscr T$ and tolerance $\varepsilon$, start with $t_{\text{perturb}}=0$. At iteration $t$: if $\|\nabla f(x_t)\|\le\varepsilon$ and $t-t_{\text{perturb}}>\mathscr T$, replace $x_t$ by $x_t-\eta\xi_t$ with $\xi_t\sim\mathrm{Uniform}(B_0(r))$ and set $t_{\text{perturb}}=t$; then $x_{t+1}=x_t-\eta\nabla f(x_t)$. The parameters are those of Eq. (6):

$$\eta=\frac1\ell,\quad r=\frac{\varepsilon}{400\iota^3},\quad\mathscr T=\frac{\ell}{\sqrt{\rho\varepsilon}}\,\iota,\quad\mathscr F=\frac{1}{50\iota^3}\sqrt{\frac{\varepsilon^3}{\rho}},\quad\mathscr S=\frac{1}{4\iota}\sqrt{\frac{\varepsilon}{\rho}},$$

where $\iota$ is a logarithmic factor, and $\omega=2^{2-\iota}\ell\mathscr S$.

Formalization targets

Goal: Theorem 18

For $T=\lceil 8\max\{\Delta_f\mathscr T/\mathscr F,\ \Delta_f/(\eta\varepsilon^2)\}\rceil$ (which equals $\lceil400\iota^4\ell\Delta_f/\varepsilon^2\rceil$) and every $\iota\ge1$ with

$$\frac{T\ell\sqrt d}{\sqrt{\rho\varepsilon}}\,\iota^2 2^{8-\iota}\le\delta,$$

with probability at least $1-\delta$ over the perturbations,

$$\#\{t<T:\ x_t\text{ is an }\varepsilon\text{-SOSP}\}\ \ge\ T/2 .$$

The paper writes the count as $\tilde O(\ell\Delta_f/\varepsilon^2)$ with $\iota=c\log(d\ell\Delta_f/(\rho\varepsilon\delta))$.

Milestones, in the order the proof uses them

1. Lemma 19 (descent): $f(x_{t+1})-f(x_t)\le-\eta\|\nabla f(x_t)\|^2/2$ for $\eta\le1/\ell$.
2. Lemma 21 (improve or localize): $\|x_\tau-x_0\|\le\sqrt{2\eta t(f(x_0)-f(x_t))}$ for $t\ge\tau>0$.
3. Lemma 22 (coupling sequence): if $\lambda_{\min}(\nabla^2f(\tilde x))\le-\sqrt{\rho\varepsilon}$ and two GD runs start within $\eta r$ of $\tilde x$, $\eta r_0$ apart along the bottom eigenvector with $r_0>\omega$, one of them decreases $f$ by $\mathscr F$ within $\mathscr T$ steps.
4. Volume display (§5, proof of Lemma 20, p. 15): $w\,\mathrm{Vol}(\mathbb B^{d-1}_0(a))/\mathrm{Vol}(\mathbb B^d_0(a))=\frac{w}{a\sqrt\pi}\frac{\Gamma(d/2+1)}{\Gamma(d/2+1/2)}\le\frac wa\sqrt{d/\pi}$.
5. Lemma 20 (escaping saddle points): at $\tilde x$ with $\|\nabla f(\tilde x)\|\le\varepsilon$ and $\lambda_{\min}\le-\sqrt{\rho\varepsilon}$,

$$\mathbb P\bigl(f(x_{\mathscr T})-f(\tilde x)\le-\mathscr F/2\bigr)\ge1-\frac{\ell\sqrt d}{\sqrt{\rho\varepsilon}}\,\iota^22^{8-\iota}\quad\text{for }x_0=\tilde x+\eta\xi .$$

Significance

The result. Theorem 18 says that adding occasional small random perturbations to gradient descent costs only a polylogarithmic factor over the first-order rate $\ell\Delta_f/\varepsilon^2$ and buys second-order stationarity. Combined with the landscape results above, it gives polynomial-time guarantees for gradient methods on those learning problems. Lemma 20, on its own, is a quantitative statement that strict saddle points are unstable under perturbed GD; Lemmas 21 and 22 are reusable tools for any analysis of first-order methods near saddle points.

Formalizing it. The results are proved in the paper; none of them is formalized. A formal development would give machine-checked versions of the descent lemma for Hessian-Lipschitz functions, the improve-or-localize lemma, the coupling argument and the probabilistic escape bound. It would also settle the issue disclosed under Formalization scope.

Difficulty

Lemmas 19 and 21 are short. The difficulty is in Lemma 22 and Lemma 20. The obvious approach, linearizing GD around the saddle and following the unstable eigendirection, fails because the stuck region (starting points that do not escape within $\mathscr T$ steps) has no simple shape once $f$ is not quadratic. The coupling argument controls the difference of two runs instead. It needs an induction in which the non-quadratic error term stays below half of the leading term for all $\mathscr T$ steps, with the constants of Eq. (6) used exactly ($2\eta\rho\mathscr S\mathscr T=1/2$). Lemma 20 then turns a statement about pairs of points into a measure bound: a set whose every line parallel to $e_1$ meets it in a segment of length at most $\eta\omega$ has volume at most $\eta\omega$ times the $(d-1)$-volume of the ball. In Lean this needs Fubini over a rotated coordinate system and measurability of the stuck region. Theorem 18 requires a probabilistic accounting over the whole run, under the product law of the perturbations.

Formalization scope

$\mathbb R^d$ is EuclideanSpace ℝ (Fin d) with $d\ge1$. The Hessian is fderiv ℝ (gradient f) x, the derivative of the gradient map, with the operator norm. Statements about $\lambda_{\min}$ use the quadratic form: $\lambda_{\min}(H)\le-c$ is "some unit $v$ has $\langle Hv,v\rangle\le-c$", and $H\succeq-cI$ is "$\langle Hv,v\rangle\ge-c\|v\|^2$ for all $v$". $\mathrm{Uniform}(B_0(r))$ is normalized Lebesgue measure on the open ball. Algorithm 4 is a deterministic function of the perturbation vectors, which have the product law on $(\mathbb R^d)^T$. The $t$-th iterate is the point tested at the start of iteration $t$, and "half of its iterations" counts $t\in\{0,\dots,T-1\}$. Probability statements bound the failure event from above.

The paper's $\tilde O(\cdot)$ is instantiated as the proof does:

• the parameters are exactly Eq. (6), and $T=\lceil8\max\{\Delta_f\mathscr T/\mathscr F,\Delta_f/(\eta\varepsilon^2)\}\rceil$ (p. 16);
• $\iota$ is any real $\ge1$ satisfying the proof's condition $(T\ell\sqrt d/\sqrt{\rho\varepsilon})\iota^22^{8-\iota}\le\delta$, in place of $\iota=c\log(d\ell\Delta_f/(\rho\varepsilon\delta))$. The printed argument of the logarithm changes under rescaling $x\mapsto\lambda x$ while every quantity in the proof does not, so the printed choice can give $\iota\le0$;
• $\mathscr T$ is a natural number equal to $\ell\iota/\sqrt{\rho\varepsilon}$, with no rounding, because the proof uses $x_{\mathscr T}$ and $2\eta\rho\mathscr S\mathscr T=1/2$ exactly;
• $\ell\ge\sqrt{\rho\varepsilon}$ (footnote 1, p. 14), $\iota\ge1$, $\eta>0$ and $f$ bounded below are the standing assumptions of §5.

A Hessian not tied to $f$, an arbitrary unit vector in place of the bottom eigenvector in Lemma 22, a per-realization or existential statement in place of the product-law probability, or a vacuous $\iota$ would each trivialize the statements; none is used.

Disclosed gap. The proof of Theorem 18 (p. 16) bounds the number of perturbations by applying Lemma 20 at each one. Algorithm 4 also perturbs at points that are already $\varepsilon$-SOSPs, where Lemma 20 does not apply, and the $\mathscr T$ iterations after such a perturbation are not counted. The goal is posed as printed; a solver who finds it false should report this in the discussion. The milestones do not depend on the gap.

Needed infrastructure: second-order Taylor bounds for Hessian-Lipschitz functions, symmetry of the Hessian and existence of a bottom eigenvector, volumes of Euclidean balls (in Mathlib through $\Gamma$), a Fubini-type slicing bound for sets of bounded width along a direction, and measurability of the GD iterates. The volume-ratio and slicing lemmas are reusable beyond this mission. Proofs of any milestone, and alternative proofs, are welcome.

Selected references

• C. Jin, P. Netrapalli, R. Ge, S. M. Kakade, M. I. Jordan, On Nonconvex Optimization for Machine Learning: Gradients, Stochasticity, and Saddle Points, arXiv:1902.04811v2 (2019); J. ACM 68(2), 2021. https://arxiv.org/abs/1902.04811
• C. Jin, R. Ge, P. Netrapalli, S. M. Kakade, M. I. Jordan, How to Escape Saddle Points Efficiently, ICML 2017. https://arxiv.org/abs/1703.00887
• R. Ge, F. Huang, C. Jin, Y. Yuan, Escaping From Saddle Points — Online Stochastic Gradient for Tensor Decomposition, COLT 2015. https://arxiv.org/abs/1503.02101
• Y. Nesterov, Introductory Lectures on Convex Programming, Volume I: Basic Course, 1998; Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9
• Y. Nesterov, B. T. Polyak, Cubic regularization of Newton method and its global performance, Math. Program. 108 (2006). https://doi.org/10.1007/s10107-006-0706-8

Motivation

In an aggregative game, each player's decision affects a common quantity, such as total production or total demand. An agent may be able to calculate its own preferred response while lacking direct access to that aggregate. Koshal, Nedić, and Shanbhag study how agents can estimate it by exchanging information only with neighbours on a communication graph. Their asynchronous gossip algorithm lets one randomly selected agent contact a neighbour at each tick; both agents update their estimates and decisions. The constant stepsize regime matters when agents cannot steadily reduce their stepsizes or want to keep responding to new information. It gives an error bound rather than exact convergence: the decisions remain near an equilibrium by an amount controlled by the step, the game, and the graph. The model and this bound are from Koshal, Nedić, and Shanbhag, 2016.

The same paper analyzes a synchronous scheme with diminishing steps and a gossip scheme with update-count steps. This mission isolates the constant-step case in §4.3, and targets the equal-probability, equal-stepsize display at the end of that section. It uses the paper's numbered Lemmas 2, 3, and 11 and relations (30), (31), (44), and (55) as intermediate targets. The restriction to the final special case is material: the argument printed for general player-specific steps and update probabilities has gaps in (53) and (54), while both problematic terms disappear when the steps and update probabilities are equal.

Setting

There are $N$ players, each choosing $x_i$ from a nonempty compact convex set $K_i\subseteq\mathbb R^n$. Write $K=\prod_iK_i$ for feasible profiles and $\bar K=\{\sum_i x_i:x_i\in K_i\}$ for feasible aggregates. Player $i$ has a component map $F_i(x_i,u)$, evaluated at its own decision and an aggregate argument. At a feasible profile $x$, the game map is $\phi(x)_i=F_i(x_i,\sum_jx_j)$. An equilibrium target is the solution $x^*$ of the variational inequality $\operatorname{VI}(K,\phi)$: for every $x\in K$, $\sum_i\langle x_i-x_i^*,\phi(x^*)_i\rangle\ge0$. The paper derives this map from player payoff gradients under its Assumption 1; the present formalization starts with the component maps used by the algorithm.

A connected undirected graph lists the players that may exchange information. At tick $k$, a uniform random player $I^k$ wakes and contacts a neighbour $J^k$ with probability $p_{I^kJ^k}>0$. These draws are independent across ticks. Only the contacted pair average their current estimates $v_i^k$ to obtain $\hat v_i^k$, then project a step using $F_i(x_i^k,N\hat v_i^k)$ onto $K_i$. All agents update their estimate by $v_i^{k+1}=\hat v_i^k+x_i^{k+1}-x_i^k$; for agents outside the pair this leaves both state variables unchanged. The mean estimate is $y^k=N^{-1}\sum_i v_i^k$. Lemma 2 identifies it with the mean decision. The update probability of player $i$ is $p_i=N^{-1}(1+\sum_jp_{ji})$. These definitions and the discrete gossip algorithm are given in §4.1 of the source.

Formalization targets

Constant-step error bound

Suppose $\phi$ is strongly monotone with modulus $\mu>0$, every player uses the same positive step $\alpha$, and all update probabilities equal $p$. Let $C$ bound the gradient evaluations as in Lemma 3. Let $\lambda\in(0,1)$ be a mean-square contraction constant for the gossip matrix $D(k)=W(k)-N^{-1}\mathbf1\mathbf1^\top$, as in (30). If $\bar L_i$ are the aggregate Lipschitz constants of Assumption 3 and $M$ bounds the diameter of each $K_i$, put $B=(\max_i\bar L_i)NM$. Under the inherited assumptions of Proposition 4 and $0<\alpha<1/(2\mu p)$, the goal is existence and uniqueness of $x^*$ together with the last display on PDF page 29:

$$\limsup_{k\to\infty}\mathbb E\|x^k-x^*\|^2 \le \frac{\alpha}{\mu}\left(2C^2N+\frac{BC\sqrt{2nN}}{1-\sqrt\lambda}\right).$$

The milestones separately assert the unique VI solution, the aggregate identity, the bounded gradient evaluations, the contraction estimates (30)–(31), the one-step disagreement relation (44), Lemma 11's limiting disagreement bounds, and the equal-case recursion (55). Together they expose the quantities appearing in the target without weakening its constant or its dependence on $n$ and $N$.

Significance

The bound separates the effects of the step, game regularity, number of agents, decision dimension, and communication quality. In particular, for fixed other parameters the right-hand side scales linearly in $\alpha$ and worsens as $\lambda$ approaches one. It is a quantitative guarantee for a decentralized procedure that sees neighbour messages instead of the exact aggregate. The VI existence and uniqueness target also identifies the equilibrium to which the error is measured. The paper proves the special case in its concluding bound on page 29, subject to the domain correction described below; it is not an unresolved research conjecture.

Formalizing the result produces a reusable interface for graph gossip matrices, random pair draws, relational Euclidean projection, and nonnegative expected disagreement. The intermediate contraction and tracking statements can support other constant-step distributed optimization arguments. The theorem declarations in this proposal are open Lean proof obligations; a successful local build checks their types and definitions, not the mathematical claims. Contributions that establish these obligations, sharpen a bound under the same model, or isolate reusable probability and projection results are in scope.

Difficulty

The estimates $v_i^k$ are coupled to both random pair averaging and the agents' decision changes, so graph connectivity alone does not state a numerical disagreement bound. The proof has to respect the actual distribution of waking and contacted agents when moving from a one-player inequality to an expected profile error. The printed general version illustrates the risk: Assumption 8 controls changes in $x_i$ at a fixed aggregate and therefore cannot justify (53), where the aggregate changes; (54) also replaces coefficients on signed terms by their minimum. The final equal-step, equal-probability case removes these two obstacles, but still requires the exact constants in Lemma 11 and the error recursion.

Formalization scope

Players are indexed by Fin N, decisions use EuclideanSpace ℝ (Fin n), and a profile's squared Euclidean norm is the sum of squared block norms. Coordinate vectors across players also use a Euclidean norm; the ordinary Lean norm on Fin N → ℝ would be a supremum norm. The run starts from a deterministic feasible profile. This fixes the initial state before the independent discrete gossip draws, representing the source's Poisson-clock protocol at its tick times. A projection is a nearest-point relation on a nonempty compact convex set, with no arbitrary value on an empty set. Positive contact probabilities on all graph edges keep the connected graph active.

Assumption 1 is expressed through nonempty compact convex $K_i$ and continuity of $F_i$ on $K_i\times\bar K$, the part of the payoff regularity used by the algorithm. Assumption 3 is stated for every aggregate argument in $\mathbb R^n$, a disclosed strengthening of its printed domain $\bar K$: $N\hat v_i^k$ can leave $\bar K$, as the paper's footnote on page 10 acknowledges. Assumption 8 remains a hypothesis inherited from Proposition 4 even though its term vanishes for equal steps. The constants $C$, $\lambda$, and $M$ carry their defining bounds as hypotheses; the conclusion does not assume Lemma 11 or (55). Expected nonnegative quantities use extended-real lintegrals and an extended-real limit superior, preventing a failed Bochner integral from silently becoming zero. The formalization asserts existence of a VI solution, so an empty solution set cannot trivialize the goal.

Selected references

• J. Koshal, A. Nedić, and U. V. Shanbhag, Distributed Algorithms for Aggregative Games on Graphs, Operations Research 64(3):680–704, 2016. arXiv:1605.00267v2; DOI:10.1287/opre.2016.1501.

Motivation

Counting the proper $q$-colorings of a graph, and sampling one uniformly at random, are basic problems of approximate counting with a long history in statistical physics, where proper colorings are the zero-temperature antiferromagnetic Potts model. On bipartite graphs these problems are tied to #BIS, the problem of approximately counting independent sets in a bipartite graph, whose complexity is unresolved. Galanis, Štefankovič, Vigoda and Yang showed that approximately counting proper $q$-colorings is #BIS-hard on bipartite graphs of maximum degree $\Delta$ whenever $q \le \Delta/(2\log\Delta)$ (SIAM J. Comput. 45(6), 2016). A positive result in that regime therefore has to use structure beyond bipartiteness and bounded degree.

Jenssen, Keevash and Perkins (SIAM J. Comput. 49(4) 2020) use expansion. Their Theorem 5 says that for $\Delta \ge Cq^2\log^2 q$ there is an FPTAS and a polynomial-time sampler for proper $q$-colorings on almost every $\Delta$-regular bipartite graph. This answered Conjecture 1 of the authors' SODA 2019 extended abstract. Liao, Lin, Lu and Mao (APPROX/RANDOM 2019) independently proved a similar result under a slightly stronger condition on $\Delta$. The organizing idea, that most colorings of a strongly expanding bipartite graph follow one of a few patterns, comes from the work of Peled and Spinka on rigidity of colorings of $\mathbb Z^d$ (arXiv:1808.03597).

This mission is the fourth of a series formalizing the four main results of that paper; it covers Theorem 5.

Setting

Fix integers $q \ge 3$, $\Delta \ge 3$ and $m \ge 1$. The vertex set is $V = \mathcal O \sqcup \mathcal E$, two sides of $m$ vertices each (so $n = 2m$). $\mathcal G^{\mathrm{bip}}(2m,\Delta)$ is the finite set of labelled simple graphs on $V$ whose edges all join $\mathcal O$ to $\mathcal E$ and in which every vertex has degree $\Delta$. A property holds for almost every $\Delta$-regular bipartite graph if the fraction of graphs in $\mathcal G^{\mathrm{bip}}(2m,\Delta)$ having it tends to $1$ as $m \to \infty$.

For $S \subseteq V$ the vertex boundary $\partial S$ is the set of vertices outside $S$ with a neighbour in $S$, and $S^+ = S \cup \partial S$. The graph is a bipartite $(\sigma,\rho)$-expander if $|\partial S| \ge \rho|S|$ for every $S$ inside one side with $|S| \le \sigma m$.

A proper $q$-coloring is a map $f : V \to [q]$ with $f(u) \ne f(v)$ on every edge; $\mathcal X_q(G)$ is their set and $Z_G(q) = |\mathcal X_q(G)|$. A pattern is a pair $(A,B)$ of disjoint sets with $A \cup B = [q]$; there are $2^q$ of them. A coloring agrees with $(A,B)$ at $v$ if $v \in \mathcal O$ and $f(v) \in A$, or $v \in \mathcal E$ and $f(v) \in B$. For $S \subseteq V$, $\chi_{A,B}(S)$ is the set of proper colorings that disagree with $(A,B)$ at every vertex of $S$ and agree everywhere else.

$G^3$ joins two vertices at $G$-distance at most $3$. A set is little if $|S| \le 4q\frac{\log\Delta}{\Delta}m$. A polymer is a little set that is connected in $G^3$; $\mathcal C(G)$ is the set of polymers, and two polymers are compatible if their $G$-distance exceeds $3$. For a pattern $(A,B)$, the weight and the polymer partition function are

$$w_{A,B}(\gamma) = \frac{|\chi_{A,B}(\gamma)|}{|A|^m|B|^m}, \qquad \Xi_{A,B}(G) = \sum_{\Gamma} \prod_{\gamma\in\Gamma} w_{A,B}(\gamma),$$

the sum over all families $\Gamma \subseteq \mathcal C(G)$ of pairwise compatible polymers, the empty family included. Finally $\hat Z$ is an $\varepsilon$-relative approximation to $Z$ if $e^{-\varepsilon}\hat Z \le Z \le e^{\varepsilon}\hat Z$.

Formalization targets

Goal: the deterministic core of Theorem 5

There is an absolute constant $C > 0$ such that for all $q \ge 3$ and $\Delta \ge Cq^2\log^2 q$, almost every $\Delta$-regular bipartite graph $G$ satisfies

$$e^{-\varepsilon}\tilde Z_G(q) \le Z_G(q) \le e^{\varepsilon}\tilde Z_G(q), \qquad \tilde Z_G(q) = \sum_{(A,B)} |A|^m|B|^m\,\Xi_{A,B}(G), \quad \varepsilon = e^{-m/(4q)},$$

and, for every pattern $(A,B)$ and every polymer $\gamma \in \mathcal C(G)$, the Kotecký–Preiss condition

$$\sum_{\gamma' \in \mathcal C(G):\ d(\gamma',\gamma)\le 3} w_{A,B}(\gamma')\,e^{|\gamma'| + g(\gamma')} \le |\gamma|, \qquad g(\gamma) = \frac{\Delta}{10q^2\log\Delta}|\gamma|.$$

The constant $C$ is left existential, as in the paper.

Milestones

In the order of the proof:

1. Lemma 23, the expansion of almost every regular bipartite graph;
2. Lemma 27, the bound on $|\chi_{A,B}(S)|$;
3. Lemma 28, the covering of $\mathcal X_q(G)$ by $\chi_{A,B}(S)$ with $S$ little;
4. the product formula after (13);
5. Claim 30, the size bound for sparse sets;
6. the binomial estimate, an existing platform theorem;
7. Lemma 29, the reduction;
8. the weight bound of §5.1;
9. the per-vertex estimate (15).

Significance

The goal is the whole mathematical content of Theorem 5. The paper's algorithm (its Theorem 8, adapted from Helmuth, Perkins and Regts, Algorithmic Pirogov–Sinai theory) takes exactly these two facts as input. Given the Kotecký–Preiss condition, the cluster expansion of each $\log\Xi_{A,B}(G)$ converges and truncating it gives the estimator; the reduction transfers the estimate to $Z_G(q)$. With the goal proved, the remaining distance to the FPTAS is algorithmic bookkeeping, not combinatorics.

The result has been proved since 2019 and is not formalized anywhere. A formal proof would add a machine-checked polymer-model reduction for a spin system with exponentially many ground states, a reusable model of uniformly random regular bipartite graphs, and a checked instance of the "expansion implies few ground states" argument used throughout this literature.

Difficulty

The obvious first idea is a one-ground-state expansion, as for the hard-core model, where configurations are close to "all even" or "all odd". For colorings there are $2^q$ patterns. A coloring can lie close to several of them, so the reduction must show that the sets $\chi_{A,B}(S)$ with $S$ little overlap only negligibly. That needs an inclusion–exclusion step whose error is exponentially small in $m/q$. A second difficulty is the size of polymers: little sets are $q$ times larger than the sets of the hard-core analysis. Claim 30 is what keeps the union of compatible polymers from becoming a large set that the expansion no longer controls. Finally, the constants must be uniform in $q$. The single condition $\Delta \ge Cq^2\log^2 q$ has to cover the expansion lemma, the reduction and the Kotecký–Preiss estimate at once.

Formalization scope

The FPTAS and the sampling algorithm are not formalized. Mathlib has no machine model in which "polynomial time" could be stated, and the running times carry unquantified constants. The goal is the mathematics the algorithm rests on: the reduction and the Kotecký–Preiss condition, with the paper's constants $e^{-m/(4q)}$, $4q\log\Delta/\Delta$ and $\Delta/(10q^2\log\Delta)$. Neither half may be dropped. Replacing $e^{-m/(4q)}$ by an existential error, or summing the Kotecký–Preiss condition over compatible rather than incompatible polymers, would make the goal trivial or wrong.

Conventions committed to in Lean:

• Vertices are Fin m ⊕ Fin m, and $\mathcal G^{\mathrm{bip}}(2m,\Delta)$ is the set of labelled $\Delta$-regular graphs with edges only between the two fixed sides. The paper does not fix a bipartition; this fixed-sides model is a disclosed choice, matching §5's $|\mathcal O| = |\mathcal E| = m$.
• Distances are Mathlib's extended distance edist, so vertices in different components are at distance $\infty$ and never incompatible.
• A pattern is encoded by $A \subseteq [q]$ with $B = [q]\setminus A$. Patterns with an empty side are kept: their weights are $0$ under Lean's $x/0 = 0$, so they contribute $0$ to $\tilde Z_G(q)$, as on the page for large $m$.
• log is the natural logarithm; the binomial estimate is used in nats.

Added hypotheses:

• $A, B \ne \emptyset$ in Lemma 27 and in the product formula, which divide by $|A|$ and $|B|$;
• $\Delta \ge 3$ in Lemma 28 and Claim 30, the paper's standing convention (§1.3);
• $m \ge 1$ in Lemma 29, which fails on the empty vertex set.

The goal needs none of these, since its limit is in $m$ and its constant absorbs $\Delta$.

A complete development needs a counting theory of random regular bipartite graphs (for Lemma 23, through Bassalygo's expansion theorem), counts of connected sets in bounded-degree graphs, and inclusion–exclusion over patterns. The random-graph model and the polymer-model definitions are reusable across this series and beyond. Proofs of any milestone, and alternative routes to Lemma 23, are welcome.

Selected references

• M. Jenssen, P. Keevash and W. Perkins, Algorithms for #BIS-hard problems on expander graphs, SIAM J. Comput. 49(4) (2020) 681–710. https://doi.org/10.1137/19M1286669
• A. Galanis, D. Štefankovič, E. Vigoda and L. Yang, Ferromagnetic Potts model: refined #BIS-hardness and related results, SIAM J. Comput. 45(6) (2016) 2004–2065.
• R. Peled and Y. Spinka, Rigidity of proper colorings of $\mathbb Z^d$, arXiv:1808.03597 (2018). https://arxiv.org/abs/1808.03597
• C. Liao, J. Lin, P. Lu and Z. Mao, Counting independent sets and colorings on random regular bipartite graphs, APPROX/RANDOM 2019, Schloss Dagstuhl–Leibniz-Zentrum für Informatik (2019).
• T. Helmuth, W. Perkins and G. Regts, Algorithmic Pirogov–Sinai theory, Probab. Theory Related Fields (2020); extended abstract at STOC 2019.
• R. Kotecký and D. Preiss, Cluster expansion for abstract polymer models, Comm. Math. Phys. 103(3) (1986) 491–498.
• L. A. Bassalygo, Asymptotically optimal switching circuits, Problems Inform. Transmission 17(3) (1981) 206–211.

Why saddle points matter for stochastic gradient methods

Most training objectives in machine learning are smooth and nonconvex, and they are minimized by stochastic gradient descent (SGD) and its variants. For nonconvex $f$ the classical guarantee is convergence to an $\epsilon$-first-order stationary point, $\|\nabla f(x)\|\le\epsilon$: Ghadimi and Lan (arXiv:1309.5549) showed that SGD reaches one in $\tilde O(\epsilon^{-4})$ stochastic gradient queries, independently of the dimension. A first-order stationary point may be a saddle point, however, and for many problems (matrix sensing and completion, phase retrieval, tensor decomposition, dictionary learning) every second-order stationary point is a global minimum. For these problems, a guarantee for second-order stationary points is a guarantee of global optimality.

Timeline:

• 2015. Ge, Huang, Jin and Yuan (arXiv:1503.02101) proved that noisy SGD escapes strict saddle points in polynomial time, with a large polynomial dependence on $d$ and $1/\epsilon$.
• 2017. Jin, Ge, Netrapalli, Kakade and Jordan (arXiv:1703.00887) showed that gradient descent with occasional perturbations finds an $\epsilon$-second-order stationary point in $\tilde O(\ell\Delta_f/\epsilon^2)$ iterations, only polylogarithmically worse than plain gradient descent for first-order points.
• 2019. The paper of this mission, Jin, Netrapalli, Ge, Kakade and Jordan (arXiv:1902.04811; J. ACM 68(2), 2021), extends this to the stochastic setting with norm-subGaussian gradient noise: perturbed SGD needs $\tilde O(\epsilon^{-4})$ queries when the stochastic gradients are Lipschitz and $\tilde O(d\epsilon^{-4})$ in general.

Setting

Let $f:\mathbb R^d\to\mathbb R$ be bounded below with $f^\star=\inf f$, and write $\Delta_f=f(x_0)-f^\star$. Assumption A: $f$ is $\ell$-gradient Lipschitz, $\|\nabla f(x_1)-\nabla f(x_2)\|\le\ell\|x_1-x_2\|$, and $\rho$-Hessian Lipschitz, $\|\nabla^2 f(x_1)-\nabla^2 f(x_2)\|\le\rho\|x_1-x_2\|$ in operator norm. A point $x$ is an $\epsilon$-second-order stationary point if

$$\|\nabla f(x)\|\le\epsilon\qquad\text{and}\qquad\lambda_{\min}(\nabla^2 f(x))\ge-\sqrt{\rho\epsilon}.$$

The algorithm sees only a stochastic gradient $g(x;\theta)$ with $\theta\sim\mathcal D$. Assumption B asks that $\mathbb E\,g(x;\theta)=\nabla f(x)$ and that the error is norm-subGaussian: $\mathbb P(\|g(x;\theta)-\nabla f(x)\|\ge t)\le2e^{-t^2/(2\sigma^2)}$ for $t\ge0$. The optional Assumption C asks that each $g(\cdot;\theta)$ is $\tilde\ell$-Lipschitz. The two cases combine into

$$\mathfrak N=1+\min\Big\{\frac{\sigma^2}{\epsilon^2}+\frac{\tilde\ell^2}{\ell\sqrt{\rho\epsilon}},\ \frac{\sigma^2d}{\epsilon^2}\Big\},$$

with $\tilde\ell=+\infty$ when Assumption C is not used.

Perturbed SGD (PSGD, Algorithm 2) draws $\theta_t\sim\mathcal D$ and an independent Gaussian $\xi_t\sim\mathcal N(0,(r^2/d)I)$ at every step and updates

$$x_{t+1}=x_t-\eta\big(g(x_t;\theta_t)+\xi_t\big).$$

Formalization targets

Goal: Theorem 16

For a log factor $\iota$, the proof uses the parameters of Eq. (8): $\eta=1/(\iota^9\ell\mathfrak N)$, $r=\iota\epsilon\sqrt{\mathfrak N}$, $\mathscr T=\lceil\iota/(\eta\sqrt{\rho\epsilon})\rceil$, $\mathscr F=\iota^{-5}\sqrt{\epsilon^3/\rho}$, and runs for $T=\lceil100\max\{\Delta_f\mathscr T/\mathscr F,\Delta_f/(\eta\epsilon^2)\}\rceil=\tilde O(\ell\Delta_f\mathfrak N/\epsilon^2)$ iterations. The goal states that there is an absolute constant $\mu_0$ such that, for $\iota\ge\mu_0(1+\log Q)$ with $Q=d\,\mathfrak N\max\{1,\ell\Delta_f/\epsilon^2\}(\ell/\sqrt{\rho\epsilon})/\delta$,

$$\mathbb P\Big(\#\{t<T:\ x_t\ \text{is an }\epsilon\text{-second-order stationary point}\}\ge T/2\Big)\ge1-\delta.$$

Milestones

The proof's two engines, in the paper's order: the concentration inequalities for norm-subGaussian martingale differences (Lemmas 36–39), the descent lemma (Lemma 23), improve-or-localize (Lemma 24), the coupling analysis around a saddle point (Lemmas 27–31), escape from a saddle point (Lemma 25), and the two claims that bound the number of iterates with large gradient and the number near saddle points.

Significance

The theorem shows that adding isotropic Gaussian noise to SGD suffices to find second-order stationary points at essentially the cost SGD pays for first-order points: $\tilde O(\epsilon^{-4})$ queries when Assumption C holds (matching Ghadimi–Lan up to logarithms) and $\tilde O(d\epsilon^{-4})$ in general. Combined with landscape results such as "every second-order stationary point is a global minimum", it yields global convergence of a simple first-order stochastic method from arbitrary initialization for the problems listed above.

The result is proved on paper. As far as is known, none of it is machine-checked: neither the escape-from-saddle-point argument by coupling sequences nor the vector-valued concentration inequalities of Appendix C, whose proofs the paper defers to a separate technical note (arXiv:1902.03736). Formalizing them yields reusable norm-subGaussian martingale bounds in $\mathbb R^d$, a checked version of the coupling technique that later saddle-escape analyses reuse, and a check of every constant hidden in the paper's $\tilde O(\cdot)$.

Difficulty

The descent lemma alone cannot rule out that the iterates stall near a strict saddle point, where the gradient is small and the negative curvature is invisible to first-order information. The obvious argument, which says that the perturbation has a component along the negative eigendirection and that component grows, fails as stated: the stochastic gradient noise, the Hessian's variation along the trajectory, and the perturbation all interact over $\mathscr T$ steps. Controlling these interactions needs concentration bounds for vector-valued martingales whose scale is itself random (Lemma 37), which have no counterpart in Mathlib. Bounding how often the iterates can return to saddle regions over the whole run is a separate difficulty, since the times at which the iterates are near a saddle point are random.

Formalization scope

$\mathbb R^d$ is EuclideanSpace ℝ (Fin d) with $d\ge1$; the Hessian is the derivative of the gradient map, and $\lambda_{\min}$ is the Rayleigh-quotient infimum over the unit sphere. The randomness is the infinite product measure of the pairs $(\theta_t,\xi_t)$, and the PSGD run is a deterministic function of it. Conventions committed to:

• Explicit constants in place of $\tilde O(\cdot)$. The paper writes $\eta=\tilde\Theta(1/(\ell\mathfrak N))$, $r=\tilde\Theta(\epsilon\sqrt{\mathfrak N})$ (Eq. (4)) and $\tilde O(\ell\Delta_f\mathfrak N/\epsilon^2)$; the statements use the proof's Eq. (8) and its $T$, with $\mathscr T$ and $T$ rounded up to integers. Every "absolute constant $c$" of a lemma is an existential quantified before the dimension, the oracle, the function and all parameters, so it cannot depend on them.
• Calibration of $\iota$. The printed $\iota=\mu\log(d\ell\Delta_f\mathfrak N/(\rho\epsilon\delta))$ is not invariant under rescaling $x\mapsto\lambda x$ and can be non-positive. The goal and the two claims assume $\iota\ge\mu_0(1+\log Q)$ with the scale-invariant $Q$ above.
• Hypotheses made explicit. $\rho>0$, $\epsilon>0$, $0<\delta<1$, $\sqrt{\rho\epsilon}\le\ell$ (the paper's footnote 1, p. 14), $\sigma>0$, joint measurability of $g$, and integrability of the stochastic gradients. Assumption B and Condition 35 hold for $t\ge0$, since the printed "$\forall t\in\mathbb R$" cannot be satisfied.
• Corrections. Lemma 29 requires $\eta\gamma>0$, Lemma 37 has failure probability $2d(\log(B/b)+1)e^{-\iota}$, and Lemma 25 is stated at $t_0=0$ from a deterministic saddle point, the case the paper proves.

A formalization that keeps the printed "$\forall t\in\mathbb R$" in Assumption B, or allows $\sigma=0$ in the tail bound, makes every statement vacuous or trivial; both are excluded. Infrastructure needed: norm-subGaussian vectors and their martingale concentration (reusable well beyond this mission), Gaussian anti-concentration in one direction, and stopping-time arguments for the Markov chain of PSGD. Contributions to any milestone, and to the concentration layer in particular, are welcome.

Selected references

• C. Jin, P. Netrapalli, R. Ge, S. M. Kakade, M. I. Jordan, On Nonconvex Optimization for Machine Learning: Gradients, Stochasticity, and Saddle Points, arXiv:1902.04811v2, 2019; J. ACM 68(2), 2021. https://arxiv.org/abs/1902.04811
• C. Jin, P. Netrapalli, R. Ge, S. M. Kakade, M. I. Jordan, A Short Note on Concentration Inequalities for Random Vectors with SubGaussian Norm, arXiv:1902.03736, 2019. https://arxiv.org/abs/1902.03736
• C. Jin, R. Ge, P. Netrapalli, S. M. Kakade, M. I. Jordan, How to Escape Saddle Points Efficiently, ICML 2017. https://arxiv.org/abs/1703.00887
• R. Ge, F. Huang, C. Jin, Y. Yuan, Escaping From Saddle Points — Online Stochastic Gradient for Tensor Decomposition, COLT 2015. https://arxiv.org/abs/1503.02101
• S. Ghadimi, G. Lan, Stochastic First- and Zeroth-Order Methods for Nonconvex Stochastic Programming, SIAM J. Optim. 23(4), 2013. https://arxiv.org/abs/1309.5549

Motivation

An online retailer that serves many kinds of customers must decide, for each arriving customer, which handful of products to display. Showing too many items is impossible (screen space, shelf space), and which items sell depends on who is looking. The retailer does not know the customers' preferences in advance and learns them only from the choices customers make among the items shown. This is dynamic assortment personalization: an online learning problem in which every display both earns revenue and produces data.

Kallus and Udell (arXiv:1610.05604) study the regime in which the number of customer types $m$ and the number of items $n$ are both large, so that learning each type's preferences separately would take on the order of $mn$ interactions. Their premise is that preferences across types are governed by a few latent features, which makes the matrix of preference parameters approximately low rank. The non-contextual problem — one customer type, multinomial-logit choice — was studied by Rusmevichientong, Shen and Shmoys (2010) and Sauré and Zeevi (2013); the paper extends it to many types and proposes an explore-then-exploit policy whose estimates come from nuclear-norm regularized maximum likelihood, the standard convex surrogate for low rank used in matrix completion.

Setting

There are $m$ customer types and $n$ items. Each type $i$ has a revenue vector $W_i\in\mathbb R^n$ (row $i$ of $W\in\mathbb R^{m\times n}$; $W_{ij}$ is the expected revenue when type $i$ buys item $j$) and a preference vector $\Theta^\star_i$ (row $i$ of the unknown matrix $\Theta^\star\in\mathbb R^{m\times n}$). Types arrive independently from an unknown distribution $\mu^\star$ in the simplex $\Delta^m$.

For an assortment $S\subseteq\{1,\dots,n\}$ and a parameter vector $\theta\in\mathbb R^n$, the multinomial-logit (MNL) choice probability of item $j\in S$ is

$$p_j(S;\theta)=\frac{e^{\theta_j}}{1+\sum_{j'\in S}e^{\theta_{j'}}},$$

and the customer buys nothing with probability $1/(1+\sum_{j'\in S}e^{\theta_{j'}})$. The expected revenue of $S$ is $F(S;w,\theta)=\sum_{j\in S}p_j(S;\theta)w_j$, and $S^\star(w,\theta;K)$ is the set of maximizers of $F(\cdot;w,\theta)$ over $|S|\le K$. The revenue gap $\delta(w,\theta;K)$ is the optimal revenue minus the best revenue of a non-optimal assortment.

In round $t=1,2,\dots$ a customer of type $i_t\sim\mu^\star$ arrives, the retailer offers $S_t$ with $|S_t|\le K$, and the customer chooses $j_t$ from the MNL law with parameters $\Theta^\star_{i_t}$. The regret (Definition 1) of a policy after $T$ rounds is the expected revenue of the $\Theta^\star$-greedy policy, which always offers an element of $S^\star(W_{i_t},\Theta^\star_{i_t};K)$, minus the expected revenue of the policy.

Algorithm 2, $\pi_{\text{nuc-norm}}(C,\lambda)$, keeps a sample $\mathcal O$ of exploration observations. At round $t$, if $|\mathcal O|\le Cr(m+n)\log t$ it explores: it offers a uniformly random subset of size exactly $K$ and records $(i_t,j_t,S_t)$. Otherwise it exploits: it offers an element of $S^\star(W_{i_t},\widehat\Theta_{i_t};K)$, where $\widehat\Theta$ is a solution of

$$\min_{\Theta}\ L(\Theta)+\lambda\|\Theta\|_*\quad\text{s.t.}\quad\|\Theta\|_\infty\le\alpha/\sqrt{mn},\tag{5}$$

with $L$ the average negative log-likelihood (4) of the sample, $\|\cdot\|_*$ the nuclear norm and $\|\Theta\|_\infty$ the largest absolute entry.

Formalization targets

Goal: Theorem 6

Let $r\ge\operatorname{rank}\Theta^\star$, $1/\rho\le m\mu^\star_i\le\rho$ for all $i$, $\|\Theta^\star\|_\infty\le\alpha/\sqrt{mn}$, $\min_i\delta(W_i,\Theta^\star_i;K)\ge\delta>0$ and $0\le W$, $\max_{ij}|W_{ij}|\le\omega$. With

$$C=\frac{4194304\,K^6\rho^3\omega^2\alpha^2e^{16\alpha}}{\delta^2},\qquad\lambda=8\sqrt{\frac{\rho K}{Crmn}},\tag{12}$$

for every selection of $\widehat\Theta$ from the solutions of (5) and of the exploited assortment,

$$\mathrm{Regret}(T;\pi_{\text{nuc-norm}}(C,\lambda))\le\big((Cr(m+n)+3)\log T+1\big)\,\omega\qquad\text{for }1\le T\le(m+n)^{mn/(Cr(m+n))}.$$

Milestones

From the printed proof of Theorem 6 (pp. 47–48): the Lipschitz bound $|p_j(S;\theta)-p_j(S;\theta')|\le\frac14\sqrt{|S|}\|\theta-\theta'\|_2$; the revenue bound $|F(S;w,\theta)-F(S;w,\theta')|\le\frac14\|w\|_\infty K^{3/2}\|\theta-\theta'\|_2$; the comparison $F(S';w,\theta)\ge F(S;w,\theta)-\frac12\|w\|_\infty K^{3/2}\|\theta-\theta'\|_2$ of optimal sets; the stability of the optimal set; and the count of exploration rounds. From the deterministic part of the recovery analysis (Sec. 8): Lemma 2 (a quadratic lower bound on the Bregman divergence of $L$), Lemma 5 (an upper bound from the regularized objective) and Lemma 6 (the nuclear-norm error is controlled by $\sqrt r$ times the Frobenius error and the spectral tail of $\Theta^\star$).

Significance

Theorem 6 is the paper's guarantee that a policy exploiting low-rank structure pays regret of order $r(m+n)\log T$ rather than the order $mn\log T$ that the paper shows (Theorem 5) for policies treating each type separately. The intermediate results are reusable: the Lipschitz bounds for MNL choice probabilities and revenue apply to any MNL assortment policy that plugs in estimated parameters, and Lemmas 2, 5 and 6 are the deterministic core of nuclear-norm regularized estimation for a likelihood that is not an entrywise loss.

To the best of current knowledge none of these results has a machine-checked proof. The mission produces a formal model of a contextual MNL assortment process with an adaptive policy, its trajectory law and regret, together with formal statements and proofs of the Lipschitz and stability facts that any explore-then-exploit analysis of MNL assortment needs. Several printed statements needed correction (see Formalization scope); machine-checked proofs settle the corrected forms.

Difficulty

The goal is a statement about the law of a $T$-round adaptive process: the offered set at round $t$ depends on the whole past through the exploration test and through an estimate defined only as some minimizer of (5). Any argument must handle this dependence exactly, for every admissible selection of minimizer and of optimal assortment, rather than for one convenient choice.

The constants are explicit and the horizon is restricted, so the inequality has to hold with the paper's normalization exactly as stated, including the box constraint of (5). The printed proof routes through the paper's high-probability recovery bound (Theorem 3), which is believed false as printed and is not part of this mission, so a proof cannot simply cite it. Lemmas 5 and 6 require Hölder's inequality for the spectral/nuclear pairing and a decomposition of the error relative to the singular subspaces of $\Theta^\star$; Lemma 2 requires a curvature estimate for the log-sum-exp function uniformly on the box.

Formalization scope

The source is the arXiv preprint arXiv:1610.05604, an unstamped PDF pinned by sha256 2b010481…216a; its printed page numbers equal the PDF page numbers.

Types and items are Fin m and Fin n, 0-based; the no-purchase option is none. Matrices are MatrixCompletion.RealMatrix m n; the nuclear, spectral and Frobenius norms, the Frobenius inner product and $\|\cdot\|_\infty$ are the published MatrixCompletion definitions, and $F$ is the published ChoiceCDLP.MNL.mnlObjective with weights $e^{\theta_j}$ and no-purchase weight $1$. All probabilities and expectations are finite sums over histories in Fin T → Fin m × Finset (Fin n) × Option (Fin n). Regret is Definition 1 after the tower property: the greedy policy earns $\sum_i\mu^\star_i\max_{|S|\le K}F(S;W_i,\Theta^\star_i)$ per round and Algorithm 2 earns $F(S_t;W_{i_t},\Theta^\star_{i_t})$ in expectation. The gap condition $\delta(w,\theta;K)\ge d$ is stated as "every non-optimal assortment of size at most $K$ earns at most the optimum minus $d$", since $\delta$ itself is undefined when every assortment is optimal.

Added hypotheses and corrections, each disclosed in the item's note:

• Theorem 6 assumes $W\ge0$, $\delta>0$, $1\le K\le n$, $m,n\ge1$ and $T\ge1$. The horizon is read as $T\le(m+n)^{mn/(Cr(m+n))}$ (the page sets $r$ beside the fraction in the exponent); for $r\ge1$ this is the smaller range. If $r=0$, Lean's division by zero gives $\lambda=0$ and horizon $T\le1$.
• The stability of the optimal set (p. 47) is false as printed (an equality of optimal sets) and is stated as the inclusion $S^\star(w,\theta';K)\subseteq S^\star(w,\theta;K)$ under the page's (non-strict) closeness hypothesis, multiplied out.
• The exploration count (p. 48) is stated as $Cr(m+n)\log T+1$, the form the next display uses, instead of the printed $C\log T+1$.
• Lemma 2 is false as printed and carries an extra factor $\frac12$; it assumes $\Theta^\star$ and $\Theta^\star+\Delta$ both feasible for (5).
• Lemmas 5 and 6 carry the standing assumptions of Sec. 8: $\widehat\Theta$ solves (5), $\Theta^\star$ is feasible, $\lambda>0$.

Theorem 3 (static recovery) and Lemma 4 (gradient concentration) are not posed: both are believed false as printed. Lemmas 3 and 7 are not posed either.

A trivializing formalization is ruled out: the estimator is any minimizer of (5) with its box constraint, the exploited set is any optimal assortment for the estimate, and both are quantified universally; exploration draws uniformly from subsets of size exactly $K$; and the benchmark is the $\Theta^\star$-greedy policy under the same arrival law. Fixing the estimator to $\Theta^\star$, dropping the box, or comparing to the best fixed assortment would change the theorem.

Contributions welcome: proofs of the milestones (the Lipschitz lemmas are calculus on the softmax function; Lemmas 5 and 6 are matrix analysis reusable for other nuclear-norm estimators), a proof that the definition of $\nabla L$ is the gradient of $L$, and a proof that the history weights form a probability distribution.

Selected references

• N. Kallus, M. Udell, Dynamic Assortment Personalization in High Dimensions, arXiv preprint, 2016–2017; Operations Research 68(4), 2020. https://arxiv.org/abs/1610.05604
• P. Rusmevichientong, Z.-J. M. Shen, D. B. Shmoys, Dynamic assortment optimization with a multinomial logit choice model and capacity constraint, Operations Research 58(6), 2010. https://doi.org/10.1287/opre.1100.0866
• D. Sauré, A. Zeevi, Optimal dynamic assortment planning with demand learning, Manufacturing & Service Operations Management 15(3), 2013. https://doi.org/10.1287/msom.1120.0412
• B. Recht, M. Fazel, P. A. Parrilo, Guaranteed minimum-rank solutions of linear matrix equations via nuclear norm minimization, SIAM Review 52(3), 2010. https://doi.org/10.1137/070697835