Missions · Prove2Me

Completed

Graph Theory Linear Optimization Operations Research+2·Captain: mikedeng1

Linear Programming and Community Detection 7: The LP Relaxation Fails w.h.p. in the Logarithmic-Degree SBMResearch Paper

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

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.
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.
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.
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

10 thms2 active usersReviewed

Completed

Algorithmic Game Theory Combinatorics Mechanism Design+1·Captain: mikedeng1

Combinatorial Auctions with Interdependent Valuations: SOS to the Rescue 4: The k-SS Mechanism Is Ex-Post IC-IR and a (2 log k + 4)-Approximation to Welfare for Strong-SOS ValuationsResearch Paper

Motivation

In auctions with interdependent values, the value an agent assigns to an outcome depends not only on her own private information but on the information of the others: a bidder for drilling rights values a tract according to every bidder's geological survey, and a buyer of a used asset values it according to every inspector's report. Each agent observes only her own signal, while the mechanism designer knows how values depend on the full signal profile. Maximizing welfare truthfully is then much harder than with private values: the VCG mechanism no longer applies, and without structural assumptions on the valuations no ex-post truthful mechanism gives a good approximation of the optimal welfare (the source's Examples 1.2–1.3).

Eden, Feldman, Fiat, Goldner and Karlin (arXiv:1903.08384) identify submodularity over signals (SOS) as a condition under which constant or near-constant approximations become possible, including for combinatorial auctions, where agents value bundles of items. For single-dimensional signals that take $k$ values, they give a $(k+3)$ -approximation under SOS (Theorem 6.1) and, under the stronger condition strong-SOS, a $(2\log_2 k+4)$ -approximation (Theorem 6.5). This mission formalizes the second result.

Timeline. Milgrom and Weber (1982) introduced the interdependent value model for auctions; Dasgupta and Maskin (2000) studied efficient auctions under the single-crossing condition. The computer science literature then gave approximation results for simple single-parameter settings (mostly single-item auctions or matroid constraints), again largely under single crossing or its variants, e.g. Roughgarden and Talgam-Cohen (2016) and Eden, Feldman, Fiat and Goldner (2018), as surveyed in the source. The SOS paper (arXiv v2, 2019; journal version in Mathematics of Operations Research, 2024) drops single crossing and gives, in its own words, the first welfare approximation guarantees for multi-dimensional combinatorial auctions with interdependent values.

Setting

There are $n$ agents and $m$ items. Agent $i$ holds a signal $s_i\in\{0,1,\dots,k-1\}$ , and $\mathbf s=(s_1,\dots,s_n)$ is the signal profile. For every bundle $T\subseteq[m]$ , agent $i$ 's value is $v_{iT}(\mathbf s)\ge0$ , with $v_{i\emptyset}=0$ ; for nonempty $T$ it is weakly increasing in every signal and strictly increasing in $s_i$ .

A function $w$ of the profile is strong-SOS if for every coordinate $j$ , every $\delta\ge0$ and profiles $\mathbf s'\le\mathbf s$ coordinate-wise,

w(\mathbf s_{-j},s_j+\delta)-w(\mathbf s)\;\le\;w(\mathbf s'_{-j},s'_j+\delta)-w(\mathbf s').

Raising one signal helps less the higher the profile, including the raised coordinate itself; in particular the effect of an agent's own signal is concave. SOS asks this only when the raised coordinate starts from the same value in both profiles.

An allocation $T=(T_1,\dots,T_n)$ gives pairwise disjoint bundles. A deterministic mechanism maps reported signals to an allocation and payments; it is ex-post IC if, whatever the true signals and with the others truthful, no agent gains by misreporting, and ex-post IR if truthful utility is nonnegative. A randomized mechanism is universally ex-post IC-IR if every deterministic mechanism in its support is.

Let $k=2^q$ . Random Bucket picks $\ell\in\{1,\dots,\log_2 k\}$ uniformly, calls $N_{B_\ell}=\{i:s_i\ge2^{\ell-1}\}$ the high agents, and allocates to them a bundle assignment maximizing $\sum_{i\in N_{B_\ell}}v_{iS_i}(\mathbf s_{N_{\neg B_\ell}},\mathbf{2^{\ell-1}}_{N_{B_\ell}})$ , the values with every high signal lowered to $2^{\ell-1}$ ; agent $i$ receiving $\bar T_i$ pays $v_{i\bar T_i}(\mathbf s_{-i},2^{\ell-1}-1)$ . Random Sampling splits the agents uniformly at random into $A$ and $B$ , allocates to $B$ a bundle assignment maximizing $\sum_{i\in B}v_{iS_i}(\mathbf s_A,\mathbf 0_B)$ , and charges nothing. k-SS runs Random Bucket with probability $p_{RB}=\frac{\log_2 k}{\log_2 k+2}$ and Random Sampling otherwise.

Formalization targets

Goal: Theorem 6.5

For strong-SOS valuations, k-SS is universally ex-post IC-IR and, for every grid profile $\mathbf s$ and every feasible allocation $T^*$ ,

\sum_i v_{iT^*_i}(\mathbf s)\;\le\;(2\log_2 k+4)\;\mathbb E\big[\text{welfare of k-SS at }\mathbf s\big].

Milestones

Strong-SOS implies SOS (p. 19).
Display (9), corrected: with $\mathsf{SELF}=\sum_{\ell=1}^{k-1}\sum_{i:s_i=\ell}v_{iT_i}(\mathbf 0_{-i},s_i)$ ,

\mathsf{SELF}\le 2\sum_{\ell=1}^{\log_2 k}\sum_{i:2^{\ell-1}\le s_i<2^\ell}v_{iT_i}(\mathbf 0_{-i},2^{\ell-1}_i).

Lemma 6.4: Random Bucket is ex-post IC-IR and $\mathsf{SELF}\le 2\log_2 k\cdot\mathbb E[\text{welfare of Random Bucket}]$ .
The combination: $\mathsf{SELF}+\mathsf{OTHER}\le(2\log_2 k+4)\,\mathbb E[\text{welfare of k-SS}]$ , where $\mathsf{OTHER}=\sum_i v_{iT_i}(\mathbf s_{-i},0_i)$ .

Significance

The theorem shows that the price of truthfulness in combinatorial auctions with interdependent values grows only logarithmically in the number of signal values once values are concave in the agents' own signals, compared with the linear $(k+3)$ of the SOS mechanism. It also exhibits a decomposition of optimal welfare into a part driven by the other agents' signals (OTHER) and a part driven by the agent's own signal (SELF), each covered by a different randomized mechanism; this template recurs in later work on interdependent values.

The result is proved in the paper; no machine-checked version exists. Formalizing it fixes the exact model behind a proof that is stated in a few lines and checks it against the paper's own appendix: the printed display (9) omits a factor 2 (it fails for one agent with $v(\mathbf s)=s_1$ , $k=4$ , $s_1=3$ ), and the mission states the corrected inequality, which is the $d=1$ case of the paper's display (12) and is what the ratio $2\log_2 k$ requires.

Difficulty

The obvious route compares the mechanism's allocation with the optimal one agent by agent, but the mechanisms allocate by proxy values computed from modified signal profiles, and the optimal allocation's value at the true profile is not directly comparable with any single proxy. Covering SELF requires bounding an agent's own-signal contribution within a bucket by its value at the bucket floor, which needs concavity in the own signal and is false under SOS alone. Covering OTHER requires the Key Lemma 3.1 on random zeroing of signals. Incentive compatibility needs the argmax to be read off the proxy profile alone; an argmax with tie-breaking on the full report fails it.

Formalization scope

Signals are natural numbers and every hypothesis (nonnegativity, monotonicity, SOS, strong-SOS, the selectors' optimality) is quantified over the grid $\{0,\dots,k-1\}^n$ only. $k=2^q$ with $\log_2 k=q$ is a disclosed reading: the buckets cover $\{1,\dots,k-1\}$ only for powers of two. The empty bundle is worth $0$ , and the monotonicity clauses apply to nonempty bundles. The argmax of each mechanism is an arbitrary selector that sees only the bucket index (or $B$ ) and the proxy profile and returns a feasible maximizer; theorems quantify over all such selectors. Random Sampling zeroes all of $B$ , the agent's own signal included (the paper's " $v_{ij}$ " is read as $v_{iT}$ ). Expectations are finite uniform averages; at $q=0$ Lean's $0^{-1}=0$ makes the Random Bucket term vanish, matching $p_{RB}=0$ .

The approximation is stated for every feasible allocation and with true values at the truthful profile, not with proxy values or a supremum; IC and IR are stated for each deterministic component, not for the mixture's expectation. Replacing the average over partitions by an existential, or the explicit payments by existence of payments, would not be this theorem.

The model layer (signal grid, combinatorial valuations, SOS, ex-post IC-IR, OTHER and SELF, Random Sampling) is shared with the companion missions and lives in InterdepSOS.KHL and InterdepSOS.RSV; strong-SOS, Random Bucket and k-SS are defined in InterdepSOS.KSS. Lemma 6.3 and the decomposition (7), which the proof uses, are posed in the companion mission on k-HL. Proofs of the milestones, and reusable lemmas on concavity in the own signal and on random zeroing, are welcome. The source is the arXiv v2 preprint; the journal version in Mathematics of Operations Research (2024) is not what the mission cites.

Selected references

A. Eden, M. Feldman, A. Fiat, K. Goldner, A. R. Karlin, Combinatorial Auctions with Interdependent Valuations: SOS to the Rescue, arXiv:1903.08384v2, 2019. https://arxiv.org/abs/1903.08384v2
P. Milgrom, R. Weber, A Theory of Auctions and Competitive Bidding, Econometrica 50(5), 1982. https://doi.org/10.2307/1911865
P. Dasgupta, E. Maskin, Efficient Auctions, Quarterly Journal of Economics 115(2), 2000. https://doi.org/10.1162/003355300554737

10 thms2 active usersReviewed

Completed

Graph Theory Linear Optimization Operations Research·Captain: mikedeng1

Linear Programming and Community Detection 4: A Distance-Based Condition Under Which the Metric LP Relaxation Fails to Recover the Planted BisectionResearch Paper

Motivation

The minimum bisection problem asks, for a graph on an even number $n$ of vertices, for a split of the vertices into two halves that cuts as few edges as possible. It is NP-hard, and it is the maximum a posteriori estimator for the two-community stochastic block model (SBM), the standard benchmark for community detection (Abbe, 2018). Convex relaxations are the usual way to make such estimators tractable while keeping guarantees. For the semidefinite relaxation, exact-recovery thresholds are known (Abbe, Bandeira, Hall, 2016; Hajek, Wu, Xu, 2016). Linear programming relaxations are cheaper and much used in combinatorial optimization, but their recovery properties were not understood.

Del Pia, Khajavirad and Kunisky (arXiv:2006.03213v2, Mathematics of Operations Research, 2023) study the best-known LP relaxation of minimum bisection, the metric relaxation. They give a sufficient condition for it to recover a planted bisection (Theorem 4) and a necessary one (Theorem 5). This mission formalizes the necessary condition. Its consequence, developed in §4 of the paper, is that the metric relaxation fails with high probability in most SBM regimes, including those where the minimum bisection itself succeeds.

Setting

Let $G=(V,E)$ be a simple graph on $V=\{1,\dots,n\}$ , and write $(i,j)$ for an edge with $i<j$ ; set $a_{ij}=1$ if $(i,j)\in E$ and $a_{ij}=0$ otherwise. A bisection is a partition of $V$ into two sets $V_1,V_2$ with $|V_1|=|V_2|=n/2$ . One fixed bisection, unknown to the solver, is the planted bisection; $E_0$ is the set of edges with one end in $V_1$ and the other in $V_2$ .

The cut vector $\bar x\in\{0,1\}^{\binom n2}$ of the planted bisection has $\bar x_{ij}=1$ exactly when $i$ and $j$ lie on different sides. The metric relaxation is the linear program, with $x_{ji}:=x_{ij}$ ,

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

where (1) ranges over distinct $i,j,k$ with $i<j$ and (2) over $i<j<k$ . The LP recovers the planted bisection if $\bar x$ is its unique optimal solution. The objective at $\bar x$ is $|E_0|$ .

The graph distance $\rho_G(i,j)$ is the length of a shortest $i$ – $j$ path ( $+\infty$ across components). The diameter and the average distance are

\rho_{\max}(G)=\max_{i,j\in V}\rho_G(i,j),\qquad \rho_{\mathrm{avg}}(G)=\frac{2}{n^2}\sum_{1\le i<j\le n}\rho_G(i,j).

The average is over all $n^2$ ordered pairs, the diagonal included. For $n\ge5$ define

c(G)=\max\Big\{0,\ \frac{3\rho_{\max}(G)-4\rho_{\mathrm{avg}}(G)}{1-4/n}\Big\}.\qquad(17)

Formalization targets

Goal: Theorem 5

For a connected graph $G$ on $n\ge5$ nodes with a planted bisection,

\frac{1+c(G)}{2\rho_{\mathrm{avg}}(G)+2c(G)(1-\frac1n)}\,|E|<|E_0|\quad(18)\qquad\Longrightarrow\qquad\text{(LP-P) does not recover the planted bisection.}

Milestones

The proof of Theorem 5 works with the point $\tilde x\in\mathbb R^{\binom n2}$ ,

\tilde x_{ij}=\frac{\rho_G(i,j)+c(G)}{2\rho_{\mathrm{avg}}(G)+2c(G)(1-\frac1n)}.

The mission poses three statements about it, for a connected $G$ on $n\ge5$ nodes:

display (19), p. 12: for $i<j<k$ , $\displaystyle\tilde x_{ij}+\tilde x_{ik}+\tilde x_{jk}\le\frac32\cdot\frac{\rho_{\max}(G)+c(G)}{\rho_{\mathrm{avg}}(G)+c(G)(1-\frac1n)}$ ;
p. 13: $\tilde x$ is feasible for (LP-P);
p. 13: the objective of (LP-P) at $\tilde x$ equals $\displaystyle\frac{1+c(G)}{\rho_{\mathrm{avg}}(G)+c(G)(1-\frac1n)}\cdot\frac{|E|}{2}$ .

Significance

The result. Theorem 5 is a deterministic certificate of failure, stated for any connected graph, not for a random model. It reduces the question "does the LP recover?" to comparing two numbers that depend only on the distance profile of $G$ and on the fraction of edges cut by the planted bisection. When typical distances are close to the diameter, $c(G)$ is small and (18) asks only that $|E_0|/|E|$ exceed roughly $1/(2\rho_{\mathrm{avg}}(G))$ . In random graphs typical distances are close to the diameter. The paper's Theorems 7 and 8 combine Theorem 5 with known distance asymptotics of Erdős–Rényi graphs (Bollobás, Random Graphs, 2001; Chung, Lu, 2001). They show that the metric relaxation fails with high probability in the dense and logarithmic-degree SBM, in contrast with the semidefinite relaxation. Those theorems are separate missions of this series and use Theorem 5 as a black box.

Formalizing it. The result is proved in the paper; no machine-checked version is known. The mission produces a formal metric relaxation of minimum bisection, with LP recovery defined as uniqueness of the optimum, and links it to graph distances through Mathlib's SimpleGraph.edist/ediam. The definitions are written to coincide with those of the other missions of this series, so that one model layer serves the sufficient condition (Theorem 4), the necessary condition (this mission), and the random-graph consequences.

Difficulty

Theorem 5 is not deep, but it is exact. The milestones fix the witness $\tilde x$ ; the work is in checking it. The obvious candidate, the graph metric $\rho_G$ itself rescaled to satisfy the equality (3), satisfies the triangle inequalities (1). It can violate the perimeter constraints (2) whenever some triangle of vertices is spread out compared with the average distance. The shift by $c(G)$ , which depends on $\rho_{\max}$ and on the factor $1-4/n$ , is tuned so that (2) holds with no slack in the worst case. A proof has to keep track of the normalization $2/n^2$ (ordered pairs, diagonal included), the factor $1-1/n$ , and the sign of $3\rho_{\max}-4\rho_{\mathrm{avg}}$ , and must use $n\ge5$ wherever it divides by $1-4/n$ . In Lean the further work is converting between sums over ordered pairs, unordered pairs and the edge set, and between extended-valued distances and their real values for a connected graph.

Formalization scope

Vertices and bisections. Vertices are Fin n (0-based). The planted bisection is a finset $V_1$ with $2|V_1|=n$ , and $V_2=V_1^{c}$ . $|E_0|$ is the number of pairs $i<j$ adjacent in $G$ and on different sides.
LP variables. A point of $\mathbb R^{\binom n2}$ is an array $x:\texttt{Fin } n\to\texttt{Fin } n\to\mathbb R$ . Feasibility includes symmetry and a zero diagonal, so the free diagonal and lower-triangle entries cannot break uniqueness of the optimum. No bounds $0\le x\le1$ are added; they are not constraints of (LP-P).
Recovery. LPRecovers G V1 says that the cut vector of $V_1$ is optimal and every optimal point equals it.
Distances. $\rho_G$ is SimpleGraph.edist (in $\mathbb N\cup\{\infty\}$ ), $\rho_{\max}$ is SimpleGraph.ediam, and $\rho_{\mathrm{avg}}$ is the printed formula computed in $[0,\infty]$ . $c(G)$ and $\tilde x$ use their real values. All statements assume $G$ connected, where these values are finite and $\rho_{\mathrm{avg}}(G)>0$ .
Standing hypotheses. Every statement carries exactly the page's hypotheses: $G$ connected and $n\ge5$ , plus, for Theorem 5, the planted bisection. The bisection forces $n$ even, so in effect $n\ge6$ ; $n\ge5$ is kept as printed. $\tilde x$ is indexed by $i<j$ on the page and is extended symmetrically with zero diagonal.
Ruled out. A formalization that adds box constraints, drops the symmetric zero-diagonal normalization, averages over $n(n-1)/2$ pairs instead of the printed $2/n^2$ , or omits connectivity (where the real value of an infinite distance would be $0$ ) states a different theorem. None of these is used here.

Contributions welcome: proofs of the three milestones and the goal. Reusable lemmas include the identity $\sum_{i<j}a_{ij}x_{ij}=\sum_{(i,j)\in E}x_{ij}$ for SimpleGraph.edgeFinset, the finiteness of ediam for connected graphs on Fin n, and the bound $\rho_{\mathrm{avg}}(G)\le(1-\frac1n)\rho_{\max}(G)$ .

Selected references

A. Del Pia, A. Khajavirad, D. Kunisky, Linear Programming and Community Detection, Mathematics of Operations Research, 2023; arXiv:2006.03213v2 (2022). https://arxiv.org/abs/2006.03213
E. Abbe, Community Detection and Stochastic Block Models: Recent Developments, Journal of Machine Learning Research 18 (2018). https://arxiv.org/abs/1703.10146
E. Abbe, A. S. Bandeira, G. Hall, Exact Recovery in the Stochastic Block Model, IEEE Transactions on Information Theory 62 (2016). https://arxiv.org/abs/1405.3267
B. Hajek, Y. Wu, J. Xu, Achieving Exact Cluster Recovery Threshold via Semidefinite Programming, IEEE Transactions on Information Theory 62 (2016). https://arxiv.org/abs/1412.6156
B. Bollobás, Random Graphs, 2nd ed., Cambridge University Press, 2001. https://doi.org/10.1017/CBO9780511814068
F. Chung, L. Lu, The Diameter of Sparse Random Graphs, Advances in Applied Mathematics 26 (2001). https://doi.org/10.1006/aama.2001.0720

8 thms2 active usersReviewed

Graph Theory Operations Research Probability·Captain: mikedeng1

Load Balancing Under Strict Compatibility Constraints 3: Inhomogeneous Random Graphs with Edge Probabilities Satisfying (3.5) Are Almost Surely Proportionally Sparse and SubcriticalResearch Paper

Motivation

Large-scale computing systems route incoming tasks to servers through dispatchers, one per task type. A task can only run on a server that holds the data or software it needs, so the set of admissible pairs forms a bipartite compatibility graph between task types and servers. Full flexibility (every server can serve every type) gives the best load balancing but requires each server to store everything. A central question is how sparse the compatibility graph can be while keeping the performance of the fully flexible system.

For the power-of- $d$ policy JSQ( $d$ ) (an arriving task samples $d$ compatible servers and joins the shortest of their queues), Rutten and Mukherjee (arXiv:2008.07562v2, Math. Oper. Res. 2023) identify two deterministic graph conditions, proportional sparsity and subcriticality, under which the occupancy process has the same mean-field limit and the same steady-state limit as in the fully flexible system (their Theorem 3.4). They then show that natural random designs satisfy both conditions almost surely. This mission covers the second random design: task types with inhomogeneous levels of flexibility, where each edge incident to task type $w$ is present independently with its own probability $p_w(N)$ (Theorem 3.6 of the paper).

Earlier work on JSQ-type policies with constrained compatibility includes the stability analyses of Bramson (Ann. Appl. Probab. 2011) and of Cardinaels, Borst and van Leeuwaarden (Queueing Syst. 2019), to which subcriticality is equivalent for a fixed system (Remark 3 of the paper), and the mean-field analysis of the supermarket model on graphs by Budhiraja, Mukherjee and Wu (Ann. Appl. Probab. 2019), whose load condition is stronger than the condition (A.19) used here (Remark 11 of the paper).

Setting

For each $N \ge 1$ there are a set $V_N$ of $N$ servers and a set $W_N$ of $M(N) \ge 1$ dispatchers. A compatibility graph is $G_N = (V_N, W_N, E_N)$ with $E_N \subseteq V_N \times W_N$ , and the neighbourhood of $w$ is $N_w = \{v : (v, w) \in E_N\}$ .

Proportional sparsity (Definition 3.1). For every $\varepsilon > 0$ ,

\sup_{U \subseteq V_N} \frac{1}{M(N)} \Bigl| \Bigl\{ w \in W_N : \Bigl| \frac{|N_w \cap U|}{|N_w|} - \frac{|U|}{N} \Bigr| \ge \varepsilon \Bigr\} \Bigr| \to 0 .

Every set $U$ of servers is seen by all but a vanishing fraction of dispatchers in roughly its global proportion.

Subcriticality (Definition 3.3). For each $N$ , $w$ and nonempty $U \subseteq V_N$ there is a probability distribution $\gamma^U_w$ on $U$ such that, with $k_w = \min(d, |N_w|)$ ,

\limsup_{N \to \infty} \max_{v \in V_N} \frac{N}{M(N)} \sum_{w \in W_N} \binom{|N_w|}{k_w}^{-1} \sum_{U \subseteq N_w,\ |U| = k_w} \gamma^U_w(v) \le 1 .

Some static routing of sampled sets loads no server asymptotically beyond its capacity.

The random graph. Given edge probabilities $p_w(N) \in (0, 1]$ , the graph $G_N$ contains each pair $(v, w)$ independently with probability $p_w(N)$ . Write $\bar p(N) = \min_{w} p_w(N)$ and $\|p(N)^{-1}\|_2^{-2} = (\sum_w p_w(N)^{-2})^{-1}$ . Only the law of each $G_N$ is prescribed; the graphs for different $N$ may be coupled arbitrarily, and "almost surely" refers to any such coupling.

Formalization targets

Goal: Theorem 3.6 (graph part)

If, as $N \to \infty$ ,

\frac{N}{\ln M(N) + \ln N}\, \bar p(N) \to \infty, \qquad M(N)\, \bar p(N) \to \infty, \qquad \frac{\ln N}{M(N)^2} \sum_{w \in W_N} \frac{1}{p_w(N)^2} \to 0, \qquad (3.5)

then almost surely $\{G_N\}$ is proportionally sparse and satisfies the subcriticality condition.

Milestones

Lemma B.1. If $\bar p(N) = \omega(1/N)$ and $\bar p(N) = \omega(1/M(N))$ , then $\{G_N\}$ is proportionally sparse almost surely.
The (A.19) reduction. For any graph sequence and $d \ge 1$ ,

\limsup_{N \to \infty} \max_{v \in V_N} \frac{N}{M(N)} \sum_{w \in W_N} \frac{\mathbb 1\{(v, w) \in E_N\}}{|N_w|} \le 1 \qquad \text{(A.19)}

implies subcriticality. 3. Lemma B.2. If $\bar p(N) = \omega((\ln M(N) + \ln N)/N)$ and $\|p(N)^{-1}\|_2^{-2} = \omega(\ln N / M(N)^2)$ , then $\{G_N\}$ satisfies the subcriticality condition almost surely.

The goal is the conjunction of Lemmas B.1 and B.2 under (3.5).

Significance

Combined with Theorem 3.4 of the paper, the goal says that JSQ( $d$ ) on a random compatibility graph with dispatcher-dependent flexibility behaves, in the large-system limit and in steady state, like JSQ( $d$ ) on the complete bipartite graph. Condition (3.5) allows the least flexible task type to be compatible with only about $\ln(M(N)N)$ times a diverging factor of servers in expectation, far below $N$ , and allows strongly heterogeneous flexibility levels as long as the spread measured by $\sum_w p_w(N)^{-2}$ is controlled. Remark 8 of the paper notes that for $M(N) = N$ and equal probabilities, $p(N) = o(\ln N / N)$ leaves a dispatcher isolated with probability tending to one, so the growth conditions are close to necessary.

The result is proved in the paper (Appendix B). As far as is known, none of it has been machine-checked. A formal proof requires a quantitative Chernoff bound for binomial tails, a bounded-differences (Azuma–Hoeffding) inequality for functions of independent Bernoulli variables, a union bound over all $2^N$ subsets of servers, and the first Borel–Cantelli lemma in a setting where only per- $N$ marginal laws are fixed.

Difficulty

Proportional sparsity quantifies over every subset $U$ of the $N$ servers. A concentration estimate for one fixed $U$ , or one fixed dispatcher, is not enough: whatever bound is used must survive a union over $2^N$ subsets, so a merely vanishing failure probability per dispatcher does not suffice.

Subcriticality is a maximum over all servers of a sum whose terms $\mathbb 1\{(v, w) \in E_N\}/|N_w|$ are not independent: $|N_w|$ depends on the edge $(v, w)$ itself, and a term is unbounded in the regime where $|N_w|$ is small. A direct concentration inequality for this sum therefore does not apply, and the logarithmic factors in (3.5) reflect the need to control all $M(N)$ neighbourhood sizes and all $N$ servers at once.

Independence across $N$ is not available, so almost-sure statements cannot use the second Borel–Cantelli lemma or any law of large numbers along $N$ ; every bound must be summable in $N$ .

Formalization scope

Servers are Fin N, dispatchers Fin (M N) with 0 < M N assumed, and a graph is a Finset (Fin N × Fin (M N)).
Edge probabilities are reals with $0 < p_w(N) \le 1$ (implicit in the paper). The random graph is a family of measurable maps $X_N : \Omega \to \{0,1\}^{V_N \times W_N}$ on one probability space whose image law is the product of Bernoulli $(p_w(N))$ laws. No assumption links different $N$ .
Every " $\limsup \le 1$ " is stated as "for every $\varepsilon > 0$ , eventually, for every server, $\le 1 + \varepsilon$ "; the supremum over $U$ in (3.1) as "for all $\varepsilon, \delta > 0$ , eventually, for every $U$ , at most $\delta M(N)$ bad dispatchers". Both are exact equivalents.
Ratios use real division; $|N_w| = 0$ gives ratio $0$ , harmless for a limit condition. At $N = 1$ the logarithms in (3.5) and Lemma B.2 can make a denominator $0$ ; this affects finitely many $N$ .
Proportional sparsity does not include connectivity: these graphs are disconnected with positive probability for every $N$ , so requiring connectivity would make the goal false.
Subcriticality is Definition 3.3 with two repairs: distributions are required only for nonempty $U$ , and the normalisation is $\binom{|N_w|}{\min(d, |N_w|)}$ instead of the printed $\binom{|N_w|}{d}$ , which is $0$ when $|N_w| < d$ , an event of positive probability here. The two agree when $|N_w| \ge d$ .
$d \ge 2$ as in the model. Under $d = 0$ the subcriticality predicate would be trivially true; the statements exclude it.
Only the graph part of Theorem 3.6 is posed; "Consequently, the conclusions of Theorem 3.4 hold" belongs to the mean-field mission of this series.

A complete development needs binomial Chernoff bounds, a bounded-differences inequality and Borel–Cantelli for summable bounds; these are reusable for other random-graph statements. Proofs of the deterministic (A.19) reduction and of either lemma are welcome independently.

Selected references

M. Rutten, D. Mukherjee, Load Balancing Under Strict Compatibility Constraints, arXiv:2008.07562v2, 2020; Math. Oper. Res. 48 (2023). https://arxiv.org/abs/2008.07562
M. Bramson, Stability of join the shortest queue networks, Ann. Appl. Probab. 21(4):1568–1625, 2011. https://doi.org/10.1214/10-AAP726
A. Budhiraja, D. Mukherjee, R. Wu, Supermarket model on graphs, Ann. Appl. Probab. 29(3):1740–1777, 2019. https://arxiv.org/abs/1712.07607
E. Cardinaels, S. C. Borst, J. S. H. van Leeuwaarden, Job assignment in large-scale service systems with affinity relations, Queueing Syst. 93(3–4):227–268, 2019.
S. Janson, T. Łuczak, A. Ruciński, Random Graphs, Wiley, 2000. https://doi.org/10.1002/9781118032718

9 thms2 active users

Differential Geometry Machine Learning Optimization+1·Captain: mikedeng1

Stochastic Zeroth-Order Riemannian Derivative Estimation and Optimization 2: ZO-RSGD Has Average Expected Squared Riemannian Gradient Norm at Most 4L(f(x₀) − f(x*))/(N+1) + 2μ²L²(d+6)³ + 16(d+4)σ²/mResearch Paper

Motivation

Many optimization problems are posed over a manifold rather than a vector space: orthogonality constraints (the Stiefel manifold), unit-norm constraints (the sphere), fixed-rank matrices. In some of them the objective can only be evaluated, not differentiated. Black-box adversarial attacks on a neural network with a norm-constrained perturbation, hyperparameter tuning and simulation-based objectives are examples, and in all of them each function value is also noisy. Zeroth-order (derivative-free) methods replace the gradient by a random finite-difference estimate built from function values alone.

In Euclidean space the analysis of such methods is well developed. Nesterov and Spokoiny (2017) analysed Gaussian-smoothing estimators for deterministic objectives, and Ghadimi and Lan (2013) gave the first non-asymptotic stationarity rates for stochastic nonconvex objectives (the RSGF method). Li, Balasubramanian and Ma (arXiv:2003.11238, published in Mathematics of Operations Research, 2023) carried this programme to embedded submanifolds. They estimate the Riemannian gradient by projecting a Gaussian vector onto the tangent space and moving along a retraction, and they prove convergence rates for the resulting methods. This mission formalizes their rate for the stochastic method, ZO-RSGD (Theorem 3.2).

Setting

Let $E$ be a finite-dimensional real inner product space (the paper's $\mathbb R^n$ ), and let $\mathcal M \subseteq E$ be a $C^1$ embedded submanifold of dimension $d$ . The tangent space $T_x\mathcal M$ at $x \in \mathcal M$ is the linear span of the tangent cone of $\mathcal M$ at $x$ . For a submanifold this is the set of velocities $\gamma'(0)$ of curves in $\mathcal M$ through $x$ , and it is a subspace of dimension $d$ . $\mathcal M$ carries the metric induced by the inner product of $E$ , and $P_x$ denotes the orthogonal projection of $E$ onto $T_x\mathcal M$ .

A retraction is a map $R$ , $(x, \eta) \mapsto R_x(\eta)$ . For every $x \in \mathcal M$ it sends all of $T_x\mathcal M$ into $\mathcal M$ and is smooth on $T_x\mathcal M$ , with $R_x(0) = x$ and differential the identity at $0$ . The Riemannian gradient of a differentiable $f$ is $\operatorname{grad} f(x) = P_x \nabla f(x)$ .

The objective is stochastic, $f(x) = \mathbb E_\xi F(x, \xi)$ , with noise $\xi$ distributed according to a probability measure $P_\xi$ . Two assumptions are imposed:

Assumption 2.1 ( $L$ -retraction-smoothness). For almost every $\xi$ , $|F(R_x(\eta),\xi) - F(x,\xi) - \langle \operatorname{grad}F(x,\xi), \eta\rangle| \le \frac L2\|\eta\|^2$ for all $x \in \mathcal M$ and $\eta \in T_x\mathcal M$ .
Assumption 2.3 (unbiased oracle, bounded variance). For every $x \in \mathcal M$ , $\mathbb E_\xi F(x,\xi) = f(x)$ , $\mathbb E_\xi \operatorname{grad}F(x,\xi) = \operatorname{grad}f(x)$ and $\mathbb E_\xi\|\operatorname{grad}F(x,\xi) - \operatorname{grad}f(x)\|^2 \le \sigma^2$ .

Given a smoothing parameter $\mu > 0$ and a batch size $m$ , draw $m$ independent pairs $(u_{0,i}, \xi_i)$ , each with $u_{0,i} \sim \mathcal N(0, I)$ independent of $\xi_i \sim P_\xi$ , and put $u_i = P_x u_{0,i}$ . The mini-batch zeroth-order Riemannian gradient is

\bar g_{\mu,\xi}(x) = \frac1m\sum_{i=1}^m \frac{F(R_x(\mu u_i), \xi_i) - F(x, \xi_i)}{\mu}\,u_i .

ZO-RSGD (Algorithm 2) starts at $x_0 \in \mathcal M$ and iterates $x_{k+1} = R_{x_k}(-\hat\eta\,\bar g_{\mu,\xi}(x_k))$ with step $\hat\eta = 1/L$ and a fresh batch at every step. $x^*$ denotes a minimizer of $f$ over $\mathcal M$ .

Formalization targets

Goal: Theorem 3.2

If $m \ge 16(d+4)$ , then for every $N$

\frac{1}{N+1}\sum_{k=0}^{N}\mathbb E\,\|\operatorname{grad} f(x_k)\|^2 \le 4L\,\frac{f(x_0) - f(x^*)}{N+1} + 2\mu^2L^2(d+6)^3 + \frac{16(d+4)}{m}\sigma^2 .

The constants are the paper's own. The goal states the rate for every $\mu$ , $m$ and $N$ . It does not state the parameter choices $\mu = O(\epsilon/d^{3/2})$ , $m = O(d\sigma^2/\epsilon^2)$ , $N = O(1/\epsilon^2)$ that follow from it.

Milestones

Lemma 2.1. For a $d$ -dimensional subspace $\mathcal X$ with projection $P$ , $u = Pu_0$ and $x \in \mathcal X$ : $\mathbb E\langle x,u\rangle u = x$ and $\mathbb E\langle x,u\rangle^2 = \|x\|^2$ .
Lemma 2.2 (Nesterov–Spokoiny). $\mathbb E\|u\|^p \le (n+p)^{p/2}$ for a standard Gaussian $u$ on $\mathbb R^n$ and $p \ge 2$ . This is already proved on the platform and is reused.
Corollary 2.1. $\mathbb E\|Pu_0\|^p \le (d+p)^{p/2}$ .
Proposition 2.1(a). $\|\mathbb E\,g_\mu(x) - \operatorname{grad}f(x)\| \le \frac{\mu L}{2}(d+3)^{3/2}$ for the single-sample estimator $g_\mu$ .
Lemma 3.1. $\mathbb E\|\bar g_{\mu,\xi}(x) - \operatorname{grad}f(x)\|^2 \le \mu^2L^2(d+6)^3 + \frac{8(d+4)}{m}\sigma^2 + \frac{8(d+4)}{m}\|\operatorname{grad}f(x)\|^2$ .

Significance

Theorem 3.2 is the basic complexity result for derivative-free stochastic optimization on manifolds. With the parameter choices of (3.10) it gives an $\epsilon$ -stationary point in expectation after $O(d/\epsilon^4)$ noisy function evaluations. The dependence is on the manifold dimension $d$ , not on the ambient dimension $n$ . This matches the Euclidean rate of Ghadimi and Lan with $n$ replaced by $d$ , and it is what makes projected-Gaussian estimators attractive when $d \ll n$ (for example, low-dimensional Stiefel manifolds embedded in large matrix spaces).

The results are proved in the paper (main text, p. 17, and Appendix C) but, to our knowledge, none of them has been machine-checked. The Euclidean Gaussian moment bound (Lemma 2.2) is formalized on the platform. The Euclidean RSGF results of Ghadimi and Lan are stated on the platform, and they are different statements: they use $x + \mu u$ instead of a retraction, the full space instead of a tangent space, and a random output index. A complete formalization would also produce reusable infrastructure: Gaussian identities for orthogonal projections, the projected-Gaussian moment bound, and a template for proving stationarity rates of random iterates on a product probability space.

Difficulty

The Euclidean argument relies on a smoothed function $f_\mu(x) = \mathbb E f(x + \mu u)$ whose gradient is exactly the mean of the estimator. That identity has no Riemannian analogue: $R_x(\mu u)$ is not a translate, so $\mathbb E\,g_\mu(x)$ is not the gradient of any smoothed function. The bias in Proposition 2.1(a) has to be bounded directly from Assumption 2.1, and this is why the estimator is only approximately unbiased.

The convergence proof needs a one-step descent inequality conditioned on the past. The direction at step $k$ is projected onto $T_{x_k}\mathcal M$ , which depends on all earlier draws, so the conditional bound of Lemma 3.1 must be integrated against the product law of the batches. A naive reading that samples every direction from one fixed subspace, or that treats the iterates as deterministic, does not describe the algorithm. A further subtlety is that the gradient term of Lemma 3.1 must be absorbed by the descent of one step. This requires the batch to be large compared with the dimension, $m \ge 16(d+4)$ .

Formalization scope

$E$ is any finite-dimensional real inner product space with its Borel σ-algebra. The Gaussian is Mathlib's stdGaussian E.
$\mathcal M$ and its dimension are given by the published ProjLikeRetr.Retractor.IsSubmanifold 1 d M (a $C^1$ coordinate-slice submanifold), so $d$ is tied to $\mathcal M$ and is never a free number. $T_x\mathcal M$ is the published ProjLikeRetr.Retractor.tangentSpace M x, never an arbitrary subspace.
The retraction is defined on all of each tangent space, as the paper requires (Assumption 2.1 holds "for all $\eta \in T_x\mathcal M$ , i.e., $\rho_x = \infty$ "). The objective $f$ and the samples $F(\cdot,\xi)$ are assumed differentiable rather than smooth, which is all the gradient formula (2.3) uses.
Added hypotheses. The goal assumes $m \ge 16(d+4)$ . The paper's proof assumes it explicitly, but the theorem statement omits it. The goal also assumes that $(x,\eta) \mapsto R_x(\eta)$ and $x \mapsto P_x$ are measurable, so that the iterates are random variables; this holds for closed $\mathcal M$ such as spheres and Stiefel manifolds. Lemma 3.1 is stated for every $m \ge 1$ . The paper's last proof step uses $m \ge 2$ , but the bound holds for $m = 1$ as well.
The iterates are defined for every $k$ on the sequence space of i.i.d. batches (the algorithm without a stopping index), so $x_{N+1}$ exists.
No junk expectations. Every expectation of a nonnegative quantity is a lower Lebesgue integral compared with ENNReal.ofReal of the bound. Every vector-valued expectation comes with an integrability conclusion, and Assumption 2.3 carries the integrability of $F(x,\cdot)$ and $\operatorname{grad}F(x,\cdot)$ . So no statement can hold because a Bochner integral defaulted to $0$ .
The $O(\cdot)$ parameter choices (3.10) and the oracle complexity $mN = O(d/\epsilon^4)$ are not formalized.
The development needs projections of Gaussian measures onto subspaces, moments of Gaussian norms, conditional expectation along an i.i.d. sequence of batches, and telescoping. Proofs of any milestone are welcome, as are general lemmas about the push-forward of stdGaussian under an orthogonal projection.

Selected references

J. Li, K. Balasubramanian, S. Ma, Stochastic Zeroth-Order Riemannian Derivative Estimation and Optimization, Mathematics of Operations Research, 2023. Preprint arXiv:2003.11238v3. https://arxiv.org/abs/2003.11238
Y. Nesterov, V. Spokoiny, Random Gradient-Free Minimization of Convex Functions, Foundations of Computational Mathematics 17, 2017. https://doi.org/10.1007/s10208-015-9296-2
S. Ghadimi, G. Lan, Stochastic First- and Zeroth-Order Methods for Nonconvex Stochastic Programming, SIAM Journal on Optimization 23(4), 2013. https://arxiv.org/abs/1309.5549
K. Balasubramanian, S. Ghadimi, Zeroth-Order Nonconvex Stochastic Optimization: Handling Constraints, High Dimensionality, and Saddle Points, Foundations of Computational Mathematics, 2022. https://arxiv.org/abs/1809.06474
N. Boumal, P.-A. Absil, C. Cartis, Global Rates of Convergence for Nonconvex Optimization on Manifolds, IMA Journal of Numerical Analysis, 2019. https://arxiv.org/abs/1605.08101
P.-A. Absil, R. Mahony, R. Sepulchre, Optimization Algorithms on Matrix Manifolds, Princeton University Press, 2008.

13 thms2 active usersReviewed

Machine Learning Reinforcement Learning Statistics·Captain: mikedeng1

Breaking the Sample Size Barrier in Model-Based Reinforcement Learning with a Generative Model 3: Plug-In Policy Evaluation Is ε-Accurate w.p. 1−δ Once N ≥ c₀log(|S|log(e/(1−γ))/δ)/((1−γ)³ε²)Research Paper

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

17 thms2 active usersReviewed

Completed

Algorithmic Game Theory Operations Research Probability·Captain: mikedeng1

Designing Approximately Optimal Search on Matching Platforms 2: Every Set of Assortments Has a Unique Profile of Thresholds Equal to Expected UtilitiesResearch Paper

Motivation

Online matching platforms for dating, freelancing or ride sharing do not match agents themselves. They decide whom each agent gets to see and how often, and the agents then accept or reject. Immorlica, Lucier, Manshadi and Wei (arXiv:2102.09017, Management Science 2023) model this as directed search. The platform designs assortments, which are rates at which types of agents meet, and the agents play an equilibrium of the induced search game. The platform's design problem only makes sense if every choice of assortments leads to a single, well-defined equilibrium outcome. Otherwise "the welfare of an assortment" is not a function of the assortment. This is not automatic: even for simple asymmetric preferences under random meetings, multiple stationary equilibria can arise (Burdett and Coles 1997).

This mission formalizes that well-posedness result, Proposition 3.1(1) of the paper, together with the fixed-point and iteration lemmas of Appendix A.3 and Appendix B.3 on which its proof rests. It is the companion of the mission on the paper's quarter-approximation theorem (Theorem 4.1), which uses the same model.

The source is the arXiv v2 preprint (18 Aug 2021). The Management Science version may number results differently.

Setting

There are finitely many agent types on each side of the market, a set $\mathcal M$ and a set $\mathcal W$ , with $\Theta=\mathcal M\cup\mathcal W$ . Agents of every type leave the market unmatched at a life-event rate $\delta>0$ , and type $\theta$ arrives at rate $\alpha_\theta>0$ . When an agent of type $m$ meets an agent of type $w$ , the pair draws one utility $u\sim F_{mw}$ . Valuations are symmetric: both agents receive $u$ if they match, and $F_{wm}:=F_{mw}$ . Each $F_{mw}$ is a probability law on $\mathbb R$ with no atoms (a "continuous distribution").

An assortment for type $\theta$ is a family of rates $\lambda_\theta(\theta')\ge0$ at which type- $\theta$ agents meet type- $\theta'$ agents on the opposite side. Under a threshold strategy with threshold $\tau_\theta$ , a type- $\theta$ agent accepts a meeting if and only if $u\ge\tau_\theta$ . A meeting turns into a match when both agents accept, i.e. when $u\ge\max(\tau_\theta,\tau_{\theta'})$ . If every type plays a threshold strategy, the expected utility of a type- $\theta$ agent is (equation (5))

\bar u_\theta(\tau)=\frac{\sum_{\theta'}\lambda_\theta(\theta')\int_{\max(\tau_\theta,\tau_{\theta'})}^\infty u\,dF_{\theta\theta'}}{\delta+\sum_{\theta'}\lambda_\theta(\theta')\int_{\max(\tau_\theta,\tau_{\theta'})}^\infty dF_{\theta\theta'}} .

A type's own threshold enters its own utility through $\max(\tau_\theta,\tau_{\theta'})$ .

One type's equation. Fix the thresholds $\tau_i$ of the opposite types. Write $B(t)$ for the right-hand side of (5) with $\tau_\theta$ replaced by $t$ . Lemma A.3 states that $t=B(t)$ has exactly one solution. The best-response map of Appendix A.3 sends a profile $\tau$ to the profile in which each type's new threshold is that solution, computed against the opposite side's thresholds in $\tau$ . A best-response sequence starts at the all-zero profile and applies this map repeatedly.

Formalization targets

Goal: Proposition 3.1, item 1 (fixed-point form)

For any fixed assortments there is exactly one threshold profile $\tau\in\mathbb R^{\mathcal M}\times\mathbb R^{\mathcal W}$ with

\tau_\theta=\bar u_\theta(\tau)\qquad\text{for every }\theta\in\Theta .

Uniqueness ranges over all real profiles.

Milestones

Lemma B.1 (p. 40). With $\lambda_i>0$ and $\tau_i\ge0$ , $\rho=\max_{t\ge0}B(t)$ is attained and satisfies $B(\rho)=\rho$ . $B$ is weakly increasing on $(-\infty,\rho]$ and weakly decreasing on $[\rho,\infty)$ .
Lemma A.3 (p. 35). With $\lambda_i\ge0$ and arbitrary $\tau_i$ , the equation $t=B(t)$ has exactly one real solution.
§A.3, p. 37, first claim. Along a best-response sequence $\tau^{(0)}\equiv0,\tau^{(1)},\dots$ , the odd iterates are weakly decreasing and the even iterates are weakly increasing, componentwise.
§A.3, p. 37, second claim. Every odd iterate dominates every even iterate: $\tau^{(2j)}\le\tau^{(2i+1)}$ .
Proposition A.4 (p. 36). There is a universal $C$ such that $\tau^{(C|\Theta|)}$ is a fixed point of the best-response map, and the sequence is constant from that index on.

Significance

Proposition 3.1 is what makes the platform's problem OptimalDirectedSearch well defined. Assortments determine a unique threshold profile. That profile determines the matching rates (Lemma 3.2) and, through stationarity, the population masses. Welfare is then a function of the assortments, and the program (6) used for Theorem 4.1 encodes exactly this fixed point as its incentive constraint (6e). The constructive proof also yields an algorithm: iterate best responses from zero, and the iteration stops after $O(|\Theta|)$ rounds.

Formalizing it adds three things beyond the paper. First, a checked version of an argument the paper gives informally, including the odd/even sandwich of the iteration, which the paper proves in a few lines. Second, a reusable fixed-point and unimodality lemma for ratios of tail integrals, $B(t)=\int_t^\infty u\,dG\,/\,(\delta+\int_t^\infty dG)$ , which recurs in reservation-value arguments in search theory. Third, an exact accounting of the hypotheses: integrable utilities and the reading of the best-response map. To our knowledge none of these results has been machine-checked.

Difficulty

The obvious route to uniqueness, a contraction argument for the map $\tau\mapsto\bar u(\tau)$ , fails. That map is neither monotone nor contractive in general, since raising a type's own threshold can raise or lower its utility. Existence by Brouwer's fixed-point theorem gives no uniqueness and no algorithm. The best-response iteration does not converge monotonically either: its odd and even iterates move in opposite directions, so convergence in finitely many rounds is a combinatorial statement about the order of the thresholds, not a limit argument. A formal proof also needs continuity and monotonicity of tail integrals of atomless laws, which Mathlib provides only in pieces.

Formalization scope

The two sides are separate finite types M and W. A threshold profile is a pair of functions (M → ℝ) × (W → ℝ), ordered componentwise. A market records $\delta$ , $\alpha$ and the laws F m w : Measure ℝ. The standing assumptions are:

$\delta>0$ ;
$\alpha_\theta>0$ , which is implicit in the paper and stated explicitly;
each $F_{mw}$ is a probability measure with no atoms (NullSingletonClass);
each $F_{mw}$ has an integrable identity. This is implicit in the paper, which uses $\int u\,dF$ as a real number, and is stated explicitly.

Tails are $\int_a^\infty dF=F([a,\infty))$ and $\int_a^\infty u\,dF=\int_{[a,\infty)}u\,dF$ . Capacity (2), flow balance (3) and stationarity (1) are not hypotheses, because Proposition 3.1 holds for any fixed assortments.

The best-response map is encoded as a relation: each new threshold solves its own equation $t=B(t)$ against the opposite side's input thresholds. This is the paper's reading ("This map is a best response by Lemma A.3"). Evaluating (5) at the old profile, own old threshold included, would be a different map. Under that reading finite convergence and the p. 37 claims are false: with one type per side, $\lambda\equiv1$ , $\delta=1$ and $F$ uniform on $[0,1]$ , its iterates are rational and converge only in the limit to $2-\sqrt3$ .

Two formalizations would trivialize the goal, and both are ruled out. Uniqueness is over all real profiles, not only nonnegative ones or those reached by the iteration. The tail integrals are not allowed to vanish by default for non-integrable laws, because integrability is a hypothesis. $O(|\Theta|)$ is encoded with a constant chosen before the market.

Not formalized: the agents' Markov decision process of Appendix A.1. Consequently "this strategy profile is a Nash equilibrium", item 2 of Proposition 3.1, Lemmas A.1–A.2 and the best-response sentences of Lemma A.3 and Proposition A.4 are out of scope.

Contributions welcome: continuity and monotonicity lemmas for $a\mapsto\int_{[a,\infty)}u\,dF$ and $a\mapsto F([a,\infty))$ for atomless integrable laws, which are reusable well beyond this mission, and proofs of the milestones in any order.

Selected references

N. Immorlica, B. Lucier, V. Manshadi, A. Wei, Designing Approximately Optimal Search on Matching Platforms, Management Science, 2023; preprint arXiv:2102.09017v2, 2021. https://arxiv.org/abs/2102.09017
K. Burdett, M. G. Coles, Marriage and Class, Quarterly Journal of Economics 112(1), 1997. https://doi.org/10.1162/003355397555127

8 thms2 active usersReviewed

Completed

Algorithmic Game Theory Combinatorics Mechanism Design+1·Captain: mikedeng1

Combinatorial Auctions with Interdependent Valuations: SOS to the Rescue 3: The k-HL Mechanism Is Ex-Post IC-IR and a (k+3)-Approximation to Welfare with k Signal ValuesResearch Paper

Motivation

In many auctions a bidder's value for what she wins depends on information held by others. The value of an oil lease, a spectrum licence or a piece of art to one bidder depends on survey data, market forecasts or expert opinions that other bidders hold privately. The model of interdependent values (Milgrom and Weber, 1982) captures this: each agent $i$ holds a private signal $s_i$ , and every agent's value is a publicly known function of the whole signal profile $\mathbf s=(s_1,\dots,s_n)$ .

With interdependent values, maximizing welfare in ex-post equilibrium is impossible unless the valuations satisfy the single-crossing condition (Maskin, 1992; Dasgupta and Maskin, 2000), and even single crossing does not suffice beyond single-item auctions with single-dimensional signals. Without any condition, there are valuations for which no deterministic mechanism achieves a bounded approximation ratio and no randomized mechanism does better than a factor $n$ (Eden, Feldman, Fiat and Goldner, ACM EC 2018; Examples 1.2–1.3 of the source). Eden, Feldman, Fiat, Goldner and Karlin (arXiv:1903.08384v2, 2019) introduce submodularity over signals (SOS): raising one signal increases a value by less when the other signals are higher. They show that SOS valuations admit constant-factor, or signal-space-dependent, approximations in settings where single crossing fails, including combinatorial auctions. This mission formalizes their Theorem 6.1, the case of combinatorial auctions with single-dimensional signals taking $k$ values.

Timeline. Milgrom–Weber (1982) introduce the interdependent values model. Maskin (1992) and Dasgupta–Maskin (2000) show that single crossing makes efficient auctions truthful. Jehiel–Moldovanu (2001) show that efficient implementation fails generically with multidimensional signals. Eden–Feldman–Fiat–Goldner (2018) give approximations under a relaxed, $c$ -single-crossing condition, with ratios depending on $c$ and $n$ . Eden–Feldman–Fiat–Goldner–Karlin (2019; Mathematics of Operations Research, 2024) introduce SOS and prove Theorems 4.1, 5.1, 6.1 and 6.5.

Setting

There are $n$ agents and $m$ items, and $k\ge1$ signal values. Each agent $i$ has a signal $s_i\in\{0,1,\dots,k-1\}$ , and $\{0,\dots,k-1\}^n$ is the grid. Agent $i$ 's value for a bundle $T\subseteq[m]$ at the profile $\mathbf s$ is $v_{iT}(\mathbf s)\ge0$ ; the empty bundle is worth $0$ , and for nonempty $T$ , $v_{iT}$ is weakly increasing in every signal and strictly increasing in $s_i$ . We write $(\mathbf s_{-i},x_i)$ for the profile with agent $i$ 's signal replaced by $x$ , and $(\mathbf s_A,\mathbf 0_B)$ for the profile that keeps the signals of the agents in $A$ and sets those in $B$ to $0$ .

A function $w$ of the profile is SOS if for every coordinate $j$ , all $x,\delta\ge0$ with $x+\delta\le k-1$ , and grid profiles with $\mathbf s'_{-j}\le\mathbf s_{-j}$ coordinatewise,

w(\mathbf s_{-j},x+\delta)-w(\mathbf s_{-j},x)\;\le\;w(\mathbf s'_{-j},x+\delta)-w(\mathbf s'_{-j},x).

The setting is SOS when every $v_{iT}$ is.

A feasible allocation gives disjoint bundles $T_1,\dots,T_n$ ; its welfare at $\mathbf s$ is $\sum_i v_{iT_i}(\mathbf s)$ . A deterministic mechanism maps reported profiles to an allocation and payments. Agent $i$ 's utility is her value, at the true profile, for the bundle she receives at the reported profile, minus her payment. The mechanism is ex-post IC if truthful reporting maximizes each agent's utility whenever the others report truthfully, and ex-post IR if that utility is nonnegative. A randomized mechanism is universally ex-post IC-IR if every deterministic mechanism in its support is.

The mechanism k-HL runs, with probability $p_{RT}=\frac{k-1}{k+3}$ , Random Threshold: choose $\ell$ uniformly in $\{1,\dots,k-1\}$ , call $N_{\ge\ell}=\{i:s_i\ge\ell\}$ the high agents, allocate to them a feasible allocation maximizing $\sum_{i\in N_{\ge\ell}}v_{iS_i}(\mathbf s_{N_{<\ell}},\ell_{N_{\ge\ell}})$ , and charge agent $i$ receiving $\bar T_i$ the price $v_{i\bar T_i}(\mathbf s_{-i},s_i=\ell-1)$ . Otherwise it runs Random Sampling: split the agents uniformly at random into $A$ and $B$ , allocate to $B$ a feasible allocation maximizing $\sum_{i\in B}v_{iS_i}(\mathbf s_A,\mathbf 0_B)$ , and charge nothing. In the Lean development (namespace InterdepSOS.KHL) these are rtAlloc, rtPay, rsAlloc and khlWelfare.

Formalization targets

Goal: Theorem 6.1 (p. 20)

For SOS valuations with $k$ signal values, every Random Threshold component and every Random Sampling component is ex-post IC and IR, and for every grid profile $\mathbf s$ and every feasible allocation $T^*$ ,

\sum_i v_{iT^*_i}(\mathbf s)\;\le\;(k+3)\,\mathbb E\bigl[\text{welfare of k-HL at }\mathbf s\bigr],

where the expectation is over $\ell$ , over $(A,B)$ and over the coin choosing between the two mechanisms, and welfare is measured with true values at the truthful profile.

Milestones

Displays (6)–(7): the welfare of any allocation is at most $\mathsf{OTHER}+\mathsf{SELF}$ , where $\mathsf{OTHER}=\sum_i v_{iT_i}(\mathbf s_{-i},0_i)$ and $\mathsf{SELF}=\sum_{\ell=1}^{k-1}\sum_{i:s_i=\ell}v_{iT_i}(\mathbf 0_{-i},s_i)$ .
Random Sampling is ex-post IC-IR for every partition.
Random Threshold is ex-post IC-IR for every threshold.
Lemma 6.2: $\mathsf{SELF}\le(k-1)\,\mathbb E[\text{welfare of Random Threshold}]$ .
Lemma 6.3: $\mathsf{OTHER}\le4\,\mathbb E[\text{welfare of Random Sampling}]$ .

Significance

Theorem 6.1 is the paper's answer for general combinatorial auctions with single-dimensional signals and arbitrary bundle valuations, a setting where single crossing gives nothing and where the random-sampling technique of the single-parameter case (Theorem 4.1) is not enough on its own: Random Sampling alone covers only the contribution of the other agents' signals. The ratio $k+3$ depends on the size of the signal space but not on the number of agents or items. The same decomposition, with Random Threshold replaced by a bucketing mechanism, yields the $(2\log_2k+4)$ -approximation for strong-SOS valuations (Theorem 6.5), so milestones 1 and 5 are shared by both results.

The result is proved in the paper; no machine-checked version is known to exist. A formalization fixes the incentive argument precisely (which data the allocation may depend on, how ties are broken) and makes the uniform averages over thresholds and partitions explicit. The development reuses the Key Lemma 3.1 of the paper, which is posed in a sibling mission of this series.

Difficulty

Two points resist a direct argument. First, incentive compatibility of Random Threshold requires that a high agent who changes her report within $\{\ell,\dots,k-1\}$ leaves the allocation unchanged, and this is true only if the argmax rule sees the reports through the proxy data $(\mathbf s_{N_{<\ell}},\ell_{N_{\ge\ell}})$ alone: an argmax rule that breaks ties using the full report profile can make a high agent's bundle, and hence her utility, depend on her report. The formalization must therefore state precisely what the allocation rule may depend on. Second, the welfare bound for Random Sampling rests on the Key Lemma 3.1 (zeroing a uniformly random half of the other signals keeps, in expectation, half of an SOS value), which here has to hold on the discrete grid $\{0,\dots,k-1\}^n$ , with SOS assumed only there; the expectations over partitions and thresholds are finite averages whose bookkeeping (agents in $A$ receive nothing, agents outside $N_{\ge\ell}$ receive nothing) must match the mechanism exactly.

Formalization scope

Agents are Fin n, items Fin m, bundles Finset (Fin m), signals natural numbers with the grid condition InGrid k s. All hypotheses on valuations (nonnegativity, monotonicity, strict monotonicity in the own signal, SOS) are imposed on grid profiles only, with the shifted coordinate staying below $k$ ; a condition on all of $\mathbb N^n$ would be stronger than the paper's. The empty bundle is worth $0$ and the monotonicity clauses concern nonempty bundles. Allocations are maps Fin n → Finset (Fin m) with pairwise disjoint values; agents outside the eligible set receive $\emptyset$ .

The argmax allocations are produced by arbitrary selectors, functions of the threshold (or of $B$ ) and of the proxy profile, required to return a feasible maximizer of the proxy welfare; the theorems quantify over all such selectors. Expectations are finite uniform averages, $\frac1{k-1}\sum_{\ell=1}^{k-1}$ and $2^{-n}\sum_{B\subseteq[n]}$ , never an existential or universal quantifier over $\ell$ or $B$ . The ratio is stated against every feasible allocation, with welfare at true values, never with proxy values and never through a supremum. IC and IR are stated for every component of the mixture, with the paper's explicit payments. Random Sampling zeroes the signals of all of $B$ , the agent's own included (the page's " $v_{ij}(\mathbf s_A,\mathbf 0_B)$ " is read as $v_{iT}(\mathbf s_A,\mathbf 0_B)$ ). For $k=1$ , $p_{RT}=0$ and the threshold average is the empty sum.

Lemmas 6.2 and 6.3 and displays (6)–(7) are stated for every feasible allocation (every assignment, for (6)–(7)), which is stronger than the paper's statements for a welfare-maximizing $T^*$ .

Needed infrastructure: the Key Lemma 3.1 on the discrete grid, finite averages over subsets, and a lemma that a maximizer over a subfamily of allocations dominates any restriction of a feasible allocation. Contributions of proofs of the milestones in any order are welcome; the IC-IR milestones are independent of the welfare milestones.

The source is the arXiv preprint arXiv:1903.08384v2; the Mathematics of Operations Research (2024) version is not the cited source, and its numbering may differ.

Selected references

A. Eden, M. Feldman, A. Fiat, K. Goldner, A. R. Karlin, Combinatorial Auctions with Interdependent Valuations: SOS to the Rescue, arXiv:1903.08384v2, 2019. https://arxiv.org/abs/1903.08384v2
A. Eden, M. Feldman, A. Fiat, K. Goldner, Interdependent Values without Single-Crossing, ACM EC 2018 (cited as [Eden et al., 2018] in the source).
E. Maskin, Auctions and Privatization, in H. Siebert (ed.), Privatization, 1992 (cited as [Maskin, 1992] in the source).
P. Milgrom, R. Weber, A Theory of Auctions and Competitive Bidding, Econometrica 50(5), 1982. https://doi.org/10.2307/1911865
P. Dasgupta, E. Maskin, Efficient Auctions, Quarterly Journal of Economics 115(2), 2000. https://doi.org/10.1162/003355300554737
P. Jehiel, B. Moldovanu, Efficient Design with Interdependent Valuations, Econometrica 69(5), 2001. https://doi.org/10.1111/1468-0262.00248

9 thms2 active usersReviewed

Algorithmic Game Theory Economics·Captain: mikedeng1

Algorithms for Competitive Division of Chores 2: Indivisible Chores Always Admit a Pareto Optimal Allocation That Is Both Weighted-EF^1_1 and Weighted-Prop1Research Paper

Motivation

Many allocation problems distribute chores: tasks, shifts, teaching duties or cleaning rotas that every recipient would rather avoid. Agents often have unequal obligations, for example a full-time and a part-time worker, and a fair division should respect these entitlements. When the tasks can be split (time shares, probabilities), the competitive rule of Bogomolnaia, Moulin, Sandomirskiy and Yanovskaya (Econometrica 2017) is the standard answer: chores are priced, each agent must "earn" a prescribed amount by taking on chores, and each takes the least unpleasant bundle that earns it. The resulting allocation is efficient and envy-free with respect to the entitlements.

Most chores cannot be split. Then exact envy-freeness or proportionality may be impossible (for instance with fewer chores than agents), and the literature asks for relaxations "up to one chore". For goods, Barman and Krishnamurthy (AAAI 2019) showed how to round a competitive allocation into an indivisible one that is Pareto efficient and approximately fair. Brânzei and Sandomirskiy (arXiv:1907.01766v2, §7; Mathematics of Operations Research, 2024) transfer this rounding to chores with arbitrary weights. This mission formalizes that result, Theorem 34 of the paper.

Setting

There are $n$ agents and $m$ chores. A bundle is a vector $x\in\mathbb R^m_{\ge0}$ ; an allocation is a matrix $z=(z_{i,j})\ge0$ , agent $i$ receiving the bundle $z_i$ ; it is feasible if $\sum_i z_{i,j}=1$ for every chore $j$ . Values form a matrix $v\in\mathbb R^{n\times m}_{<0}$ , and agent $i$ 's utility is additive, $u_i(x)=\sum_j v_{i,j}x_j$ . The utility profile of $z$ is $u(z)=(u_1(z_1),\dots,u_n(z_n))$ , and $\mathcal U(v)$ is the set of utility profiles of feasible allocations.

At prices $p\in\mathbb R^m_{<0}$ a bundle costs $p(x)=\sum_j p_jx_j$ . Given budgets $b\in\mathbb R^n_{<0}$ , a feasible allocation $z$ is competitive at $p$ (Definition 3) if every agent's bundle satisfies $p(z_i)\le b_i$ and maximizes $u_i$ among all bundles $x\ge0$ with $p(x)\le b_i$ . It is Pareto optimal (Definition 5) if no feasible allocation makes every agent weakly and some agent strictly better off; the Pareto frontier $\mathcal U^*(v)$ is the set of their utility profiles. The Nash social welfare of $z$ is $\prod_i|u_i(z_i)|^{|b_i|}$ .

An allocation is indivisible if every $z_{i,j}\in\{0,1\}$ ; then $z_i$ is identified with a set of chores, and $u_i(S)=\sum_{j\in S}v_{i,j}$ . Fix weights $\beta\in\mathbb R^n_{>0}$ .

Weighted-EF¹₁ (Definition 32): for all agents $i$ with $z_i\neq\emptyset$ and $i'$ there are $j\in z_i$ and $j'\in[m]$ with $u_i(z_i\setminus\{j\})/\beta_i\ \ge\ u_i(z_{i'}\cup\{j'\})/\beta_{i'}$ .
Weighted-Prop1 (Definition 33): for each agent $i$ with $z_i\ne\emptyset$ there is $j\in z_i$ with $u_i(z_i\setminus\{j\})/\beta_i\ \ge\ u_i([m])/\sum_{i'}\beta_{i'}$ .

Formalization targets

Goal: Theorem 34

For every $v\in\mathbb R^{n\times m}_{<0}$ and $\beta\in\mathbb R^n_{>0}$ there is an indivisible allocation $z$ with

u(z)\in\mathcal U^*(v),\qquad z\ \text{weighted-EF}^1_1,\qquad z\ \text{weighted-Prop1}.

Pareto optimality is in the divisible problem: $z$ is compared with all fractional allocations.

Milestones

Existence (§2.3, p. 14): for $v<0$ , $b<0$ a competitive allocation exists, and one maximizes the Nash social welfare over all Pareto optimal allocations.
Cycle elimination (proof of Theorem 35, pp. 37–38): a competitive allocation at prices $p$ can be replaced by one with the same utility profile and an acyclic consumption graph, competitive at the same $p$ and $b$ .
Theorem 35 (p. 37): a competitive allocation at prices $p$ rounds to an indivisible allocation competitive at the same $p$ for budgets $b'\le0$ with

b_i-|p_j|\le b'_i\le b_i+|p_{j'}|\quad(j\in z'_i)\qquad\text{or}\qquad b_i<b'_i=0<b_i+|p_{j'}|\ \text{ if } z'_i=\emptyset.

The weighted-EF¹₁ step (pp. 38–39): for an indivisible competitive allocation, the price inequalities $\sum_{c\in z'_i\setminus\{j\}}p_c\ge-\beta_i$ and $\sum_{c\in z'_{i'}\cup\{j'\}}p_c\le-\beta_{i'}$ imply inequality (10).
The weighted-Prop1 step (p. 39): if in addition all chores together cost $-\sum_i\beta_i$ , the first price inequality implies (11).

The proof also uses two results of the paper that are formalized in the companion mission Algorithms for Competitive Division of Chores 1: the First welfare theorem (Theorem 9, item 1, p. 14) and the characterization of competitive allocations by minimum pain-per-buck chores (Lemma 36, p. 50). They will be linked as reference milestones once published.

Significance

Theorem 34 says that weighted envy-freeness up to one chore, weighted proportionality up to one chore and Pareto efficiency are compatible for indivisible chores with arbitrary entitlements. Envy-freeness alone can be achieved by simple procedures, but those allocations are typically inefficient; the theorem shows that efficiency need not be given up. Its proof produces the allocation from a divisible competitive allocation, which makes the competitive rule a single source for both divisible and indivisible fair division of chores. The paper also gives a strongly polynomial algorithm when $n$ or $m$ is fixed; that part is not in scope here.

The result is proved in the paper, partly by reference to Barman and Krishnamurthy for goods and to Bogomolnaia et al. for existence. No machine-checked version of it, of the competitive rule for chores, or of the rounding procedure is known to exist. The formalization would make all three available, and would make the deduction of Theorem 34 from Theorem 35 precise: as written, that deduction needs a chore $j'$ outside agent $i'$ 's bundle, which the statement of Theorem 35 does not provide.

Difficulty

The main obstacle is existence. For goods, competitive allocations maximize the Nash social welfare over the whole feasible set, a convex program. For chores the set of competitive allocations can be disconnected; their utility profiles lie on the Pareto frontier and are critical points of Nash welfare on the feasible utility set. Maximizing the Nash welfare over the feasible set does not characterize all of them, and the frontier itself has to be handled as a polyhedral surface.

The rounding is combinatorial: it needs an acyclic consumption graph, a forest of agents and chores, which is traversed from roots to leaves. The bounds (12) and (13) come from an invariant of that traversal, not from a local exchange argument.

Formalization scope

Agents are Fin n and chores Fin m, both 0-based. Values v : Fin n → Fin m → ℝ and budgets b : Fin n → ℝ carry the sign hypotheses v i j < 0, b i < 0 in each theorem, not in the definitions, because Theorem 35 applies Definition 3 to budgets $b'\le0$ . Competitiveness at prices $p$ requires $p<0$ , the budget constraint $p(z_i)\le b_i$ and optimality among all bundles in $\mathbb R^m_{\ge0}$ within the budget. An indivisible feasible allocation is a map σ : Fin m → Fin n, its 0/1 matrix is indicator σ, and bundles are Finsets. Graphs are edge sets Finset (Fin n × Fin m); acyclic means no simple cycle with at least two agents. Weights are arbitrary positive reals, never normalized.

Added hypotheses: $0<n$ in the goal (with no agents and $m\ge1$ chores no allocation exists), and $0<n$ , $0<m$ in the existence milestone (with $m=0$ no bundle meets a negative budget). The running-time statements of Theorems 34 and 35 are not formalized.

The trivializing readings are excluded: competitiveness always includes the budget constraint; values and budgets are strictly negative, not non-negative; Pareto optimality of the goal is with respect to all fractional allocations, not only indivisible ones; and (10) ranges over all ordered pairs of agents and all chores $j'$ .

A complete development needs the existence theorem for chores (via the critical-point characterization of Theorem 7 or a fixed-point argument), the minimum pain-per-buck characterization of competitive allocations, cycle elimination in consumption graphs, and the forest traversal of Algorithm 3. The definitions of competitive allocations, Pareto frontier and weighted EF¹₁/Prop1 are shared with the companion mission and reusable for other fair-division results. Proofs of any milestone, and alternative proofs of the existence theorem, are welcome.

Selected references

S. Brânzei and F. Sandomirskiy, Algorithms for Competitive Division of Chores, arXiv:1907.01766v2, 2023; Mathematics of Operations Research, 2024. https://arxiv.org/abs/1907.01766v2
A. Bogomolnaia, H. Moulin, F. Sandomirskiy and E. Yanovskaya, Competitive division of a mixed manna, Econometrica 85(6), 2017. https://doi.org/10.3982/ECTA14564
A. Bogomolnaia, H. Moulin, F. Sandomirskiy and E. Yanovskaya, Dividing bads under additive utilities, Social Choice and Welfare 52, 2019. https://doi.org/10.1007/s00355-018-1157-x
S. Barman and S. K. Krishnamurthy, On the proximity of markets with integral equilibria, AAAI 2019. https://doi.org/10.1609/aaai.v33i01.33011748
V. Conitzer, R. Freeman and N. Shah, Fair public decision making, ACM EC 2017 (proportionality up to one item). https://doi.org/10.1145/3033274.3085125

11 thms2 active usersReviewed

Completed

Algorithmic Game Theory Linear Optimization Optimization·Captain: mikedeng1

Quantum Algorithms for Zero-Sum Games 2: The Value of a Zero-Sum Game, Known to Error ε/(6R(r+1)), Decides Whether an LP Has OPT < α or OPT ≥ α − εResearch Paper

Linear programs as zero-sum games

Linear programming and two-player zero-sum matrix games are two faces of one theory. Von Neumann's minimax theorem is a statement of LP duality, and conversely, since Dantzig's 1951 note, every linear program can be rewritten as a zero-sum game. The equivalence matters in practice whenever an algorithm is much better at one of the two problems. Game solvers based on multiplicative weights and sampling, such as the randomized algorithm of Grigoriadis and Khachiyan (GK95), approximate the value of an $n\times m$ game in time sublinear in the size of the matrix. Carmon, Duchi, Sidford and Tian (arXiv:1903.02675) and van Apeldoorn and Gilyén (arXiv:1904.03180) use such game solvers, classical or quantum, as linear-programming solvers. For that to work, the reduction from a linear program to a game must be explicit, with the exact error budget that the game solver has to meet.

This mission formalizes that reduction as it is stated in §4 of van Apeldoorn and Gilyén (2019), Lemma 12 (p. 14). The paper uses it to turn its quantum zero-sum game solvers into quantum LP solvers with cubic dependence on $R(r+1)/\varepsilon$ (Theorem 13, p. 15).

Setting

The linear program. Let $A \in \mathbb R^{n\times m}$ , $b \in \mathbb R^m$ and $c \in \mathbb R^n$ . The primal LP (4) and its dual (5) are

\max_{y \in \mathbb R^m}\ \{\, b^{\mathsf T}y : Ay \le c,\ y \ge 0 \,\}, \qquad \min_{x \in \mathbb R^n}\ \{\, c^{\mathsf T}x : A^{\mathsf T}x \ge b,\ x \ge 0 \,\}.

The paper's standing assumptions (p. 12) are:

every entry of $A$ , $b$ and $c$ lies in $[-1,1]$ ;
a constant $R > 0$ is known such that adding $\sum_j y_j \le R$ to the primal does not change its optimal value, and $|c_i| \le R$ for every $i$ ;
a constant $r$ is known such that adding $\sum_i x_i \le r$ to the dual does not change its optimal value. The two optimal values coincide, and $\mathrm{OPT}$ denotes the common value.

The game. In a zero-sum game with payoff matrix $M$ , the column player picks a mixed strategy $y$ in the standard simplex $\Delta = \{y \ge 0 : \sum_k y_k = 1\}$ , and the row player picks the row with the largest payoff. The value of the game (LP (1), p. 2) is

\lambda^*(M) = \min_{y \in \Delta}\ \max_i\ (My)_i .

The reduction. Fix a threshold $\alpha$ . With $e$ the all-ones vector of length $m$ , the game matrix (6) acts on the variables $(y, z, h)$ (the original variables, one slack variable and one homogenizing variable):

A''' = \begin{pmatrix} e^{\mathsf T} & 1 & -1 \\ -e^{\mathsf T} & -1 & 1 \\ -b^{\mathsf T} & 0 & \alpha/R \\ A & 0 & -c/R \end{pmatrix}.

Write $\lambda^* = \lambda^*(A''')$ for its value, and set the error level $\varepsilon''' = \varepsilon/(6R(r+1))$ .

Formalization targets

Goal: Lemma 12

For every $\varepsilon > 0$ , every threshold $\alpha$ with $|\alpha| \le R$ , and every estimate $\tilde\lambda$ with $|\tilde\lambda - \lambda^*| \le \varepsilon'''$ ,

\tilde\lambda > \varepsilon''' \implies \mathrm{OPT} < \alpha, \qquad \tilde\lambda \le \varepsilon''' \implies \mathrm{OPT} \ge \alpha - \varepsilon .

This is the paper's "finding the optimal value $\lambda^*$ of the game (6) up to additive error $\varepsilon'''$ suffices to correctly conclude either $\mathrm{OPT} < \alpha$ or $\mathrm{OPT} \ge \alpha - \varepsilon$ ", with the decision rule its proof uses.

The two cases (milestones)

The goal splits into the two exact implications of the proof:

\lambda^* > 0 \implies \mathrm{OPT} < \alpha, \qquad\qquad \lambda^* \le 2\varepsilon''' \implies \mathrm{OPT} \ge \alpha - \varepsilon .

The milestones follow the printed proof, all on p. 14:

the explicit strategy $\hat y$ built from a primal point with objective at least $\alpha$ ;
the first case;
the existence of a strategy that attains the value;
the bound $|h - 1/2| \le \varepsilon'''$ ;
the approximate feasibility and optimality bounds (7)–(8);
weak duality with relaxed constraints;
the second case.

Significance

The result. Lemma 12 is the bridge that makes any approximate zero-sum game solver an approximate LP solver. It turns the question "is $\mathrm{OPT} \ge \alpha$ ?" into a single approximate value computation, and binary search over $\alpha \in [-R, R]$ (p. 12) then locates $\mathrm{OPT}$ to additive error $\varepsilon$ . The constant $6R(r+1)$ is the price of the reduction. It fixes how accurately the game must be solved, and therefore the $(R(r+1)/\varepsilon)^3$ and $(R(r+1)/\varepsilon)^{3.5}$ factors of Theorem 13. The same reduction appears, in other forms, in classical sublinear LP solvers.

Formalizing it. The lemma is proved in the paper; this mission produces a machine-checked version with every constant explicit. That is not a formality here. As printed, the second row of (6) is $(-e^{\mathsf T}, 1, 1)$ , and with that row the lemma is false: for $n = m = 1$ , $A = 1$ , $c = 1$ , $b = -1$ , $R = 1$ , $r = 0$ and $\alpha = 0$ , one has $\mathrm{OPT} = 0 \ge \alpha$ but $\lambda^* > 0$ . The derivation on p. 13 gives $(-e^{\mathsf T}, -1, 1)$ , which the mission uses. Step (7) of the proof is written for $\alpha \ge 0$ and needs $|\alpha| \le R$ in general. The mission states the lemma with both repairs, so that later LP-solver formalizations can cite an exact statement. To our knowledge no machine-checked version of this reduction exists.

Difficulty

Each step is elementary, and the difficulty is bookkeeping. The game value is an infimum over the simplex, and the second case needs a strategy that actually attains it, or an approximation argument with slack. The homogenizing variable $h$ is pinned only approximately: an approximately optimal strategy satisfies $h \approx 1/2$ only up to $\varepsilon'''$ . That error is multiplied by $\alpha/R$ and $c_i/R$ , whose signs are arbitrary, so the inequalities that look natural for nonnegative data fail for negative $\alpha$ or $c_i$ . The relaxed constraints then pass through weak duality, where the dual bound $r$ enters, and the errors have to add up to exactly $\varepsilon$ . A reading with $\alpha \ge 0$ would cover only half of the binary search.

Formalization scope

Data. $A$ is Matrix (Fin n) (Fin m) ℝ, $b$ is Fin m → ℝ and $c$ is Fin n → ℝ: constraints are indexed by Fin n and variables by Fin m, as in (4). The paper's index letters in §4 vary.
Standing assumptions. A structure LPStanding A b c R r OPT collects them:
- entries of $A$ , $b$ , $c$ in $[-1,1]$ ;
- $R > 0$ and $|c_i| \le R$ ;
- $\mathrm{OPT}$ bounds every primal feasible objective and is attained by a primal feasible $y$ with $\sum_j y_j \le R$ ;
- $\mathrm{OPT}$ is attained by a dual feasible $x$ with $\sum_i x_i \le r$ .
The last item is the paper's assumption of strong duality, in the form its proof uses. It is a hypothesis, not a theorem to derive.
The game. The matrix (6) has rows Fin 2 ⊕ (Unit ⊕ Fin n) and columns Fin m ⊕ Fin 2 (with $z$ = inr 0 and $h$ = inr 1), and its second row is the corrected $(-e^{\mathsf T}, -1, 1)$ .
The value. The value is sInf of the image of stdSimplex under $y \mapsto \max_i (My)_i$ . It is not an infimum over a membership proposition, which in Lean would return $\min(0, \lambda^*)$ and make the first case vacuous. LP (1)'s side constraint $\lambda \in [-1, 1]$ is omitted because it is inactive for entries in $[-1, 1]$ .
Constants. $\varepsilon''' = \varepsilon/(6R(r+1))$ exactly, with $\varepsilon > 0$ .
Added hypothesis. $|\alpha| \le R$ is the one hypothesis not written in the lemma. §4 supplies it through the binary search range, and through the requirement that (6) be a game with entries in $[-1,1]$ .

Trivializing formalizations are ruled out. LPStanding is satisfiable, the second row forces $\sum_j y_j + z = h$ , the value is not junk on a positive game, and the goal is stated for every estimate within $\varepsilon'''$ rather than only at $\lambda^* = 0$ . A sanity file checks the first three on small instances.

Infrastructure. Everything is built from Mathlib's stdSimplex, Matrix.mulVec and dotProduct. The attainment of the value of a finite matrix game (milestone exists_strategy_le) and weak duality with relaxed constraints are reusable beyond this mission. Proofs of any milestone are welcome, and so are alternative proofs of the second case that avoid attainment by a slack argument.

Selected references

J. van Apeldoorn and A. Gilyén, Quantum algorithms for zero-sum games, arXiv:1904.03180v1, 2019. https://arxiv.org/abs/1904.03180
M. D. Grigoriadis and L. G. Khachiyan, A sublinear-time randomized approximation algorithm for matrix games, Operations Research Letters 18(2):53–58, 1995. https://doi.org/10.1016/0167-6377(95)00032-0
Y. Carmon, J. C. Duchi, A. Sidford and K. Tian, A rank-1 sketch for matrix multiplicative weights, arXiv:1903.02675, 2019. https://arxiv.org/abs/1903.02675
G. B. Dantzig, A proof of the equivalence of the programming problem and the game problem, in T. C. Koopmans (ed.), Activity Analysis of Production and Allocation, Wiley, 1951, pp. 330–335.
I. Adler, The equivalence of linear programs and zero-sum games, International Journal of Game Theory 42(1):165–177, 2013. https://doi.org/10.1007/s00182-012-0328-8

10 thms2 active usersReviewed

Completed

Graph Theory Operations Research Probability·Captain: mikedeng1

Load Balancing Under Strict Compatibility Constraints 2: Random Graphs with Server Degree c(N) → ∞ and Nc(N)/(M(N) ln N) → ∞ Are Almost Surely Proportionally Sparse and SubcriticalResearch Paper

Motivation

In large data centres, an incoming task often cannot run on every server: its data, software or licences sit on only some of the machines. Such strict compatibility constraints are modelled by a bipartite graph between task types (dispatchers) and servers. For the fully flexible system, in which every task can go to every server, the JSQ( $d$ ) policy (sample $d$ servers at random and join the shortest queue) is described in the large-system limit by the mean-field ODE of Vvedenskaya, Dobrushin and Karpelevich (1996) and Mitzenmacher (1996). Rutten and Mukherjee (arXiv:2008.07562, Math. Oper. Res. 2023) identify two graph conditions, proportional sparsity and subcriticality, under which JSQ( $d$ ) on a sparse compatibility graph has the same mean-field limit and the same steady state as the fully flexible system (their Theorem 3.4).

The two conditions are useful in system design only if there are natural graph families that satisfy them. A storage designer controls the server degree: the number of task types a server can process is roughly proportional to the data it must store. Theorem 3.5 of the paper answers this design question for random graphs. If every server stores data for $c(N)$ task types chosen uniformly at random, then $c(N)\to\infty$ together with a mild density condition suffices, even when $c(N)$ is negligible compared with the number $M(N)$ of task types. This mission formalizes Theorem 3.5's graph-theoretic content and the chain of lemmas in Appendix A that proves it.

Setting

A system with $N$ servers $V_N=\{1,\dots,N\}$ and $M(N)$ dispatchers $W_N=\{1,\dots,M(N)\}$ has a compatibility graph $G_N=(V_N,W_N,E_N)$ with $E_N\subseteq V_N\times W_N$ . The neighbourhood of a dispatcher $w$ is $\mathcal N_w=\{v:(v,w)\in E_N\}$ ; that of a server $v$ is $\mathcal N_v=\{w:(v,w)\in E_N\}$ .

Proportional sparsity (Definition 3.1): for every $\varepsilon>0$ ,

\sup_{U\subseteq V_N}\Big|\Big\{w\in W_N:\Big|\tfrac{|\mathcal N_w\cap U|}{|\mathcal N_w|}-\tfrac{|U|}{N}\Big|\ge\varepsilon\Big\}\Big|\Big/M(N)\to0 .

In words, for every set $U$ of servers, all but a vanishing fraction of the dispatchers see $U$ in roughly the proportion $|U|/N$ .

Subcriticality (Definition 3.3) with sample size $d\ge2$ : there are probability distributions $\gamma^U_w$ on the sets $U\subseteq V_N$ such that

\limsup_{N\to\infty}\max_{v\in V_N}\frac{N}{M(N)}\sum_{w\in W_N}\binom{|\mathcal N_w|}{k_w}^{-1}\sum_{U\subseteq\mathcal N_w,\ |U|=k_w}\gamma^U_w(v)\le1,\qquad k_w=\min(d,|\mathcal N_w|).

Think of a static policy that routes a task arriving at $w$ to a server in a sampled set $U$ according to $\gamma^U_w$ . The condition says that no server receives more than its fair share of load. Its uniform-weight special case is condition (A.19):

\limsup_{N\to\infty}\max_{v\in V_N}\frac{N}{M(N)}\sum_{w\in W_N}\frac{\mathbb 1\{(v,w)\in E_N\}}{|\mathcal N_w|}\le1 .

The random graph. Let $1\le c(N)\le M(N)$ . For each $N$ , each server independently chooses its neighbourhood $\mathcal N_v$ uniformly among the $c(N)$ -subsets of $W_N$ , so every server has degree exactly $c(N)$ . All graphs live on one probability space, but only the law of each $G_N$ is prescribed; the joint law across different $N$ is arbitrary.

Formalization targets

Goal: Theorem 3.5 (graph part)

If $c(N)\to\infty$ and $Nc(N)/(M(N)\ln N)\to\infty$ , then almost surely

\{G_N\}_{N\ge1}\ \text{is proportionally sparse}\quad\text{and}\quad\{G_N\}_{N\ge1}\ \text{satisfies the subcriticality condition.}

Milestones, in the order of the proof in Appendix A

Lemma A.1. If $X_N\sim\mathrm{Bin}(N,p(N))$ and $p(N)\to0$ , then for each $\delta\in(0,1/2)$ there are $N_0\ge1$ and $a>0$ with $\mathbb P(X_N\ge\delta N)\le(a\,p(N)^\delta)^N$ for $N\ge N_0$ .
Lemma A.2. Let $B_N(X)$ be the set of servers whose number of neighbours in $X$ deviates from $c(N)|X|/M(N)$ by at least $\varepsilon c(N)|X|/M(N)$ . If $c(N)\to\infty$ and $Nc(N)/M(N)\to\infty$ , then for $0<\varepsilon\le3/2$ , $0<\delta<1/2$ and $\eta>0$ , almost surely eventually $|B_N(X)|\le\delta N$ for all $X$ with $|X|\ge\eta M(N)$ .
Lemma A.3. Under the same growth conditions, almost surely eventually at most $\delta M(N)$ dispatchers have $|\mathcal N_w|\le(1-\varepsilon)Nc(N)/M(N)$ .
Proposition A.4. Under the same growth conditions, $\{G_N\}$ is proportionally sparse almost surely.
(A.19) reduction (p. 34). For any graph sequence, (A.19) implies subcriticality.
Lemma A.5. If $Nc(N)/(M(N)\ln N)\to\infty$ , then $\{G_N\}$ satisfies (A.19) almost surely.

Significance

The result. Theorem 3.5 shows that the performance of the fully flexible JSQ( $d$ ) system, in the mean-field limit and in steady state, can be achieved with a server degree $c(N)$ that grows arbitrarily slowly. The only requirement is that each dispatcher's mean degree $Nc(N)/M(N)$ grow faster than $\ln N$ . Each server then needs to store data for only $c(N)$ task types, a vanishing fraction of the $M(N)$ types. The $\ln N$ threshold matches the scale below which some dispatchers have too few neighbours to share the load evenly.

Formalizing it. The result is proved in the paper, and no part of it has been machine-checked. The mission produces reusable statements about random bipartite graphs with fixed left degree: hypergeometric concentration over all large dispatcher sets, the degree lower tail, and a Borel–Cantelli argument without independence across $N$ . It also produces a deterministic reduction from subcriticality to (A.19). That reduction is shared with Theorem 3.6 of the same paper (inhomogeneous random graphs). The printed proof of Lemma A.5 has a gap: (A.23) bounds the probability that some dispatcher has low degree by $N^{1-a^2/2}$ , but the union over $M(N)$ dispatchers gives $M(N)N^{-a^2/2}$ . This is not summable when $M(N)$ grows faster than every polynomial, which the hypotheses allow. A complete formal proof must close this gap or show that low-degree dispatchers contribute too little to matter.

Difficulty

Every statement is almost sure along the whole sequence, but the graphs for different $N$ may be coupled arbitrarily, so no strong law over $N$ is available. Each a.s. claim needs a failure probability that is summable in $N$ , followed by the first Borel–Cantelli lemma. Proportional sparsity quantifies over all $2^N$ server sets $U$ , and Lemma A.2 over all $2^{M(N)}$ dispatcher sets $X$ . The obvious argument would concentrate each $|\mathcal N_w\cap U|$ separately and take a union bound. It fails because $|\mathcal N_w|$ is only of order $Nc(N)/M(N)$ , which may be far smaller than $N$ and $M(N)$ , so per-dispatcher tails cannot absorb an $e^{N}$ or $e^{M(N)}$ union. Uniform control over all large sets $X$ (Lemma A.2) is therefore the crux. For subcriticality, the difficulty is that the maximum over $v$ runs over $N$ servers while the minimum degree runs over $M(N)$ dispatchers.

Formalization scope

Servers are Fin N, dispatchers Fin (M N); a graph is a Finset (Fin N × Fin (M N)), and a random graph is a measurable random adjacency matrix Fin N → Fin (M N) → Bool (the space $\{0,1\}^{N\times M(N)}$ of p. 13).
The law of each random matrix is prescribed pointwise: every matrix with all row sums equal to $c(N)$ has probability $\binom{M(N)}{c(N)}^{-N}$ . This is the uniform, independent-over-servers choice. No independence across $N$ is assumed. A formalization that assumes independent graphs for different $N$ proves a weaker theorem.
Hypotheses $1\le c(N)\le M(N)$ for every $N$ , $d\ge2$ , and the growth conditions as real limits (Tendsto … atTop atTop). $\ln N$ is Real.log, so the ratio is $0$ at $N=1$ , which does not affect a limit.
Proportional sparsity is the limit condition (3.1) as "for every $\varepsilon,\delta>0$ , eventually, for every $U$ , at most $\delta M(N)$ bad dispatchers". The connectivity in Definition 3.1 is not included, because the random graphs are disconnected for small $N$ . A dispatcher with $|\mathcal N_w|=0$ gives the ratio $0/0=0$ in Lean.
Subcriticality constrains $\gamma^U_w$ only for nonempty $U$ and normalises by $\binom{|\mathcal N_w|}{\min(d,|\mathcal N_w|)}$ . The paper's $\binom{|\mathcal N_w|}{d}$ is $1/0$ when $|\mathcal N_w|<d$ , and the empty $U$ admits no distribution. With the literal definition the goal would be false. Both " $\limsup\le1$ " conditions are written as "for every $\varepsilon>0$ , eventually at most $1+\varepsilon$ ".
Not formalized: the sentence "Consequently, the conclusions of Theorem 3.4 hold", which composes this mission's goal with the mean-field mission of this series.
Infrastructure that is welcome and reusable: hypergeometric and binomial Chernoff bounds in a form usable with Finset.powersetCard, and Borel–Cantelli for eventually-uniform statements over families of finite sets.

Selected references

D. Rutten and D. Mukherjee, Load Balancing Under Strict Compatibility Constraints, Math. Oper. Res., 2023; arXiv:2008.07562v2. https://arxiv.org/abs/2008.07562
A. Budhiraja, D. Mukherjee and R. Wu, Supermarket model on graphs, Ann. Appl. Probab. 29(3):1740–1777, 2019. https://doi.org/10.1214/18-AAP1437
M. Bramson, Stability of join the shortest queue networks, Ann. Appl. Probab. 21(4):1568–1625, 2011. https://doi.org/10.1214/10-AAP726
S. Janson, T. Łuczak and A. Ruciński, Random Graphs, Wiley, 2000. https://doi.org/10.1002/9781118032718
N. D. Vvedenskaya, R. L. Dobrushin and F. I. Karpelevich, Queueing system with selection of the shortest of two queues: an asymptotic approach, Probl. Inf. Transm. 32(1):15–27, 1996.
M. Mitzenmacher, The power of two choices in randomized load balancing, IEEE Trans. Parallel Distrib. Syst. 12(10):1094–1104, 2001. https://doi.org/10.1109/71.963420

10 thms2 active usersReviewed

Completed

Economics Operations Research Optimization·Captain: mikedeng1

Revenue Management in Crowdfunding 2: Optimal Pledge Level and Campaign Duration When Each Backer Type Shares One Valuation and Herding Is WeakResearch Paper

Motivation

On reward-based crowdfunding platforms such as Kickstarter, a project creator fixes two numbers before launch: the pledge level $p$ , the amount a backer commits, and the campaign duration $T$ . Both are set once and cannot be revised. A higher pledge earns more per backer but turns away backers whose valuation falls short, and a longer campaign reaches more backers but makes them wait longer for a project they value less the further away its delivery is. Zhang, Savin and Veeraraghavan (Revenue Management in Crowdfunding, Manufacturing & Service Operations Management, 2022; manuscript SSRN 3065267) model this trade-off with two kinds of backers. Independent backers decide on their own valuation. Herding backers arrive in proportion to the pledges already collected, so early success attracts more pledges. The paper asks when the creator should exploit herding and when it should ignore it.

This mission formalizes the paper's answer in the simplest setting it treats: every independent backer values the project at the same $v_i$ , and every herding backer at the same $v_h$ .

Setting

A campaign has a population $\hat I>0$ of independent backers, who arrive at rate $k>0$ times the number still to come. Every backer discounts the project's value at rate $r>0$ : a backer arriving at time $t$ with valuation $v$ pledges if and only if $v e^{-r(T-t)}\ge p$ . Herding backers arrive at time $t$ at rate $\Lambda_h q p$ times the number of pledges so far, where $\Lambda_h\ge0$ is an arrival rate and $q\ge0$ a propensity to pledge, and they pledge under the same discounted-value rule. Valuations lie in $[0,\bar v]$ and enter only through the survival functions $\bar F_i=1-F_i$ and $\bar F_h=1-F_h$ of the two valuation laws.

The paper solves the pledging dynamics in closed form (its Propositions 1 and 2). The numbers of pledging independent and herding backers at time $t$ are

n^p_i(t,p,T)=k\hat I\int_0^t e^{-kx}\bar F_i\big(pe^{r(T-x)}\big)\,dx,

n^p_h(t,p,T)=\Lambda_hqp\,k\hat I\int_0^t e^{\Lambda_hqp\int_\tau^t\bar F_h(pe^{r(T-u)})du}\,\bar F_h\big(pe^{r(T-\tau)}\big)\int_0^\tau e^{-kx}\bar F_i\big(pe^{r(T-x)}\big)dx\,d\tau .

The total number of pledges is $n(p,T)=n^p_i(T,p,T)+n^p_h(T,p,T)$ , and the creator's problem (18) is

\max\ \pi(p,T)=p\,n(p,T)\quad\text{over}\quad 0<p\le\bar v,\ \ 0\le T\le\tfrac1r\ln(\bar v/p).

With identical valuations, $\bar F_i(y)=1$ for $y<v_i$ and $0$ for $y\ge v_i$ , and likewise $\bar F_h$ with $v_h$ , where $0<v_i,v_h\le\bar v$ . Proposition 6 adds the constraint $T\le\frac1r\ln(v_i/p)$ , under which every independent backer pledges from the start.

Formalization targets

Goal: Proposition 6(ii)

Let $\Lambda_h,q>0$ , $v_i>v_h$ , and set $\delta=\Lambda_hqv_h/r$ , $a=k/(\Lambda_hq)$ , $b=\Lambda_hq/r$ and

X=e^{bv_h/e}\frac1{4a}\Big(\frac kr v_he^{-2}+0.5\,bv_h^2e^{-3}+2a+v_h\Big)+\frac1a\Big(\frac kr(v_h+a)+a\Big).

If $\delta<1$ and $v_i/v_h>(X/(1-\delta))^{r/k}$ , then on Proposition 6's feasible set the unique maximizer of $\pi$ is

p^*=v_i\Big(\frac r{k+r}\Big)^{r/k},\qquad T^*=\frac1r\ln\frac{v_i}{p^*}.

Milestones

Corollary 1. If $0<p\le\min(v_ie^{-rT},v_h)$ , then for $t\in[0,T]$ , $n^p_i(t,p,T)=\hat I(1-e^{-kt})$ and $n^p_h$ equals the explicit formula (15).
Proposition 3(b). If $\Lambda_hqv_h/r<1$ and $k/r>2$ , then for every sufficiently long fixed duration $T$ , the unique optimal pledge level on (18)'s range is $p^*(T)=v_ie^{-rT}$ .
Proposition 6(i). If $v_i\le v_h$ , an optimal campaign exists on Proposition 6's feasible set, and every optimum has $p^*\ge v_i/e$ and $T^*\le 1/r$ .

Significance

Proposition 6 separates two regimes. When herding backers value the project at least as much as independent ones, the optimal campaign is short, $T^*\le1/r$ , and its pledge is at least $v_i/e$ . When herding is weak ( $\delta<1$ ) and independent backers value the project enough more than herding ones, the creator's best response is to price herding backers out entirely and run the campaign that would be optimal if no herding backer existed. The threshold (33) quantifies "enough more". Together with Proposition 3(b), which fixes the duration and finds that the optimal pledge sits exactly at the highest level that keeps every independent backer in from the start, these results give a creator explicit rules rather than a numerical optimization.

The paper states that the proofs of Propositions 3 to 7 are in an online Technical Appendix, which is not part of the manuscript this mission cites; the manuscript's own Appendix proves only Propositions 1 and 2 and Corollaries 1 and 2. None of the results has a machine-checked proof. Formalizing Proposition 6(ii) would supply a verified proof of a result whose published proof is not in the source held here, and would check the threshold (33), whose grouping of terms is read off the typeset page.

Difficulty

The objective $\pi$ is defined through nested integrals of step functions, so it is not differentiable everywhere: the jumps of $\bar F_i$ and $\bar F_h$ put kinks in $\pi$ where $p=v_ie^{-rT}$ and where $p=v_he^{-rT}$ or $p=v_h$ , at which a backer type starts or stops pledging during the campaign. Setting a gradient to zero does not identify the optimum. The obvious argument for the goal, that herding backers do not pledge at $p^*>v_h$ and so the no-herding optimum is optimal, compares only campaigns that exclude herding backers; it says nothing about the campaigns with a lower pledge level that do attract them. Those campaigns gain a herding term growing exponentially in $\Lambda_hqp$ times the time during which herding backers pledge, and the comparison must hold uniformly over the whole feasible region, which is what the threshold (33) is for. Uniqueness, not only optimality, must also be shown.

Formalization scope

All objects live in the namespace CrowdfundRM.Identical. Parameters form a structure Campaign with fields Ihat, k, r, Lh (for $\Lambda_h$ ), q, vbar, Fbi, Fbh. The standing assumptions, implicit in the paper, are $\hat I,k,r,\bar v>0$ , $\Lambda_h,q\ge0$ , and that each survival function is nonincreasing, takes values in $[0,1]$ , equals $1$ below $0$ and $0$ from $\bar v$ on. Identical valuations set $\bar F_i$ , $\bar F_h$ to the step functions above with $0<v_i,v_h\le\bar v$ .

Conventions: real numbers throughout; the pledge counts are the closed forms (5) and (11); the feasible set of (18) adds $p>0$ , which $\ln(\bar v/p)$ requires; "the optimal" is the unique maximizer over the stated feasible set, and Proposition 6(i), which does not claim uniqueness, asserts that a maximizer exists and bounds every maximizer; "sufficiently long" in Proposition 3(b) is an unspecified threshold $T_0>0$ ; $\Lambda_h,q>0$ is added in Proposition 6(ii) because $a$ and $b$ divide by $\Lambda_hq$ . The paper's $T^*=\frac1r\ln(v_i/\bar p)$ has an undefined $\bar p$ and is read as $p^*$ . In (33) the factors $e^{bv_h/e}$ and $1/(4a)$ multiply only the first bracket.

The following formalizations would trivialize the targets and are ruled out: defining $n(p,T)$ by the explicit formulas (14)–(15) or by the paper's single formula (17) instead of (5) and (11); stating optimality through sSup or a first-order condition; stating Proposition 6(i) for maximizers without asserting that one exists; and stating Proposition 3(b) with a chosen threshold or with Proposition 6's narrower feasible set. The pledging differential equations themselves and their solution (Propositions 1–2) are formalized in the companion mission on triangular valuations; this mission works from their closed forms.

Infrastructure needed: interval integrals of monotone step functions, the exponential, logarithm and real power from Mathlib. Explicit evaluation of the nested integrals under step laws (Corollary 1) is reusable for any proof in this model. Contributions are welcome on each milestone and on lemmas such as continuity of $\pi$ on the feasible set and the closed form of $\pi$ in each region of $(p,T)$ .

Selected references

J. Zhang, S. Savin, S. Veeraraghavan, Revenue Management in Crowdfunding, Manufacturing & Service Operations Management, 2022. https://doi.org/10.1287/msom.2022.1147. Cited from the authors' manuscript of May 26, 2021, SSRN 3065267: https://ssrn.com/abstract=3065267

6 thms2 active usersReviewed

Completed

Combinatorics Operations Research Probability·Captain: mikedeng1

Secretary Problems with Biased Evaluations Using Partial Ordinal Information II: No Algorithm Beats Competitive Ratio ω on Posets of Width ωResearch Paper

Motivation

In hiring, admissions and procurement, candidates are often judged by scores that are known to be biased: two candidates from different groups, schools or evaluation pipelines cannot be compared by their observed scores, while two candidates from the same pipeline can. Salem and Gupta (SSRN 3444283, published in Management Science, 2023) model this situation as a poset secretary problem. The decision maker sees only a partial order between candidates, namely the comparisons that are trustworthy, and must still make irrevocable online selections.

The classical secretary problem and its $k$ -selection variant (Kleinberg, 2005) assume a total order. With only partial comparisons, the natural question is how much the missing comparisons cost. Salem and Gupta answer it in terms of the width of the poset. This mission formalizes their lower bound: no algorithm can do better than a factor of the width.

Setting

A finite set $\mathcal C$ of $N$ candidates carries a partial order $\preceq$ . Each candidate $a$ has a true score $w(a)$ . The scores are nonnegative and pairwise distinct, and they are consistent with the order: $a\prec b$ implies $w(a)<w(b)$ . The pair $\mathcal I=(\mathcal P,w)$ is an instance. Candidates arrive in uniformly random order. An algorithm knows $N$ and a capacity $k$ , observes the comparisons of $\mathcal P$ among the candidates that have arrived, and selects at most $k$ candidates, irrevocably. It never observes the scores.

The offline optimum is

\mathrm{OPT}(w,k)=\max\Big\{\textstyle\sum_{a\in S}w(a)\;:\;S\subseteq\mathcal C,\ |S|\le k\Big\}.

An algorithm is $\alpha$ -competitive if $\mathbb E[w(\mathsf{Alg}(\mathcal I))]\ge\mathrm{OPT}(\mathcal I)/\alpha$ on every instance (Definition 3.4).

The width $\omega$ of $\mathcal P$ is the largest number of pairwise incomparable candidates (an antichain).

Because an algorithm sees only the poset and the arrival order, on a fixed poset its randomness (arrival order and internal coins) induces a probability distribution $\mu$ on the selected set, supported on sets of at most $k$ elements, and $\mu$ does not depend on the scores. Such a $\mu$ is called a selection rule with capacity $k$ . Its expected score is $\mathbb E_\mu[w(\mathrm{Alg})]=\sum_S\mu(S)\sum_{a\in S}w(a)$ . The selection probability of $a$ is $p(a)=\sum_{S\ni a}\mu(S)$ .

The instance of the lower bound is $\mathrm{Chains}(\omega,k)$ : $\omega$ disjoint chains of $k$ elements each, with elements in different chains incomparable (Figure 8 of the paper, with $n=\omega k$ ).

Formalization targets

Goal: Proposition 5.1 (p. 14, proof in Appendix F, p. 42)

For every $k\ge1$ and $\omega\ge1$ there is a poset $\mathcal P$ of width $\omega$ such that for every selection rule $\mu$ with capacity $k$ and every $\varepsilon>0$ there is a consistent scoring $w$ with $\mathrm{OPT}(w,k)>0$ and

\mathbb E_\mu[w(\mathrm{Alg})]\le\frac{(1+\varepsilon)\,\mathrm{OPT}(w,k)}{\omega}.

Equivalently, for every algorithm, $\sup_{\mathcal I}\mathrm{OPT}(\mathcal I)/\mathbb E[w(\mathsf{Alg}(\mathcal I))]\ge\omega$ , the supremum taken over the scorings of $\mathcal P$ .

Milestones (Appendix F, p. 42)

The width of $\mathrm{Chains}(\omega,k)$ is $\omega$ for $k\ge1$ .
For every selection rule with capacity $k$ on $\mathrm{Chains}(\omega,k)$ , some chain $i$ has $\sum_j p^i_j\le k/\omega$ .
If $w$ is a consistent perturbation of the scoring that gives $M/k$ to each element of one chain $i_0$ and $0$ elsewhere, with perturbations below $M/2k$ in absolute value, nonnegative off $i_0$ , and summing to $0$ on $i_0$ , then $\mathrm{OPT}(w,k)=M$ .
Given such a chain $i_0$ , $M>0$ and $\varepsilon>0$ , there is a consistent scoring with $\mathrm{OPT}=M$ and $\mathbb E_\mu[w(\mathrm{Alg})]\le(1+\varepsilon)\mathrm{OPT}/\omega$ .

Significance

The result shows that the width of the poset is a genuine barrier: whatever the algorithm, an adversary choosing scores after seeing how the algorithm spreads its selections can force a ratio arbitrarily close to $\omega$ . The paper's ProxyLabel algorithm has competitive ratio at most $e(\omega+1)/(1-1/k)^{k-1}\le e^2(\omega+1)$ when the width is known (Corollary 5.1, p. 15). Together the two results show that the best achievable competitive ratio in the poset secretary problem is of order $\omega$ , which the paper calls order-optimal. The lower bound also covers the group-bias model of the paper: $\omega$ groups whose members are compared only within their group form exactly the instance used here.

On the formal side, the result is proved in the paper but has no machine-checked proof. The mission produces a formal model of score-independent randomized selection on a finite poset, a formal offline optimum with $k$ selections, and the width of a disjoint union of chains. These can be reused for other lower bounds in online selection.

Difficulty

The argument is short, and the work lies in getting the quantifiers and the encoding right. The printed statement places "there is an instance" before "for any algorithm". Read literally this is false for $\omega\ge2$ : on a fixed instance, the algorithm that always selects the $k$ highest-scoring elements achieves ratio $1$ . The proof establishes the other order: the poset is fixed, then the algorithm, then the scoring. A formalization must keep the scoring chosen after the algorithm while preventing the algorithm from depending on the scores.

The printed chain of inequalities also needs care. Its middle step drops the term $\sum_j p^\omega_j\varepsilon^\omega_j$ , which the stated constraints on the perturbation do not make nonpositive. The bound therefore holds for perturbations chosen small enough, not for every perturbation satisfying the printed constraints. The existence of distinct, order-consistent scores meeting all the constraints at once has to be shown, and so does the identification of the optimum with the heavy chain.

Formalization scope

Elements form a finite type with a partial order. A consistent scoring is a function to $\mathbb R$ that is nonnegative, injective and strictly monotone ( $a<b\Rightarrow w(a)<w(b)$ ). These are the standing assumptions of the model (§3.1, p. 7), not additions. $\mathrm{OPT}$ is a finite maximum over subsets of at most $k$ elements. Width is the published definition AppliedComb.Posets.width, the size of a largest antichain, not a minimum number of chains, so the width milestone is a real claim. Algorithms are represented by selection rules: nonnegative weights on subsets summing to $1$ and vanishing on subsets of more than $k$ elements. This class contains the selected-set law of every online algorithm, so a lower bound for it is a lower bound for online algorithms. Expectations and probabilities are finite sums. Competitiveness is stated as $\mathbb E\le(1+\varepsilon)\mathrm{OPT}/\omega$ together with $\mathrm{OPT}>0$ , with no division by an expectation that may vanish. The hypotheses $k\ge1$ and $\omega\ge1$ are standing: with $\omega=0$ the poset is empty, and with $k=0$ every ratio is $0/0$ . The instance is the sigma type $\Sigma\,(i:\mathrm{Fin}\,\omega),\mathrm{Fin}\,k$ with Mathlib's disjoint order.

Trivializing formalizations are ruled out explicitly. A selection rule must have total mass $1$ , so the zero rule does not make the expected score vanish. It must respect the capacity, so the rule selecting everything is excluded. The scoring is quantified after the selection rule, never before it and never as an input to it. $\mathrm{OPT}>0$ is part of the conclusion.

The development needs finite sums over subsets, the order on sigma types, and antichains. Contributions are welcome on any milestone. The width of a disjoint union of chains and the pigeonhole bound on selection probabilities are reusable beyond this mission.

Selected references

J. Salem and S. Gupta, Secretary Problems with Biased Evaluations Using Partial Ordinal Information, Management Science, 2023. Preprint: SSRN 3444283 (version of 2022-04-17), https://ssrn.com/abstract=3444283. Published version: https://doi.org/10.1287/mnsc.2023.4926
R. Kleinberg, A multiple-choice secretary algorithm with applications to online auctions, Proceedings of SODA, 2005. https://dl.acm.org/doi/10.5555/1070432.1070519
R. P. Dilworth, A decomposition theorem for partially ordered sets, Annals of Mathematics 51(1), 1950. https://doi.org/10.2307/1969503

8 thms2 active usersReviewed

Algorithmic Game Theory Operations Research Optimization+1·Captain: mikedeng1

Managing Outpatient Service with Strategic Walk-ins II: The Triage Model Costs Less When C_L/C_O ≤ α̲ and the Strategic Model Costs Less When C_L/C_O ≥ ᾱResearch Paper

Motivation

Many outpatient clinics offer two ways in: an appointment booked online, and walk-in hours on the day. Some patients have no choice (acute cases arrive as walk-ins), but many can pick either channel, and they pick the one that costs them less: a long appointment delay pushes them into the walk-in room, a crowded walk-in room pushes them to book or to give up. A clinic deciding how to split its daily capacity between the two channels therefore faces a game, not a forecasting problem.

Liu, van Jaarsveld, Wang and Xiao (SSRN 3558209; Management Science 2023, doi:10.1287/mnsc.2023.4676) model this game and compare three operational levers: the capacity split, how much delay information the booking system reveals, and triage, that is, reserving walk-in hours for acute patients only (as some practices do, e.g. Centre Pediatrics 2021). This mission formalizes the triage comparison, Proposition 6 of the paper: closing walk-in hours to patients who could book pays off exactly when lost demand is cheap relative to overtime.

Setting

Patients. Exogenous walk-ins arrive at rate $\lambda_E$ and are always served on the day, possibly in overtime. Strategic patients arrive as a Poisson process of rate $\lambda>0$ . A served patient gains $R>0$ .

Capacity. The clinic has total capacity $\mu>0$ per day, split into appointment hours $\mu_S$ and walk-in hours $\mu_W=\mu-\mu_S$ , with $\mu_S\in[0,\mu)$ .

The appointment queue. Appointments form a single-server queue with deterministic service time $1/\mu_S$ . In the observable setting a patient sees the queue: with $k$ patients waiting, the delay is $(k+\tilde u)/\mu_S$ , $\tilde u$ uniform on $[0,1]$ . A patient schedules when this delay is at most a threshold $\delta$ , and scheduling at delay $d$ is worth $u^2_S(d)=R-C_D d$ . The fraction of strategic patients who do not schedule is the blocking probability $\pi(\delta,\mu_S)$ of this M/D/1/K−1+p queue, where $K=\lceil\delta\mu_S\rceil$ and $p=\delta\mu_S+1-K$ . With $\rho=\lambda/\mu_S$ it has the closed form $\pi(\delta,\mu_S)=1-1/(q_0+\rho)$ , where $q_0$ is built from the Poisson weights $\alpha_j=\rho^je^{-\rho}/j!$ by the Brun–Garcia recursion (Online Appendix C, (26)–(27), Corollary C.1). With no appointment hours, $\pi(\delta,0)=1$ .

Walking in and balking. A patient who does not schedule walks in with probability proportional to $p_W$ or balks with probability proportional to $p_B$ . Walking in is worth $u^2_W(p_W)=R-C_W\,w\big((\lambda_E+p_W\lambda)/\mu_W\big)$ , with $w$ convex, strictly increasing and $w(0)=0$ ; balking is worth $0$ . An observable equilibrium $(\delta,p_W,p_B)$ is a solution of conditions (6)–(10): the threshold $\delta$ makes scheduling at least as good as the walk-in/balk mixture up to $\delta$ and worse beyond it, $p_W+p_B=\pi(\delta,\mu_S)$ , and patients walk in (balk) only if walking in is worth at least (at most) zero.

Costs. The provider pays $C_L$ per balking patient and $C_O\,o(\cdot)$ for overtime, with $o$ convex and strictly increasing. In the strategic model patients choose freely, and the cost at allocation $\mu_S$ and equilibrium $(\delta,p_W,p_B)$ is

Z^s=C_L\,p_B\lambda+C_O\,o\Big(\frac{p_W\lambda+\lambda_E}{\mu_W}\Big). \qquad\text{(Ob.P)}

In the triage model strategic patients may only schedule or balk, so they behave with threshold $R/C_D$ and

Z^t=C_L\,\pi(R/C_D,\mu_S)\,\lambda+C_O\,o\Big(\frac{\lambda_E}{\mu_W}\Big). \qquad\text{(T.Ob.P)}

Let $\underline\mu_W$ solve $R-C_W\,w(\lambda_E/\underline\mu_W)=0$ (15): below these walk-in hours the exogenous walk-ins alone make walking in worthless.

Formalization targets

Goal: Proposition 6

Suppose $\mu>\underline\mu_W$ and set

\underline\alpha=\frac{o'(\lambda_E/\mu)}{\mu},\qquad \overline\alpha=\frac{o'(\lambda_E/\underline\mu_W)}{\underline\mu_W}\max\Big\{\frac{\lambda_E}{\lambda\,\pi(R/C_D,\mu-\underline\mu_W)},1\Big\}.

Then

\frac{C_L}{C_O}\le\underline\alpha\ \Longrightarrow\ \inf Z^t\le\inf Z^s,\qquad \frac{C_L}{C_O}\ge\overline\alpha\ \Longrightarrow\ \inf Z^s\le\inf Z^t,

where the infima are over allocations $\mu_S\in[0,\mu)$ and, on the strategic side, over the equilibria at each allocation. The Lean statement says this without infima: every strategic configuration is matched by a triage allocation that costs no more, and every triage allocation is matched by a strategic allocation at which an equilibrium exists and every equilibrium costs no more.

Milestones

Proposition C.2 ( $\mu_S$ -part): $\mu_S\mapsto\pi(\delta,\mu_S)$ is continuous and strictly decreasing on $(0,\infty)$ .
Proposition 1 (observable setting): an observable equilibrium exists at every allocation.
Proposition 2 (1): if $\mu_W\le\underline\mu_W$ , every equilibrium is schedule-and-balk, $p_W=0$ , $\delta=R/C_D$ , $p_B=\pi(R/C_D,\mu_S)$ .
From the proof of part 1: $\lambda\,(1-\pi(\delta,\mu_S))\le\lambda\,(1-\pi(R/C_D,\mu_S))$ at every equilibrium.
From the proof of part 2: if nobody balks, $(\lambda p_W+\lambda_E)/\mu_W\le\lambda_E/\underline\mu_W$ .
From the proof of part 2: if patients mix between walking in and balking, $(\lambda p_W+\lambda_E)/\mu_W=\lambda_E/\underline\mu_W$ .

Significance

Proposition 6 turns a qualitative trade-off into two explicit thresholds on the ratio of the lost-demand cost to the overtime cost. Free choice reduces balking but lets strategic patients crowd the walk-in hours; triage removes that crowding at the price of more balking. The thresholds $\underline\alpha$ and $\overline\alpha$ depend only on the overtime function, the capacity and the blocking probability, so a clinic can evaluate them from its own data. The paper also shows (Remark 4, Appendix D.8) that the same insight holds in the unobservable setting, with capacity playing an additional role; that variant is not part of this mission.

The result is proved in the paper (Online Appendix E.3, pp. 35–37) and has no machine-checked proof. The formalization adds three things. It fixes the equilibrium concept precisely, including the mixture weights and the endpoint conventions. It states the comparison of optimal costs without presupposing that the optima are attained; the paper's proof begins "denote the optimal capacity allocations" without proving existence. And it ties the blocking probability to the paper's closed form, so the monotonicity in $\mu_S$ that the proof invokes becomes a statement about an explicit function rather than about a queue described in words.

Difficulty

The comparison itself is a chain of convexity inequalities at a single allocation. The hard part is the blocking probability. The paper proves that $\pi(\delta,\mu_S)$ decreases in $\mu_S$ by a sample-path argument on the queue, but a formal development has only the closed form, in which $K=\lceil\delta\mu_S\rceil$ jumps at every $\mu_S$ where $\delta\mu_S$ is an integer, $p$ jumps from $1$ to $0$ there, and $\rho=\lambda/\mu_S$ moves continuously. Monotonicity and continuity must be shown across these seams, through alternating sums whose terms cancel heavily. The obvious route, differentiating the closed form for fixed $K$ , does not give the sign without a further structural argument on the coefficients $a_j$ .

Existence of an equilibrium (milestone 2) is an intermediate-value argument in $\delta$ , which in turn needs continuity of $\pi$ in $\delta$ and positivity of $\pi$ .

Formalization scope

Everything lives in the namespace OutpatientWalkIn.Triage. The definition Queue contains the closed-form blocking probability blockProb lam δ μS; the definition Setting contains the model, the standing assumptions, the utilities, the equilibrium IsObsEq, the costs obsCost and triageCost, and the thresholds alphaLow, alphaHigh.

Conventions:

Standing assumptions, hypotheses of every theorem: $\lambda>0$ , $\lambda_E\ge0$ , $R,C_D,C_W>0$ , $C_L,C_O\ge0$ , $\mu>0$ ; $w$ convex and strictly increasing on $[0,\infty)$ with $w(0)=0$ (Assumption 1); $o$ convex and strictly increasing on $[0,\infty)$ (Assumption 2).
Allocations range over $\mu_S\in[0,\mu)$ on both sides, so that $\mu_W>0$ ; the paper's $\mu_S=\mu$ leaves the exogenous walk-ins with no walk-in hours.
$\pi(\delta,0)=1$ ; the observable setting is defined directly (the paper's $C_G=0$ ).
The equilibrium carries the guard $p_W+p_B>0$ , which by (8) is $\pi(\delta,\mu_S)>0$ and excludes no equilibrium of the paper.
Added hypotheses of the goal: $C_O>0$ , $\lambda_E>0$ , $\underline\mu_W>0$ given by (15), and differentiability of $o$ at $\lambda_E/\mu$ and $\lambda_E/\underline\mu_W$ (where $o'$ is evaluated). Without them Lean's $C_L/0=0$ and the zero derivative of a non-differentiable function would make $\underline\alpha=0$ and turn part 1 into a different claim.
"Costs less" is "costs no more" (p. 26).

A formalization that compares the two models at one fixed allocation only, that lets the prover choose a cheap equilibrium when several might exist, or that replaces $\pi$ by an arbitrary decreasing function, is not the paper's theorem; the statements here rule these out.

Contributions welcome: properties of the closed-form $\pi$ (positivity, $\pi\le1$ , monotonicity and continuity in both arguments), the existence of equilibria, and the convexity estimates of the final comparison. The queue file is reusable for any M/D/1/K model with partial joining.

Selected references

N. Liu, W. van Jaarsveld, S. Wang, G. Xiao, Managing Outpatient Service with Strategic Walk-ins, SSRN 3558209 (version of 2022-07-05); Management Science, 2023. https://ssrn.com/abstract=3558209, https://doi.org/10.1287/mnsc.2023.4676
O. Brun, J.-M. Garcia, Analytical solution of finite capacity M/D/1 queues, Journal of Applied Probability 37(4), 2000 (the source of the $a_j$ recursion, cited in the paper's Online Appendix C).
P. Naor, The regulation of queue size by levying tolls, Econometrica 37(1), 1969. https://doi.org/10.2307/1909200

15 thms2 active usersReviewed

Machine Learning Reinforcement Learning Statistics·Captain: mikedeng1

Breaking the Sample Size Barrier in Model-Based Reinforcement Learning with a Generative Model 1: The Perturbed Model-Based Planner Is ε-Optimal w.p. 1−δ Once N ≥ c₀log(|S||A|/((1−γ)εδ))/((1−γ)³ε²)Research Paper

Motivation

A generative model lets a planner request independent next-state samples for any state-action pair. This is a useful idealization for studying how many simulator calls are needed before a policy computed from an estimated model performs well in the true environment. Li, Wei, Chi, and Chen show that a small independent perturbation of the rewards lets a model-based planner meet a sample-size bound with cubic dependence on the effective horizon $1/(1-\gamma)$ , while providing guarantees for both values and action values (Li et al., 2024). This mission isolates their perturbed-planning result and the source lemmas that support it.

Setting

A finite discounted Markov decision process consists of a state set $S$ , an action set $A$ , a transition probability $P(s'\mid s,a)$ , an immediate reward $r(s,a)\in[0,1]$ , and a discount factor $\gamma\in(0,1)$ . A deterministic policy $\pi:S\to A$ chooses an action at each state. Its value $V^\pi(s)$ is the expected sum of rewards, discounted by $\gamma^t$ , from state $s$ . Its action value $Q^\pi(s,a)$ takes action $a$ first and follows $\pi$ thereafter. The optimal values $V^\star$ and $Q^\star$ are those of an optimal deterministic policy; equivalently, $Q^\star(s,a)=r(s,a)+\gamma\sum_{s'}P(s'\mid s,a)V^\star(s')$ .

For each $(s,a)$ , draw $N$ independent next states from $P(\cdot\mid s,a)$ , independently across pairs. The empirical kernel $\widehat P$ is their frequency table. Independently draw one reward perturbation $\zeta(s,a)\sim\operatorname{Unif}(0,\xi)$ per pair and set $r_p=r+\zeta$ . The planner returns an optimal deterministic policy $\widehat\pi_p^\star$ for the empirical MDP $(S,A,\widehat P,r_p,\gamma)$ . The performance claim evaluates this policy under the original $P$ and $r$ , so the perturbation changes policy selection but not the evaluation target.

Formalization targets

Perturbed model-based planning

Theorem 1 of Li et al. asserts that absolute constants $c_0,c_1>0$ can be chosen before $S$ , $A$ , $P$ , $r$ , $\gamma$ , $\varepsilon$ , and $\delta$ . For $\delta>0$ , $0<\varepsilon\le1/(1-\gamma)$ , and $\xi=c_1(1-\gamma)\varepsilon/(|S|^5|A|^5)$ , the sample-size condition is

N\ge\frac{c_0\log\!\bigl(|S||A|/((1-\gamma)\varepsilon\delta)\bigr)}{(1-\gamma)^3\varepsilon^2}.

With probability at least $1-\delta$ over both the samples and the perturbation, every optimal policy of the perturbed empirical MDP simultaneously satisfies

V^{\widehat\pi_p^\star}(s)\ge V^\star(s)-\varepsilon,\qquad Q^{\widehat\pi_p^\star}(s,a)\ge Q^\star(s,a)-\gamma\varepsilon\quad\text{for all }(s,a).

The milestone list follows the paper's numbered statements: fixed-policy and Bernstein-condition value bounds (Lemmas 1–2), calibrated state-action absorbing models and their finite reward grid (Lemma 3, (88), Lemma 4), planning under a separated optimum (Lemma 5), separation induced by random rewards (Lemma 6), and the reward-change bound before (49). The paper's additional claim about iteration counts for empirical QVI and PI is outside this target.

Significance

The theorem gives a policy guarantee from a finite number of calls to a generative model. It bounds the true value of the selected policy at every state and its true action value at every state-action pair, rather than only the empirical objective used to select the policy. Its $N$ is the number of samples per pair; the total number of transitions observed is $N|S||A|$ . The statement is a theorem proved in the cited paper, not an open mathematical conjecture (Li et al., Theorem 1).

The formalization work is to turn the paper's probability experiment, policy choice, and linked inequalities into machine-checked statements and eventually machine-checked proofs. The published FoundationsML transition kernel and policy-value definitions provide reusable base objects. This mission adds a finite generative-sample law, the reward-perturbation law, and an absorbing-MDP interface. Those objects can support later formalizations of empirical planning and policy evaluation beyond this theorem. The goal and milestone proofs remain open in the present draft.

Difficulty

A fixed policy can be evaluated against an empirical transition kernel using concentration at that policy. The planner's policy depends on the same sampled kernel, so a fixed-policy bound cannot simply be applied to it. Small changes in transition frequencies may also switch the chosen optimal action when actions have nearly equal values. The paper's intermediate results specify the needed value-control and separation properties; a Lean proof must track their constants and their probability events without silently assuming that the data-dependent policy was fixed before sampling (Li et al., §§6.2–6.3).

Formalization scope

The Lean state and action types are finite, and both are nonempty where cardinalities occur in denominators. A transition kernel is a probability vector at each state-action pair. Policies are deterministic functions $S\to A$ , embedded as point-mass stochastic policies for the published value definitions. $V^\star$ is the maximum over the finite set of deterministic policies; $Q^\star$ is $r+\gamma PV^\star$ . Function norms are supremum norms. The empirical kernel is the frequency table of a finite array of samples, with $N>0$ in the goal because its formula divides by $N$ . The independent perturbation is the uniform measure on the cube $[0,\xi]^{S\times A}$ .

Probability claims bound the failure event. The data law is a finite product, and the auxiliary continuous draw is measured section by section. This formulation allows an outer measure for a section whose measurability is not already known; it does not let a nonmeasurable success event satisfy the result for free. The main theorem quantifies over every optimal policy of the empirical perturbed model, and its universal constants do not depend on the instance. These choices rule out treating the selected policy as arbitrary, fixing the perturbation in advance, or choosing constants after seeing the MDP.

The absorbing-MDP construction changes one transition row and one reward. The reward at that row may leave $[0,1]$ , so the underlying value function accepts arbitrary real rewards even though the main MDP has normalized rewards. Lemma 5 is stated with normalized rewards as printed. Reusable contributions include basic properties of the sampling law, optimal-policy existence, the absorbing construction, and quantitative value stability; the milestone statements themselves are the intended proof targets.

Selected references

G. Li, Y. Wei, Y. Chi, and Y. Chen, Breaking the Sample Size Barrier in Model-Based Reinforcement Learning with a Generative Model, Operations Research, 2024; arXiv:2005.12900v8.

15 thms2 active usersReviewed

Differential Geometry Machine Learning Optimization+1·Captain: mikedeng1

Stochastic Zeroth-Order Riemannian Derivative Estimation and Optimization 1: ZO-RGD Has Average Expected Squared Riemannian Gradient Norm at Most 8(d+4)L(f(x₀) − f(x*))/(N+1) + 8(d+4)L·C(μ)Research Paper

Motivation

Many optimization problems in statistics and machine learning constrain the variable to a smooth manifold: orthonormal frames in sparse PCA and dictionary learning (the Stiefel manifold), unit vectors in phase retrieval (the sphere), fixed-rank matrices in matrix completion. Riemannian optimization handles these problems directly on the manifold. A step is taken in the tangent space and mapped back to the manifold by a retraction.

In several applications the objective can be evaluated but not differentiated: black-box adversarial attacks, simulation-based models, and hyperparameter or policy tuning. Zeroth-order (derivative-free) methods replace the gradient by an estimator built from function values. In Euclidean space the standard construction is Gaussian smoothing, analysed by Nesterov and Spokoiny (2017) and Ghadimi and Lan (2013). Li, Balasubramanian and Ma (arXiv:2003.11238; Mathematics of Operations Research, 2023) carry the construction over to embedded submanifolds. They sample a Gaussian vector, project it onto the tangent space, and use the retraction in place of the straight line $x+\mu u$ . This mission formalizes their first optimization guarantee: the convergence rate of zeroth-order Riemannian gradient descent (ZO-RGD).

Setting

Let $E$ be a finite-dimensional real inner product space (the ambient $\mathbb R^n$ ). Let $M\subseteq E$ be a $C^1$ embedded submanifold of dimension $d$ . At each $x\in M$ the tangent space $T_xM$ is a $d$ -dimensional linear subspace of $E$ ; let $P_x$ denote the orthogonal projection onto it. $M$ carries the metric induced by the inner product of $E$ .

A retraction is a map $(x,\eta)\mapsto R_x(\eta)$ such that, for every $x\in M$ , $R_x$ is smooth on $T_xM$ , maps $T_xM$ into $M$ , satisfies $R_x(0)=x$ , and has the identity as its differential at $0$ . In this mission $R_x$ is defined on all of $T_xM$ .

For a differentiable $f:E\to\mathbb R$ the Riemannian gradient is $\operatorname{grad} f(x)=P_x\nabla f(x)$ . Assumption 2.1 (retraction smoothness) asks for a constant $L\ge0$ such that

\big|f(R_x(\eta))-f(x)-\langle \operatorname{grad} f(x),\eta\rangle\big|\le \tfrac L2\|\eta\|^2\qquad(x\in M,\ \eta\in T_xM).

Given $\mu>0$ and a standard Gaussian vector $u_0\sim N(0,I_n)$ of $E$ , set $u=P_xu_0$ . The zeroth-order Riemannian gradient estimator is

g_\mu(x)=\frac{f(R_x(\mu u))-f(x)}{\mu}\,u .

ZO-RGD (Algorithm 1) starts at $x_0\in M$ , draws independent Gaussian vectors $u_0^0,u_0^1,\dots$ , and sets $x_{k+1}=R_{x_k}(-\hat\eta\, g_\mu(x_k))$ , where $g_\mu(x_k)$ uses $u_k=P_{x_k}u_0^k$ . The step size is $\hat\eta=1/(2(d+4)L)$ . Let $x^*\in M$ be a minimizer of $f$ over $M$ .

Formalization targets

Goal: Theorem 3.1

For every $N\ge0$ ,

\frac1{N+1}\sum_{k=0}^{N}\mathbb E\,\|\operatorname{grad} f(x_k)\|^2\le\frac4{\hat\eta}\left(\frac{f(x_0)-f(x^*)}{N+1}+C(\mu)\right),

where $4/\hat\eta=8(d+4)L$ and

C(\mu)=\frac{\mu^2L}{16}\frac{(d+3)^3}{d+4}+\frac{\mu^2L}{16}\frac{(d+6)^3}{d+4}+\frac{\mu^2L}{16}\frac{(d+6)^3}{(d+4)^2}.

Milestones

These are the paper's own intermediate results (§2.2, p. 8):

Lemma 2.1. For a subspace $\mathcal X$ with projection $P$ , $u=Pu_0$ and $x\in\mathcal X$ : $\mathbb E\langle x,u\rangle u=x$ and $\mathbb E\langle x,u\rangle^2=\|x\|^2$ .
Lemma 2.2 (Nesterov–Spokoiny). $\mathbb E\|u\|^p\le(n+p)^{p/2}$ for $p\ge2$ . This result is already on the platform as a proved theorem and is referenced.
Corollary 2.1. If $\dim\mathcal X=d$ , then $\mathbb E\|Pu_0\|^p\le(d+p)^{p/2}$ .
Proposition 2.1(a). $\|\mathbb E g_\mu(x)-\operatorname{grad} f(x)\|\le\frac{\mu L}{2}(d+3)^{3/2}$ .
Proposition 2.1(b). $\|\operatorname{grad} f(x)\|^2\le2\|\mathbb E g_\mu(x)\|^2+\frac{\mu^2}{2}L^2(d+6)^3$ .
Proposition 2.1(c). $\mathbb E\|g_\mu(x)\|^2\le\frac{\mu^2}{2}L^2(d+6)^3+2(d+4)\|\operatorname{grad} f(x)\|^2$ .

Significance

Theorem 3.1 shows that ZO-RGD reaches an $\epsilon$ -stationary point in expectation using $O(d/\epsilon^2)$ function evaluations, provided the smoothing parameter is of order $\epsilon/d^{3/2}$ . The dimension that enters is the intrinsic dimension $d$ of the manifold, not the ambient dimension $n$ . For the Stiefel manifold of $n\times p$ orthonormal frames this is the difference between $np-p(p+1)/2$ and $np$ , and for the sphere between $n-1$ and $n$ . More importantly, the estimator never explores normal directions. The three estimates of Proposition 2.1 are the toolkit that the paper reuses for its stochastic (ZO-RSGD), proximal (ZO-ManPG) and second-order variants.

The paper proves these results on paper; none of them has a machine-checked proof. The mission adds three things. It gives a precise model of a random iterate sequence on a submanifold, driven by the infinite product of Gaussian draws. It formalizes the projected-Gaussian identities, which are reusable for any method that samples in tangent spaces. And it pins down the constants. In checking the constants, the printed Proposition 2.1(b) turned out to be false for large $L$ (its proof yields $L^2$ , not $L$ ), and the middle term of the printed $C(\mu)$ inherits that slip. The statements here carry the constants the proofs actually give.

Difficulty

In Euclidean space, $\mathbb E\,g_\mu(x)$ is exactly the gradient of the Gaussian-smoothed function $f_\mu(x)=\mathbb E f(x+\mu u)$ , and the analysis runs on $f_\mu$ . Once a retraction replaces $x+\mu u$ , no smoothed function has $\mathbb E g_\mu$ as its gradient. The bias must be estimated directly from Assumption 2.1, which controls $f\circ R_x$ only along the tangent space. The moment bounds must then be taken for a Gaussian projected onto a subspace that changes with $x$ .

In the descent argument, the direction $u_k$ is sampled in $T_{x_k}M$ , which depends on all earlier draws. The expectation of step $k$ is therefore conditional on the past. Summing the one-step inequality requires conditional expectations on the product space, together with measurability of the iterate map. Finiteness of $\mathbb E f(x_k)$ is not given and must be handled as well.

Formalization scope

Space. The ambient space is a finite-dimensional real inner product space $E$ . The standard Gaussian is Mathlib's stdGaussian E, so $\kappa^{-1}\int\cdots e^{-\|u_0\|^2/2}du_0$ becomes integration against it.
Manifold and tangent spaces. The manifold is given by the published coordinate-slice predicate ProjLikeRetr.Retractor.IsSubmanifold 1 d M, which ties $d$ to $M$ . The tangent space is the published ProjLikeRetr.Retractor.tangentSpace M x, the span of Mathlib's tangent cone. Neither $d$ nor the tangent spaces are free parameters.
Retraction. The retraction is global: Assumption 2.1 is required for every $\eta\in T_xM$ (the paper's " $\rho_x=\infty$ "). "Smooth" means $C^\infty$ , not analytic.
Regularity of $f$ . $f$ is assumed differentiable on $E$ , which is what the definition $\operatorname{grad} f=P_x\nabla f$ needs. This is weaker than the paper's "smooth".
Constants. The goal takes $L>0$ , because the step size divides by $L$ . The milestones take $L\ge0$ and $\mu>0$ .
Draws and iterates. The draws live on $E^{\mathbb N}$ with the infinite product of standard Gaussian measures. The iterates are defined for every $k$ : the algorithm runs without a stopping time, so the sum over $k=0,\dots,N$ is meaningful.
Minimizer. $x^*$ is an attained minimizer over $M$ .
Measurability. The goal adds two measurability hypotheses that make the iterates random variables: $(x,\eta)\mapsto R_x(\eta)$ is measurable and $x\mapsto P_x$ is measurable. Both hold for closed manifolds such as spheres and Stiefel manifolds.
Corrected constants. Proposition 2.1(b) carries $L^2$ , and the middle term of $C(\mu)$ carries $L$ . The milestone texts keep the printed forms. Proposition 2.1(a) and (c) are as printed.
Not formalized. The parameter choices $\mu=O(\epsilon/d^{3/2})$ , $N=O(d/\epsilon^2)$ in the theorem's second sentence are an $O(\cdot)$ statement.

Several trivializing formalizations are ruled out. A Bochner integral of a non-integrable function is $0$ , so every expectation in a conclusion is either a lower Lebesgue integral compared with a finite bound or paired with an integrability conjunct. The dimension $d$ comes from the manifold, not from a free natural number. The projection is onto $M$ 's own tangent space, never onto an arbitrary subspace field.

A complete development needs the following infrastructure:

the law of $P u_0$ (a standard Gaussian on the subspace);
Gaussian moment bounds;
conditional expectation along the product filtration;
measurability of the iterate map.

The projected-Gaussian lemmas and the iterate model are reusable for the stochastic variant (ZO-RSGD) in the companion mission. Contributions of proofs for any milestone, and of general lemmas about Gaussian measures restricted to subspaces, are welcome.

Selected references

J. Li, K. Balasubramanian, S. Ma, Stochastic Zeroth-Order Riemannian Derivative Estimation and Optimization, Mathematics of Operations Research, 2023; preprint arXiv:2003.11238v3, 2021. https://arxiv.org/abs/2003.11238
Y. Nesterov, V. Spokoiny, Random Gradient-Free Minimization of Convex Functions, Foundations of Computational Mathematics 17 (2017) 527–566. https://doi.org/10.1007/s10208-015-9296-2
S. Ghadimi, G. Lan, Stochastic First- and Zeroth-Order Methods for Nonconvex Stochastic Programming, SIAM Journal on Optimization 23 (2013) 2341–2368. https://doi.org/10.1137/120880811
P.-A. Absil, R. Mahony, R. Sepulchre, Optimization Algorithms on Matrix Manifolds, Princeton University Press, 2008. https://doi.org/10.1515/9781400830244

13 thms2 active usersReviewed

Completed

Combinatorics Graph Theory Operations Research·Captain: mikedeng1

Linear Programming and Community Detection 2: The Minimum Bisection Recovery Condition d_in − d_out > n/4 − 1 Is TightResearch Paper

Why minimum bisection recovery matters

The minimum bisection problem partitions an even-sized graph into two equally large groups while cutting as few edges as possible. In community detection, a graph may have been generated around an unknown, balanced pair of groups. The statistical question is whether an optimizer can identify that planted partition from the edges. Before studying random graph models or relaxations, it is useful to know which properties of a single observed graph suffice for recovery and whether those properties can be weakened.

Del Pia, Khajavirad and Kunisky express a deterministic sufficient condition through two vertex-degree parameters. Their Theorem 1 says that minimum bisection recovers the planted partition when the smallest within-community degree exceeds the largest cross-community degree by more than $n/4-1$ . Theorem 2 supplies graphs at or below that boundary where recovery fails. Thus the degree difference has a sharp worst-case boundary within the theorem's stated size and degree ranges. This mission formalizes that second, tightness result.

Graphs, bisections, and degrees

Let $G=(V,E)$ be a simple undirected graph with $n$ vertices. A bisection is a partition $V_1,V_2$ of $V$ with $|V_1|=|V_2|=n/2$ . Its cut cost is the number of edges with one endpoint in each side. The planted bisection is a designated partition regarded as the answer the optimizer should recover. Since exchanging $V_1$ and $V_2$ leaves the partition unchanged, uniqueness is always understood up to this exchange.

For each vertex $v$ , count its neighbors on its own side of the planted bisection and its neighbors on the opposite side. Write $d_{\mathrm{in}}(v)$ and $d_{\mathrm{out}}(v)$ for these counts. The two parameters of the planted graph are

d_{\mathrm{in}}=\min_{v\in V}d_{\mathrm{in}}(v),\qquad d_{\mathrm{out}}=\max_{v\in V}d_{\mathrm{out}}(v).

Minimum bisection recovers the planted partition if every bisection with cost at most that of the planted one is the planted partition, up to swapping its sides. This formulation requires both optimality and uniqueness. If the planted bisection costs more than a competitor, recovery fails; it also fails when a distinct bisection ties it. These definitions follow §2 of the pinned preprint.

Formalization targets

Existence of regular graph pieces

Lemma 1 supplies two finite-graph existence statements. For positive even $t$ , a simple $d$ -regular bipartite graph exists on $t$ vertices with $t/2$ vertices per side whenever $0\le d\le t/2$ . For the same $t$ , a simple $d$ -regular graph exists whenever $0\le d\le t-1$ . The bipartite part includes the edgeless graph at $d=0$ and the complete bipartite graph at $d=t/2$ . The second part includes the edgeless and complete graphs at its own endpoints.

Tightness of the recovery threshold

The mission's goal is Theorem 2. For every positive multiple of eight $n$ and every pair of nonnegative integers satisfying

d_{\mathrm{in}}\le \frac n2-1,\qquad d_{\mathrm{out}}\le \frac n2,\qquad d_{\mathrm{in}}-d_{\mathrm{out}}\le \frac n4-1,

there exist a graph $G$ on $n$ vertices and a planted bisection with those exact parameters for which minimum bisection does not recover the planted partition. The inequalities delimit the claimed family; the goal does not assert failure for every graph with those degrees. The word “exact” matters because a construction with merely smaller within-side degrees or larger cross-side degrees would not establish tightness for the requested parameter pair.

What the result establishes

Together with the paper's Theorem 1, the goal locates the worst-case threshold for recovery by minimum bisection: a strictly larger degree difference guarantees recovery, while every admissible parameter pair at or below the boundary occurs in a counterexample. This separates a guarantee about all graphs with given degree extrema from a claim about a particular graph. It also gives a deterministic baseline for comparing the behavior of the paper's linear programming relaxation and stochastic block model, whose recovery guarantees concern different optimization procedures and graph distributions.

The theorem is proved in the cited paper; the task here is to state its graph model, parameter extrema, and recovery conclusion in Lean with the same quantifiers and boundary cases, then obtain a machine-checked proof. The regular-graph existence lemma is independently reusable for other finite graph constructions. The definition layer can also support later exact-recovery statements for the same paper after the series' graph conventions are consolidated.

The obstacle to a direct argument

A strict threshold being sufficient does not itself show that it is necessary. At equality, an inequality used in a recovery guarantee no longer forces a unique optimum, but that leaves open whether a graph with the prescribed degree extrema actually has a competing bisection. Every requested pair $(d_{\mathrm{in}},d_{\mathrm{out}})$ must be realized by a genuine simple graph, including the degree endpoints, and the competing partition must be balanced and distinct even after sides are exchanged. The proof therefore needs graph existence and degree bookkeeping as well as a comparison of cut costs. The page states one numbered supporting lemma, Lemma 1; its two clauses are the mission's milestone.

Formalization scope

Vertices are represented by Fin n, indexed from zero rather than the paper's $1,\ldots,n$ . A side of a bisection is a Finset; its complement represents the other side. Graphs are Mathlib SimpleGraph values, and cut cost counts each undirected crossing edge once by ordering its endpoints. The within and across degrees are filtered neighbor counts. Their minimum and maximum range over all vertices, matching the paper. An empty vertex type receives a conventional zero degree extremum, while Theorem 2 requires $n>0$ .

The bounds involving $n/2-1$ and $n/4-1$ are compared in the reals, so natural-number subtraction cannot truncate a negative difference. The hypothesis $8\mid n$ makes $n/4$ an integer in the theorem's actual domain. Lemma 1 uses positive even $t$ , with Mathlib's regular-degree predicate and a bisection set witnessing equal bipartition sizes. Its bound $t-1$ is safe in natural numbers because $t>0$ .

The formal goal requires a witness graph whose minimum within-side degree equals the requested $d_{\mathrm{in}}$ and whose maximum across-side degree equals the requested $d_{\mathrm{out}}$ . It also requires an actual planted bisection and failure of uniqueness up to complement. Replacing either equality with a loose degree bound, or allowing a non-bisection witness, would make the claim easier and lose the paper's result. Contributions toward finite regular graph constructions, exact degree calculations, and cut-cost comparisons are within scope.

Selected references

A. Del Pia, A. Khajavirad and D. Kunisky, Linear Programming and Community Detection, Mathematics of Operations Research, 2023; pinned source: arXiv:2006.03213v2, §2, pp. 3–6, especially Lemma 1 and Theorem 2 on p. 5.

3 thms2 active usersReviewed

Completed

Dynamic Programming Operations Research Optimization+1·Captain: mikedeng1

A First-Order Approach to Accelerated Value Iteration 4: Safe Accelerated Value Iteration Converges to v* at Rate O(λ′^s) for Every λ′ ∈ [λ, 1)Research Paper

Motivation

Value iteration (VI) is the standard method for computing the optimal value function of a discounted Markov decision process (MDP). It applies the Bellman operator repeatedly, and because that operator is a $\lambda$ -contraction in the sup norm, the error after $s$ steps is at most $\lambda^s$ times the initial error. When the discount factor $\lambda$ is close to $1$ , as in long-horizon planning, this rate is slow.

Goyal and Grand-Clément (arXiv:1905.09963, Operations Research 2023) read value iteration as a gradient-type method and transfer momentum schemes from convex optimization (Nesterov acceleration, heavy-ball momentum) to the Bellman operator. On reversible policy chains these accelerated schemes provably converge faster than VI. On general MDPs, however, the accelerated iterates need not converge at all: the paper exhibits instances on which Accelerated Value Iteration (A-VI) oscillates or diverges. Section 7 of the paper resolves this tension with Safe Accelerated Value Iteration (S-AVI, Algorithm 1), which tries an accelerated step at every period and keeps it only when it makes enough progress on the Bellman equation $v = T(v)$ . This mission formalizes the convergence guarantee of S-AVI, Theorem 7.1.

Setting

Let $\mathbb S$ be a finite set of states and $\mathbb A$ a nonempty finite set of actions. A discounted MDP is given by a transition kernel $P$ , with $P_{iaj}\ge 0$ the probability of moving from state $i$ to state $j$ under action $a$ and $\sum_j P_{iaj} = 1$ ; a reward $r_{ia}\in\mathbb R$ for each state-action pair; and a discount factor $\lambda \in (0,1)$ . The Bellman operator $T : \mathbb R^{\mathbb S} \to \mathbb R^{\mathbb S}$ is

T(v)_i = \max_{a\in\mathbb A}\Big\{ r_{ia} + \lambda \sum_{j} P_{iaj}\, v_j \Big\}.

The sup norm is $\|v\|_\infty = \max_i |v_i|$ . The optimal value function $v^*$ is the unique fixed point of $T$ . For a vector $v$ , the quantity $\|v - T(v)\|_\infty$ is its Bellman residual.

S-AVI (Algorithm 1) takes a scalar $\lambda' \in [\lambda, 1)$ , step sizes $\alpha, \gamma > 0$ and any starting vector $v_0$ . It sets $v_1 = T(v_0)$ , and at each period $s \ge 1$ forms

h_s = v_s + \gamma\,(v_s - v_{s-1}), \qquad v_{s+1/2} = h_s - \alpha\,\big(h_s - T(h_s)\big).

If $\|v_{s+1/2} - T(v_{s+1/2})\|_\infty \le \lambda'^{\,s+1}\,\|v_0 - T(v_0)\|_\infty$ , the accelerated candidate is accepted, $v_{s+1} = v_{s+1/2}$ ; otherwise the algorithm takes a value-iteration step, $v_{s+1} = T(v_s)$ . In the Lean development the MDP is AccelVI.SafeAVI.MDP with validity predicate MDP.Valid, the operator is bellman M, and the iterates are savi M lam' α γ v0 : ℕ → (S → ℝ).

Formalization targets

Goal: Theorem 7.1

For a valid MDP, any $\lambda' \in [\lambda, 1)$ , any $\alpha, \gamma > 0$ and any $v_0$ , the S-AVI iterates converge to $v^*$ , and

v_s = v^* + O(\lambda'^{\,s}), \quad \forall s \ge 0,

that is, there is a constant $C$ with $\|v_s - v^*\|_\infty \le C\,\lambda'^{\,s}$ for every $s \ge 0$ . The constant is left unspecified, as in the paper.

Milestones

$T$ is a $\lambda$ -contraction: $\|T(v) - T(w)\|_\infty \le \lambda\|v - w\|_\infty$ (§2, p. 3).
The first period: $\|v_1 - T(v_1)\|_\infty \le \lambda\|v_0 - T(v_0)\|_\infty \le \lambda'\|v_0 - T(v_0)\|_\infty$ (p. 13).
Geometric decay of the residual: $\|v_s - T(v_s)\|_\infty \le \lambda'^{\,s}\|v_0 - T(v_0)\|_\infty$ for all $s$ (p. 14).
The residual controls the error: $\|v - v^*\|_\infty \le (1-\lambda)^{-1}\|v - T(v)\|_\infty$ for every $v$ (p. 14).

Significance

The result. Theorem 7.1 says that the safeguard costs nothing in the worst case: S-AVI converges on every MDP at rate $\lambda'$ , and with $\lambda' = \lambda$ it matches the rate of value iteration, which Theorem 6.3 of the same paper shows cannot be beaten by any first-order method uniformly over MDPs. At the same time it accepts accelerated steps whenever they reduce the residual fast enough, so it keeps the empirical speed-ups of A-VI. Remark 7.2 of the paper describes the role of $\lambda'$ : values closer to $1$ admit more accelerated steps. The guarantee also gives a computable stopping rule, since the residual bounds the distance to $v^*$ .

Formalizing it. The result is proved in the paper; to our knowledge it has not been machine-checked. This mission produces a Lean statement of the finite discounted MDP layer, the Bellman operator and Algorithm 1 itself (including its two-step recursion and its data-dependent branch), and a formal proof that the safeguarded iteration converges. The contraction property of $T$ and the residual-to-error bound are reusable for any later value-iteration development on the platform. Three sibling missions of this series pose the paper's other main results: the rate of Accelerated Value Computation on reversible chains (Theorem 5.1), the rate of Momentum Value Computation (Theorem 5.5), and the first-order lower bound (Theorem 6.3).

Difficulty

The accelerated candidate $v_{s+1/2}$ is built from two past iterates through a momentum step, and on a general MDP nothing controls it: A-VI is not a descent method, and its iterates may diverge. The natural first attempt, proving that A-VI steps contract the error, therefore fails. The difficulty in the formal setting lies elsewhere: the iterates are defined by a two-step recursion with a branch on a real inequality, so any argument must handle both branches at every period and keep the paper's indexing straight (the threshold at period $s$ is $\lambda'^{\,s+1}$ and it compares with the residual of $v_0$ , not of $v_s$ ). Existence and uniqueness of $v^*$ and the contraction property of a max of affine maps also need to be established for the specific operator, from the stochasticity of $P$ .

Formalization scope

States and actions are finite types, [Fintype S], [Fintype A], and [Nonempty A] so that the maximum in $T$ exists. Vectors are functions S → ℝ with Mathlib's sup norm, which is $\|\cdot\|_\infty$ . Rewards are arbitrary reals. The discount factor is M.lam with $0 < \lambda < 1$ inside MDP.Valid; the initial distribution $p_0$ of the paper's tuple is omitted because no statement uses it. The optimal value function enters each statement as a vector vstar with bellman M vstar = vstar; this is not vacuous, since a valid MDP has exactly one such vector. The scalar $\lambda'$ ranges over the closed interval $[\lambda, 1)$ , and $\alpha, \gamma > 0$ as in Algorithm 1, although the convergence argument does not need the step sizes to be positive. The sequence savi is indexed as the paper's $v_s$ : its recursive case s + 2 is the paper's period $s+1$ , with threshold lam' ^ (s + 2). " $v_s = v^* + O(\lambda'^s)$ for all $s \ge 0$ " is encoded as a single constant valid for every $s$ , which is stronger than an eventual big-O.

A formalization that replaced the test by the per-step condition (7.2) of Remark 7.3, used the residual of $v_s$ instead of $v_0$ , fell back to $T(v_{s+1/2})$ , or allowed $\lambda \ge 1$ would be a different theorem; none of these is posed. Remark 7.4's extension to arbitrary contractions is not posed either.

The development needs the contraction property of $T$ , the Banach fixed-point bound relating error and residual, and an induction over the iterates. Proofs of the milestones as separate lemmas are welcome, as are general statements about safeguarded fixed-point iterations for $\lambda$ -contractions that specialize to this one.

Selected references

V. Goyal and J. Grand-Clément, A First-Order Approach to Accelerated Value Iteration, Operations Research, 2023; preprint arXiv:1905.09963v7, 2021. https://arxiv.org/abs/1905.09963
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994, reprinted 2014 (Chapter 6.3, value iteration). https://doi.org/10.1002/9780470316887
Y. Nesterov, A method for solving the convex programming problem with convergence rate O(1/k²), Soviet Mathematics Doklady 27, 1983.

8 thms2 active usersReviewed

Completed

Algorithmic Game Theory Economics·Captain: mikedeng1

Sharing Sequentially Triggered Losses: Automated Conflict Resolution Through Smart Contracts 2: For Equal Losses the Midpoint Fixed-Fraction Rule Is Equidistant from All Ideal AllocationsResearch Paper

Motivation

When a contract breach propagates along a supply chain, one failure triggers the next: a supplier delivers late, the manufacturer misses its own delivery, the distributor misses its, and so on. Each link suffers a loss caused by its predecessor, and the question is who should be liable for what. Gudmundsson, Hougaard and Ko (Management Science 70(3), 2024) study this as an axiomatic cost-sharing problem, with the aim of rules simple enough to be executed automatically by a smart contract.

Their first main result characterizes a one-parameter family, the fixed-fraction rules $\varphi^\lambda$ , $\lambda\in[0,1]$ , by four axioms. The axioms do not single out a member of the family. Section 4 of the paper gives two normative arguments for the midpoint $\lambda=1/2$ . This mission formalizes the first of them, Theorem 2: for loss chains with equal losses, $\varphi^{1/2}$ is the allocation at equal Euclidean distance from every agent's "ideal" allocation. The construction follows the tradition of ideal points in bankruptcy, taxation and bargaining (Yu 1973; Chun 1988), with one ideal allocation per agent instead of a single ideal point.

Setting

There are $n\ge 1$ agents $1,\dots,n$ in a chain. Agent $i$ causes a loss $\ell_i\ge 0$ to agent $i+1$ ; a loss problem is $\ell=(\ell_1,\dots,\ell_n)\in L^n=\mathbb R^n_{\ge 0}$ , with total loss $L=\ell_1+\dots+\ell_n$ .

An allocation of $\ell$ is a vector $x\in\mathbb R^n$ of liabilities with $x_i\ge 0$ , with $x_1+\dots+x_m\ge \ell_1+\dots+\ell_m$ for $m=1,\dots,n-1$ (no initial segment of the chain pays less than the losses it caused), and with $x_1+\dots+x_n=L$ . The set of allocations is $X(\ell)$ , and the ordered allocations are $\bar X(\ell)=\{x\in X(\ell)\mid x_1\ge\dots\ge x_n\}$ .

The fixed-fraction rule with parameter $\lambda$ (Definition 1) is

\varphi^\lambda_1(\ell)=\lambda\ell_1+(1-\lambda)L,\qquad \varphi^\lambda_i(\ell)=\lambda\ell_i\quad (i\ge 2).

Each agent pays the fraction $\lambda$ of the loss it caused directly, and the initiator also pays the residual $(1-\lambda)L$ .

For $k=1,\dots,n$ the ideal allocation $c_k$ charges the first $k$ agents equally and the rest nothing:

c_k=\Big(\tfrac Lk,\dots,\tfrac Lk,0,\dots,0\Big)\qquad(k\text{ entries equal to }L/k).

When $\ell_1=\dots=\ell_n$ , $c_1=(L,0,\dots,0)$ is the allocation agent 2 would prefer among the ordered allocations, $c_{k-1}$ is the one agent $k$ would prefer, and $c_n=\ell$ is agent 1's. Distances are Euclidean: $d(x,y)=\big(\sum_i (x_i-y_i)^2\big)^{1/2}$ .

Formalization targets

Goal: Theorem 2 (p. 14)

For every $n\ge 1$ and $\ell\in L^n$ with $\ell_1=\dots=\ell_n$ ,

d\big(\varphi^{1/2}(\ell),c_k\big)=d\big(\varphi^{1/2}(\ell),c_{k'}\big)\qquad\text{for all }k,k'\in\{1,\dots,n\}.

Milestones (proof of Theorem 2, Appendix A, pp. 23–24)

For every $x\in\mathbb R^n$ and $1\le k\le n$ ,

d(x,c_k)^2=\sum_{i=1}^n x_i^2-\frac{2L}{k}\sum_{i=1}^k x_i+\frac{L^2}{k}.

If $L\neq 0$ , then $x$ is equidistant from $c_1,\dots,c_n$ if and only if there is $\alpha\in\mathbb R$ with $\sum_{i=1}^k x_i-L/2=\alpha k$ for $k=1,\dots,n$ .
If $x_1+\dots+x_n=L$ and the prefix system of milestone 2 holds, then $\alpha=L/(2n)$ , and for equal losses $x=\varphi^{1/2}(\ell)$ .

Companions (§4.1, p. 14)

Uniqueness: for equal losses, $\varphi^{1/2}(\ell)$ is the only allocation in $X(\ell)$ equidistant from $c_1,\dots,c_n$ .
Geometry: for equal losses, $\bar X(\ell)=\operatorname{conv}\{c_1,\dots,c_n\}$ .

Significance

Theorem 2 is one of the two arguments the paper gives for recommending $\varphi^{1/2}$ among the fixed-fraction rules; the other is that $\varphi^{1/2}$ is the Shapley value and the nucleolus of the associated liability game (Theorem 3, a separate mission of this series). The uniqueness companion turns the theorem into a selection principle: equalizing distances to ideal allocations determines the allocation completely. The paper also remarks that the same principle, applied to the elementary problems with unit-vector ideal allocations, selects the serial rule, which shows that the choice of ideal allocations drives the result.

The result is proved in the paper; to the best of our knowledge it has no machine-checked proof. The mission produces a formal model of loss chains, allocations and fixed-fraction rules on which the other missions of the series also build, and a checked version of the paper's computation, including the boundary cases ( $L=0$ , $n=1$ ) that the printed proof passes over.

Difficulty

The theorem is a computation, and the obstacles are the ones a careful formalization has to face rather than conceptual ones. The squared distance to $c_k$ splits into a part common to all $k$ and a part linear in the prefix sum $\sum_{i\le k}x_i$ , and the printed argument passes between the two forms by dividing by $L$ , which is not allowed for the zero problem. The uniqueness statement must also hold at $L=0$ , where every ideal allocation is the zero vector and the prefix characterization breaks down. Prefix sums over $\{1,\dots,k\}$ must be matched exactly with the $k$ nonzero coordinates of $c_k$ ; an off-by-one in either produces a different family of points. Finally, the equal-loss hypothesis cannot be dropped: for $\ell=(1,0)$ , $\varphi^{1/2}(\ell)=(1,0)=c_1$ , at distance $0$ from $c_1$ and $\sqrt{1/2}$ from $c_2$ .

Formalization scope

Agents are indexed $0,\dots,n-1$ in Lean (the paper's agent $i$ is index $i-1$ ), vectors are functions Fin n → ℝ, and nonnegativity of a loss vector is the predicate IsLoss. The fixed-fraction rule is a function of $\lambda$ , $n$ and $\ell$ ; $\lambda$ is named lam. The ideal allocation ideal ℓ k is defined for every natural $k$ but is used only for $1\le k\le n$ ; every statement quantifies over exactly that range, because ideal ℓ 0 is the zero vector in Lean and is not one of the paper's points. Distances are Mathlib's distance on EuclideanSpace ℝ (Fin n); the sup distance on Fin n → ℝ is not used, and would not even be detected by the Figure 1 example, where the sup distances to $c_1,c_2,c_3$ are also all equal.

Disclosed additions and corrections:

$n\ge 1$ in the goal, in milestone 3 and in the companions (the paper's $\mathbb N$ starts at $1$ ; at $n=0$ the convex-hull companion would be false and milestone 3's $\alpha$ undetermined).
$L\neq 0$ in milestone 2, where the paper divides by $L$ ; the equivalence is false at $L=0$ .
Milestone 3 uses $x_1+\dots+x_n=L$ where the page prints " $=1$ ".
Milestones 1 and 2 are stated for every $x\in\mathbb R^n$ ; the paper writes them for $x\in\bar X(\ell)$ but does not use that restriction.

A formalization that states the conclusion with the sup metric, that ranges $k$ over $0,\dots,n$ or $0,\dots,n-1$ , or that drops the equal-loss hypothesis does not formalize Theorem 2. Contributions of proofs of any item are welcome; milestone 1 is a finite-sum computation reusable for any distance-to-ideal-point argument in this setting.

Selected references

J. Gudmundsson, J. L. Hougaard, C. Y. Ko, Sharing Sequentially Triggered Losses: Automated Conflict Resolution Through Smart Contracts, Management Science 70(3), 1773–1786, 2024. https://doi.org/10.1287/mnsc.2023.4772 (formalized from the authors' accepted manuscript, 2023).
P. L. Yu, A class of solutions for group decision problems, Management Science 19, 936–946, 1973. https://doi.org/10.1287/mnsc.19.8.936
Y. Chun, The equal-loss principle for bargaining problems, Economics Letters 26, 103–106, 1988. https://doi.org/10.1016/0165-1765(88)90022-5
B.-G. Ju, J. D. Moreno-Ternero, Fair allocation of disputed properties, International Economic Review 58, 1279–1301, 2017. https://doi.org/10.1111/iere.12251

6 thms2 active usersReviewed

Completed

Dynamic Programming Operations Research Optimization+1·Captain: mikedeng1

A First-Order Approach to Accelerated Value Iteration 3: On the n-State Chain MDP, Every First-Order Method Has ‖v_s − v*‖∞ ≥ λ^s/(1+λ) for s = 1, …, n − 1Research Paper

Motivation

Value iteration (VI) is the basic algorithm for computing the optimal value function of a discounted Markov decision process (MDP). Its error contracts by the discount factor $\lambda$ per step, so it needs on the order of $(1-\lambda)^{-1}\log(1/\epsilon)$ iterations, which is slow when $\lambda$ is close to $1$ , the regime of interest in long-horizon planning and reinforcement learning. Goyal and Grand-Clément (arXiv:1905.09963, Operations Research 2023) read VI as gradient descent on the residual map $v \mapsto v - T(v)$ and import Nesterov's acceleration and heavy-ball momentum from convex optimization. In convex optimization the corresponding lower bounds of Nesterov (2004/2013) show that acceleration is optimal among first-order methods. The question this mission formalizes is the MDP counterpart: can any method that only combines past iterates and their Bellman images beat the rate $\lambda$ of plain VI on every MDP? Theorem 6.3 of the paper answers no.

Setting

A finite MDP consists of a state set $S$ with $|S| = n$ , a finite nonempty action set $A$ , transition probabilities $P_{iaj} \ge 0$ with $\sum_j P_{iaj} = 1$ , rewards $r_{ia} \in \mathbb{R}$ , and a discount factor $\lambda \in (0,1)$ . Its Bellman operator $T : \mathbb{R}^n \to \mathbb{R}^n$ is

T(v)_i = \max_{a \in A}\Big\{ r_{ia} + \lambda \sum_{j} P_{iaj} v_j \Big\}, \qquad i \in S,

a $\lambda$ -contraction for the sup norm $\|\cdot\|_\infty$ . Its unique fixed point $v^*$ is the optimal value function.

A sequence $(v_s)_{s \ge 0}$ in $\mathbb{R}^n$ is a first-order sequence for $T$ if

v_0 = 0, \qquad v_{s+1} \in \operatorname{span}\{v_0, \dots, v_s, T(v_0), \dots, T(v_s)\}, \quad s \ge 0 .

VI from $v_0 = 0$ ( $v_{s+1} = T(v_s)$ ) and relaxed VI ( $v_{s+1} = v_s - \alpha_s(v_s - T(v_s))$ ) from $0$ produce such sequences.

The chain MDP of Figure 1 has $n$ states and a single action. State $1$ is absorbing with reward $r_1 = 1$ ; every state $i \ge 2$ moves deterministically to $i - 1$ and earns nothing. In Lean (namespace AccelVI.LowerBound) the MDP is MDP, validity is MDP.Valid, $T$ is bellman, the chain is chainMDP n lam, and the first-order condition is IsFirstOrder T v.

Formalization targets

Goal: Theorem 6.3 (p. 12)

For every $n$ , every $\lambda \in (0,1)$ , the fixed point $v^*$ of the Bellman operator $T$ of the $n$ -state chain, every first-order sequence $(v_s)$ for $T$ , and every $s \in \{1, \dots, n-1\}$ ,

\|v_s - v^*\|_\infty \ge \frac{\lambda^s}{1+\lambda}.

Milestones

$T$ is a $\lambda$ -contraction: $\|T(v) - T(w)\|_\infty \le \lambda\|v - w\|_\infty$ (§2, p. 3).
(3.5): $(1-\lambda)\|v - w\|_\infty \le \|(I-T)(v) - (I-T)(w)\|_\infty$ (p. 6).
(3.6): $\|(I-T)(v) - (I-T)(w)\|_\infty \le (1+\lambda)\|v - w\|_\infty$ (p. 6).
On the chain, the value function is $v^*_i = \lambda^{i-1}/(1-\lambda)$ , and it is the only fixed point of $T$ (p. 12).
On the chain, every first-order sequence satisfies $v_{s,i} = 0$ for $i \ge s+1$ (p. 12).
(6.2)–(6.4): on the chain, $\|v_s - T(v_s)\|_\infty \ge \lambda^s$ for $1 \le s \le n-1$ (p. 12).

Significance

The result. Theorem 6.3 shows that, measured by the number of Bellman evaluations, no first-order method improves on the worst-case rate $\lambda$ of value iteration uniformly over MDPs, as long as the number of steps is below the number of states. In convex optimization the analogous class admits acceleration from $1 - \mu/L$ to $1 - \sqrt{\mu/L}$ ; with $\mu = 1-\lambda$ , $L = 1+\lambda$ , the analogue for MDPs would be a rate of about $1 - \sqrt{1-\lambda}$ , and this theorem rules it out. It is the reason the paper's accelerated schemes are analysed under extra structure, such as reversible policy-evaluation chains, or are safeguarded.

Formalizing it. The result is proved in the paper; no machine-checked version exists. The mission produces a checked lower bound for fixed-point iterations of Bellman operators, the contraction inequalities (3.5)–(3.6) for a general finite MDP, and an explicit value function for a hard instance. The paper's other main results, Theorems 5.1, 5.5 and 7.1, are posed as the sibling missions 1, 2 and 4.

Difficulty

The obvious argument that the error is at least the contribution of states never reached fails without control of the span: the first-order class allows arbitrary real coefficients, including ones that change with $s$ and depend on all past iterates, so one has to show that no such combination puts mass on states beyond index $s$ . The support claim has to be carried through the nonlinear max in $T$ , which is benign here only because the chain has a single action. The second ingredient converts a bound on a few coordinates of $v_s - v^*$ into a bound in sup norm with the exact constant $1/(1+\lambda)$ , which requires the two-sided inequalities (3.5)–(3.6) for $I - T$ and the explicit value $v^*_{s+1} = \lambda^s/(1-\lambda)$ .

Formalization scope

States are Fin n and are 0-based: the paper's state $i$ is index $i - 1$ , so $v^*_i = \lambda^{i-1}/(1-\lambda)$ is lam ^ k / (1 - lam) at index $k$ and " $i \ge s+1$ " is $s \le k$ . The action set of the chain is Unit.
$\|\cdot\|_\infty$ is Mathlib's sup norm on Fin n → ℝ. "span" is the real linear span Submodule.span ℝ, with both lists running to index $s$ inclusive.
$v^*$ enters the goal through its defining equation $T(v^*) = v^*$ ; it is not replaced by the explicit vector. The initial distribution $p_0$ of the paper's MDP tuple is omitted, since no result here uses it.
Pinned quantifiers. As printed, Theorem 6.3 asserts that there exists an MDP instance, with $n$ its own number of states; read literally, an instance with $n = 1$ has no admissible $s$ . The proof fixes an arbitrary $n$ and $\lambda \in (0,1)$ and uses the chain. The goal states that claim for every $n$ and $\lambda$ on the explicit chain, which implies the printed form.
$n - 1$ is natural-number subtraction, so the goal has content exactly when $n \ge 2$ .
The goal's constant is $\lambda^s/(1+\lambda)$ as printed; the sharper bound $\lambda^s/(1-\lambda)$ , which the proof's chain also gives, is not the target.
The Bellman operator and the kernel condition are the published platform definitions FoundationsML_ReinforcementLearning_BellmanOperator and FoundationsML_ReinforcementLearning_IsTransitionKernel.
A trivializing formalization would take an unsatisfiable fixed-point hypothesis or an empty first-order class. Both are satisfiable: the explicit vector is a fixed point (milestone 4), and VI from $0$ is first-order.

Contributions welcome: proofs of the contraction inequalities for general finite MDPs (reusable by every Bellman-operator mission), of the support recursion, and of the final chain of inequalities.

Selected references

V. Goyal and J. Grand-Clément, A First-Order Approach to Accelerated Value Iteration, Operations Research 71(2), 2023; preprint arXiv:1905.09963v7, 2021. https://arxiv.org/abs/1905.09963
Yu. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Springer, 2004. https://doi.org/10.1007/978-1-4419-8853-9
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994/2014. https://doi.org/10.1002/9780470316887

10 thms2 active usersReviewed

Optimization Quantum Information Theoretical Computer Science·Captain: mikedeng1

A Quantum Approximate Optimization Algorithm Applied to a Bounded Occurrence Constraint Problem I: Level-One QAOA Satisfies (1/2 + 1/(101 D^(1/2) ln D))m Equations of Max E3LIN2 for Large DResearch Paper

Motivation

The Quantum Approximate Optimization Algorithm (QAOA) of Farhi, Goldstone and Gutmann (arXiv:1411.4028) is a family of shallow quantum circuits for combinatorial optimization. At its lowest level, $p = 1$ , the circuit has two real parameters, and its output is a random bit string. The question is how many constraints that string satisfies, compared with the best classical algorithms.

Max E3LIN2 is a natural test problem. Each constraint is a linear equation modulo $2$ on exactly three bits, and the task is to satisfy as many of the $m$ equations as possible. A uniformly random string satisfies $m/2$ in expectation, and for general instances no efficient algorithm does better than $(1/2 + \varepsilon)m$ unless P = NP (Håstad 2001). The interesting regime is bounded occurrence: every bit lies in at most $D + 1$ equations.

Timeline, as recorded on p. 3 of the paper:

2000: Håstad gives a classical algorithm with approximation ratio $1/2 + \mathrm{const}/D$ (doi:10.1016/S0020-0190(00)00032-6).
2001: Trevisan shows that an efficient algorithm with ratio $1/2 + \mathrm{const}/D^{1/2}$ , for a sufficiently large constant, would imply P = NP (doi:10.1145/380752.380839).
December 2014: the first version of this paper shows that the $p = 1$ QAOA yields a string satisfying $(1/2 + 1/(22D^{3/4}))m$ equations. That beat every classical algorithm known at the time.
2015: Barak et al. (arXiv:1505.03424) and Håstad give efficient classical algorithms reaching $(1/2 + \mathrm{const}/D^{1/2})m$ .
June 2015: version 2 of this paper (arXiv:1412.6062v2) improves the QAOA bound to $(1/2 + 1/(101D^{1/2}\ln D))m$ . This mission formalizes that bound.

Setting

An instance on $n$ bits consists of $m$ equations. Equation $i$ is

x_a + x_b + x_c \equiv r_i \pmod 2,

on a triple of distinct bits $a < b < c$ , with right-hand side $r_i \in \{0, 1\}$ , and no triple carries two equations. The instance has occurrence bound $D$ if every bit appears in at most $D + 1$ equations.

Let $C(z)$ be the number of equations satisfied by the string $z$ , viewed as a diagonal operator on the $2^n$ -dimensional space spanned by the basis states $|z\rangle$ . Let $B = X_1 + \dots + X_n$ be the sum of the Pauli $X$ operators, and $|s\rangle$ the uniform superposition of all basis states. For real angles $\gamma, \beta$ the level-one QAOA state is

|\gamma, \beta\rangle = e^{-i\beta B} e^{-i\gamma C} |s\rangle .

Measuring it in the computational basis returns $z$ with probability $|\langle z|\gamma,\beta\rangle|^2$ . The expected satisfied count is

F(\gamma, \beta) = \sum_z |\langle z|\gamma,\beta\rangle|^2\, C(z).

The paper writes the objective as $m/2 + \tfrac12\sum d_{abc} Z_a Z_b Z_c$ , with $d_{abc} = (-1)^{r}$ for the equation on $a, b, c$ . The analysis is phrased through the shifted quantity $\langle\gamma,\beta|\tfrac12\sum d_{abc}Z_aZ_bZ_c|\gamma,\beta\rangle = F(\gamma,\beta) - m/2$ .

The angles used are $\beta = \pi/4$ and, for an odd integer $k$ ,

\gamma_r = \frac{1}{10 D^{1/2}} \cos\frac{\pi r}{k}, \qquad r = 0, 1, \dots, k .

Formalization targets

Goal: (44)–(45), pp. 8–9

There is a threshold $D_0$ such that for every $D \ge D_0$ there is an odd $k$ with $5\ln D \le k \le 5\ln D + 2$ , such that on every instance with occurrence bound $D$ some grid angle satisfies

F(\gamma_r, \pi/4) \ \ge\ \Big(\frac12 + \frac{1}{101\, D^{1/2} \ln D}\Big)\, m .

$D_0$ and $k$ depend on $D$ only, never on the instance. Equivalently, in the paper's form (44), $\max_r \langle\gamma_r,\pi/4|\tfrac12\sum d_{abc}Z_aZ_bZ_c|\gamma_r,\pi/4\rangle \ge m/(101D^{1/2}\ln D)$ .

Milestones

The milestones are the displayed claims of Section II, in the order the argument uses them:

the sum form of $F$ and its oddness in $\gamma$ (p. 4);
the exact single-clause formula (25);
the Taylor remainder bound (28);
hypercontractivity for degree-2 polynomials (29);
the second-moment bounds (31) and (32);
the uniform remainder bound (34) and the triangle-inequality step (37);
the Chebyshev-node inequality (39), and its consequence (41) on the grid;
the numerical threshold (43).

Significance

The theorem shows that a single layer of the QAOA, with fixed $\beta$ and $O(\ln D)$ predetermined angles, beats random guessing by $\Omega(m/(D^{1/2}\ln D))$ on every bounded-occurrence instance. Up to the $\ln D$ factor this matches the $1/2 + \Theta(D^{-1/2})$ threshold that Trevisan's hardness result places on efficient algorithms.

Two ingredients are reusable well beyond this paper. The hypercontractive inequality (29) bounds all moments of a degree-2 polynomial in uniform $\pm1$ variables, at every exponent $q = k + 2$ . The Chebyshev-node inequality (39) bounds from below the maximum of a polynomial with unit linear coefficient over the points $\cos(\pi r/k)$ . Neither is in Mathlib or on the platform in this generality.

The result is proved on paper, with explicit constants, but none of it has been machine-checked. A complete formalization would also pin down two places where the printed argument is loose (see Formalization scope).

Difficulty

The obvious approach is to expand the expected count as a power series in $\gamma$ and keep the linear term $m\gamma/2$ . That fails because the higher-order terms are not small: each clause interacts with up to $3D$ others, so the coefficient of $\gamma^j$ can grow like $D^{j/2}$ , and their signs are uncontrolled. Uniform small-angle estimates therefore lose the linear gain unless $|\gamma| \lesssim D^{-1/2}$ . Even there, the polynomial part of degree up to $k$ can cancel the linear term at any single angle. The step that needs a genuinely new input is showing that some angle of a short fixed grid avoids this cancellation for every instance at once. The remaining difficulty is bookkeeping: the threshold where the explicit constants start to work is enormous ( $\ln D$ of order several hundred), so it has to be existential.

Formalization scope

Representation. Strings are Qubits n = Fin n → Bool, with true the bit $1$ . An instance is tri : Fin m → Fin n × Fin n × Fin n (strictly increasing coordinates, injective) and rhs : Fin m → Bool. Bounded occurrence counts, for each bit, the equations whose triple contains it.
Reused quantum layer. The published QAlgorithms definitions supply act, prob, uniformState, problemHamiltonian, qaoaMixer and qaoaUnitary.
Phase operator. The state uses the full count $C$ as phase operator, not the paper's $C - m/2$ . This changes the state by a global phase only, so every probability is the same.
Averages. $E_z$ is the uniform average over all $2^n$ strings. The paper averages over the bits occurring in $c_1, c_2, c_3$ only, which gives the same number.
Pinned forms. "For large $D$ " is an existential threshold $D_0$ , uniform over instances. " $k = 5\ln D$ " is an odd $k$ with $5\ln D \le k \le 5\ln D + 2$ : the Chebyshev-node step requires $k$ odd, and $5\ln D$ is not an integer. The grid therefore has at most $5\ln D + 3$ angles rather than the printed "no more than $5\ln D$ ".
Added hypothesis. The remainder bound (34) and its consumers assume $D \ge 1$ . The printed last step $e(1+9D)^{1/2} \le 9D^{1/2}$ holds for $D \ge 1$ only, and the printed justification " $e < 3$ " does not by itself give it.
Scope. The goal is about the expected satisfied count of the measured $p = 1$ state, which is what the paper's analysis bounds. Out of scope: the repetition and sampling procedure after (45), running time, circuit size, and the search over angles.
No trivialization. The goal cannot be met by a degenerate encoding: $D_0$ and $k$ precede the instance, the grid angles are fixed by $D$ and $k$ , and the hypotheses on the instance (distinct bits, one equation per triple, occurrence at most $D + 1$ ) are satisfiable for every $D$ .
Infrastructure. A complete development needs moments of polynomials on the Boolean cube (hypercontractivity at general $q$ ), Taylor remainders for $\sin$ , an extremal inequality for polynomials on Chebyshev extreme points, and exponential-of-Pauli computations on $n$ qubits. Hypercontractivity and the Chebyshev-node inequality are stated independently of the QAOA and are the most reusable contributions. Proofs of any milestone are welcome. Platform statements of $L^4$ – $L^2$ Bonami inequalities for bilinear chaos exist, but they cover only $q = 4$ and do not imply (29).

Selected references

E. Farhi, J. Goldstone, S. Gutmann, A Quantum Approximate Optimization Algorithm Applied to a Bounded Occurrence Constraint Problem, arXiv preprint, v2, 2015. https://arxiv.org/abs/1412.6062v2
E. Farhi, J. Goldstone, S. Gutmann, A Quantum Approximate Optimization Algorithm, arXiv preprint, 2014. https://arxiv.org/abs/1411.4028
I. Dinur, E. Friedgut, G. Kindler, R. O'Donnell, On the Fourier tails of bounded functions over the discrete cube, Israel Journal of Mathematics 160 (2007), 389–412. https://doi.org/10.1007/s11856-007-0068-z
J. Håstad, Some optimal inapproximability results, Journal of the ACM 48 (2001), 798–859. https://doi.org/10.1145/502090.502098
J. Håstad, On bounded occurrence constraint satisfaction, Information Processing Letters 74 (2000), 1–6. https://doi.org/10.1016/S0020-0190(00)00032-6
L. Trevisan, Non-approximability results for optimization problems on bounded degree instances, Proc. 33rd ACM STOC (2001), 453–461. https://doi.org/10.1145/380752.380839
B. Barak et al., Beating the random assignment on constraint satisfaction problems of bounded degree, ECCC TR15-082 / arXiv preprint, 2015. https://arxiv.org/abs/1505.03424

18 thms2 active usersReviewed

Completed

Algorithmic Game Theory Mechanism Design Operations Research·Captain: mikedeng1

Combinatorial Auctions with Interdependent Valuations: SOS to the Rescue 2: Random-Sampling VCG Is Ex-Post IC-IR and a 4-Approximation to Welfare for Separable SOS ValuationsResearch Paper

Motivation

In many auctions a bidder's value for what is sold depends on information held by other bidders: the value of an oil-drilling lease depends on every bidder's geological survey, the value of a piece of art on what other experts know about its provenance. This is the interdependent values model of Milgrom and Weber (1982). With interdependent values the standard private-value tools fail: the Vickrey–Clarke–Groves (VCG) mechanism is no longer incentive compatible, exact efficiency in ex-post equilibrium requires a single-crossing condition, and with multidimensional signals maximizing welfare is generically impossible even in Bayes–Nash equilibrium (Jehiel and Moldovanu 2001). Without some structural condition on how values respond to others' information, even a single-item auction can force every truthful randomized mechanism to lose a factor of order $n$ (Example 1.3, after Eden et al. 2018), when values treat the signals as complements.

Eden, Feldman, Fiat, Goldner and Karlin (arXiv:1903.08384, Mathematics of Operations Research 2024) identify such a condition, submodularity over signals (SOS), and show that under SOS simple randomized mechanisms recover a constant fraction of the optimal welfare in rich settings. This mission formalizes their result for combinatorial auctions with multidimensional signals and separable SOS valuations, where the mechanism is a random-sampling variant of VCG with explicit payments.

Timeline of the line of work:

Milgrom and Weber (1982): the interdependent values model.
Jehiel and Moldovanu (2001): with multidimensional signals, welfare maximization is generically impossible even in Bayes–Nash equilibrium.
Chawla, Fu and Karlin (2014): revenue approximation in interdependent value settings under single crossing.
Roughgarden and Talgam-Cohen (2016): characterization of ex-post IC for single-parameter settings by monotone allocation rules.
Eden, Feldman, Fiat and Goldner (2018): welfare approximation for single-item auctions under a relaxed c-single crossing condition; an SOS notion also appears there.
Eden, Feldman, Fiat, Goldner and Karlin (2019, arXiv v2): welfare approximation under SOS, without single crossing, for downward-closed single-parameter settings and combinatorial auctions; the subject of this mission.

Setting

There are $n$ agents and $m$ items; a bundle is a set $T \subseteq [m]$ . Each agent $i$ privately holds a signal $s_{iT} \ge 0$ for every bundle $T$ , and $s_T = (s_{1T}, \dots, s_{nT})$ collects all agents' signals for $T$ . Agent $i$ 's value for bundle $T$ is $v_{iT}(s_T) \ge 0$ , a known function of $s_T$ , weakly increasing in every signal and strictly increasing in $s_{iT}$ ; the empty bundle is worth $0$ .

A function $w$ of the signal vector is SOS when raising a single coordinate helps at least as much at a coordinatewise lower profile of the other coordinates: for every coordinate $j$ , $x, \delta \ge 0$ and profiles $s' \le s$ off $j$ ,

w(s_{-j}, x + \delta) - w(s_{-j}, x) \le w(s'_{-j}, x + \delta) - w(s'_{-j}, x).

The valuations are separable SOS when

v_{iT}(s_T) = g_{-iT}(s_{-iT}) + h_{iT}(s_{iT}),

with $g_{-iT}$ (depending only on the other agents' signals for $T$ ) and $h_{iT}$ weakly increasing and $g_{-iT}$ SOS.

An allocation gives agent $i$ the bundle $T_i$ , with the bundles pairwise disjoint. A deterministic mechanism maps reported signals to an allocation and payments. It is ex-post incentive compatible (IC) if, whatever the true signals, no agent gains by misreporting when the others report truthfully, where the agent's utility is her value at the true signals for the bundle she receives minus her payment; it is ex-post individually rational (IR) if the truthful utility is nonnegative. A randomized mechanism is universally ex-post IC-IR when every deterministic mechanism in its support is.

Random-Sampling VCG (RS-VCG) partitions the agents uniformly at random into $A$ and $B$ . For $j \in B$ it sets the proxy weight

w_{jT} := v_{jT}(\tilde s_{jT}, \tilde s_{AT}, 0_{B - jT}),

the value with the bundle- $T$ signals of the other members of $B$ replaced by $0$ . It allocates to $B$ a feasible allocation $\{T_i\}_{i\in B}$ maximising $\sum_{i \in B} w_{iT_i}$ , and a winner $i \in B$ pays

p_i(\tilde s) = g_{-iT_i}(\tilde s_{-iT_i}) - g_{-iT_i}(\tilde s_{AT_i}, 0_{B-iT_i}) - \sum_{j \in B\setminus\{i\}} w_{jT_j} + w_{-i},

where $w_{-i}$ is the maximum proxy welfare of an allocation to $B \setminus \{i\}$ .

Formalization targets

Goal: Theorem 5.1 (p. 17)

For separable SOS valuations, RS-VCG is ex-post IC and IR for every partition, and for every true profile $s$ and every feasible allocation $(S^*_i)$ ,

\sum_i v_{iS^*_i}(s_{S^*_i}) \le 4\, \mathbb{E}_B\Bigl[\sum_i v_{iT_i(B)}(s_{T_i(B)})\Bigr].

Milestones

Observation 2.2 (p. 12): a separable SOS valuation is SOS.
Display (5) (p. 17): $\mathbb{E}_B[w_{iT}\cdot\mathbf 1_{i\in B}] \ge \frac{v_{iT}(s_T)}{2}\cdot\frac12$ for every agent $i$ and bundle $T$ .
Payment sign (p. 17): the payments $p_i(\tilde s)$ are nonnegative.
IC display (p. 18): for every partition, truthful reporting maximises each agent's utility.
IR display (p. 18): for every partition, the truthful utility is nonnegative.

Significance

The theorem shows that VCG-style reasoning survives interdependence when the dependence on other agents' information enters additively and submodularly: separability makes the payment absorb the effect of the others' signals, so that each agent of $B$ faces the proxy welfare as its objective. It gives a constant-factor welfare guarantee in ex-post equilibrium for combinatorial auctions with multidimensional interdependent signals, a setting in which exact efficiency is generically out of reach. The construction is the template for the paper's single-dimensional results in §6.

The result is proved in the paper; to our knowledge it has no machine-checked proof. Formalizing it produces a reusable Lean model of interdependent-value combinatorial auctions (multidimensional signals, ex-post IC/IR, universal truthfulness of random mixtures) and of the SOS condition, and a checked account of the VCG accounting identity in this setting.

Difficulty

The approximation part rests on the Key Lemma 3.1: a uniformly random half of the other agents' signals set to zero keeps, in expectation, half of an SOS value. The obvious argument — monotonicity alone — gives no constant: with values depending on many signals, zeroing half of them can destroy almost all of the value, and the SOS condition is exactly what rules this out. The incentive part is where the obvious transfer of VCG fails: the proxy weight $w_{iT}$ of agent $i$ is not its value, and the true value $v_{iT}$ depends on signals that the proxy zeroes. Without separability, the payment of a VCG-style rule would itself depend on the agent's report (the paper's remark at the start of §5), and alignment of the agent's utility with the proxy objective breaks. Ties in the argmax and agents receiving the empty bundle must be handled for every tie-breaking rule.

Formalization scope

Agents are Fin n and items Fin m, with $n, m$ arbitrary; bundles are Finset (Fin m). Signals are NNReal, one per (agent, bundle), and $v_{iT}$ is a function of the bundle- $T$ signal vector. The empty bundle is worth $0$ ; monotonicity, strict own-signal monotonicity and the separable decomposition are assumed for nonempty bundles. The function $g_{-iT}$ is written on the whole vector with the hypothesis that it ignores coordinate $i$ . The decomposition $(g, h)$ is data of the mechanism, since the payments use $g$ .

The allocation is produced by an arbitrary selector returning a feasible maximiser of the proxy welfare for every partition and report; all statements hold for every such selector. $w_{-i}$ is a maximum over the finite set of feasible allocations to $B \setminus \{i\}$ . Agents of $A$ , and agents of $B$ that receive the empty bundle, pay $0$ (the paper defines payments for winners only). The expectation over the partition is the uniform average $2^{-n}\sum_{B \subseteq [n]}$ , never an existential or universal over $B$ ; the approximation is stated for every feasible comparator allocation, with welfare at true values under truthful reports, never for proxy welfare or through a supremum. IC and IR are stated for each partition with the paper's explicit payments, not with existentially chosen payments.

A complete development needs finite averages over subsets, the Key Lemma 3.1 for SOS functions (posed in the companion mission on RS-V and not restated here), and finite argmax reasoning; the SOS layer and the combinatorial mechanism model are reusable for the other missions of this series. Proofs of the milestones, and of the d-SOS variant mentioned after the proof (a $2(d+1)$ -approximation, not posed here), are welcome.

The source is the arXiv preprint arXiv:1903.08384v2 (2 June 2019); all page and display numbers refer to it, not to the journal version in Mathematics of Operations Research (2024).

Selected references

A. Eden, M. Feldman, A. Fiat, K. Goldner, A. R. Karlin, Combinatorial Auctions with Interdependent Valuations: SOS to the Rescue, arXiv:1903.08384v2, 2019; Mathematics of Operations Research, 2024. https://arxiv.org/abs/1903.08384
P. R. Milgrom, R. J. Weber, A Theory of Auctions and Competitive Bidding, Econometrica 50(5), 1982. https://doi.org/10.2307/1911865
P. Jehiel, B. Moldovanu, Efficient Design with Interdependent Valuations, Econometrica 69(5), 2001. https://doi.org/10.1111/1468-0262.00241
S. Chawla, H. Fu, A. R. Karlin, Approximate Revenue Maximization in Interdependent Value Settings, EC 2014. https://doi.org/10.1145/2600057.2602858
A. Eden, M. Feldman, A. Fiat, K. Goldner, Interdependent Values without Single-Crossing, EC 2018. https://arxiv.org/abs/1806.03865
T. Roughgarden, I. Talgam-Cohen, Optimal and Robust Mechanism Design with Interdependent Values, ACM TEAC 4(3), 2016. https://doi.org/10.1145/2897185

8 thms2 active usersReviewed

Completed

Algorithmic Game Theory Economics Operations Research+1·Captain: mikedeng1

Proof-of-Work Cryptocurrencies: Does Mining Technology Undermine Decentralization? 3: Sensitivities of Equilibrium Hash Rates to Mining Capacity and Reward, and Shares Shift to Smaller MinersResearch Paper

Motivation

Bitcoin and other proof-of-work cryptocurrencies rely on miners, who spend computing power ("hash rate") to win the right to append a block and collect a reward. The security argument for such systems assumes that no single miner, or small coalition, controls a large share of the total hash rate. Whether the economics of mining push the system towards or away from that decentralized state is therefore a basic question for anyone designing or regulating these protocols.

A. Capponi, S. Ólafsson and H. Alsabah, in Proof-of-Work Cryptocurrencies: Does Mining Technology Undermine Decentralization? (arXiv:2106.09783v1, 2021), model mining as a contest in which miners differ in their cost per hash and face a common capacity constraint. Their §4.3 asks how equilibrium hash rates respond to the model's parameters. This mission formalizes the answer for two of them: the capacity parameter $\gamma$ , which measures how quickly a miner's operating cost grows with its scale, and the mining reward $R$ . The finding is that increasing either parameter shifts hash rate share from large miners to small ones. This is the third mission of a four-part series on the paper; the first poses the existence and structure of the mining equilibrium, the second its sensitivity to mining costs.

Setting

There are $n \ge 2$ active miners, indexed $i = 1, \dots, n$ , with costs per hash $0 < c_1 \le c_2 \le \dots \le c_n$ (sorted, without loss of generality), a reward $R > 0$ and a capacity parameter $\gamma > 0$ . Miner $i$ choosing hash rate $h_i$ earns $(h_i/H)R - c_ih_i - (\gamma/2)h_i^2$ , where $H = \sum_j h_j$ is the aggregate hash rate (the paper's (3.4)). The cumulative cost is $c^{(n)} = c_1 + \dots + c_n$ .

In the paper's Proposition 4.1, the equilibrium aggregate hash rate is the positive root of $\gamma H^2 + c^{(n)}H - (n-1)R = 0$ , and the equilibrium hash rates are given in closed form. The paper's appendix (B.3) writes them as functions of the active miners' data:

g = g(c_1,\dots,c_n,\gamma,R) = \frac{\sqrt{(c^{(n)})^2 + 4(n-1)R\gamma} - c^{(n)}}{2\gamma},\qquad f_i = f_i(c_1,\dots,c_n,\gamma,R) = g\,\frac{R - c_i g}{R + \gamma g^2},

with $H^* = g$ and $h^*_i = f_i$ . Miner $i$ is active exactly when $R - c_i g > 0$ . The hash rate share of miner $i$ is $h^*_i/H^*$ .

The paper's sensitivities are derivatives of these maps at a state where small parameter changes leave the set of active miners unchanged (pp. 15–16). For $x \in \{\gamma, R\}$ , (B.4) splits the derivative of $h^*_i$ into a direct part, $\Delta^{(x)}_{i,1} = \partial f_i/\partial x$ with $g$ held fixed, and an indirect part through the aggregate, $\Delta^{(x)}_{i,2} = (\partial f_i/\partial g)(\partial g/\partial x)$ .

Formalization targets

Goal: Proposition 4.8 (p. 20)

For every active miner $i$ ,

\frac{\partial h^*_i}{\partial\gamma} = \Delta^{(\gamma)}_{i,1}+\Delta^{(\gamma)}_{i,2},\quad \Delta^{(\gamma)}_{i,1}<0,\quad \Delta^{(\gamma)}_{i,2}>0 \iff \frac{h^*_i}{H^*}<\frac12,

\frac{\partial h^*_i}{\partial R} = \Delta^{(R)}_{i,1}+\Delta^{(R)}_{i,2} > 0,\quad \Delta^{(R)}_{i,1}>0,\quad \Delta^{(R)}_{i,2}<0 \iff \frac{h^*_i}{H^*}<\frac12,

and the derivatives of $h^*_i/H^*$ with respect to $\gamma$ and to $R$ are increasing in $i$ , for $1 \le i \le n$ .

Milestones (the steps of the appendix proof)

(B.2), p. 39: $\partial H^*/\partial\gamma = -(H^*)^2/(c^{(n)}+2\gamma H^*) < 0$ and $\partial H^*/\partial R = (n-1)/(c^{(n)}+2\gamma H^*) > 0$ .
p. 40: $\partial f_i/\partial\gamma = -g^3(R-c_ig)/(R+\gamma g^2)^2 < 0$ and $\partial f_i/\partial R = g^2(c_i+\gamma g)/(R+\gamma g^2)^2 > 0$ .
(B.4), pp. 40–41: closed forms of $\partial h^*_i/\partial\gamma$ and $\partial h^*_i/\partial R$ .
(B.6), pp. 42–43: closed forms of the share derivatives, and the p. 43 rewrites in which $i$ enters only through $f_i$ and $c_i + \gamma f_i$ .

Significance

The result. Proposition 4.8 says that a tighter capacity constraint and a larger reward both favour small miners. The direct effect of a larger $\gamma$ lowers every miner's hash rate. The indirect effect raises the hash rate of every miner with less than half of the total, because the aggregate falls and the marginal gain of hashing rises. For the reward, every miner's hash rate rises, but the share derivatives are increasing in the miner's index, i.e. in its cost: costlier, smaller miners gain share. Table 1 of the paper (p. 16) lists the signs; this proposition supplies the $\gamma$ and $R$ columns. The paper uses it to argue that rising block rewards or tighter hardware constraints work against concentration (§4.3.3), in contrast to cost reductions from new hardware (§5).

Formalizing it. The result is proved in the paper by explicit differentiation (Appendix B). No machine-checked version exists. The mission produces checked closed forms of every derivative in (B.2), (B.4) and (B.6) for the $\gamma$ and $R$ directions, the sign analysis, and the monotonicity in $i$ . The proof text on p. 43 says "decreasing in $i$ " where the proposition says "increasing"; a formal proof settles which is right (the displayed expressions give increasing, which is what is posed).

Difficulty

Each derivative is an exercise; the difficulty lies in keeping the algebra correct over several layers. The aggregate $g$ is the root of a quadratic, so its derivatives involve the square root, and every simplification of (B.4) and (B.6) uses the root identity $\gamma g^2 + c^{(n)}g = (n-1)R$ , i.e. $\sqrt{(c^{(n)})^2+4(n-1)R\gamma} = c^{(n)} + 2\gamma g$ , and the first-order identity $c_i + \gamma f_i = (R/g)(1 - f_i/g)$ . The sign of the indirect parts is not visible from the raw derivative: it requires rewriting $\partial f_i/\partial g$ so that the threshold $f_i/g = 1/2$ appears. The positivity of $\partial h^*_i/\partial R$ needs a separate bound, since its indirect part can be negative. The monotonicity in $i$ is the most delicate part: it is not true term by term in (B.6) as first displayed, and only becomes visible after the p. 43 rewrite, which separates the dependence on $f_i$ (decreasing in $i$ ) from that on $c_i + \gamma f_i$ (increasing in $i$ ), with coefficients whose signs again come from the root identity. Without the sorting of the costs, the monotonicity claim is false.

Formalization scope

Everything lives in the namespace PoWMining.CapacityStatics. Miners are Fin n, 0-based: Lean miner i is the paper's miner $i+1$ , so "increasing in $i$ " is Monotone on Fin n, and "increasing" is weak, as in the paper's footnote 12. The definition ClosedForms provides cumCost ( $c^{(n)}$ ), gH ((4.1)/(B.3), with both branches of (4.1)), fH ( $f_i$ with the aggregate as a free argument), hstar, share, and the standing assumptions Standing: $n\ge2$ , $R>0$ , $\gamma>0$ , $c_k>0$ , costs sorted, and $R - c_kg > 0$ for every $k$ (all $n$ miners active). The condition $\gamma > 0$ is the paper's: (B.3) defines $g$ only for $\gamma>0$ . The definition Sensitivities defines the four $\Delta$ 's as derivatives (Lean deriv) of the (B.3) maps, never by their closed forms; derivative claims in theorems are stated with HasDerivAt, so a junk value of deriv at a non-differentiable point cannot make a statement true.

The mission takes the active miners' costs as its data, which is the paper's own meaning of a sensitivity at a fixed active set. That $f_i$ and $g$ are the equilibrium of the mining game is Proposition 4.1, posed in mission 1 of this series; the cost derivatives, (B.5) and $\partial f_i/\partial g$ are posed in mission 2. This mission uses those identities but does not pose them.

Trivializing formalizations are ruled out: the $\Delta$ 's are derivatives, not formulas whose signs can be read off; the standing assumptions are satisfiable (two miners with $c = (1,1)$ , $\gamma = 1$ , $R = 3$ give $g = 1$ , $h^*_i = 1/2$ ); and the monotonicity is stated for derivatives asserted to exist.

Needed infrastructure: one-variable calculus in Mathlib (HasDerivAt for square roots, quotients and compositions) and finite sums. A reusable lemma library for $g$ (the root identity, positivity, $c^{(n)}+2\gamma g > 0$ ) serves all three of missions 1–3 and is welcome, as are proofs of the milestones in any order.

Selected references

A. Capponi, S. Ólafsson, H. Alsabah, Proof-of-Work Cryptocurrencies: Does Mining Technology Undermine Decentralization?, arXiv preprint, 2021. https://arxiv.org/abs/2106.09783v1
G. Tullock, The Welfare Costs of Tariffs, Monopolies, and Theft, Western Economic Journal 5(3), 224–232, 1967 (the rent-seeking model the paper builds on). https://doi.org/10.1111/j.1465-7295.1967.tb01923.x
S. Nakamoto, Bitcoin: A Peer-to-Peer Electronic Cash System, 2008. https://bitcoin.org/bitcoin.pdf

8 thms2 active usersReviewed

Algorithmic Game Theory Economics·Captain: mikedeng1

Algorithms for Competitive Division of Chores 1: At Most min{(2m−1)^{n(n−1)/2}, (2n−1)^{m(m−1)/2}} Competitive Utility Profiles and Pareto-Frontier Faces Meeting the Negative OrthantResearch Paper

Motivation

Many allocation problems divide work, not goods: shifts among employees, teaching loads among faculty, cleaning duties among housemates, maintenance tasks among the owners of a shared resource. For divisible goods the standard fair and efficient solution is the competitive rule (competitive equilibrium from budgets): give every agent a budget, find prices at which every agent demands what she receives, and the outcome is Pareto optimal and envy-free (weighted by budgets). For goods with additive utilities this rule is single-valued and is the solution of the Eisenberg–Gale convex program, which yields polynomial-time algorithms.

For chores (bads) the competitive rule keeps its fairness and efficiency guarantees but loses the convex structure: Bogomolnaia, Moulin, Sandomirskiy and Yanovskaya (BMSY17) showed it is generally multi-valued, with competitive allocations corresponding to critical points, not maximizers, of the Nash social welfare on the Pareto frontier. Brânzei and Sandomirskiy (arXiv:1907.01766v2, Mathematics of Operations Research, 2024) enumerate all competitive utility profiles in strongly polynomial time when the number of agents or the number of chores is fixed. Their counting result is the target of this mission.

Setting

There are $n$ agents and $m$ divisible chores, one unit of each. Agent $i$ 's value for one unit of chore $j$ is $v_{i,j}<0$ , and her budget is $b_i<0$ . A feasible allocation is $z\in\mathbb R^{n\times m}_{\ge0}$ with $\sum_i z_{i,j}=1$ for every chore $j$ ; agent $i$ 's utility is $u_i(z_i)=\sum_j v_{i,j}z_{i,j}$ , the utility profile is $u(z)=(u_1(z_1),\dots,u_n(z_n))$ , and $\mathcal U(v)$ is the set of utility profiles of feasible allocations.

A feasible allocation $z$ is competitive for budgets $b$ if there are prices $p\in\mathbb R^m_{<0}$ such that for every agent $i$ the bundle $z_i$ costs $p(z_i)=\sum_j p_jz_{i,j}\le b_i$ and maximizes $u_i$ among all bundles $x\ge0$ with $p(x)\le b_i$ . A competitive utility profile is $u(z)$ for a competitive $z$ .

$z$ is Pareto optimal if no feasible allocation makes every agent weakly better off and some agent strictly better off; the Pareto frontier $\mathcal U^*(v)$ consists of their utility profiles. For weights $\tau\in\mathbb R^n_{>0}$ the face $f_\tau$ of the Pareto frontier is the set of maximizers of $\langle\tau,u\rangle=\sum_i\tau_iu_i$ over $u\in\mathcal U(v)$ .

The proof runs through graphs. The consumption graph $G_z$ links agent $i$ and chore $j$ when $z_{i,j}>0$ . The maximal weighted welfare (MWW) graph $G_\tau(v)$ links $i$ and $j$ when $\tau_i|v_{i,j}|\le\tau_{i'}|v_{i',j}|$ for every agent $i'$ . A family of graphs is rich if every Pareto optimal profile in $\mathbb R^n_{<0}$ is $u(z)$ for a feasible $z$ whose consumption graph is in the family. Along a path $\mathcal P=(i_1,j_1,\dots,i_L,j_L,i_{L+1})$ the product of disutilities is $\pi(\mathcal P)=\prod_{k=1}^L|v_{i_k,j_k}|/|v_{i_{k+1},j_k}|$ .

Formalization targets

Goal: Corollary 25 (p. 27)

For $n,m\ge1$ , $v\in\mathbb R^{n\times m}_{<0}$ and $b\in\mathbb R^n_{<0}$ ,

\#\{f\text{ face of the Pareto frontier}: f\cap\mathbb R^n_{<0}\ne\emptyset\}\le B,\qquad \#\{\text{competitive utility profiles for } b\}\le B,

B=\min\Big\{(2m-1)^{\frac{n(n-1)}{2}},\ (2n-1)^{\frac{m(m-1)}{2}}\Big\}.

Milestones

Lemmas 36–38 (pp. 50–51): competitive allocations are characterized by the maximal bang-per-buck condition with budget exhaustion; prices satisfy $p_j=v_{i,j}b_i/u_i(z_i)$ on consumed chores; competitiveness is equivalent to inequalities (14) and to weighted-welfare maximality with weights $b_i/u_i(z_i)$ .
Theorem 9 and Corollary 10 (p. 14): the first and second welfare theorems, and Pareto indifference.
Lemma 14 (p. 17): Pareto optimality $\iff$ no simple profitable trading cycle $\iff$ $G_z\subseteq G_\tau(v)$ for some $\tau>0$ $\iff$ weighted-welfare maximality. Corollary 15 is included as a companion statement.
Lemma 18, Lemma 19, Corollary 21 (pp. 21–23): faces correspond to MWW graphs; MWW graphs, and those with no lonely agents, form rich families; the latter correspond to the faces meeting $\mathbb R^n_{<0}$ .
Lemma 22 (p. 23): $\mathrm{MWW}_{non\text{-}lonely}(v)=\mathrm{MWW}_{non\text{-}lonely}(v^T)$ .
Lemma 23, first bullet (p. 24): a rich family of at most $B$ graphs exists.
Lemma 26 (p. 29): a competitive profile is determined by its consumption graph through formula (4).

Significance

The result. Corollary 25 says that the competitive rule for chores, although multi-valued and non-convex, has at most polynomially many outcomes when $n$ or $m$ is fixed, and that the Pareto frontier has polynomially many faces meeting the negative orthant. It is the exact mathematical content of the paper's algorithmic Theorem 17: an enumeration that tries every graph of a rich family and recovers at most one candidate profile from each cannot miss a competitive profile and cannot produce more than $B$ of them. For $n=2$ the bound $2m-1$ is attained in Example 1 of the paper by the face count.

Formalizing it. The result is proved in the paper; nothing is known to be machine-checked. The mission builds a reusable layer for linear Fisher-type economies with bads: the competitive rule with negative prices and budgets, welfare theorems, the trading-cycle and weighted-welfare criteria of Pareto optimality, and the graph-theoretic description of the faces of a polytope of feasible utilities. Lemma 14 and Lemma 18 are of independent use for any linear allocation model.

Difficulty

The obvious argument for goods, uniqueness of the equilibrium utility profile via a strictly concave program, fails: for chores there may be several competitive profiles, even on a single closed face (in Example 1 of the paper, both competitive profiles lie on one edge of the frontier). The count must therefore pass through combinatorics. Two steps carry the weight. First, the faces of the Pareto frontier, a continuous object, must be put in bijection with a finite set of graphs, and the graphs must be chosen so that each competitive profile is realized by an allocation whose consumption graph is exactly an MWW graph, not merely contained in one. Second, the size bound cannot come from counting bipartite graphs, which gives only $2^{nm}$ ; it has to exploit the structure of MWW graphs, and its second term, polynomial in $n$ for fixed $m$ , requires the agent–chore symmetry of Lemma 22, whose natural route goes through the second welfare theorem.

Formalization scope

Agents are Fin n, chores Fin m (0-based); values, budgets and prices are real functions; graphs are Finset (Fin n × Fin m) of edges; a path is a record of its length $L$ , $L+1$ agents and $L$ chores. Faces are the sets of maximizers of $\langle\tau,u\rangle$ over $\mathcal U(v)$ for $\tau\in\mathbb R^n_{>0}$ , the dual representation of p. 16. Counts are Set.encard in $\mathbb N\cup\{\infty\}$ and the bound $B$ is computed in $\mathbb N$ . Added relative to the paper: $n\ge1$ and $m\ge1$ (the paper's sets of agents and chores are non-empty) where a statement needs them. Not formalized: the running-time claims (Theorem 17, the second bullet of Lemma 23), item 4 of Lemma 38 (critical points of the Nash social welfare), and the sentence on p. 27 that each face carries at most one competitive profile, which is false for closed faces.

The following formalizations would trivialize the goal and are ruled out: a competitive allocation without the budget constraint $p(z_i)\le b_i$ ; non-negative values, budgets or prices; faces exposed by $\tau\ge0$ or by $\tau$ of arbitrary sign; counts over sets assumed finite; Pareto optimality restricted to a subclass of allocations.

All definitions live in CompetitiveChores.RichFamily; Mathlib supplies only finite sums and products, Finset, and Set.encard. Contributions welcome: proofs of the appendix lemmas (pure linear algebra on finite sums), of Lemma 14 (the cycle-cancelling argument of Appendix B), and of the two-agent splits-and-cuts count inside Lemma 23.

Selected references

S. Brânzei and F. Sandomirskiy, Algorithms for Competitive Division of Chores, arXiv:1907.01766v2 (2023); Mathematics of Operations Research (2024). https://arxiv.org/abs/1907.01766v2
A. Bogomolnaia, H. Moulin, F. Sandomirskiy and E. Yanovskaya, Competitive division of a mixed manna, Econometrica 85(6), 2017. https://doi.org/10.3982/ECTA14438
A. Bogomolnaia, H. Moulin, F. Sandomirskiy and E. Yanovskaya, Dividing bads under additive utilities, Social Choice and Welfare 52, 2019. https://doi.org/10.1007/s00355-018-1157-x
N. Devanur, C. Papadimitriou, A. Saberi and V. Vazirani, Market equilibrium via a primal–dual algorithm for a convex program, Journal of the ACM 55(5), 2008. https://doi.org/10.1145/1411509.1411512

15 thms2 active usersReviewed

Completed

Algorithmic Game Theory Analysis Mechanism Design+1·Captain: mikedeng1

Mechanism Design under Approximate Incentive Compatibility 4: Randomized Perturbed Delayed Mechanisms Gain Ω(ε^(α/(2α−1))) Revenue Under Local α-Power EnvelopesResearch Paper

Motivation

Classical mechanism design assumes that agents optimize exactly: a buyer facing a menu of lotteries picks the one that maximizes expected utility, and an incentive compatible (IC) mechanism makes truth-telling optimal. Buyers that are only approximately rational, or that face small costs of computing or reporting, need only be made to prefer the truth up to a slack $\varepsilon$ . Approximate incentive compatibility ( $\varepsilon$ -IC) is the corresponding relaxation of the IC constraints. It is also used in computer science as a robustness notion and in learning settings where a mechanism is only approximately optimal for the buyer.

Balseiro, Besbes and Castro (arXiv:2103.03403) ask how much revenue a seller of one item can gain from such a relaxation. For a single buyer, Myerson's theory gives the IC optimum as a posted price. With $\varepsilon$ -IC the feasible set grows, and the paper determines the order of the additional revenue as $\varepsilon\downarrow 0$ .

Timeline. The rounding argument attributed to Noam Nisan, first used by Balcan, Blum, Hartline and Mansour (FOCS 2005), turns an $\varepsilon$ -IC mechanism into an IC one with a small revenue loss; for a single buyer it bounds the gain by $O(\sqrt\varepsilon)$ for every distribution (Proposition 1 of the paper). Balseiro, Besbes and Castro (2021; v2 2022; Operations Research 2024) prove an $\tilde O(\varepsilon^{\alpha/(2\alpha-1)})$ upper bound (Theorem 1) under a curvature condition on the revenue curve, show that deterministic mechanisms gain only $\Theta(\varepsilon)$ (Theorem 2), and give a matching $\Omega(\varepsilon^{\alpha/(2\alpha-1)})$ lower bound by an explicit randomized construction (Theorem 3). This mission formalizes the lower bound.

Setting

A seller sells one item to one buyer. The buyer's value $v$ has a cumulative distribution function $F$ with density $f$ supported on $S=[0,\bar v]$ , $\bar v>0$ . Assumption 1 requires $f$ to have bounded variation on $S$ . Write $\bar F=1-F$ , the revenue curve $R(v)=v\,\bar F(v)$ (the revenue of a posted price $v$ ), and $\dot R(v)=\bar F(v)-v f(v)$ .

A direct mechanism $m=(x,t)$ gives a buyer who reports $v$ the item with probability $x(v)\in[0,1]$ and charges $t(v)$ . It is individually rational (IR) if $v\,x(v)-t(v)\ge 0$ for all $v\in S$ , and $\varepsilon$ -incentive compatible (IC $_\varepsilon$ ) if

v\,x(v)-t(v)\ \ge\ v\,x(v')-t(v')-\varepsilon\qquad\forall v,v'\in S.

$\mathcal M(\varepsilon)$ is the set of IR and IC $_\varepsilon$ mechanisms, $\Pi(m)=\int_0^{\bar v}t(v)f(v)\,dv$ the expected revenue, and $\Pi^\star(\mathcal M(\varepsilon))=\sup_{m\in\mathcal M(\varepsilon)}\Pi(m)$ . A best reporting mapping $v^\star$ for $m$ picks, for each value $v$ , a report in $\arg\max_{w\in S}\{v\,x(w)-t(w)\}$ .

Local $\alpha$ -power envelopes (Definition 1): $R$ has a unique maximizer $p^\star$ on $S$ , interior, and there are $\alpha>1$ , $\kappa_L,\kappa_U>0$ and $\ell>0$ with $(p^\star-\ell,p^\star+\ell)\subset(0,\bar v)$ and

\kappa_L\alpha|v-p^\star|^\alpha\le(p^\star-v)\,\dot R(v)\le\kappa_U\alpha|v-p^\star|^\alpha\quad\text{on }(p^\star-\ell,p^\star+\ell).

The parameter $\alpha$ measures how flat $R$ is at its peak; $\alpha=2$ is the generic smooth case.

Perturbed delayed mechanisms (§5.1). For $\mu,\delta>0$ the buyer is steered to report $v^\star(v\,|\,\mu,\delta)$ , equal to $0$ below $p^\star-\delta$ , to $v-\mu$ on $[p^\star-\delta,p^\star+\delta+\mu]$ , and to $p^\star+\delta$ above. With $w$ its generalized inverse, the allocation $x_{pd}$ solves on $[0,p^\star+\delta]$ the ordinary and delay differential equations

\dot x(v)=\frac{x(v)}{w(v)-v}\ \ (v\le p^\star-\delta),\qquad x(0)=\frac{\varepsilon}{p^\star-\delta},\qquad \dot x(v)=\frac{x(v)-x(v^\star(v))}{w(v)-v}\ \ (p^\star-\delta\le v\le p^\star+\delta),

is $1$ above $p^\star+\delta$ , and the payment $t_{pd}$ is given explicitly in terms of $x_{pd}$ and $v^\star$ .

Formalization targets

Goal: Theorem 3 (p. 27)

Under Assumption 1 and local $\alpha$ -power envelopes there are $C>0$ and $\varepsilon_0>0$ such that for all $\varepsilon\in(0,\varepsilon_0]$ some $m\in\mathcal M(\varepsilon)$ satisfies

\Pi(m)\ \ge\ \Pi^\star(\mathcal M(0))+C\,\varepsilon^{\alpha/(2\alpha-1)} .

The constants may depend on the distribution, but not on $\varepsilon$ .

Milestones

Lemma 5 (p. 59): solutions of (ODE)-(DDE) are non-decreasing on $[0,p^\star+\delta]$ .
Proposition 3 (p. 31): if $x_{pd}(v)\to 1$ as $v\uparrow p^\star+\delta$ , then $v^\star(\cdot\,|\,\mu,\delta)$ is a best reporting mapping for $m_{pd}$ .
Proposition 4 (p. 33): the system has a unique solution on $[0,p^\star+\delta]$ , which is positive, non-decreasing and given in closed form (eq. (25)).
Lemma 6 (p. 60): with $\Gamma(t)=\sum_{j=0}^{\lfloor t\rfloor+1}\frac{(-1)^je^{-j}}{j!}(t+1-j)^j$ ,

2(t+1)e^{-1}e^{-t}<\Gamma(t)\le2(t+2)e^{-(t+1)}\qquad(t\ge0).

Proposition 5 (p. 34): for $\mu>\varepsilon e$ some $\delta\in[\mu^2/(4\varepsilon)-\mu,\ \mu^2/(4\varepsilon)]$ makes $x_{pd}$ reach $1$ at $p^\star+\delta$ , and then $m_{pd}\in\mathcal M(\varepsilon)$ .
Proposition 6 (p. 35): the revenue identity

\Pi(m_{pd})=\int_0^{p^\star+\delta}x_{pd}(v)\big(vf(v)-\bar F(v+\mu)\dot w(v)\big)dv+R(p^\star+\delta)+\int_{p^\star+\delta}^{p^\star+\delta+\mu}\bar F(v)\,dv .

Significance

The result. Theorem 3 shows that the $\tilde O(\varepsilon^{\alpha/(2\alpha-1)})$ upper bound of Theorem 1 is tight up to the logarithm. Since $\alpha/(2\alpha-1)<1$ for $\alpha>1$ , the revenue gain from approximate incentive compatibility is supralinear in $\varepsilon$ : a seller who exploits $\varepsilon$ -optimizing buyers gains strictly more than the order- $\varepsilon$ gain available to deterministic mechanisms (Theorem 2). Randomization is therefore what makes the relaxation valuable, and the curvature $\alpha$ of the revenue curve at the optimal price determines the exponent, which ranges from $1$ (as $\alpha\downarrow1$ ) to $1/2$ (as $\alpha\to\infty$ ), the latter matching Nisan's universal bound.

Formalizing it. The result is proved in the paper's online appendix; none of it is formalized. A formal development would supply a machine-checked revenue lower bound for an explicit class of $\varepsilon$ -IC mechanisms, a formal treatment of a linear delay differential equation with a piecewise history (method of steps, closed-form solution), and the two-sided bound on $\Gamma$ , which the paper derives from the renewal function of uniform interarrival times.

Difficulty

The obvious approach, perturbing the optimal posted price or a hard/soft floor mechanism, gains only order $\varepsilon$ (Theorem 2). To gain more, the mechanism must make the buyer misreport downward in a coordinated way, and the allocation that sustains a prescribed misreporting strategy is the solution of a delay differential equation. Three steps are delicate: showing that this solution exists, is unique and is monotone (the delay term couples $x(v)$ to $x(v-\mu)$ ); choosing the delay $\delta$ so that the allocation reaches exactly $1$ at $p^\star+\delta$ , which requires the sharp two-sided bound on $\Gamma$ and an intermediate value argument; and verifying global $\varepsilon$ -IC, since a best-response argument must rule out every deviation, not only local ones. The final bound balances the gain $\bar F(p^\star+\delta+\mu)\,\mu$ against losses of order $\kappa_U(\delta+\mu)^\alpha$ , with $\mu$ of order $\varepsilon^{\alpha/(2\alpha-1)}$ .

Formalization scope

Values are reals, every function is a total function $\mathbb R\to\mathbb R$ whose values matter only on $S=[0,\bar v]$ , and the density is integrable on $S$ with total mass $1$ . Mechanisms are required to be measurable, which the expectation $\mathbb E_v[t(v)]$ presumes. $\Pi^\star$ is a supremum (sSup); the goal is stated with an explicit witness $m\in\mathcal M(\varepsilon)$ , which is equivalent because the revenue image is nonempty and bounded above by $\bar v$ . $\dot R$ is defined as $\bar F-vf$ , not as a derivative. The $\Omega$ constants are quantified after the distribution and before $\varepsilon$ .

The derivatives in (ODE)-(DDE) are one-sided at the endpoints of their closed intervals. At $p^\star-\delta$ the two right-hand sides differ, so a two-sided derivative would make the system unsolvable and every statement about its solutions vacuous; this encoding rules out that trivialization. The goal does not mention perturbed delayed mechanisms: any witness is acceptable.

Disclosed additions relative to the page: $\mu\le p^\star-\delta$ in the §5.1 statements (presumed by the paper's definition of $w$ ); Propositions 3–6 and Lemma 5 are stated for any price $p^\star$ with $0<\delta<p^\star$ and $p^\star+\delta+\mu<\bar v$ , since their proofs never use optimality of $p^\star$ ; in Proposition 6 the integrand $\psi\cdot f$ is written in product form because $\psi$ divides by $f$ .

A complete development needs: absolutely continuous distribution functions and integration by parts on intervals; existence and uniqueness for linear ODEs and for a delay equation by the method of steps; Irwin–Hall distributions or a direct analytic bound for Lemma 6; and the intermediate value theorem. The delay-equation and $\Gamma$ results are reusable outside mechanism design. Contributions to any milestone, and alternative proofs of Lemma 6, are welcome.

Selected references

S. R. Balseiro, O. Besbes, F. Castro, Mechanism Design under Approximate Incentive Compatibility, arXiv:2103.03403v2, 2022; Operations Research, 2024. https://arxiv.org/abs/2103.03403
M.-F. Balcan, A. Blum, J. D. Hartline, Y. Mansour, Mechanism Design via Machine Learning, FOCS 2005, 605–614. https://doi.org/10.1109/SFCS.2005.50
R. B. Myerson, Optimal Auction Design, Mathematics of Operations Research 6(1), 58–73, 1981. https://doi.org/10.1287/moor.6.1.58
P. Milgrom, I. Segal, Envelope Theorems for Arbitrary Choice Sets, Econometrica 70(2), 583–601, 2002. https://doi.org/10.1111/1468-0262.00296
R. D. Driver, Ordinary and Delay Differential Equations, Springer, 1977 (reprint 2012). https://doi.org/10.1007/978-1-4684-9467-9

10 thms2 active usersReviewed

All missions

Linear Programming and Community Detection 7: The LP Relaxation Fails w.h.p. in the Logarithmic-Degree SBMResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 8 (p. 18)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Combinatorial Auctions with Interdependent Valuations: SOS to the Rescue 4: The k-SS Mechanism Is Ex-Post IC-IR and a (2 log k + 4)-Approximation to Welfare for Strong-SOS ValuationsResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 6.5

Milestones

Significance

Difficulty

Formalization scope

Selected references

Linear Programming and Community Detection 4: A Distance-Based Condition Under Which the Metric LP Relaxation Fails to Recover the Planted BisectionResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 5

Milestones

Significance

Difficulty

Formalization scope

Selected references

Load Balancing Under Strict Compatibility Constraints 3: Inhomogeneous Random Graphs with Edge Probabilities Satisfying (3.5) Are Almost Surely Proportionally Sparse and SubcriticalResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3.6 (graph part)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Stochastic Zeroth-Order Riemannian Derivative Estimation and Optimization 2: ZO-RSGD Has Average Expected Squared Riemannian Gradient Norm at Most 4L(f(x₀) − f(x*))/(N+1) + 2μ²L²(d+6)³ + 16(d+4)σ²/mResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3.2

Milestones

Significance

Difficulty

Formalization scope

Selected references

Breaking the Sample Size Barrier in Model-Based Reinforcement Learning with a Generative Model 3: Plug-In Policy Evaluation Is ε-Accurate w.p. 1−δ Once N ≥ c₀log(|S|log(e/(1−γ))/δ)/((1−γ)³ε²)Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 3 (p. 9)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Designing Approximately Optimal Search on Matching Platforms 2: Every Set of Assortments Has a Unique Profile of Thresholds Equal to Expected UtilitiesResearch Paper

Motivation

Setting

Formalization targets

Goal: Proposition 3.1, item 1 (fixed-point form)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Combinatorial Auctions with Interdependent Valuations: SOS to the Rescue 3: The k-HL Mechanism Is Ex-Post IC-IR and a (k+3)-Approximation to Welfare with k Signal ValuesResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 6.1 (p. 20)

Milestones

Significance

Difficulty

Formalization scope