Statistics

Why a lower bound for best subsets

Best subset selection fits a linear model by least squares using at most $k$ of $p$ available predictors. It is the classical $\ell_0$-constrained estimator of sparse regression. Mixed-integer optimization now computes it for problems with thousands of variables (Bertsimas, King & Mazumder 2016), so its statistical behaviour matters in practice. Simulations in Hastie, Tibshirani & Tibshirani 2020 found that it predicts worse than shrinkage methods such as the Lasso when the signal-to-noise ratio (SNR) is low.

Mazumder, Radchenko and Dedieu (arXiv:1708.03288v4; Operations Research, 2023) add an $\ell_1$ or $\ell_2$ shrinkage penalty to best subsets. They prove upper bounds of two kinds: slow rates, linear in the tuning parameter $\lambda$, and fast rates, quadratic in $\lambda$. Theorems 2 and 3 of the paper give them for the shrunken estimators. For best subsets, the paper only has a fast-rate bound, of order $\sigma^2 k\log(ep/k)$. When $\|\beta^*\|/\sigma$ is small, the shrunken estimators' slow rate beats that bound. Theorem 4, the goal of this mission, shows that the comparison is meaningful: in that regime best subsets really does incur an error of the order of its upper bound.

Setting

The data follow the linear model

$$y = X\beta^* + \epsilon ,\qquad y,\epsilon\in\mathbb R^n,\ \beta^*\in\mathbb R^p ,$$

where the design $X$ is a deterministic real $n\times p$ matrix whose columns have unit Euclidean norm. The noise $\epsilon$ has independent $N(0,\sigma^2)$ entries, with $\sigma>0$. Write $\|v\|$ for the Euclidean norm, $\|v\|_1=\sum_i|v_i|$, $\operatorname{supp}(v)=\{i:v_i\ne0\}$ and $\|v\|_0=|\operatorname{supp}(v)|$. The $\ell_0$ ball is $B_0(s)=\{u\in\mathbb R^p:\|u\|_0\le s\}$. The minimal $s$-sparse eigenvalue of $X$ is

$$\gamma_s=\min_{u\ne0,\ u\in B_0(s)}\frac{\|Xu\|}{\|u\|} .$$

A best-subsets solution of size $k$ is any minimizer

$$\hat\beta_{\ell_0}\in\arg\min\ \|y-X\beta\|^2\quad\text{s.t.}\quad\|\beta\|_0\le k .\tag{1}$$

A constant is universal if it does not depend on $n,p,k,X,\sigma,\beta^*$. The symbols $\lesssim$ and $\gtrsim$ mean $\le$ and $\ge$ up to positive universal factors. Logarithms are natural, and $e=\exp(1)$.

Formalization targets

Goal: Theorem 4 (p. 18)

There are universal constants $c_0,c,C>0$ such that the following holds. Suppose $2\le k\le p$, $\|\beta^*\|_0\le k$ and $\|\beta^*\|\le c_0\sigma\gamma_k\sqrt{k\log(ep/k)}$. Then, with probability at least $1-2(ep/k)^{-c\gamma_k^2k}-(ep/k)^{-k}$, every best-subsets solution satisfies

$$\|X\hat\beta_{\ell_0}-X\beta^*\|^2\ \ge\ C\,\sigma^2\gamma_k^2\,k\log(ep/k).$$

The constants are left unfixed, as in the paper. The statement asserts the order of the error, which is what the comparison with the upper bounds needs.

Milestones

1. Maurey approximation (p. 44). For unit columns and every $\beta^*$, some $\tilde\beta^*$ with $\|\tilde\beta^*\|_0\le k/2$ has $\|X\beta^*-X\tilde\beta^*\|^2\le2\|\beta^*\|_1^2/k$.
2. (39) (p. 44). With $\Delta^*=X\beta^*-X\tilde\beta^*$, define $G(\beta)=\|y-X\beta\|^2-\|y-X\tilde\beta^*\|^2$ and $H(u)=\|Xu\|^2-2(\Delta^*+\epsilon)^\top Xu$. Then $G(\beta)$ equals $\|X\beta-X\tilde\beta^*\|^2+2(\Delta^*+\epsilon)^\top(X\tilde\beta^*-X\beta)$, and $\min_{\|\beta\|_0\le k}G\le\min H(u)$ over $u$ supported off $\operatorname{supp}(\tilde\beta^*)$ with $\|u\|_0\le k/2$.
3. (40) (p. 45). $\min_{\|\beta\|_0\le k}G(\beta)\le-\max_{v\in\mathcal V_k}|(\Delta^*+\epsilon)^\top Xv|^2$, where $\mathcal V_k$ is the set of $v$ supported off $\operatorname{supp}(\tilde\beta^*)$ with $\|v\|_0\le k/2$ and $\|Xv\|=1$.
4. Lemma 1 (p. 44). Let $S$ have $q$ elements and let $s\in[1,q]$ be an integer. Then $\max|\epsilon^\top Xv|\gtrsim\sigma\gamma_{2s}\sqrt{s\log(eq/s)}$ over $\operatorname{supp}(v)\subseteq S$, $\|v\|_0\le s$, $\|Xv\|=1$, with probability at least $1-2(eq/s)^{-\tilde c\gamma_{2s}^2s}$.

Significance

Theorem 4 matches the fast-rate upper bound for best subsets from Corollary 1 of the paper. When $\gamma_k$ is bounded below, the prediction error of best subsets is of exact order $\sigma^2k\log(ep/k)$ in the low-SNR regime (Remark 10). This is the theoretical counterpart of the empirical observation that best subsets overfits at low SNR. It is also what makes the paper's case for shrinkage a theorem rather than a comparison of upper bounds. The paper's Proposition 4 applies it to a concrete correlated design, where it gives a ratio of prediction errors between best subsets and its $\ell_2$-shrunken version that grows with $k$.

The result is proved in the paper; this mission formalizes it. No formalization of this result exists on the platform. The mission also produces a reusable Gaussian lower bound on sparse correlations (Lemma 1) and a deterministic reduction of the best-subsets objective, (39)–(40), which are of independent use for $\ell_0$ estimators.

Difficulty

An upper bound on best subsets follows from comparing $\hat\beta_{\ell_0}$ with $\beta^*$ in a basic inequality. A lower bound must hold for every minimizer, and $\beta^*$ itself gives no lower bound. The first idea is to compare with the noiseless fit. It fails because the noise can be fitted by sparse directions, which is exactly the effect to be quantified. The difficult step is Lemma 1. It requires a large set of sparse directions that remain separated after multiplication by $X$, a lower bound on the expected maximum of a Gaussian process over that set, and concentration of that maximum around its mean, with all constants universal. A second subtlety is that the statement is about every minimizer of a nonconvex problem, so the proof has to bound the objective rather than the estimator.

Formalization scope

Vectors are Fin n → ℝ and Fin p → ℝ, with indices starting at 0. The design is X : Matrix (Fin n) (Fin p) ℝ. The Euclidean norm, $\ell_1$ norm, support and $\|\cdot\|_0$ are explicit definitions, since Mathlib's norm on Fin m → ℝ is the sup norm. $\gamma_s$ is an infimum over the nonzero vectors with $\|u\|_0\le s$; this set is nonempty when $p,s\ge1$, and every ratio is $\ge0$. The noise law is the product of $n$ centred Gaussians of variance $\sigma^2$ on $\mathbb R^n$. "With probability at least $1-\eta$" means that a measurable set of noise vectors of probability at least $1-\eta$ exists on which the conclusion holds. Best subsets is an argmin predicate: Theorem 4 quantifies over every minimizer, and existence is neither assumed nor needed. Universal constants are quantified before every other parameter. "$\|\cdot\|_0\le k/2$" is a comparison of real numbers.

The model consists of $X$, $\beta^*$ (with $f^*=X\beta^*$), $\epsilon$ and its Gaussian law, the estimator (1), and the minimal sparse eigenvalue $\gamma_s$.

Two hypotheses are pinned relative to the printed theorem:

• $k\ge2$, because the statement is false for $k=1$. Take every column equal to $e_1$ and $\beta^*=0$: the error is $\epsilon_1^2$, while the bound demands order $\sigma^2\log(ep)$ with probability tending to one.
• $\|\beta^*\|_0\le k$, because the proof uses $\|\beta^*\|_1$, which the printed $\ell_2$ hypothesis controls only for sparse $\beta^*$, and §3.4 places the theorem in Corollary 1's setting $\beta^*\in B_0(k)$.

The milestones carry neither pin. Because the constants are existential, a formalization in which $c_0$, $c$ or $C$ may depend on $p$, $k$ or $X$ would be trivial, and is ruled out by quantifying them first. A version asserting the bound for some minimizer would be weaker than the theorem.

Not formalized here: the upper bounds (Theorems 2, 3, 5), the noise events of Theorem 1, Corollaries 1–6, Propositions 3–4, and the numerical experiments. The proof of the goal also uses Theorem 1's event $\mathcal G_{2k}$, which belongs to a separate mission of this series. Proved platform results that a proof of Lemma 1 can use include Sudakov minoration for separated Gaussian families (HighDimProb.RandomProcesses.sudakov_minoration_finite_separated), Gaussian Lipschitz concentration (HighDimStat.TailBounds.lipschitz_gaussian_concentration) and a lower bound on Gaussian maxima (HighDimProb.RandomProcesses.standard_gaussian_max_lower_bound). Contributions are welcome on any milestone, and on supporting lemmas: a packing of sparse sign vectors (Gilbert–Varshamov type), and the approximation of $\ell_1$-bounded vectors by sparse ones.

Selected references

• R. Mazumder, P. Radchenko, A. Dedieu, Subset Selection with Shrinkage: Sparse Linear Modeling When the SNR Is Low, Operations Research, 2023; preprint arXiv:1708.03288v4, 2022. https://arxiv.org/abs/1708.03288v4
• D. Bertsimas, A. King, R. Mazumder, Best subset selection via a modern optimization lens, Annals of Statistics 44(2), 2016. https://doi.org/10.1214/15-AOS1388
• T. Hastie, R. Tibshirani, R. Tibshirani, Best Subset, Forward Stepwise or Lasso? Analysis and Recommendations Based on Extensive Comparisons, Statistical Science 35(4), 2020. https://doi.org/10.1214/19-STS733
• P. C. Bellec, G. Lecué, A. B. Tsybakov, Slope meets Lasso: improved oracle bounds and optimality, Annals of Statistics 46(6B), 2018. https://doi.org/10.1214/17-AOS1670
• R. Vershynin, High-Dimensional Probability, Cambridge University Press, 2018. https://doi.org/10.1017/9781108231596

Why shrink a best subset?

Best subset selection fits a linear predictor using at most $k$ of $p$ available columns. Its explicit limit on the number of selected variables makes the model easy to interpret, but the search can still fit noise: among many subsets of the same size, one can align unusually well with a noisy response. Mazumder, Radchenko and Dedieu study this effect in Subset Selection with Shrinkage. They add a penalty on the size of the selected coefficients and show how this changes prediction error when the signal-to-noise ratio is low.

An $\ell_1$ penalty is familiar from the Lasso. The estimator here also keeps the subset-size constraint, so its comparison class and its tuning parameter have a different role from those in an unconstrained Lasso. The paper's Theorem 3 gives three deterministic error bounds for this estimator, each valid on a specified event of the Gaussian noise. These bounds are the target of this mission. The separate probability estimates for the events are Theorem 1 of the paper and belong to another mission in this series.

Setting

Let $X\in\mathbb R^{n\times p}$ be a fixed design matrix whose columns have Euclidean norm one. The observation is $y=f^*+\epsilon$, where $f^*\in\mathbb R^n$ is a fixed mean and the coordinates of $\epsilon$ are independent $N(0,\sigma^2)$ random variables, with $\sigma>0$. The result below fixes one realized noise vector $\epsilon$ and assumes it lies in an event stated below. No assumption that $f^*$ is itself a linear combination of columns of $X$ is required.

For $1\le k\le p$, write $B_0(k)=\{\beta\in\mathbb R^p:\|\beta\|_0\le k\}$, where $\|\beta\|_0$ counts nonzero coordinates. An $\ell_1$-regularized best subset estimator is any minimizer

$$\hat\beta_1\in\operatorname*{argmin}_{\beta\in B_0(k)}\bigl\{\|y-X\beta\|_2^2+\lambda\|\beta\|_1\bigr\}.\tag{16}$$

The objective has no factor $1/2$. The assertion applies to every minimizer, so tied solutions are covered. The sparse minimum singular value is $\gamma_s=\inf\{\|Xu\|_2/\|u\|_2:u\ne0,\ \|u\|_0\le s\}$. When $p\ge1$ and $s\ge1$ its domain is nonempty. Write $u_1^\sharp,\ldots,u_p^\sharp$ for the decreasing rearrangement of $|u_1|,\ldots,|u_p|$.

The paper defines three noise events used here. $\mathcal H$ bounds the largest coordinate of $X^\top\epsilon$ by $\sigma\sqrt{2\log(2p)}+\sigma\sqrt{2\log(1/\delta_0)}$. On $\mathcal F$, every $u\in\mathbb R^p$ satisfies

$$\epsilon^\top Xu\le(4+\sqrt2)\sigma\max\left\{\sum_{j=1}^{p}u_j^\sharp\sqrt{\log(2p/j)},\ \sqrt{\log(1/\delta_0)}\,\|Xu\|_2\right\}.$$

On $\mathcal G_s$, every $u\in B_0(s)$ satisfies $\epsilon^\top Xu\le\sigma\sqrt{5s\log(ep/s)+\log(1/\delta_0)}\,\|Xu\|_2$. Here $\delta_0\in(0,1]$ and all logarithms are natural. These definitions, including the constant in $\mathcal G_s$, are the printed deterministic events of p. 13.

Formalization targets

Exact slow rate on $\mathcal H$

At $\lambda=2\sigma\sqrt{2\log(2p)}+2\sigma\sqrt{2\log(1/\delta_0)}$, Theorem 3(A) states

$$\|f^*-X\hat\beta_1\|_2^2\le\inf_{\beta\in B_0(k)}\bigl[\|f^*-X\beta\|_2^2+2\lambda\|\beta\|_1\bigr]\qquad(\epsilon\in\mathcal H).$$

Slow rate on $\mathcal F$

For $\lambda\ge(8+2\sqrt2)\sigma\sqrt{\log(2p)}$, a positive universal constant $C_A$ gives

$$\|f^*-X\hat\beta_1\|_2^2\le C_A\left[\inf_{\beta\in B_0(k)}\bigl(\|f^*-X\beta\|_2^2+\lambda\|\beta\|_1\bigr)+\sigma^2\log(1/\delta_0)\right]\qquad(\epsilon\in\mathcal F).$$

Fast rate on $\mathcal G_{2k}$

For every $\lambda\ge0$, a positive universal constant $C_B$ gives

$$\|f^*-X\hat\beta_1\|_2^2\le C_B\left[\inf_{\beta\in B_0(k)}\|f^*-X\beta\|_2^2+\sigma^2k\log(ep/k)+\gamma_{2k}^{-2}\lambda^2 k+\sigma^2\log(1/\delta_0)\right]\qquad(\epsilon\in\mathcal G_{2k}).$$

The $k$ multiplying $\gamma_{2k}^{-2}\lambda^2$ distinguishes this rate from the $\ell_2$-penalized estimator's bound. The three claims together, with their separate tuning conditions, are Theorem 3 on p. 16. The milestones follow the displays of its proof in Supplement B.6, pp. 42–43.

What the result provides

Each inequality compares the prediction of any selected minimizer with that of every sparse competitor. The first bound has an exact leading constant and no additive noise term on $\mathcal H$. The second keeps a linear penalty term when $\lambda$ meets a fixed noise-dependent threshold. The third replaces the linear term with a quadratic $\lambda$ term controlled by the sparse minimum singular value. This distinguishes regimes in which coefficient shrinkage changes the error rate. The paper also combines deterministic bounds with event probabilities in subsequent corollaries; those probability statements are separate from this goal.

The paper proves Theorem 3. The formalization task is to verify its model definitions, event interpretation and all three inequalities in Lean, with the same constants and quantifiers. The milestone statements isolate the basic inequality, the $\mathcal H$ bound, the rearranged-coordinate bound, the $\mathcal F$ case split and the sparse $\ell_1$ step. A complete proof would also provide reusable finite-dimensional norm and matrix estimates. This mission does not include the paper's numerical experiments, data-driven model-size selection, the $\ell_2$-penalized estimator, or the event-probability theorem.

Difficulty

The constraint $\|\beta\|_0\le k$ makes the estimator a minimizer over a nonconvex set. A standard unconstrained Lasso argument does not directly supply the paper's bound for every feasible sparse comparator. The slow rates rely on two different noise controls: a coordinatewise bound on $\mathcal H$ and a maximum of a sorted-coordinate term and a prediction-norm term on $\mathcal F$. The fast rate also needs the sparse minimum singular value to relate coefficient error to prediction error. The constants in these steps matter: replacing the exact first tuning equality or dropping the factor $k$ in the fast rate would state a different theorem.

Formalization scope

Lean uses Fin n → ℝ and Fin p → ℝ for vectors and Matrix (Fin n) (Fin p) ℝ for $X$. Norms are explicit finite sums, rather than the function type's default supremum norm. The paper's one-based sorted index $j$ is j.val + 1; the sum using $u^\sharp$ is encoded as a maximum over coordinate permutations, which agrees with the decreasing rearrangement. The events are predicates on realized noise vectors. The Gaussian law explains the model but is not needed in these deterministic statements. The estimator is an argmin predicate, never a chosen minimizer.

The universal constants precede all dimensions and data in the Lean goal. The infima in the three displayed bounds are expressed as inequalities for every $\beta\in B_0(k)$, avoiding the default value of an empty or unbounded real infimum. The standing conditions are $1\le k\le p$, unit-norm columns, $\sigma>0$ and $0<\delta_0\le1$. The first slow-rate branch retains the paper's equality for $\lambda$. The fast branch additionally requires $\gamma_{2k}>0$ or $\lambda=0$: this makes the $\lambda^2/\gamma_{2k}^2$ term meaningful under Lean's total division, which returns zero at a zero denominator. The displayed events use the paper's original $\mathcal G_s$ constant; this mission makes only a deterministic claim on that event.

The sparse domain for $\gamma_{2k}$ is nonempty under these conditions. All square-root radicands and logarithm arguments in the target are in their intended ranges. The formalization must rule out a universal constant that depends on $n$, $p$, $k$, $X$ or $\lambda$, and must apply to every minimizer. Contributions to the shared norm inequalities, rearrangement identity and matrix calculations are useful beyond this theorem.

Selected references

• Rahul Mazumder, Peter Radchenko and Antoine Dedieu, Subset Selection with Shrinkage: Sparse Linear Modeling When the SNR Is Low, Operations Research 71 (2023), arXiv preprint version 4 (2022), arXiv:1708.03288v4. This mission cites the preprint's page and theorem numbering.

Motivation

Community detection asks for a hidden partition of the nodes of a graph from its edges. Its simplest probabilistic benchmark is the two-community stochastic block model (SBM), in which the minimum bisection problem is the maximum a posteriori estimator. That problem is NP-hard, so convex relaxations are used in its place, and the question is when a relaxation still returns the hidden partition exactly. For semidefinite relaxations this question has sharp answers (Abbe, Bandeira, Hall 2016; Bandeira 2018). Del Pia, Khajavirad and Kunisky (arXiv:2006.03213v2) ask the same question for the most common linear programming relaxation of minimum bisection, the metric relaxation. They show that it recovers the planted bisection in very dense graphs when $p-q>1/2$ (their Theorem 6). This mission is their converse in the very dense and dense regimes, Theorem 7: above explicit thresholds the LP fails with high probability.

Setting

The node set is $V=\{1,\dots,n\}$, $n$ even. A bisection is a partition $V=V_1\sqcup V_2$ with $|V_1|=|V_2|=n/2$. The cut vector $\bar x\in\{0,1\}^{\binom n2}$ of $V_1,V_2$ has $\bar x_{ij}=1$ exactly when $i$ and $j$ lie on different sides. For a graph $G$ with adjacency indicators $a_{ij}$, the metric relaxation is

$$\text{(LP-P)}\qquad \min_x \sum_{i<j}a_{ij}x_{ij}\quad\text{s.t.}\quad x_{ij}\le x_{ik}+x_{jk},\quad x_{ij}+x_{ik}+x_{jk}\le2,\quad \sum_{i<j}x_{ij}=\frac{n^2}{4},$$

over $x\in\mathbb R^{\binom n2}$, with the first family over distinct $i,j,k$ with $i<j$ and the second over $i<j<k$. The LP recovers the planted bisection if $\bar x$ is its unique optimal solution.

In the SBM $\mathcal G_{n,p,q}$ a bisection $V_1,V_2$ is first drawn uniformly at random; then each pair on the same side is an edge with probability $p$ and each pair across with probability $q$, independently, with $p>q$. The Erdős–Rényi graph $\mathcal G_{n,p}$ has every pair an edge with probability $p$. The dense scaling (20) is $p=\alpha n^{-\omega}$, $q=\beta n^{-\omega}$ with $\alpha>\beta>0$, $0\le\omega<1$; $\omega=0$ is the very dense regime. An event holds with high probability (w.h.p.) if its probability tends to $1$ as $n\to\infty$.

For a graph $G$, $\rho_G(i,j)$ is the shortest-path distance ($+\infty$ across components), $\rho_{\max}(G)=\max_{i,j}\rho_G(i,j)$ is the diameter, and $\rho_{\mathrm{avg}}(G)=\frac2{n^2}\sum_{i<j}\rho_G(i,j)$ is the average distance. $E$ is the edge set of $G$, $E_0$ the set of edges across the planted bisection.

Formalization targets

Goal: Theorem 7 (pp. 15–16)

Let $p=\alpha n^{-\omega}$, $q=\beta n^{-\omega}$ with $\alpha>\beta>0$, $\omega\in[0,1)$, and $\alpha,\beta<1$ if $\omega=0$. If one of

1. $\omega=0$ and $\beta>\max\big\{\tfrac{3-\alpha-\sqrt{(3-\alpha)^2-4\alpha}}2,\ 2\alpha-1\big\}$ (22),
2. $\omega\in(0,1)$, $\tfrac1{1-\omega}\notin\mathbb N$ and $\beta>\alpha/(2\lceil\tfrac1{1-\omega}\rceil-1)$ (23),
3. $\omega=\tfrac12$ and $\beta>\max\big\{\tfrac{1-2e^{-\alpha^2}}{2-e^{-\alpha^2}},\tfrac1{3+2e^{-\alpha^2}}\big\}\alpha$ (24),
4. $\omega\in(0,1)$, $\tfrac1{1-\omega}\in\mathbb N\setminus\{2\}$ and $\beta>\alpha/\big(\tfrac2{1-\omega}-1+2e^{-\alpha^{1/(1-\omega)}}\big)$ (25)

holds, then

$$\lim_{n\to\infty}\mathbb P_{(V_1,G)\sim\mathcal G_{n,p,q}}\big[\text{(LP-P) does not recover }V_1,V_2\big]=1.$$

Milestones

1. (26), p. 16: for $p,q=\Omega(\log n/n)$ with $\lim q/p\in(0,1]$, the ratio $|E_0|/|E|$ lies in $(1\pm\epsilon)\,q/(p+q)$ w.h.p.
2. Proposition 11, p. 28: a coupling of $\mathcal G_{n,q}$, $\mathcal G_{n,q,p}$ and $\mathcal G_{n,p}$ in which the three graphs are nested.
3. Proposition 12, p. 28: w.h.p. $\rho_{\max}(\mathcal G_{n,\alpha n^{-\omega}})=1+\lfloor\frac1{1-\omega}\rfloor$.
4. Proposition 14, p. 29 (Shimizu): w.h.p. $\rho_{\mathrm{avg}}(\mathcal G_{n,\alpha n^{-\omega}})\in((1-\epsilon)\mu,(1+\epsilon)\mu)$, where $\mu=\lceil\frac1{1-\omega}\rceil+\mathbf 1\{\frac1{1-\omega}\in\mathbb N\}e^{-\alpha^{1/(1-\omega)}}$.
5. Propositions 16, 17, 18, pp. 29–30: the diameter of the very dense and dense SBM, and lower bounds on its average distance, in the three cases $\omega=0$, $\frac1{1-\omega}\notin\mathbb N$ and $\frac1{1-\omega}\in\mathbb N$.

Significance

Theorem 6 and Theorem 7 together bracket the success region of the metric relaxation in the very dense regime: recovery for $p-q>1/2$, failure above the curve (22). In the dense regime, Theorem 7 gives explicit linear thresholds $\beta>c(\omega,\alpha)\,\alpha$ above which the LP fails. The proof reduces failure to a deterministic distance criterion (Theorem 5, posed in mission 4 of this series) and turns asymptotic distance distributions of random graphs into statements about an LP.

The results are proved in the paper, partly by citing Bollobás's diameter theorems and Shimizu's average-distance theorem; none of them has a machine-checked proof. Formalizing the mission yields, besides Theorem 7, the diameter and average distance of dense Erdős–Rényi graphs (Propositions 12 and 14) and the monotone coupling between Erdős–Rényi graphs and the SBM (Proposition 11), each of which is usable beyond this paper. The coupling and (26) are also the inputs of the logarithmic-degree result (Theorem 8, mission 7).

Difficulty

The deterministic half is short: once $|E_0|/|E|$, $\rho_{\max}$ and $\rho_{\mathrm{avg}}$ are pinned down, the case computations (28)–(29) reduce to inequalities between explicit expressions in $\alpha$, $\beta$ and $\omega$. The difficulty is the random-graph input. The diameter of $\mathcal G_{n,p}$ for $p=\alpha n^{-\omega}$ needs the second-moment analysis of the number of pairs at distance greater than $d$ (Bollobás, Corollaries 10.11–10.12), and the average distance needs the finer limit law for path counts at the critical exponent $\frac1{1-\omega}\in\mathbb N$, where the constant $e^{-\alpha^{1/(1-\omega)}}$ appears. A first-moment argument gives only one side of each estimate. Concentration of $|E|$ and $|E_0|$ (26) is a Hoeffding bound, but it must hold uniformly over the random planted bisection.

Formalization scope

Nodes are Fin n and graphs SimpleGraph (Fin n). A bisection is its side $V_1$ with $2|V_1|=n$. The LP variable is a symmetric, zero-diagonal array Fin n → Fin n → ℝ, with no box constraints, so uniqueness is uniqueness over $\mathbb R^{\binom n2}$. Probabilities are finite sums over all graphs (and all bisections for the SBM). Edge probabilities are clamped into $[0,1]$, which affects only finitely many $n$. SBM limits run over even $n=2m$. Distances are in ℕ∞ and $\rho_{\mathrm{avg}}$ in $[0,\infty]$, so disconnected samples have infinite diameter and average distance; no real truncation is used.

Disclosed choices:

• Theorem 7 adds $\alpha>\beta$, the SBM's standing assumption $p>q$ (§4, p. 13), also assumed by Proposition 18 and (26).
• (26) is posed for $p=\alpha s(n)$, $q=\beta s(n)$ with $s(n)\ge c\log n/n$ and $\alpha s(n)\le1$ eventually. Then $q/p=\beta/\alpha$, which avoids the printed "$\lim p/q\in(0,1]$", a slip for $q/p$.
• Proposition 11 is posed as printed, with middle law $\mathcal G_{n,q,p}$ (within $q$, across $p$).

Two encodings would make the statements trivial, and both are excluded. Unnormalized LP variables would make uniqueness false. Reading $\rho$ in $\mathbb R$ via toReal would make the upper bounds hold for disconnected graphs.

The deterministic distance criterion (Theorem 5) is posed in mission 4 and is not restated. Contributions are welcome on the coupling, Hoeffding-type concentration of edge counts, and the Erdős–Rényi distance asymptotics. These are reusable for any finite random-graph development.

Selected references

• A. Del Pia, A. Khajavirad, D. Kunisky, Linear Programming and Community Detection, Mathematics of Operations Research, 2023; arXiv:2006.03213v2. https://arxiv.org/abs/2006.03213
• E. Abbe, A. S. Bandeira, G. Hall, Exact recovery in the stochastic block model, IEEE Trans. Inf. Theory 62 (2016) 471–487. https://arxiv.org/abs/1405.3267
• A. S. Bandeira, Random Laplacian matrices and convex relaxations, Found. Comput. Math. 18 (2018) 345–379. https://arxiv.org/abs/1504.03987
• B. Bollobás, Random Graphs, 2nd ed., Cambridge Studies in Advanced Mathematics 73, Cambridge University Press, 2001. https://doi.org/10.1017/CBO9780511814068
• N. Shimizu, The average distance of dense homogeneous random graphs, Mathematical Engineering Technical Report, Department of Mathematical Informatics, The University of Tokyo, November 2017 (Theorem 1; reference [38] of the paper). https://www.keisu.t.u-tokyo.ac.jp/research/techrep/

Motivation

The stochastic block model (SBM) is the standard benchmark for community detection: a random graph whose vertices are split into hidden communities, with denser connections inside a community than across. For two equal communities, the best possible estimator of the hidden partition is the minimum bisection problem, which is NP-hard in the worst case. Its tractable relaxations are therefore compared by asking for which edge densities they still recover the hidden partition exactly.

For semidefinite programming the answer is complete in the logarithmic-degree regime: Abbe, Bandeira and Hall (arXiv:1405.3267) located the information-theoretic threshold $\sqrt\alpha-\sqrt\beta=\sqrt2$, and the SDP relaxation was shown to reach it by Hajek, Wu and Xu (arXiv:1412.6156) and by Bandeira (arXiv:1504.03987). Linear programming relaxations are cheaper and widely used in combinatorial optimization, but their behaviour on the SBM was not known. Del Pia, Khajavirad and Kunisky (arXiv:2006.03213, Mathematics of Operations Research, 2023) study the most common one, the metric relaxation. This mission formalizes their result for the logarithmic-degree regime (Theorem 8): there the LP relaxation fails to recover the hidden partition with high probability, at every choice of the parameters.

Setting

Let $V=\{1,\dots,n\}$ with $n$ even. A bisection is a partition $V=V_1\sqcup V_2$ with $|V_1|=|V_2|=n/2$; its cost in a graph $G$ is the number of edges between $V_1$ and $V_2$. Given a fixed planted bisection $V_1,V_2$, an optimization problem recovers it if its unique optimal solution corresponds to $V_1,V_2$.

The cut vector $\bar x\in\{0,1\}^{\binom n2}$ of $V_1,V_2$ has $\bar x_{ij}=1$ exactly when $i,j$ lie on different sides. With $a_{ij}=1$ for edges and $0$ otherwise, the metric relaxation is

$$\text{(LP-P)}\quad \min_x \sum_{i<j}a_{ij}x_{ij}\ \ \text{s.t.}\ \ x_{ij}\le x_{ik}+x_{jk},\ \ x_{ij}+x_{ik}+x_{jk}\le2,\ \ \sum_{i<j}x_{ij}=\frac{n^2}{4},$$

the first family over distinct $i,j,k$ and the second over $i<j<k$, with $x_{ji}:=x_{ij}$. Every bisection's cut vector is feasible.

The distance $\rho_G(i,j)$ is the length of a shortest $i$–$j$ path ($+\infty$ across components). The diameter is $\rho_{\max}(G)=\max_{i,j}\rho_G(i,j)$ and the average distance is $\rho_{\mathrm{avg}}(G)=\frac{2}{n^2}\sum_{i<j}\rho_G(i,j)$.

The Erdős–Rényi model $\mathcal G_{n,p}$ draws each edge independently with probability $p$. The SBM $\mathcal G_{n,p,q}$ chooses a bisection $V_1,V_2$ uniformly at random, then draws each pair inside a side with probability $p$ and each pair across with probability $q$, independently, where $p>q$. The logarithmic-degree regime (21) is

$$p=\alpha\frac{\log n}{n},\qquad q=\beta\frac{\log n}{n},\qquad \alpha>\beta>0 .$$

An event $A_n$ holds with high probability if $\mathbb P[A_n]\to1$ as $n\to\infty$.

Formalization targets

Goal: Theorem 8 (p. 18)

$$\alpha>\beta>0\ \Longrightarrow\ \lim_{n\to\infty}\mathbb P_{\mathcal G_{n,p,q}}\big[\text{(LP-P) does not recover }V_1,V_2\big]=1 .$$

Milestones

1. The threshold of [2] (p. 14, strict cases): if $\sqrt\alpha-\sqrt\beta>\sqrt2$, the minimum bisection problem recovers $V_1,V_2$ with high probability; if $\sqrt\alpha-\sqrt\beta<\sqrt2$, it does not.
2. Proposition 13 (p. 29): for $\alpha>1$ and $G\sim\mathcal G_{n,\alpha\log n/n}$, $\rho_{\max}(G)\in\big((1-\epsilon)\frac{\log n}{\log\log n},(1+\epsilon)\frac{\log n}{\log\log n}\big)$ with high probability.
3. Proposition 15 (p. 29, Theorem 1 of Chung–Lu): for $\alpha>1$, $\rho_{\mathrm{avg}}(G)\in\big((1-\epsilon)\frac{\log n}{\log pn},(1+\epsilon)\frac{\log n}{\log pn}\big)$ with high probability.
4. Proposition 19 (p. 30): for $\alpha>\beta>0$ with $\frac{\alpha+\beta}{2}>1$ and $G\sim\mathcal G_{n,p,q}$,

$$(1-\epsilon)\frac{\log n}{\log\log n}\le\rho_{\mathrm{avg}}(G)\le\rho_{\max}(G)\le(1+\epsilon)\frac{\log n}{\log\log n}$$

with high probability.

Two results the proof of Theorem 8 uses are posed in sibling missions of this series and are not restated here: Theorem 5 (a distance-based non-recovery criterion for (LP-P), mission 4) and the coupling Proposition 11 together with the crossing-edge count (26) (mission 6).

Significance

The result. Theorem 8 separates linear from semidefinite programming on a natural statistical problem. In the logarithmic regime the SDP relaxation recovers the planted bisection whenever any method can, while the metric LP fails with high probability for all $\alpha>\beta>0$, including parameters far above the information-theoretic threshold. The paper's Theorem 6 shows that in the very dense regime (constant $p,q$) the LP does succeed when $p-q>1/2$; Theorem 8 shows that at logarithmic degree no such window exists.

Formalizing it. The theorem is proved in the paper, modulo results cited from the random-graph literature. Nothing in this mission is machine-checked yet. Formalization adds a precise account of what the cited distance asymptotics assert; Proposition 19's upper bound is justified in the paper only by reference to "a standard result on the diameter of the SBM" obtained by adapting an argument of Abbe's survey, so a complete proof of it is new work. Propositions 13 and 15 are classical facts about Erdős–Rényi graphs that have no formal proof in any library known to the curators, and are reusable well beyond community detection.

Difficulty

The LP side of the argument is deterministic and finite. The difficulty is probabilistic. The distance results require tight control of breadth-first neighbourhood growth in sparse random graphs near the connectivity threshold, where the average degree is only logarithmic, with error terms small enough to pin the diameter to a $(1\pm\epsilon)$ window. A first-moment estimate of path counts gives only one side of each bound. In the SBM the two edge probabilities make neighbourhood growth inhomogeneous, so the Erdős–Rényi results do not transfer verbatim. The threshold of [2] is a separate sharp large-deviation statement, at the level of individual vertices' in- and out-degrees.

Formalization scope

Vertices are Fin n (0-based); graphs are SimpleGraph (Fin n). A bisection is recorded by its side $V_1$ with $2|V_1|=n$. The LP variable is a symmetric, zero-diagonal array $x:V\times V\to\mathbb R$, which is a point of $\mathbb R^{\binom n2}$; no box constraints are added. LP recovery means that the planted cut vector is the unique optimal solution; minimum-bisection recovery means that every bisection of cost at most the planted one is the planted unordered partition. Distances are in $\mathbb N\cup\{\infty\}$ and the average distance in $[0,\infty]$, so a disconnected sample has infinite diameter. The random-graph laws are finite sums over all graphs; the SBM averages over all bisections. Edge probabilities are clamped into $[0,1]$, which matters only for the finitely many $n$ with $\alpha\log n/n>1$. "With high probability" is a limit of probabilities equal to $1$; for the SBM the limit runs along $n=2m$. Logarithms are natural.

Disclosed choices relative to the printed statements: Theorem 8 prints only $\alpha,\beta>0$, and $\alpha>\beta$ is added as the SBM's standing assumption $p>q$ (p. 13) and that of (21). The threshold of [2] is printed as an "if and only if"; only the two strict implications are posed, and the boundary $\sqrt\alpha-\sqrt\beta=\sqrt2$ is left out.

The statements cannot be satisfied vacuously: the laws are genuine probability distributions for every $n$, the events compare extended-valued distances without truncation, and recovery requires uniqueness over all real feasible points of (LP-P). An encoding with an empty or degenerate feasible set, or with distances truncated to finite reals, would change the theorems and is excluded.

A complete development needs: Erdős–Rényi and SBM laws, breadth-first exploration bounds for sparse random graphs, the coupling of the SBM between two Erdős–Rényi graphs (mission 6), the LP non-recovery criterion (mission 4), and the information-theoretic threshold of [2]. Contributions on the random-graph distance asymptotics are reusable on their own and especially welcome.

Selected references

• A. Del Pia, A. Khajavirad, D. Kunisky, Linear Programming and Community Detection, Mathematics of Operations Research, 2023. https://arxiv.org/abs/2006.03213 (v2 is the cited version)
• E. Abbe, A. S. Bandeira, G. Hall, Exact recovery in the stochastic block model, IEEE Transactions on Information Theory 62:471–487, 2016. https://arxiv.org/abs/1405.3267
• E. Abbe, Community detection and stochastic block models: recent developments, Journal of Machine Learning Research 18:1–86, 2018. https://arxiv.org/abs/1703.10146
• F. Chung, L. Lu, The diameter of sparse random graphs, Advances in Applied Mathematics 26(4):257–279, 2001. https://doi.org/10.1006/aama.2001.0720
• F. Chung, L. Lu, The average distances in random graphs with given expected degrees, PNAS 99(25):15879–15882, 2002. https://doi.org/10.1073/pnas.252631999
• B. Hajek, Y. Wu, J. Xu, Achieving exact cluster recovery threshold via semidefinite programming, IEEE Transactions on Information Theory 62(5):2788–2797, 2016. https://arxiv.org/abs/1412.6156
• A. S. Bandeira, Random Laplacian matrices and convex relaxations, Foundations of Computational Mathematics 18(2):345–379, 2018. https://arxiv.org/abs/1504.03987

Motivation

The stochastic block model (SBM), introduced by Holland, Laskey and Leinhardt (1983), is the standard random model for networks with community structure, and the basic benchmark for community-detection algorithms (Abbe 2018). In its two-community form the nodes are split into two equal halves, edges inside a half appear with probability $p$, and edges across with probability $q<p$. The task of exact recovery is to identify the hidden halves from the graph alone.

The maximum a posteriori estimator for this model is the minimum bisection problem (find a balanced cut with the fewest crossing edges), which is NP-hard in general. Abbe, Bandeira and Hall (2016) determined when it recovers the planted bisection, and showed that a semidefinite relaxation is as good as the integer program. Del Pia, Khajavirad and Kunisky (arXiv:2006.03213, Mathematics of Operations Research 2023) ask the same question for the cheapest standard relaxation: the metric linear programming relaxation, defined by triangle inequalities. This mission is their positive result in the very dense regime.

Setting

Let $V=\{1,\dots,n\}$ with $n$ even. A bisection is a partition $V=V_1\cup V_2$ with $|V_1|=|V_2|=n/2$. For a graph $G=(V,E)$ let $a_{ij}=1$ if $(i,j)\in E$ and $0$ otherwise. The metric relaxation (LP-P) is

$$\min_{x\in\mathbb R^{\binom n2}}\ \sum_{i<j}a_{ij}x_{ij}\quad\text{s.t.}\quad x_{ij}\le x_{ik}+x_{jk},\quad x_{ij}+x_{ik}+x_{jk}\le 2,\quad \sum_{i<j}x_{ij}=\frac{n^2}{4},$$

the first constraint for all distinct $i,j,k$ with $i<j$, the second for all $i<j<k$, and $x_{ji}:=x_{ij}$. The cut vector $\bar x$ of a bisection has $\bar x_{ij}=0$ for $i,j$ on the same side and $\bar x_{ij}=1$ otherwise. (LP-P) recovers the planted bisection when $\bar x$ is its unique optimal solution.

In the Erdős–Rényi model $\mathcal G_{n,p}$ every pair of nodes is an edge independently with probability $p$. In the SBM $\mathcal G_{n,p,q}$ a bisection $V_1,V_2$ is first chosen uniformly at random; then pairs inside $V_1$ or inside $V_2$ are edges with probability $p$, pairs between them with probability $q$, all independently. $\mathcal G_{n,0,q}$ is the random bipartite graph across a random bisection. An event occurs with high probability (w.h.p.) if its probability tends to $1$ as $n\to\infty$. The graph is very dense when $p$ and $q$ are constants.

For a finite graph $G=(V,E)$ and $b\in\mathbb Z_{\ge0}^V$, a $b$-factor (or $f$-factor) is a set $F\subseteq E$ with exactly $b_v$ edges of $F$ at each node $v$; $N(U,U')$ counts edges with one endpoint in $U$ and one in $U'$; $d_{\min}$, $d_{\max}$ are the minimum and maximum degrees; and the node connectivity $\kappa(G)$ is the minimum number of nodes whose deletion disconnects $G$ (the number of nodes, for a complete graph).

Formalization targets

Goal: Theorem 6 (p. 15)

For constants $0<q<p<1$,

$$p-q>\tfrac12\ \Longrightarrow\ \mathbb P_{G\sim\mathcal G_{n,p,q}}\big[\text{(LP-P) recovers the planted bisection}\big]\xrightarrow[n\to\infty]{}1 .$$

Milestones

1. Proposition 6 (p. 20): for $G\sim\mathcal G_{2m,0,q}$ there is $C>0$ with $d_{\max}\le qm+C\sqrt{m\log m}$ w.h.p.
2. Proposition 5 (p. 20; Schrijver, Cor. 21.4a): a bipartite graph has a $b$-factor iff $N(U,U)\ge b(U)-\frac12 b(V)$ for every $U\subseteq V$.
3. Proposition 3 (p. 14): there is $C_{\mathrm{reg},2}>0$ such that for every $q\in(0,1)$, w.h.p. $G\sim\mathcal G_{n,0,q}$ is a subgraph of a regular bipartite graph with the same bipartition, of degree $d_{\mathrm{reg}}=\frac{qn}2+C_{\mathrm{reg},2}\sqrt{\frac n2\log\frac n2}$ (rounded down).
4. Proposition 8 (p. 24): for $G\sim\mathcal G_{n,p}$ there is $C>0$ with $d_{\min}\ge pn-C\sqrt{n\log n}$ w.h.p.
5. Proposition 9 (p. 24; Bollobás–Thomason): for $G\sim\mathcal G_{n,p}$, $\kappa(G)=d_{\min}$ w.h.p.
6. Proposition 7 (p. 24; Tutte's $f$-factor theorem).
7. Proposition 4 (p. 14): there is $C_{\mathrm{reg},1}>0$ such that for every $p\in(0,1)$, w.h.p. $G\sim\mathcal G_{n,p}$ contains a spanning regular subgraph of degree $d_{\mathrm{reg}}=pn-C_{\mathrm{reg},1}\sqrt{n\log n}$ (rounded up to an even integer).

The deterministic recovery criterion that the goal also depends on, Theorem 4 of the paper (regular sandwiching with $d_{\mathrm{in}}-d_{\mathrm{out}}\ge n/4$), is the goal of mission 3 of this series and is not restated here.

Significance

The result. Theorem 6 is the only positive recovery guarantee for the metric LP in the random setting of the paper. Together with the failure results of Theorems 7 and 8 (missions 6 and 7), it locates the LP strictly between trivial and information-theoretically optimal: it recovers in a region of constant $p,q$, but not up to the threshold $p>q$ that the minimum bisection problem and its SDP relaxation reach. Propositions 3 and 4, that dense random graphs sit inside, and contain, regular graphs of nearly their average degree, are of independent interest in random graph theory, as the authors note.

Formalizing it. The result is proved in the paper; none of it is machine-checked. The mission also requires three classical theorems that are not in Mathlib: the $b$-factor criterion for bipartite graphs, Tutte's $f$-factor theorem (Mathlib has only the perfect-matching case $f\equiv 1$), and the Bollobás–Thomason theorem $\kappa=d_{\min}$ for random graphs, together with degree concentration for $\mathcal G_{n,p}$ and the bipartite SBM. Each is reusable well beyond this paper.

Difficulty

The obvious argument for recovery is to exhibit a dual certificate for (LP-P), which needs regularity of the communities and of the cross edges; a random graph is not regular. The paper bridges the gap by sandwiching the random graph between regular graphs of nearly equal degree, and that step is where the difficulty lies: the existence of a regular sub- or supergraph is a global combinatorial property, characterized by factor theorems with exponentially many conditions, each of which must hold simultaneously with high probability. Degree concentration alone, the first idea, controls only the singleton conditions. Tutte's $f$-factor theorem and the bipartite $b$-factor criterion are themselves substantial combinatorial theorems, and the connectivity statement of Bollobás and Thomason is a deep result on random graphs.

Formalization scope

Nodes are Fin n (0-based). A bisection is a Finset $V_1$ with $2|V_1|=n$. Points of $\mathbb R^{\binom n2}$ are symmetric arrays with zero diagonal; (LP-P) has no box constraints $0\le x\le1$ (they are implied by the constraints and adding them would change the LP). Recovery means: $\bar x$ is optimal and every optimal solution equals $\bar x$.

The random-graph laws are finite: a probability is a weighted sum over all graphs on Fin n, with independent edge weights, and for the SBM an average over all bisections; the event may depend on the drawn bisection. Edge probabilities are clamped into $[0,1]$, which is the identity on the parameters used here. "With high probability" is Tendsto … atTop (𝓝 1), along $n=2m$ for the SBM. The standing assumption $p>q$ is not built into the law, so that $\mathcal G_{n,0,q}$ is the case $p=0$.

Disclosed readings: the printed $d_{\mathrm{reg}}$ of Propositions 3 and 4 is not an integer; Proposition 3 is posed with degree $\lfloor d_{\mathrm{reg}}\rfloor$ and Proposition 4 with $2\lceil d_{\mathrm{reg}}/2\rceil$, the least even integer $\ge d_{\mathrm{reg}}$ (the proof assumes $d_{\mathrm{reg}}$ even). $\kappa(K_n)=n$ as on p. 24. Quantifier order follows each page: in Propositions 3 and 4 the constant precedes the probability parameter, in Propositions 6 and 8 it follows it; no constant depends on $n$.

A statement in which "with high probability" is replaced by a positive probability or an eventual bound, in which the bisection is fixed rather than random, or in which the regular degree is compared with an irrational real (an empty event) is not this mission's target.

Infrastructure needed: the finite random-graph laws, Hoeffding-type concentration over them, the two factor theorems, and node connectivity. Proofs of any milestone, and of the classical results as general graph theory, are welcome.

Selected references

• A. Del Pia, A. Khajavirad, D. Kunisky, Linear Programming and Community Detection, Mathematics of Operations Research, 2023; arXiv:2006.03213v2. https://arxiv.org/abs/2006.03213
• E. Abbe, A. S. Bandeira, G. Hall, Exact Recovery in the Stochastic Block Model, IEEE Transactions on Information Theory 62(1), 2016. https://arxiv.org/abs/1405.3267
• E. Abbe, Community Detection and Stochastic Block Models: Recent Developments, Journal of Machine Learning Research 18, 2018. https://arxiv.org/abs/1703.10146
• P. W. Holland, K. B. Laskey, S. Leinhardt, Stochastic Blockmodels: First Steps, Social Networks 5(2), 1983. https://doi.org/10.1016/0378-8733(83)90021-7
• W. T. Tutte, The Factors of Graphs, Canadian Journal of Mathematics 4, 1952. https://doi.org/10.4153/CJM-1952-028-2
• A. Schrijver, Combinatorial Optimization: Polyhedra and Efficiency, Springer, 2003 (Corollary 21.4a).
• B. Bollobás, A. Thomason, Random Graphs of Small Order, in Random Graphs '83, North-Holland Mathematics Studies 118, 1985 (Theorem 1).
• A. Frieze, M. Karoński, Introduction to Random Graphs, Cambridge University Press, 2016 (Chapter 3). https://doi.org/10.1017/CBO9781316339831

Motivation

Policy evaluation asks for the value of a fixed decision rule in a Markov decision process whose transition probabilities are unknown. It is the inner loop of policy iteration, the subroutine behind actor-critic methods, and the question an operator faces before deploying a policy in an inventory, queueing or routing system that can only be simulated. The simplest estimator is the plug-in (model-based) one: sample transitions from a simulator, build the empirical transition kernel, and compute the value of the policy in the resulting empirical MDP.

How many samples this estimator needs has a short history. Azar, Munos and Kappen (Machine Learning, 2013) introduced the total-variance argument that yields the $(1-\gamma)^{-3}$ dependence for planning with a generative model. Agarwal, Kakade and Yang (COLT 2020) proved minimax-optimal guarantees for model-based planning, but only when the sample size per state-action pair exceeds roughly $(1-\gamma)^{-2}$. Pananjady and Wainwright (IEEE Trans. Inf. Theory, 2021) gave instance-dependent policy-evaluation bounds and a minimax lower bound, again under a sample-size requirement of order $(1-\gamma)^{-2}$. Li, Wei, Chi and Chen (arXiv:2005.12900v8; Operations Research, 2024) removed this barrier: their Theorem 3 shows that the plug-in estimate is accurate across the whole accuracy range once the sample size exceeds $(1-\gamma)^{-1}$ up to logarithmic factors. This mission formalizes that theorem and the lemmas its proof rests on.

Setting

A discounted Markov decision process consists of a finite state set $\mathcal S$, a finite action set $\mathcal A$, a transition kernel $P$ (for each pair $(s,a)$, $P(\cdot\mid s,a)$ is a probability vector over $\mathcal S$), a reward $r:\mathcal S\times\mathcal A\to[0,1]$ and a discount factor $0<\gamma<1$. A deterministic policy is a map $\pi:\mathcal S\to\mathcal A$. Its value function is

$$V^\pi(s)=\mathbb E\Big[\sum_{t=0}^\infty\gamma^t r(s^t,a^t)\,\Big|\,s^0=s\Big],\qquad a^t=\pi(s^t),\quad s^{t+1}\sim P(\cdot\mid s^t,a^t).$$

Write $P_\pi(s,s')=P(s'\mid s,\pi(s))$ for the state transition matrix of $\pi$ and $r_\pi(s)=r(s,\pi(s))$ for its reward vector, so that $V^\pi=(I-\gamma P_\pi)^{-1}r_\pi$. For a vector $V\in\mathbb R^{\mathcal S}$, $\mathrm{Var}_{P_\pi}(V)(s)=\sum_{s'}P_\pi(s,s')V(s')^2-\big(\sum_{s'}P_\pi(s,s')V(s')\big)^2$ is the one-step variance of $V$ under the chain.

The generative model returns, for every pair $(s,a)$, $N$ independent next states $s^1_{s,a},\dots,s^N_{s,a}\sim P(\cdot\mid s,a)$. The empirical kernel is $\widehat P(s'\mid s,a)=\frac1N\sum_{i=1}^N\mathbb 1\{s^i_{s,a}=s'\}$, and for a policy $\pi$ chosen independently of the data the plug-in estimate $\widehat V^\pi$ is the value function of $\pi$ in the empirical MDP $(\mathcal S,\mathcal A,\widehat P,r,\gamma)$, that is, $\widehat V^\pi=(I-\gamma\widehat P_\pi)^{-1}r_\pi$. Norms $\|\cdot\|_\infty$ are maxima of absolute entries; $e=\exp(1)$ and $\log$ is natural.

Formalization targets

Goal: Theorem 3 (p. 9)

There is a universal constant $c_0>0$ such that for every MDP as above, every fixed policy $\pi$, every $0<\delta<1$ and every $0<\varepsilon\le\frac1{1-\gamma}$,

$$N\ge c_0\,\frac{\log\big(|\mathcal S|\log\frac{e}{1-\gamma}/\delta\big)}{(1-\gamma)^3\varepsilon^2} \quad\Longrightarrow\quad \mathbb P\Big(\max_{s}\big|\widehat V^\pi(s)-V^\pi(s)\big|\le\varepsilon\Big)\ge1-\delta .$$

The constant $c_0$ is not specified, so the goal survives any later improvement of the constants.

Milestones

In attack order: Lemma 10 (elementary facts on $(I-\gamma P_\pi)^{-1}$, p. 23); the matrix form (27) of $V^\pi$ (p. 12); Lemma 11, $\|(I-\gamma P_\pi)^{-1}\sqrt{\mathrm{Var}_{P_\pi}(V)}\|_\infty\le\frac{4}{\gamma\sqrt{1-\gamma}}\|V\|_\infty$ for $V=(I-\gamma P_\pi)^{-1}r_\pi$ with $r_\pi\ge0$ (p. 24); the total-variance bound (70) of Azar et al. (p. 24); the deterministic instance-dependent bound (80) under a Bernstein-type condition (pp. 25–26); Lemma 2, the worst-case bound $\|\widehat V^\pi-V^\pi\|_\infty\le\frac{6}{1-\gamma}\sqrt{\frac{\beta_1}{N(1-\gamma)}}$ under the same condition (p. 15); the high-probability Bernstein bound (82) for a fixed policy (p. 27); and Lemma 1, the explicit-constant version of the goal with an instance-dependent refinement (p. 13):

$$\big\|\widehat V^\pi-V^\pi\big\|_\infty\le 4\gamma\sqrt{\tfrac{2L}{N}}\Big\|(I-\gamma P_\pi)^{-1}\sqrt{\mathrm{Var}_{P_\pi}[V^\pi]}\Big\|_\infty+\tfrac{2\gamma L}{(1-\gamma)N}\|V^\pi\|_\infty\le 6\sqrt{\tfrac{2L}{N(1-\gamma)^3}},$$

with $L=\log\big(4|\mathcal S|\log\frac{e}{1-\gamma}/\delta\big)$ and $N\ge\frac{32e^2}{1-\gamma}L$.

Significance

The theorem says that the plug-in estimate of a fixed policy's value beats a random guess as soon as $N$ exceeds $\frac1{1-\gamma}$ up to logarithmic factors, and that its sample size matches the minimax lower bound of Pananjady and Wainwright (2019, Theorem 2(b)) up to a $\log\log\frac1{1-\gamma}$ factor over the full range $\varepsilon\in(0,\frac1{1-\gamma}]$. Lemma 2, which does not require the policy to be independent of the data, is the step the paper reuses to analyze the data-dependent optimal policy of the empirical MDP (Theorems 1 and 2, posed in sibling missions of this series).

The result is proved in the paper; none of it is formalized. The mission produces a machine-checked account of the variance-aware analysis of tabular MDPs: the resolvent calculus of Lemma 10, the total-variance bounds (70) and Lemma 11, which recur across the reinforcement-learning sample-complexity literature, and a high-order expansion argument that turns a Bernstein-type condition into an error bound. A formal proof of (70), which the paper quotes without proof, would itself be a reusable result.

Difficulty

The obvious argument writes $\widehat V^\pi-V^\pi=\gamma(I-\gamma\widehat P_\pi)^{-1}(\widehat P_\pi-P_\pi)V^\pi$ and bounds the two factors separately. The resolvent of the empirical chain is correlated with the deviation $(\widehat P_\pi-P_\pi)V^\pi$, and bounding $(I-\gamma\widehat P_\pi)^{-1}$ crudely by its row sums $\frac1{1-\gamma}$ loses a factor that forces $N\gtrsim(1-\gamma)^{-2}$; this is exactly the barrier in earlier work. Removing it requires controlling a whole sequence of auxiliary vectors $V^{(l)}$, each defined through the variance of the previous one, up to a logarithmic depth, and showing that their norms do not blow up (Lemma 11). The Bernstein step must also use the variance, not the range, of $V^{(l)}$; a Hoeffding bound gives the wrong power of $1-\gamma$.

Formalization scope

States and actions are finite types; the kernel is P : S → A → S → ℝ with P s a s' $=P(s'\mid s,a)$, a probability vector for each (s, a) (the published IsTransitionKernel). The standing setting is the predicate IsDiscountedMDP P r γ: a kernel, $r(s,a)\in[0,1]$, $0<\gamma<1$, and nonempty state and action sets ($\mathcal S=\{1,\dots,|\mathcal S|\}$, $\mathcal A=\{1,\dots,|\mathcal A|\}$, p. 5). Policies are deterministic maps S → A; the value function is the published series PolicyValue of the induced point-mass policy. Vector norms are Mathlib's sup norm on finite function types, matching $\|\cdot\|_\infty$; vector inequalities and square roots are entrywise.

The data set is the finite type of arrays of $N$ next states per pair, its law is the product of the kernel probabilities, and $\mathbb P$ of an event is a finite sum. "With probability at least $1-\delta$, $E$" is stated as $\mathbb P(\text{not }E)\le\delta$. The goal assumes $N>0$, the standing assumption of the empirical kernel (3), which is implied by the sample-size condition since $\mathcal S$ is nonempty. Index ranges "$0\le l\le\log\frac{e}{1-\gamma}$" range over the integers in that interval. The deterministic milestones (80) and Lemma 2 are stated for an arbitrary transition kernel $\widehat P$, which is what their proofs use.

Three formalizations would trivialize the goal and are ruled out: computing $\widehat V^\pi$ from the true kernel $P$ instead of the empirical one; letting $\pi$ be chosen after the data are seen; and letting $c_0$ depend on $\mathcal S$, $\mathcal A$, $\gamma$, $P$, $r$ or $\pi$ (the existential over $c_0$ precedes all of them).

A complete development needs: the matrix form of the value function, Neumann series and nonnegativity of $(I-\gamma P_\pi)^{-1}$; variance identities for finite distributions; a Bernstein inequality for i.i.d. bounded categorical samples with a union bound over states and indices; and the algebra of the recursive expansion. The resolvent and total-variance lemmas are reusable for any tabular discounted MDP. Proofs of individual milestones are welcome independently; (70) is a standalone classical result.

Selected references

• G. Li, Y. Wei, Y. Chi, Y. Chen, Breaking the Sample Size Barrier in Model-Based Reinforcement Learning with a Generative Model, Operations Research, 2024; arXiv:2005.12900v8, 2023. https://arxiv.org/abs/2005.12900
• M. G. Azar, R. Munos, H. J. Kappen, Minimax PAC bounds on the sample complexity of reinforcement learning with a generative model, Machine Learning 91(3), 2013. https://doi.org/10.1007/s10994-013-5368-1
• A. Agarwal, S. Kakade, L. F. Yang, Model-Based Reinforcement Learning with a Generative Model is Minimax Optimal, COLT 2020. https://arxiv.org/abs/1906.03804
• A. Pananjady, M. J. Wainwright, Instance-Dependent ℓ∞-Bounds for Policy Evaluation in Tabular Reinforcement Learning, IEEE Transactions on Information Theory 67(1), 2021. https://arxiv.org/abs/1909.08749