The OR Formalization Drive

Motivation

Online bipartite matching models decisions that must be made as requests arrive: an advertiser can be assigned to a compatible request once, and an assignment cannot be revised when later requests reveal a better alternative. Display advertising is the motivating example in Feldman, Mehta, Mirrokni, and Muthukrishnan's 2009 preprint: an ad server knows which advertisers accept each kind of impression and has estimates of how frequently those kinds will arrive. The question is how much this advance distributional information helps when decisions still have to be immediate.

This mission studies the paper's first offline-guided algorithm. It computes a maximum matching for the expected traffic and follows that matching during the actual random run. The paper shows that this natural policy reaches the familiar $1-1/e$ performance level and that its own analysis cannot be improved for this policy, even if performance is averaged over runs. The result sets the baseline for the paper's later two-suggested-matchings algorithm, which improves on that level under its stated assumptions. Feldman et al., §§1 and 4.1

Setting

An instance consists of a finite advertiser set $A$, a finite impression-type set $I$, and allowed edges $E\subseteq A\times I$. For each type $i$, the nonnegative integer $e_i$ is its expected number of arrivals. There are $n=\sum_{i\in I}e_i>0$ arrivals. Each arrival independently has type $i$ with probability $e_i/n$. A type with $e_i=0$ remains in the graph but has zero arrival probability. On an arrival of type $i$, an online algorithm may assign it to an adjacent advertiser that has not been assigned before, or may leave it unassigned. The hindsight optimum, $\mathrm{OPT}(\omega)$, is the largest matching in the realization graph with one vertex for every arrival position, including separate vertices for repeated types. Feldman et al., §2, pp. 3–4

The suggested matching algorithm first selects any maximum integral flow in the expected-instance network. Each advertiser has capacity one, and each type $i$ has capacity $e_i$. Equivalently, the selected edges form a maximum degree-capped bipartite matching $M\subseteq E$. Let $A^*$ be the advertisers covered by $M$. When type $i$ arrives, the algorithm chooses each advertiser joined to $i$ by a selected edge with probability $1/e_i$; any remaining probability chooses no advertiser. It assigns the chosen advertiser if available and otherwise makes no assignment. Its number of assignments is $\mathrm{ALG}(\omega)$. This rule includes the algorithm's random choice in addition to the random arrival types. Feldman et al., §4.1, p. 5

The canonical residual cut of $M$ places each advertiser and impression type on the source side if it is reachable from the source by residual edges. Write $A_T$ for advertisers on the sink side and $I_S$ for types on the source side. These sets describe the comparison between the expected-instance matching and the optimum of a realized run. The mission also uses occupancy: after $n$ independent uniform throws into $n$ bins, count how many bins in a fixed subset receive at least one ball. Feldman et al., §§2.1 and 4.1

Formalization targets

Theorem 4's general-instance guarantee is expressed in the additive form established by its analysis. For every $\varepsilon>0$, there are $\delta>0$ and $N$, uniform across all finite instances, all maximum integral flows, and all valid ways of realizing the algorithm's random choice, such that $n\ge N$ implies

$$\Pr\!\left[\mathrm{ALG}(\omega)\ge(1-e^{-1})\mathrm{OPT}(\omega)-\varepsilon n\right] \ge 1-e^{-\delta n}.$$

The complete bipartite family gives the tightness target. When $A=I=\{0,\ldots,n-1\}$ and every $e_i=1$, every maximum expected-instance matching is perfect. For every run, $\mathrm{OPT}=n$, and

$$\mathbb E[\mathrm{ALG}] =n\left(1-\left(1-\frac1n\right)^n\right), \qquad \lim_{n\to\infty}\frac{\mathbb E[\mathrm{ALG}]}{n}=1-e^{-1}.$$

The milestone list follows the paper's Fact 1 and the named passages “Bounding ALG,” “Bounding OPT,” and “Tightness of the Analysis” in §4.1. The cut identity $|A^*|=|A_T|+\sum_{i\in I_S}e_i$ is a separate deterministic milestone. Feldman et al., Theorem 4 and §4.1, pp. 5–6

Significance

The result establishes exactly what this one-matching policy achieves under integer-frequency independent arrivals. It gives a guarantee for the actual number of assignments relative to the best assignment made with hindsight, and a family on which the limiting expected ratio equals the guarantee. That tight family explains why the paper introduces a second suggested matching rather than seeking a stronger bound for the same policy. Feldman et al., §4

The mathematical theorem is proved in the paper; the mission asks for its machine-checked formalization. The development would also provide reusable finite models of repeated-type realizations, integral degree-capped bipartite matchings, uniform occupancy, and residual reachability cuts. No machine-checked proof of these mission items is being claimed by this draft.

Difficulty

The expected-instance matching is selected before the arrivals, but the hindsight optimum can exploit the actual multiplicities of every type. Counting only the ads selected online does not compare the algorithm with that hindsight optimum. Also, a type may have several selected advertisers when $e_i>1$, so replacing the algorithm's random choice by a deterministic designated ad would change its law. The cut and concentration statements have to apply uniformly to every maximum integral flow, including flows chosen by different tie-breaking rules. Feldman et al., §4.1, pp. 5–6

Formalization scope

Advertisers and types are finite Lean types. The edge relation is a finite set, and $e_i$ and $n$ are natural numbers with $n=\sum_i e_i>0$. An integral maximum flow is represented by a maximum cardinality edge set with advertiser degree at most one and type-$i$ degree at most $e_i$. The theorem quantifies over every such set. This is the unit-advertiser, integer-type-capacity flow used in §4.1, without a separate real-valued flow object. The canonical cut is defined through residual reachability. The hindsight optimum maximizes over matchings of the realized graph, with each arrival position distinct.

The run uses $n$ independent uniform draws from $\sum_i\{0,\ldots,e_i-1\}$. A valid labelling assigns each selected advertiser at type $i$ to a distinct copy. The drawn copy determines the type and, if labelled, the ad selected by the algorithm. This gives type probability $e_i/n$, conditional ad probability $1/e_i$ on selected edges, and the remaining “no ad” probability. Counts, probabilities, and expectations use finite sums, so there is no integrability convention. Since $n>0$, the run sample space is nonempty; no value of $\mathrm{ALG}/\mathrm{OPT}$ at $\mathrm{OPT}=0$ is needed. The complete-graph family has $n\ge1$.

The paper writes $1-e^{-\Omega(n)}$ in both bounding passages. The Lean statements spell this out as $\forall\varepsilon>0,\ \exists\delta>0,\ \exists N,\ \forall$ instances with $n\ge N$, with $\delta,N$ preceding the instance. Theorem 4's ratio language is represented by the additive estimate its proof yields; a vanishing ratio error requires a separate lower bound on $\mathrm{OPT}/n$. The exact finite-$n$ expectation and its limit make “tight, even in expectation” precise. The printed Fact 1 exponent is $\varepsilon n/2$, while its Appendix A proof yields $\varepsilon^2n/2$; the formalized concentration statement uses the proved exponent and the milestone retains the printed wording. Neither a ratio with a zero denominator nor a labelling that changes the algorithm's choice law is accepted as a shortcut.

Contributions toward the occupancy bound, the residual cut identity, the realized matching bound, and the complete-graph expectation are welcome. The finite occupancy and matching interfaces are intended for reuse beyond this specific algorithm.

Selected references

• Jon Feldman, Aranyak Mehta, Vahab Mirrokni, and S. Muthukrishnan, Online Stochastic Matching: Beating 1-1/e, arXiv:0905.4100v1, 2009; FOCS 2009. Preprint

Motivation

Online bipartite matching asks an algorithm to assign arriving requests to resources it cannot reassign later. In display advertising, the requests are page views (impressions) and the resources are advertisers who have bought a fixed number of impressions in advance; each impression must be served immediately or lost. In the adversarial model, Karp, Vazirani and Vazirani (STOC 1990) showed that the RANKING algorithm achieves a $1 - 1/e$ fraction of the optimum in expectation, and that no online algorithm does better. Advertising systems, however, have historical traffic data, which motivates the i.i.d. model: the impression types are drawn independently from a distribution that is known in advance.

Feldman, Mehta, Mirrokni and Muthukrishnan (arXiv:0905.4100, FOCS 2009) were the first to beat $1 - 1/e$ in this model, with an algorithm that achieves $\approx 0.67$ with high probability. Their Section 3 asks the complementary question: how close to $1$ can any online algorithm get when the distribution is known? Their Theorem 3 answers that the expected approximation factor of every online algorithm is bounded strictly away from $1$, already on a graph with six vertices. Later work in the same model (Manshadi, Oveis Gharan and Saberi, SODA 2011, arXiv:1007.1673) sharpened both the algorithmic and the hardness side.

Setting

An instance consists of a bipartite graph $G = (A, I, E)$ between a finite set $A$ of advertisers and a finite set $I$ of impression types, a distribution $D$ on $I$, and a number $n$ of arrivals. In this mission $D$ is the uniform distribution on $I$. Online, $n$ impressions arrive one at a time; their types $\omega(0), \dots, \omega(n-1)$ are independent draws from $D$. When impression $t$ arrives, the algorithm must immediately either assign it to an advertiser $a$ with $(a, \omega(t)) \in E$ that has not yet been used, or leave it unassigned. Each advertiser can be used at most once, and decisions are final.

A deterministic online algorithm decides what to do with arrival $t$ from the types $\omega(0), \dots, \omega(t)$ seen so far; it knows $G$, $D$ and $n$, but not the future. A randomized online algorithm is a probability distribution over deterministic ones. $\mathrm{ALG}(\omega)$ is the number of impressions the algorithm assigns on the arrival sequence $\omega$. $\mathrm{OPT}(\omega)$ is the size of a maximum matching of the realization graph, which has one node per arrival $t$, joined to every advertiser adjacent to $\omega(t)$: the most impressions that could have been assigned with hindsight. The expected approximation factor of an algorithm is

$$\mathbb E\!\left[\frac{\mathrm{ALG}(\omega)}{\mathrm{OPT}(\omega)}\right],$$

the expectation taken over the algorithm's randomness and the arrivals.

The 6-cycle instance has $A = \{a, b, c\}$, $I = \{x, y, z\}$ and $E = \{(x,a),(y,a),(y,b),(z,b),(z,c),(x,c)\}$, with the uniform distribution and $n = 3$. The family $\Gamma_k$ consists of $k$ disjoint copies of the 6-cycle, with the uniform distribution on its $3k$ impression types and $n = 3k$ arrivals.

Formalization targets

Goal: Theorem 3

On the 6-cycle, every randomized online algorithm satisfies

$$\mathbb E\!\left[\frac{\mathrm{ALG}}{\mathrm{OPT}}\right] \le \frac{26}{27},$$

and there are a constant $c < 1$ and a threshold $K_0$ such that for every $k \ge K_0$ and every randomized online algorithm on $\Gamma_k$,

$$\mathbb E\!\left[\frac{\mathrm{ALG}}{\mathrm{OPT}}\right] \le c .$$

The second part is the paper's "there exists a family of instances with $n \to \infty$ for which no algorithm can achieve an expected approximation of $1 - o(1)$", stated on the paper's own family. It leaves $c$ unspecified: Appendix B estimates $c \approx 0.9898$ through approximate counts, and a sharper constant would not invalidate the goal.

Milestones

1. The $(x, y, y)$ scenario (§3, p. 4). For every deterministic online algorithm on the 6-cycle and every type $u$ of the first arrival there is a type $v$ with $\mathrm{ALG}(u, v, v) \le 2$ and $\mathrm{OPT}(u, v, v) = 3$.
2. Theorem 3, first sentence (p. 4). The bound $26/27$ on the 6-cycle, for every randomized online algorithm.

Significance

Theorem 3 sets the ceiling against which algorithms in the i.i.d. model are measured. It rules out an online algorithm with expected factor arbitrarily close to $1$, even though the distribution is known and the instance is tiny, so a constant-factor gap between online and offline matching is intrinsic to the model and not an artefact of adversarial arrivals. The paper's positive results ($1 - 1/e$ for the Suggested Matching algorithm, $\approx 0.67$ for Two Suggested Matchings) sit between $1 - 1/e$ and this ceiling.

The single-instance bound has a short counting proof. The family statement is argued in the paper only in outline: Appendix B approximates the fractions of copies receiving $1$, $2$, $3$ or more impressions, assumes the most favourable outcome on each, and reports the resulting ratio as approximately $0.9898$. A machine-checked proof of the family statement would turn that sketch into a theorem with an explicit constant. To our knowledge neither part has been formalized before.

Difficulty

The single-cycle bound reduces to a finite check, but the paper's "without loss of generality (from the symmetry of the 6-cycle)" hides the cases the algorithm can choose: assigning the first impression to either neighbour, or not assigning it at all. Each case needs its own bad continuation. The passage from deterministic to randomized algorithms is an averaging step.

The family bound is harder. On $\Gamma_k$ the algorithm sees all arrivals in all copies and may coordinate its decisions across copies, so the per-copy loss of the single cycle does not transfer by independence. Moreover the target is the expectation of a ratio, $\mathbb E[\mathrm{ALG}/\mathrm{OPT}]$, not a ratio of expectations: a bound on the expected loss must be combined with concentration of the number of copies that receive exactly three impressions, and with a lower bound on $\mathrm{OPT}$ that holds with high probability. The approximations "$\simeq 3/e^3$, $9/(2e^3)$, $27/(6e^3)$" of Appendix B have unquantified errors and cannot be used as they stand.

Formalization scope

The model is formalized for general finite $A$ and $I$ with uniform arrivals. Arrival sequences are functions Fin n → I. A deterministic online algorithm is a function that receives the time $t$, the prefix of the first $t$ types (Fin t → I) and the current type, and returns an advertiser or none; it cannot read later arrivals. A proposal of a non-adjacent or already used advertiser leaves the impression unassigned, so the encoding covers all online algorithms, including ones that skip an impression while a neighbour is free. A randomized online algorithm is a probability distribution (PMF) on the finite type of deterministic algorithms; by Kuhn's theorem this is equivalent to fresh random choices at each step. $\mathrm{OPT}$ is the maximum size of an injective, edge-respecting partial assignment of arrivals to advertisers. The expected approximation factor is a finite average over all $|I|^n$ arrival sequences, weighted by the algorithm distribution.

The explicit instantiations of the paper's asymptotic wording are as follows:

• "no algorithm can achieve an expected approximation of $1 - o(1)$" becomes $\exists\, c < 1,\ \exists K_0,\ \forall k \ge K_0,\ \forall P:\ \mathbb E[\mathrm{ALG}/\mathrm{OPT}] \le c$ on $\Gamma_k$, with $n = 3k$ tied to $k$, and with $c$ and $K_0$ chosen before $k$ and before the algorithm.
• The paper's constant $0.9898$ is not part of the statement.

Lean's division sets $x/0 = 0$. A formalization of the form "there is an instance on which every algorithm has expected factor at most $26/27$" would be satisfied trivially by a graph without edges, where $\mathrm{OPT} = 0$; the statements here are on the paper's explicit instances, where every impression type has an adjacent advertiser and $\mathrm{OPT} \ge 1$ on every arrival sequence.

A complete development needs finite case analysis on runs of online algorithms, averaging over mixed strategies, and, for the family, concentration inequalities for occupancy counts (Azuma or McDiarmid, both available on the platform) together with bounds on maximum matchings of disjoint unions. The online-algorithm model and the averaging lemmas are reusable for other lower bounds in the i.i.d. model. Proofs of either milestone, and independent proofs of the family statement with any explicit $c < 1$, are welcome.

Selected references

• J. Feldman, A. Mehta, V. Mirrokni, S. Muthukrishnan, Online Stochastic Matching: Beating 1-1/e, FOCS 2009; arXiv:0905.4100v1. https://arxiv.org/abs/0905.4100
• R. M. Karp, U. V. Vazirani, V. V. Vazirani, An optimal algorithm for on-line bipartite matching, STOC 1990. https://doi.org/10.1145/100216.100262
• V. H. Manshadi, S. Oveis Gharan, A. Saberi, Online Stochastic Matching: Online Actions Based on Offline Statistics, SODA 2011; arXiv:1007.1673. https://arxiv.org/abs/1007.1673

Why coverage of an optimal value matters

Many stochastic optimization problems choose a decision by minimizing an expected loss. The optimum depends on an unknown distribution, so a data-based optimum alone gives no measure of uncertainty about the best achievable expected loss. This mission concerns a confidence set for that optimal value, rather than a confidence set for the decision itself. The result of Duchi, Glynn, and Namkoong shows that a broad class of divergence neighborhoods of the empirical distribution yields a calibrated limit for this set. The same construction covers nonsmooth losses and constrained decisions when the regularity assumptions below hold.

The paper develops generalized empirical likelihood for smooth functionals of a distribution and then applies it to optimization. Its Theorem 3 states the exact asymptotic coverage result for the optimal value; Appendix C identifies the functional derivative, while Appendix B gives the uniform linearization and expansion on which calibration rests. The statistical result is proved in the paper. The mission asks for a machine-checked development of its statements and proof under an explicit nondegeneracy condition required by the paper's general coverage theorem.

Decisions, losses, and divergence neighborhoods

Let $\mathcal X\subseteq\mathbb R^d$ be a nonempty compact decision set. An observation $\xi$ has population law $P_0$, and $\ell(x;\xi)\in\mathbb R$ is the loss at decision $x$. The quantity of interest is the optimal-value functional

$$T_{\rm opt}(P)=\inf_{x\in\mathcal X}\mathbb E_P[\ell(x;\xi)].$$

The observations $\xi_1,\ldots,\xi_n$ are independent and identically distributed with law $P_0$. Write $\widehat P_n$ for their empirical distribution. A candidate distribution supported on the indexed observations is represented by nonnegative weights $p_i$ with $\sum_i p_i=1$. Indexed weights also cover samples with repeated observations. For a convex divergence generator $f$ normalized by $f(1)=f'(1)=0$ and $f''(1)=2$, its divergence from the empirical law is $D_f(p\|\widehat P_n)=n^{-1}\sum_i f(np_i)$. Assumption A further requires $f$ to be three times continuously differentiable near $1$; it permits $f(0)=+\infty$.

At radius $\rho/n$, the divergence ball consists of the weights with $\sum_i f(np_i)\le\rho$. The confidence set is its image under $T_{\rm opt}$:

$$C_{n,\rho}=\{T_{\rm opt}(p):D_f(p\|\widehat P_n)\le\rho/n\}.$$

Assumption B makes $\mathcal X$ compact and requires $\ell(\cdot;\xi)$ to be Lipschitz on it with a measurable random coefficient $M(\xi)$. The theorem adds finite second moments for $M$ and for the loss at one feasible decision. These conditions control losses at every feasible decision. They also make the population and weighted empirical infima finite on the cases used in the limit.

Formalization targets

The goal is the exact asymptotic coverage of the population optimal value, with $x^\star$ the unique optimizer and $\operatorname{Var}_{P_0}(\ell(x^\star;\xi))>0$:

$$P^*\!\left(T_{\rm opt}(P_0)\in C_{n,\rho}\right)\longrightarrow P(\chi_1^2\le\rho),\qquad \rho\ge0.$$

Here $P^*$ denotes outer probability, and $\chi_1^2$ is the square of a standard normal variable. The milestone statements follow the paper's path to this theorem. Lemma 17 gives the directional derivative of an optimal-value functional. Lemma 13 bounds feasible empirical weights relative to uniform weights. Lemma 16 makes the nonlinear remainder uniformly negligible on the divergence ball. The display after (37) then gives a first-order expansion of the upper endpoint of $C_{n,\rho}$; the next display gives its one-sided Gaussian coverage limit. The goal concerns membership in the image set $C_{n,\rho}$, including both sides of that interval.

What the result provides

The limit specifies a radius through a one degree of freedom chi square quantile. It applies to the value of a constrained stochastic optimization problem without requiring the optimizer or the loss to be differentiable. The positive variance condition ensures that the influence function supplies a genuine Gaussian scale. Without such a condition, a deterministic optimal loss can make coverage identically one, so the stated chi square limit would fail. The general theorem in the paper explicitly requires positive influence variance; this mission makes the condition visible in the specialized optimal-value statement.

A complete formalization would connect finite-sample divergence geometry to an asymptotic confidence claim about an optimization functional. The empirical mean and variance definitions, divergence ball, and normalized generator already exist as reusable declarations. This mission adds the optimal-value functional, its influence function, the nonlinear remainder, and the statistical limits. Those definitions can also support later confidence statements for other stochastic optimization models. The result is proved in the source paper; the Lean statements here are open targets awaiting proofs.

The mathematical obstacle

Pointwise control of each loss $\ell(x;\xi)$ is insufficient for the optimal value: the decision minimizing an empirical weighted objective can move with the weights. A pointwise mean expansion therefore does not by itself control the infimum over $x$. The required limit combines uniform control over the loss class with sensitivity of the infimum functional near its population minimizer. The uniform remainder in Lemma 16 is stronger than a statement for the ordinary empirical distribution because it covers every distribution in the shrinking divergence ball. The final event is membership in the image of that ball; bounds on its upper endpoint alone do not establish two-sided coverage.

Formalization scope

Lean represents decisions by EuclideanSpace ℝ (Fin d) and assumes a nonempty compact feasible set. Assumption B uses its Euclidean norm. The paper allows any norm in finite dimension; norm equivalence permits this choice after rescaling the Lipschitz coefficient. The population law is the pushforward of the first measurable observation from a probability space. Samples are indexed from zero, so the first $n$ observations are indices $0,\ldots,n-1$. Independence and identical distribution are explicit hypotheses. Loss measurability is explicit so the population integrals have their intended values. Square integrability and compact Lipschitz control keep the real infima meaningful.

The generator takes values in EReal so a divergence infinite at zero is representable. The ball uses the published probability uncertainty set with radius $\rho/n$ and includes nonnegativity and unit mass. Its weights represent distributions absolutely continuous with respect to the empirical law. With tied observations, equal splitting across copies preserves the induced distribution and does not increase a convex divergence. The upper endpoint is $\sup_p\inf_x$; the different minimax expression $\inf_x\sup_p$ is not substituted. The chi square target uses the standard Gaussian measure of $\{z:z^2\le\rho\}$.

Mathlib measures are outer measures on arbitrary sets, so the probability of a possibly nonmeasurable membership or supremum event is the paper's outer probability. The Lemma 17 milestone expresses a signed measure through its action $H(x)$ on the losses, as Appendix C.2 does, and uses positive directional steps. Real suprema and infima are used only where the hypotheses provide nonempty bounded values. The variance hypothesis rules out the trivial deterministic-loss counterexample. Useful contributions include the compactness and continuity facts needed for those extrema, the action-level derivative, empirical process limits, and the final two-sided event argument.

Selected references

• John C. Duchi, Peter W. Glynn, and Hongseok Namkoong, Statistics of Robust Optimization: A Generalized Empirical Likelihood Approach, arXiv:1610.03425v3, 2018; published in Mathematics of Operations Research 46(3), 2021. arXiv preprint

Motivation

A retailer that decides which products to display, an online platform that decides which items to show in a recommendation slot, and an airline that decides which fare classes to open all face the same problem: the set of options offered changes what customers buy, and the substitution pattern is not known in advance. The multinomial logit (MNL) model is the standard model of this substitution in revenue management (Talluri and van Ryzin 2004), and optimizing the offered set under a known MNL model is a classical, efficiently solvable problem (e.g. Rusmevichientong, Shen and Shmoys 2010, for a capacity constraint).

The MNL-Bandit asks what happens when the MNL parameters are unknown and must be learned from the purchases themselves, while revenue is being earned. Earlier approaches (Rusmevichientong, Shen and Shmoys 2010; Sauré and Zeevi 2013) separate exploration from exploitation and need the gap between the best and the second-best assortment to be known. Agrawal, Avadhanula, Goyal and Zeevi (Oper. Res. 2019, arXiv:1706.03880) give a single upper-confidence-bound policy whose regret is of order $\sqrt{NT}$ up to logarithmic factors, with no such knowledge. This mission formalizes that result, Theorem 1 of the paper.

Setting

There are $N$ products with known revenues $r_i\in[0,1]$. At each time $t=1,\dots,T$ the seller offers an assortment $S_t$ from a family $\mathcal S$ of feasible subsets of $\{1,\dots,N\}$, and one customer either buys a product $c_t\in S_t$ or buys nothing ($c_t=0$). Given $S_t=S$, the choice follows the MNL model with attraction parameters $v_1,\dots,v_N\ge0$ and $v_0=1$:

$$p_i(S)=\frac{v_i}{1+\sum_{j\in S}v_j}\quad(i\in S\cup\{0\}),\qquad p_i(S)=0\ \text{otherwise},$$

independently of the past. The expected revenue of $S$ is $R(S,v)=\sum_{i\in S}r_iv_i\big/\big(1+\sum_{j\in S}v_j\big)$. The family $\mathcal S$ is described by totally unimodular constraints, $\mathcal S=\{S : A\,x(S)\le b\}$ with $x(S)$ the incidence vector of $S$, $A$ totally unimodular and $b$ integral (cardinality constraints are the main example). A policy chooses $S_t$ from the past choices, and its regret is

$$\mathrm{Reg}_\pi(T,v)=T\,R(S^*,v)-\mathbb E_\pi\Big[\sum_{t=1}^TR(S_t,v)\Big],\qquad R(S^*,v)=\max_{S\in\mathcal S}R(S,v).$$

The seller knows $r$ and $\mathcal S$ but not $v$.

Algorithm 1 works in epochs: epoch $\ell$ offers one assortment $S_\ell$ repeatedly until a customer buys nothing. Let $\hat v_{i,\ell}$ be the number of purchases of $i$ in epoch $\ell$, $T_i(\ell)$ the number of the first $\ell$ epochs that offered $i$, and $\bar v_{i,\ell}$ the average of $\hat v_{i,\tau}$ over those epochs. The algorithm forms the upper confidence bounds

$$v^{\mathrm{UCB}}_{i,\ell}=\bar v_{i,\ell}+\sqrt{\bar v_{i,\ell}\,\frac{48\log(\sqrt N\ell+1)}{T_i(\ell)}}+\frac{48\log(\sqrt N\ell+1)}{T_i(\ell)},$$

starting from $v^{\mathrm{UCB}}_{i,0}=1$, and offers next the assortment in $\mathcal S$ that maximizes $R(S,v^{\mathrm{UCB}}_{\cdot,\ell})$.

Formalization targets

Goal: Theorem 1 (p. 11)

Under Assumption 4.1 (every $v_i\le v_0=1$, and $\mathcal S$ is closed under taking subsets) there are absolute constants $C_1,C_2$ such that for every instance and every horizon $T$,

$$\mathrm{Reg}_\pi(T,v)\le C_1\sqrt{NT\log NT}+C_2N\log^2NT .$$

The constants are not fixed: the goal asserts the order of the regret, which is what the paper claims.

Milestones

The milestones follow the proof in Appendix A of the paper:

1. The law of an epoch's purchase count: Lemma A.1, its moment generating function given the offered assortment.
2. Concentration: Theorem 5, Chernoff bounds for geometric variables; Corollary D.1; and Lemma A.2 for the averages $\bar v_{i,\ell}$ along Algorithm 1.
3. Lemma 4.1: $v^{\mathrm{UCB}}_{i,\ell}\ge v_i$ with probability at least $1-6/(N\ell)$, and its rate of convergence.
4. Optimism of the revenue estimate: Lemma A.3 (monotonicity of the optimal revenue in $v$) and Lemma 4.2.
5. The per-epoch error: Lemma A.4 (a Lipschitz bound) and Lemma 4.3.
6. The epoch decomposition of the regret, (A.14).

Significance

Theorem 1 shows that learning the choice model costs only $\tilde O(\sqrt{NT})$ revenue, with no dependence on how separated the instance is. The paper also proves a lower bound of order $\sqrt{NT/K}$ under a $K$-cardinality constraint (its Theorem 2), so for small $K$ the bound is optimal up to logarithmic factors. The epoch device used here reduces the analysis of a choice model with substitution to unbiased i.i.d. estimates of each $v_i$.

The result is proved in the paper (Appendix A, with the concentration bounds in Appendix D). It has not been machine-checked. A formal proof would also settle several printed slips that the formalization had to repair (listed under Formalization scope). The concentration bounds for geometric variables, Theorem 5 and Corollary D.1, are useful outside this mission.

Difficulty

The estimates $\hat v_{i,\ell}$ are counted in epochs whose assortments are chosen adaptively from earlier estimates, so they are not independent a priori. The paper's argument that they are i.i.d. geometric with mean $v_i$ has to be made rigorous for an adaptive policy. The variables are unbounded, so the standard Chernoff–Hoeffding bounds for bounded variables do not apply, and the number of samples $T_i(\ell)$ is random, which requires a union bound over all its possible values. Finally, the regret is a sum over customers while the analysis is per epoch, and the two are linked through the expected epoch length $1+\sum_{j\in S_\ell}v_j$ under a random number of epochs and a horizon that cuts the last one.

Formalization scope

• Model. Products are Fin N; a choice is none (no purchase) or some i. The parameter $v_0$ is normalized to $1$, as the paper allows. Algorithm 1 is deterministic, so a history of horizon $T$ is a sequence of $T$ choices with the product law $\prod_tp_{c_t}(S_t)$, and every expectation is a finite sum. The revenue $R(S,v)$ is the published definition ChoiceCDLP.MNL.mnlObjective v r 1 S.
• Feasible family. $\mathcal S$ is a finite family with the TU representation (2.3), closed under subsets, and nonempty (the paper presupposes nonemptiness when it writes $S^*=\arg\max$).
• Algorithm. Algorithm 1 is a policy defined by recursion on the history. It receives $r$ and an argmax selector for $\mathcal S$, never $v$. Every statement quantifies over all selectors, that is, over every tie-breaking rule. While a product has never been offered, its $v^{\mathrm{UCB}}$ stays at the initial value $1$.
• Epoch events. The lemmas about epoch $\ell$ are stated for every finite horizon $T$, on the event that epoch $\ell$ is completed by customer $T$; uniformity in $T$ is the paper's infinite-horizon statement.
• Repairs of the page, all disclosed in the items:
  1. Lemma A.2's misprinted $\log(\ell+1)$ is replaced by $\log(\sqrt N\ell+1)$.
  2. Lemmas 4.2 and 4.3 are indexed by the estimate built at the end of epoch $\ell$.
  3. Lemma 4.3's free index $i$ becomes the sum over $i\in S_{\ell+1}$.
  4. Lemmas 4.1 and 4.3 use the explicit constants $C_1=\sqrt{72}+\sqrt{24}$ and $C_2=144$ of the proof.
  5. Lemma A.3 and Lemma 4.2 require positive parameters on the optimal set; the printed versions are false otherwise.
  6. (A.14) is an inequality, since the horizon cuts the last epoch.
• Not stated. Corollary A.1 (the epoch estimates are i.i.d. geometric across the epochs of the adaptive policy) is not posed as an item: a single-epoch law would be a weaker statement than the page's.
• No trivialization. The policy cannot see $v$, the constants of the goal precede every other quantifier, and the regret is the paper's (2.6), so the goal cannot be met by a policy that offers $S^*$ or by constants that depend on the instance.
• Welcome contributions. Infrastructure for adaptive sampling (the i.i.d. property of the epoch estimates), Chernoff bounds for geometric and sub-exponential variables, and a Wald-type identity for epochs.

The paper's own proofs are in its Appendices A and D.

Selected references

• S. Agrawal, V. Avadhanula, V. Goyal, A. Zeevi, MNL-Bandit: A Dynamic Learning Approach to Assortment Selection, Operations Research 67(5):1453–1485, 2019. arXiv:1706.03880v2, doi:10.1287/opre.2018.1832
• P. Rusmevichientong, Z.-J. M. Shen, D. B. Shmoys, Dynamic assortment optimization with a multinomial logit choice model and capacity constraint, Operations Research 58(6):1666–1680, 2010. doi:10.1287/opre.1100.0866
• D. Sauré, A. Zeevi, Optimal dynamic assortment planning with demand learning, Manufacturing & Service Operations Management 15(3):387–404, 2013. doi:10.1287/msom.2013.0429
• K. Talluri, G. van Ryzin, Revenue management under a general discrete choice model of consumer behavior, Management Science 50(1):15–33, 2004. doi:10.1287/mnsc.1030.0147
• M. Mitzenmacher, E. Upfal, Probability and Computing, Cambridge University Press, 2005.

Motivation

A retailer or an airline chooses which products to offer, and customers choose among what is offered, or buy nothing. Choosing the offer set that maximizes expected revenue is the assortment problem, central to revenue management (Talluri and van Ryzin, 2004). It is NP-hard even for simple mixtures of logit models, so practice relies on heuristics. The most common one is the revenue-ordered assortments strategy: offer the products whose price is above a threshold, and pick the best threshold.

Berbeglia and Joret (arXiv:1606.01371) analyse this heuristic under every regular choice model, the broad class in which enlarging the offer set never raises the probability of choosing any given alternative, including not buying. They prove three approximation guarantees, then show that none of the three can be improved. This mission formalizes that last result, Theorem 3.4.

Timeline:

• Talluri and van Ryzin (2004) showed that revenue-ordered assortments are optimal under the multinomial logit model.
• Rusmevichientong, Shmoys, Tong and Topaloglu (2014) showed the problem NP-hard under a mixture of two logit models, and proved that revenue-ordered assortments earn at least $\mathrm{OPT}/(e(1+\ln(r_k/r_1)))$ under mixed logit.
• Aouad, Farias, Levi and Segev (2018) proved an $\Omega(1/\ln(r_k/r_1))$ guarantee under random utility models, and that the assortment problem there is NP-hard to approximate within $\Omega(1/n^{1-\epsilon})$ and $\Omega(1/\log^{1-\epsilon}(r_k/r_1))$.
• Berbeglia and Joret (2016–2020, Algorithmica) proved the guarantees $1/k$, $1/\sum_{i}(r_i-r_{i-1})/r_i\ge1/(1+\ln(r_k/r_1))$ and a purchase-probability bound under any regular model, and an instance on which all three, in their sum forms, are attained in the limit.

Setting

The products form a finite set $\mathcal C$. A system of choice probabilities gives, for every offer set $S\subseteq\mathcal C$ and product $x$, the probability $\mathcal P(x,S)$ that a customer buys $x$. The no-purchase probability is $\mathcal P(0,S)=1-\sum_{x\in S}\mathcal P(x,S)$. The model is regular if

1. $\mathcal P(x,S)\ge0$ for $x\in\mathcal C\cup\{0\}$;
2. $\mathcal P(x,S)=0$ for $x\notin S$;
3. $\sum_{x\in S}\mathcal P(x,S)\le1$;
4. $\mathcal P(x,S)\ge\mathcal P(x,S')$ for $S\subseteq S'$ and every $x\in S\cup\{0\}$.

Each product has a revenue $r(x)>0$. Offering $S$ earns $\mathrm{rev}(S)=\sum_{x\in S}\mathcal P(x,S)\,r(x)$, and $\mathrm{OPT}=\max_{S\subseteq\mathcal C}\mathrm{rev}(S)$.

Let $r_1<\dots<r_k$ be the distinct revenues, with $r_0:=0$, and $S_i=\{x: r(x)\ge r_i\}$. The heuristic earns

$$\mathrm{RO}=\max_{i\in[k]}\mathrm{rev}(S_i).$$

For an optimal $S^*$ let $N_i=\sum_{x\in S^*,\,r(x)\ge r_i}\mathcal P(x,S^*)$, $N_{k+1}=0$, and $\ell$ the largest index with $N_\ell>0$. Section 3 of the paper proves

• (A) $\mathrm{OPT}\le k\cdot\mathrm{RO}$ (Theorem 3.1);
• (B) $\mathrm{OPT}\le D_r\cdot\mathrm{RO}$, with $D_r=\sum_{i=1}^{k}\frac{r_i-r_{i-1}}{r_i}\le 1+\ln(r_k/r_1)$ (Theorem 3.2);
• (C) $\mathrm{OPT}\le D_N(S^*)\cdot\mathrm{RO}$, with $D_N(S^*)=\sum_{i=1}^{\ell}\frac{N_i-N_{i+1}}{N_i}\le 1+\ln(N_1/N_\ell)$ (Theorem 3.3).

Formalization targets

Goal: Theorem 3.4

For every $k\ge1$ and every $\delta>0$ there are a finite nonempty product set, a regular $\mathcal P$, revenues $r>0$ with exactly $k$ distinct values, and an optimal $S^*$ with $N_1>0$, such that

$$k\cdot\mathrm{RO}<(1+\delta)\,\mathrm{OPT},\qquad D_r\cdot\mathrm{RO}<(1+\delta)\,\mathrm{OPT},\qquad D_N(S^*)\cdot\mathrm{RO}<(1+\delta)\,\mathrm{OPT}.$$

So none of the bounds (A), (B), (C) stays true when multiplied by $1+\delta$, for any number $k$ of distinct revenues.

The tight instance (milestones)

The paper's witness has products $(i,j)$ with $i\in[k]$ and $j\in[i]$. Product $(i,j)$ has revenue $\varepsilon^{-j}$, and $\mathcal P((i,j),S)=\varepsilon^i$ when $(i,j)\in S$ and $(i,1),\dots,(i,j-1)\notin S$, and $0$ otherwise, for $0<\varepsilon\le\tfrac12$. The milestones follow the proof on pp. 10–11:

• the axiom (iii) bound;
• (7);
• (8);
• (9);
• regularity;
• the distinct revenues $r_i=\varepsilon^{-i}$;
• $\mathrm{RO}=\mathrm{rev}(\mathcal C)<1/(1-\varepsilon)$;
• $\mathrm{OPT}=k$, attained by $\{(i,i)\}$;
• the limits $\mathrm{OPT}/\mathrm{RO}\to k$ and $D_r\to k$;
• $N_i=\varepsilon^i+\dots+\varepsilon^k$ and $D_N\to k$ as $\varepsilon\to0^+$.

Significance

With Theorems 3.1–3.3, Theorem 3.4 closes the analysis: in terms of the parameters $k$, $D_r$ and $D_N$, revenue-ordered assortments are understood exactly under regular choice. It complements the hardness results of Aouad et al., which already show that no efficient strategy can do much better than (A) and (B) in general; Theorem 3.4 shows that the analysis of this particular heuristic is exact. The instance is also a concrete regular choice model in which the optimal offer set is far from every nested one.

On the formal side, the mission produces a reusable formal definition of regular discrete choice models, revenue-ordered assortments and the three bound quantities. These are shared, under other sub-namespaces, with the companion missions on Theorems 3.2 and 3.3. The result is proved in the paper. As far as is known it has not been machine-checked anywhere; the remaining work is formalizing the paper's proof, including the steps it leaves to the reader.

Difficulty

The proof is a construction, and the paper verifies most of it in a sentence each. The work lies in those sentences:

• the regularity of the instance at the no-purchase option, (9), which needs the row decomposition (8);
• the claim that $\{(i,i)\}$ is optimal among all $2^{k(k+1)/2}$ offer sets, asserted without proof;
• the claim that the full set is the best threshold set;
• the evaluation of $D_N(S^*)$, which needs $\ell=k$.

The naive witness, one instance per bound, does not help: the goal asks for one instance with exactly $k$ revenues on which all three bounds are nearly attained, for every $k$.

Formalization scope

• Products are an arbitrary finite type C. The no-purchase option is not a product: $\mathcal P(0,S)$ is the derived quantity noPurchase P S. Offer sets are Finset C.
• IsRegular carries axioms (i)–(iv), with (i) and (iv) stated both for products and for the no-purchase option. Regularity at $x=0$ is essential: without it the guarantees fail.
• $\mathrm{OPT}$ is Finset.sup' over all subsets, including $\emptyset$. $\mathrm{RO}$ is Finset.sup' over the $k$ threshold sets only, and needs Nonempty C.
• The distinct revenues are the sorted image of r, indexed by Fin k from $0$: the Lean index $i$ is the paper's $i+1$, and $r_0=0$ is a separate case. $\ell$ lives in WithBot (Fin k).
• Bounds are multiplicative ($\mathrm{OPT}\le D\cdot\mathrm{RO}$); there is no ratio $\mathrm{RO}/\mathrm{OPT}$ in the goal. Limits are along 𝓝[>] 0.
• The tight instance keeps the paper's 1-based pairs $(i,j)$ as a subtype of Fin (k+1) × Fin (k+1). Its regularity is a theorem to prove, never a field assumed.

Ruled out:

• a fixed $k$, since "for every $k$" is the content;
• tightness of the logarithmic forms $1/(1+\ln(r_k/r_1))$ and $1/(1+\ln\nu)$, which this instance does not show (there $1+\ln(r_k/r_1)\to\infty$ while $\mathrm{OPT}/\mathrm{RO}\to k$), so only the sum forms are claimed tight;
• an instance whose regularity is assumed;
• a heuristic maximizing over all subsets.

Contributions welcome: proofs of the milestones, especially (8), (9) and the optimality of $\{(i,i)\}$, and general lemmas on sorted distinct values of a finite function.

Selected references

• G. Berbeglia and G. Joret, Assortment Optimisation Under a General Discrete Choice Model: A Tight Analysis of Revenue-Ordered Assortments, arXiv:1606.01371v3, 2019; published in Algorithmica, 2020. https://arxiv.org/abs/1606.01371
• K. Talluri and G. van Ryzin, Revenue Management Under a General Discrete Choice Model of Consumer Behavior, Management Science 50(1), 2004. https://doi.org/10.1287/mnsc.1030.0147
• P. Rusmevichientong, D. Shmoys, C. Tong and H. Topaloglu, Assortment Optimization under the Multinomial Logit Model with Random Choice Parameters, Production and Operations Management 23(11), 2014. https://doi.org/10.1111/poms.12191
• A. Aouad, V. Farias, R. Levi and D. Segev, The Approximability of Assortment Optimization Under Ranking Preferences, Operations Research 66(6), 2018. https://doi.org/10.1287/opre.2018.1724