Machine Learning

Motivation

AdaBoost (Freund and Schapire, 1996) combines many weak classifiers, such as small decision trees, into a single strong classifier by repeatedly reweighting the training data. In the late 1990s it was among the most accurate off-the-shelf classifiers, but why it worked was unclear. Friedman, Hastie and Tibshirani (Ann. Statist. 28 (2000) 337–407) gave a statistical explanation: AdaBoost fits an additive model by stagewise minimization of the exponential criterion $E(e^{-yF(x)})$, and the population minimizer of that criterion is half the log-odds of the class probability. Boosting is therefore a form of additive logistic regression. This reading underlies gradient boosting, LogitBoost, and the later theory of classification-calibrated surrogate losses.

The exponential criterion was introduced by Schapire and Singer (1998) as an upper bound on misclassification error, and Breiman (1997) used it in his analysis of AdaBoost. Lemma 1 of the 2000 paper is the statement that identifies its population minimizer.

Setting

A feature $x$ ranges over a measurable space $X$ and a label $y$ takes the values $-1$ and $1$. The pair $(x, y)$ has a joint law $\nu$, a probability measure on $X \times \{-1, 1\}$, with marginal $\nu_X$ on $X$. Disintegrating $\nu$ gives the conditional class probabilities $P(y = 1 \mid x)$ and $P(y = -1 \mid x)$.

For a function $F : X \to \mathbb R$ the exponential criterion (11) is the joint expectation

$$J(F) = E\big(e^{-yF(x)}\big) = \int e^{-yF(x)}\, d\nu(x, y),$$

a number in $[0, \infty]$. Its conditional version at $x$ is $E(e^{-yF(x)} \mid x)$. Given a current estimate $F$, the weighted conditional expectation with weight $w(x, y) = e^{-yF(x)}$ is

$$E_w[g(x, y) \mid x] = \frac{E[w(x, y)\, g(x, y) \mid x]}{E[w(x, y) \mid x]},$$

and $P_w(y = \pm 1 \mid x) = E_w[1_{[y = \pm 1]} \mid x]$. The half log-odds is

$$F^\star(x) = \tfrac12 \log \frac{P(y = 1 \mid x)}{P(y = -1 \mid x)}.$$

Formalization targets

Goal: Lemma 1

Assume $0 < P(y = 1 \mid x) < 1$ for $\nu_X$-almost every $x$. Then $F^\star$ is measurable, and for every measurable $F : X \to \mathbb R$,

$$E\big(e^{-yF^\star(x)}\big) \le E\big(e^{-yF(x)}\big),$$

and, for $\nu_X$-almost every $x$, (13) and (14) hold:

$$P(y = 1 \mid x) = \frac{e^{F^\star(x)}}{e^{-F^\star(x)} + e^{F^\star(x)}}, \qquad P(y = -1 \mid x) = \frac{e^{-F^\star(x)}}{e^{-F^\star(x)} + e^{F^\star(x)}}.$$

Milestones

1. The conditional criterion (proof of Lemma 1): $E(e^{-yF(x)} \mid x) = P(y = 1 \mid x) e^{-F(x)} + P(y = -1 \mid x) e^{F(x)}$, and $J(F)$ is the $\nu_X$-average of the conditional criterion for measurable $F$.
2. Its derivative in $F(x)$: $-P(y = 1 \mid x) e^{-F(x)} + P(y = -1 \mid x) e^{F(x)}$.
3. Corollary 3: at an optimal $F$, the weighted conditional mean of $y$ vanishes, $E_w(y \mid x) = 0$ almost everywhere.
4. Result 2 with (23)–(24): for a measurable current estimate $F$, the Real AdaBoost step $f(x) = \tfrac12 \log\big(P_w(y = 1 \mid x)/P_w(y = -1 \mid x)\big)$ minimizes $J(F + f)$ over measurable $f$, and $F + f = F^\star$ almost everywhere.
5. Corollary 1: on a region where $F$ is a constant $c$, the average of $e^{-y_i c}$ is minimized at $c = \tfrac12 \log(n_+/n_-)$, and the sample proportions are the symmetric logistic transform of that $c$.
6. Display (15): $e^{F}/(e^{-F} + e^{F}) = e^{2F}/(1 + e^{2F})$, so the symmetric logistic transform of (13) is the usual logistic model with a factor $2$.

Significance

Lemma 1 is what makes the rest of the paper a statement about logistic regression. Because the minimizer of $J$ is the half log-odds, an additive model $F = \sum_m f_m$ built by minimizing $J$ estimates $\tfrac12 \operatorname{logit} P(y = 1 \mid x)$, and the transform (13) converts it into a class probability. Result 2 shows that one population step of Real AdaBoost from any starting point already reaches $F^\star$, so the many iterations used in practice come from the crude approximation of conditional expectations by trees, not from the criterion. Corollary 3 gives the first-order condition used to interpret the AdaBoost weights. The other missions of this series (Discrete AdaBoost, LogitBoost, Gentle AdaBoost, multiclass LogitBoost) all rest on these population facts.

All of these results are proved in the paper; none is open. What this mission adds is a machine-checked version in the population setting, with conditional probabilities obtained from an honest disintegration of the joint law instead of being postulated. No formalization of the exponential criterion's population minimizer is known to exist on the platform or in Mathlib. The pointwise calculus is elementary; the work is in the measure-theoretic layer.

Difficulty

The paper's proof minimizes the conditional criterion pointwise and sets the derivative to zero. Turning this into a statement about $J$ requires three things the one-line proof does not mention. First, the joint expectation must be rewritten as an iterated integral, which needs the disintegration of $\nu$ and measurability of everything integrated. Second, the pointwise minimizer $F^\star$ must itself be a measurable function of $x$, which the calculus says nothing about. Third, the comparison is against every measurable competitor, including those with $J(F) = \infty$, so integrability cannot be assumed. Corollary 3 has a further difficulty: it assumes nothing about the class probabilities, so a proof must show that optimality of $F$ forces them strictly between $0$ and $1$ almost everywhere, a fact the paper's one-line proof does not address.

Formalization scope

Labels live on Bool, with sgn true = 1 and sgn false = -1. The joint law is ν : Measure (X × Bool) with [IsProbabilityMeasure ν] on an arbitrary measurable space X. $P(y = b \mid x)$ is (ν.condKernel x {b}).toReal, read off Mathlib's conditional kernel. It is determined only $\nu_X$-almost everywhere, so (13), (14), Corollary 3 and the identity of Result 2 are almost-everywhere statements; the conditional formula and its derivative hold at every $x$. $J$ is a lower Lebesgue integral in $[0, \infty]$. Competitors range over all measurable functions $X \to \mathbb R$. Derivatives are stated with HasDerivAt.

The hypothesis $0 < P(y = 1 \mid x) < 1$ almost everywhere is added to Lemma 1 and Result 2. Without it the ratio in (12) is $0$ or undefined, Real.log 0 = 0 would give a junk value, and no minimizer of $J$ exists. Corollary 1 assumes both labels occur in the region, which is the sample counterpart.

Several formalizations would make the targets trivial, and none is used here. Defining $J$ through its conditional formula would make milestone 1 a definition and the goal pointwise, so $J$ is the joint expectation under $\nu$. A Bochner integral would return $0$ for a non-integrable $e^{-yF}$ and make every such $F$ a minimizer, so $J$ takes values in $[0, \infty]$. A bare deriv is $0$ at points of non-differentiability. Writing the logistic transform as $1/(1 + e^{-F})$ in place of $e^{F}/(e^{-F} + e^{F})$ would lose the factor $2$ that (15) records.

A complete development needs the disintegration of a measure on $X \times \mathrm{Bool}$, iterated lower integrals, measurability of the conditional kernel, and elementary calculus of $t \mapsto a e^{-t} + b e^{t}$. Lemmas about conditional expectations against condKernel on a finite label set, and the measurability of $x \mapsto P(y = 1 \mid x)$, are reusable in the other missions of this series. Contributions of either kind are welcome.

Selected references

• J. Friedman, T. Hastie and R. Tibshirani, Additive logistic regression: a statistical view of boosting (with discussion), Annals of Statistics 28(2), 337–407, 2000. https://doi.org/10.1214/aos/1016218223
• Y. Freund and R. E. Schapire, Experiments with a new boosting algorithm, Proceedings of ICML, 148–156, 1996. https://dl.acm.org/doi/10.5555/3091696.3091715
• R. E. Schapire and Y. Singer, Improved boosting algorithms using confidence-rated predictions, Proceedings of COLT, 80–91, 1998; Machine Learning 37, 297–336, 1999. https://doi.org/10.1023/A:1007614523901
• L. Breiman, Prediction games and arcing algorithms, Technical Report 504, Statistics Department, UC Berkeley, 1997; Neural Computation 11(7), 1493–1517, 1999. https://doi.org/10.1162/089976699300016106

Motivation

Boosting combines many weak classifiers into a strong one. Friedman, Hastie and Tibshirani (Ann. Statist. 28 (2000) 337–407) explained the two-class AdaBoost algorithms statistically: in the population, boosting fits an additive logistic regression model by stagewise optimization of a criterion on the log-odds scale. Section 5 of that paper carries the explanation to $J>2$ classes. It answers two questions a practitioner faces when boosting a multiclass problem:

• what the widely used AdaBoost.MH algorithm of Schapire and Singer (1998) actually estimates;
• how to obtain a coupled multiclass procedure whose class probabilities sum to one.

The paper's answer to the second question is LogitBoost for $J$ classes (Algorithm 6). Result 6 asserts that it takes quasi-Newton steps on the multinomial log-likelihood. Algorithm 6 underlies later multiclass gradient boosting, where the per-class Newton step with a diagonal Hessian and the factor $(J-1)/J$ reappears (Friedman, Ann. Statist. 29 (2001)).

Setting

Fix $J\ge2$ classes, labelled $1,\dots,J$, and a measurable space $X$ of features. A probability measure $\nu$ on $X\times\{1,\dots,J\}$ is the joint law of the feature $x$ and the class $y$. The classes are mutually exclusive.

• The indicator responses are $y^*_j = \mathbf 1_{[y=j]}$, and the $\{-1,1\}$ responses are $y_j = 2y^*_j-1$.
• Conditional expectations $E(\cdot\mid x)$ are integrals against the conditional law $\nu(\cdot\mid x)$ of the class given $x$.
• The class probabilities are $p_j(x) = P(y_j=1\mid x)$.

Definition 1 (p. 354) introduces the symmetric multiple logistic transformation

$$F_j(x) = \log p_j(x) - \frac1J\sum_{k=1}^J\log p_k(x),\tag{39}$$

and states that it is equivalent to

$$p_j(x) = \frac{e^{F_j(x)}}{\sum_{k=1}^J e^{F_k(x)}},\qquad \sum_{k=1}^J F_k(x) = 0.\tag{40}$$

For $J=2$ this is the two-class $F(x) = \frac12\log[p(x)/(1-p(x))]$.

AdaBoost.MH (Algorithm 5) treats each class against the rest. Its population criterion is $\sum_{j=1}^J E\,e^{-y_jG_j(x)}$.

LogitBoost ($J$ classes) (Algorithm 6, population version) keeps a fit $F(x) = (F_1(x),\dots,F_J(x))$ and the probabilities $p_j(x)$ given by (40). For each class $j$ it forms the working response and weight

$$z_j = \frac{y^*_j-p_j(x)}{p_j(x)(1-p_j(x))},\qquad w_j = p_j(x)(1-p_j(x)).$$

It takes the weighted conditional mean $f_j(x) = E_{w_j}(z_j\mid x) = E(w_jz_j\mid x)/E(w_j\mid x)$, and updates

$$F_j(x)\ \leftarrow\ F_j(x) + \frac{J-1}{J}\Big(f_j(x) - \frac1J\sum_{k=1}^Jf_k(x)\Big).$$

The multilogit parametrization with base class $b$ writes $G_j(x) = F_j(x)-F_b(x)$, so that $G_b = 0$. The multinomial log-likelihood of one observation is

$$l(G) = \sum_{j\ne b}y^*_jG_j - \log\Big(1+\sum_{k\ne b}e^{G_k}\Big).$$

Formalization targets

Goal: Result 6 (p. 356), as its Derivation (p. 357) makes precise

Result 6 states that the LogitBoost algorithm ($J$ classes, population version) uses quasi-Newton steps for fitting an additive symmetric logistic model by maximum likelihood. The goal states, for every $x$ and every current fit $F$, the three facts the Derivation makes precise:

1. For every base class $b$ and $j,k\ne b$, the score and Hessian of $g\mapsto E(l(G+g)\mid x)$ at $g = 0$ are

$$s_j(x) = E\big(y^*_j-p_j(x)\mid x\big),\qquad H_{j,k}(x) = -p_j(x)\big(\delta_{jk}-p_k(x)\big).$$

2. The diagonal step $g^{(b)}_j = -H_{j,j}(x)^{-1}s_j(x)$ is well defined and equals $E(y^*_j-p_j(x)\mid x)/(p_j(x)(1-p_j(x)))$.
3. The Algorithm 6 update is the average over all base classes of the symmetrized diagonal step:

$$F_j(x) + \frac{J-1}{J}\Big(f_j - \frac1J\sum_k f_k\Big) = F_j(x) + \frac1J\sum_{b=1}^J\Big(g^{(b)}_j - \frac1J\sum_{k=1}^J g^{(b)}_k\Big).$$

Milestones

• Definition 1: the equivalence of (39) and (40), and the two-class case.
• The multilogit coordinates with base class $b$.
• Derivation steps 1, 2 and 3 separately.
• The population form of Algorithm 6's weighted least-squares fit.
• For $J=2$, Algorithm 6 reduces to two-class LogitBoost (Algorithm 3).
• Result 5 (p. 355): population AdaBoost.MH fits $J$ uncoupled models

$$G_j(x) = \tfrac12\log\frac{p_j(x)}{1-p_j(x)},$$

each minimizing the class-$j$-against-the-rest exponential criterion.

Significance

The result places J-class LogitBoost inside likelihood theory. Its population step is a Newton-type step for multinomial maximum likelihood. Two approximations separate it from the full Newton step: the Hessian is replaced by its diagonal, and the base class is averaged out. Result 5 shows that AdaBoost.MH, in contrast, solves $J$ decoupled one-against-the-rest problems whose implied probabilities need not sum to one. That contrast is the paper's argument for the coupled procedure.

All statements here are proved in the paper by direct calculation. They have not been formalized before. The mission produces machine-checked versions of the population claims and of the algebra behind them. That algebra comprises the softmax/centred-logit equivalence, the multinomial score and Hessian in base-class coordinates, and the base-class averaging identity. These pieces are reusable for any multinomial logistic or softmax model.

Difficulty

There is no deep step. The work lies in keeping two parametrizations apart: the base-class multilogit coordinates $G$, with $J-1$ free entries, and the symmetric centred coordinates $F$, with $J$ entries summing to zero. The derivatives are taken in $G$. The algorithm and (40) live in $F$. The step is converted back by symmetrization. Mixing the two makes the averaging identity false or vacuous.

A second point is that the update is not the Newton step $-H^{-1}s$. The page states this explicitly: for full Newton stepping the symmetrization would be redundant. The tempting shortcut of proving that Algorithm 6 equals the full Newton step therefore does not prove Result 6.

Formalization scope

• Classes are Fin J, with $J\ge2$ where needed.
• $\nu$ is a probability measure on $X\times$ Fin J.
• Conditional expectations given $x$ are integrals against Mathlib's ν.condKernel x.
• The constants $1/J$ and $(J-1)/J$ are real numbers.
• Every statement about Result 6 is conditional on a fixed $x$ and holds for every $x$, with no integrability or positivity hypothesis on the true class probabilities.
• The model probabilities (40) lie strictly in $(0,1)$ when $J\ge2$, so $p_j(1-p_j)\ne0$ is proved, not assumed.
• The page fixes the base class $J$. Here the base class is a parameter $b$, as the averaging in step 3 requires.
• The AdaBoost.MH criteria are lower Lebesgue integrals in $[0,\infty]$.
• Result 5 adds the hypothesis $0<p_j(x)<1$ for almost every $x$, because the log-odds is undefined at $0$ and $1$.
• Definition 1 is stated for positive probability vectors.

Trivializing encodings are ruled out:

• Derivatives are stated with HasDerivAt along coordinate lines, and the Hessian is the derivative of an explicitly given partial derivative, never a deriv equation that would be a junk $0$ at non-differentiable points.
• The conditional expectations $E(y^*_j\mid x)$ are integrals against the conditional law of the joint $\nu$, not a free vector.
• The exponential criteria are never Bochner integrals, which would return $0$ on non-integrable integrands.
• (40) is the softmax of the centred scores itself.

All objects are defined in one definitions file in the namespace AddLogReg.Multiclass. Proofs of any of the milestones are welcome. Lemmas on the softmax map, such as positivity, the derivative of log-sum-exp in base coordinates and shift invariance, are reusable beyond this mission.

Selected references

• J. Friedman, T. Hastie, R. Tibshirani, Additive logistic regression: a statistical view of boosting, Ann. Statist. 28(2) (2000) 337–407. https://doi.org/10.1214/aos/1016218223
• R. E. Schapire, Y. Singer, Improved boosting algorithms using confidence-rated predictions, Machine Learning 37 (1999) 297–336 (COLT 1998). https://doi.org/10.1023/A:1007614523901
• J. Friedman, Greedy function approximation: a gradient boosting machine, Ann. Statist. 29(5) (2001) 1189–1232. https://doi.org/10.1214/aos/1013203451

Motivation

Prediction with expert advice asks a learner to predict a binary label on each of a sequence of trials, after seeing the predictions of a pool of candidate functions, and to make few more mistakes than the best member of the pool. Littlestone and Warmuth's The Weighted Majority Algorithm (Inform. and Comput. 108, 1994) gave the deterministic algorithm WM and its randomized variant WMR, and proved worst-case bounds that hold for every sequence of trials, with no probabilistic assumption on the data. Their §8 asks how good such bounds can possibly be when the data contain anomalies: disagreements with a candidate function, counted relative to the best-fitting member of the pool. Such disagreements can arise from noise in the instances or labels, or from instances that do not determine the label.

For the randomized algorithm WMR the expected number of mistakes grows, by Corollary 6.1 of the paper, at rate $\ln(1/\beta)/(1-\beta)$ per anomaly, which tends to $1$ as $\beta \to 1$. Theorem 8.2 shows that no randomized learner, however it is built, can do better than rate $1$: an adversary who fixes the sequence in advance can force half the noise-free optimum plus one expected mistake per anomaly. Together with the deterministic counterpart, Theorem 8.1 (rate $2$), it locates the cost of label noise in online learning exactly. Mistake-bound lower bounds of this kind are a standard reference point for the analysis of online classification and of the expert-advice algorithms descended from WM (Cesa-Bianchi and Lugosi, Prediction, Learning, and Games, 2006).

Timeline: Littlestone (1988) characterized the optimal noise-free mistake bound $\mathrm{opt}(F,0)$ by complete mistake trees (the Littlestone dimension); Littlestone and Warmuth (FOCS 1989; journal version 1994) introduced WM and WMR and proved Theorems 8.1 and 8.2.

Setting

Let $X$ be an arbitrary domain and $F$ a pool of functions $X \to \{0,1\}$, finite or infinite. A trial is a pair $(x,y)$ with $x\in X$ and $y\in\{0,1\}$; a sequence of trials is a finite list $\mathcal S = ((x_1,y_1),\dots,(x_T,y_T))$, in which an instance may repeat with different labels. The number of anomalies of $\mathcal S$ with respect to $f$ is $\#\{t : f(x_t)\ne y_t\}$, and $S_\eta$ is the collection of sequences for which some $f\in F$ has at most $\eta$ anomalies.

A deterministic algorithm maps the past trials and the current instance to a predicted label; $M_A(\mathcal S)$ counts its wrong predictions, and

$$\mathrm{opt}(F,\eta) = \inf_A \sup_{\mathcal S\in S_\eta} M_A(\mathcal S).$$

A randomized algorithm uses random choices independent of the sequence. On a fixed sequence its behaviour at trial $t$ is summarized by $p_t\in[0,1]$, the probability that it predicts $1$ given the preceding instances and labels and the current instance; its expected number of mistakes is $\sum_t |p_t - y_t|$, and

$$\mathrm{opt}_{\mathrm{RAND}}(F,\eta) = \inf_A \sup_{\mathcal S\in S_\eta} \sum_{t=1}^T |p_t-y_t|,$$

the infimum ranging over all maps $A$ from (past trials, current instance) to $p_t \in [0,1]$.

Formalization targets

Goal: Theorem 8.2 (p. 252)

For every pool $F$ with $|F|>1$ and every integer $\eta\ge 0$,

$$\mathrm{opt}_{\mathrm{RAND}}(F,\eta)\ \ge\ \tfrac12\,\mathrm{opt}(F,0)+\eta .$$

Both sides live in $[0,\infty]$; when $\mathrm{opt}(F,0)=\infty$ the statement says $\mathrm{opt}_{\mathrm{RAND}}(F,\eta)=\infty$.

Milestone: complete mistake trees (§8, p. 251)

"For any pool of functions $F$ there exists a complete $\mathrm{opt}(F,0)$-mistake tree" ([Lit88]). On the platform this is the proved Lemma 21.7 of Shalev-Shwartz and Ben-David, $M_{\mathrm{SOA}}(F)\le \mathrm{Ldim}(F)$, together with Lemma 21.6, $\mathrm{Ldim}(F) \le M_A(F)$ for every $A$; a tree shattered by $F$ is a complete mistake tree.

Significance

The theorem shows that the expected-mistake bound of WMR is optimal in its dependence on the number of anomalies: its coefficient of $\eta$ approaches $1$, and no randomized learner achieves a smaller one on every pool with two or more functions. It also quantifies the advantage of randomization: the deterministic rate is $2$ (Theorem 8.1), the randomized rate is $1$, and the noise-free term halves. The lower bound is obliviously adversarial, since the sequence is chosen before any coin is tossed, so it applies equally to the stronger model in which the adversary adapts to the learner's predictions.

The result has been proved since 1994. To our knowledge it has no machine-checked proof; the platform holds the Littlestone-dimension characterization of the noise-free optimum (Shalev-Shwartz and Ben-David, Chapter 21) but no statement about anomalies or randomized lower bounds. This mission formalizes the definitions of anomalies, $\mathrm{opt}(F,\eta)$ and $\mathrm{opt}_{\mathrm{RAND}}(F,\eta)$, and the theorem.

Difficulty

An adversary against a randomized learner cannot react to its predictions: the whole sequence, instances and labels, must be fixed in advance, so the adaptive adversary that proves the deterministic bound is not directly available. The lower bound must instead come from the learner's prediction probabilities, which depend only on the sequence prefix; the content of the theorem is that this information is enough to construct, for every learner, one fixed sequence that stays inside $S_\eta$ while forcing the stated expected count. Taking the infimum over learners inside an extended-real supremum over sequences of every length adds bookkeeping when $\mathrm{opt}(F,0)$ is infinite.

Formalization scope

Sequences are Fin T → X × Bool for every T : ℕ. Deterministic algorithms, the mistake count, shattered trees and the Littlestone dimension are reused from the published definition UnderstandingML_Online (OnlineAlg, mistakes, ShattersTree, ldim, soa); randomized algorithms are its OnlineAlgR X := List (X × Bool) → X → ℝ restricted by IsRandAlg to values in $[0,1]$, and the expected mistake count is its cumLoss. $\eta$ is a natural number. $\mathrm{opt}(F,\eta)$ takes values in ℕ∞ and $\mathrm{opt}_{\mathrm{RAND}}(F,\eta)$ in ℝ≥0∞; the paper's "minimum" is read as an infimum. $|F|>1$ is F.Nontrivial, which admits infinite pools.

The reduction of randomized algorithms to probability maps is the main modelling choice: on a fixed sequence the expected number of mistakes of any algorithm whose randomization is independent of the sequence equals $\sum_t|p_t-y_t|$, and every map with values in $[0,1]$ is realized by such an algorithm, so the two infima coincide. Dropping the constraint $p_t\in[0,1]$, or quantifying only over deterministic algorithms, gives a different quantity and is ruled out.

Needed: the definitions above, and the existence of a complete $\mathrm{opt}(F,0)$-mistake tree, available through the proved platform theorems on ldim and soa. Lemmas relating mistakes along a path of a shattered tree to ldim, and a reusable statement that an oblivious adversary can force expected loss $\tfrac12$ per trial, would serve other lower bounds in the Littlestone–Warmuth series and in online learning generally. Contributions of such lemmas are welcome.

Selected references

• N. Littlestone, M. K. Warmuth, The Weighted Majority Algorithm, Information and Computation 108(2):212–261, 1994. https://doi.org/10.1006/inco.1994.1009
• N. Littlestone, Learning Quickly When Irrelevant Attributes Abound: A New Linear-Threshold Algorithm, Machine Learning 2:285–318, 1988. https://doi.org/10.1007/BF00116827
• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 21. https://doi.org/10.1017/CBO9781107298019
• N. Cesa-Bianchi, G. Lugosi, Prediction, Learning, and Games, Cambridge University Press, 2006. https://doi.org/10.1017/CBO9780511546921

Motivation

A retailer who stocks a perishable or storable product each period must choose an order-up-to level without knowing the demand distribution. Worse, demand is censored: when the shelf empties, the retailer observes sales, not demand. Huh and Rusmevichientong (Math. Oper. Res. 34(1), 2009) proposed the Adaptive Inventory Management (AIM) algorithm, a projected stochastic subgradient method that uses only the censored observation "was there stock left at the end of the period?". They proved that its average expected cost converges to the cost of the optimal newsvendor level at rate $O(1/\sqrt T)$, with no parametric assumption on demand.

In the non-perishable case, where leftover stock carries over, the main convergence theorem (Theorem 2, p. 7) requires the step-size scale $\gamma$ to satisfy $\gamma\le\rho\max\{b,h\}/(h\bar y)$, where $\rho$ is a known lower bound on mean demand. Section 3.2 of the paper removes this requirement. Its Theorem 8 bounds the excess cost of AIM for every step scale $\gamma>0$, at the price of a hitting time and a busy period in the bound. This mission formalizes Theorem 8 and the steps of its proof.

Setting

Demands $D_1,D_2,\dots$ are independent, nonnegative, identically distributed, with finite positive mean $E[D_1]$ and otherwise unknown law. The holding cost is $h>0$ per unit left over and the penalty is $b>0$ per unit of unmet demand. The newsvendor cost of stocking up to $y\ge0$ is

$$Q(y)=h\,E[y-D_1]^+ + b\,E[D_1-y]^+ ,$$

and the newsvendor quantity is $y^{NV}=\inf\{y\ge0: P(D_1\le y)\ge b/(b+h)\}$. The manager knows an upper bound $\bar y\ge y^{NV}$.

AIM, non-perishable case. Fix $\gamma>0$ and a starting target $\hat y_1\in[0,\bar y]$. Put $y_1=\hat y_1$, $x_1=0$. In period $t\ge1$ the step is $\epsilon_t=\gamma\bar y/(\max\{b,h\}\sqrt t)$, the observed slope is $H_t=h$ if $D_t<\hat y_t$ and $H_t=-b$ otherwise, and

$$\hat y_{t+1}=\max\{\min\{\hat y_t-\epsilon_tH_t,\bar y\},0\},\qquad x_{t+1}=[y_t-D_t]^+,\qquad y_{t+1}=\max\{\hat y_{t+1},x_{t+1}\}.$$

The target $\hat y_t$ follows the gradient step. The implemented level $y_t$ can exceed it because stock that has already been bought cannot be returned. The excess-cost term is

$$\Lambda_2(T)=E\Big[\frac1T\sum_{t=1}^T\big(Q(y_t)-Q(\hat y_t)\big)\Big].$$

Auxiliary processes. Let $m=h\gamma\bar y/\max\{b,h\}$. For a real $\theta$:

• $W_1(\theta)=0$, $W_{t+1}(\theta)=[W_t(\theta)+\theta-D_t]^+$ is a queue with constant inflow. Its first busy period has length $|J_1(\theta)|=\inf\{t>1:W_t(\theta)=0\}-1$.
• $Z_1(\theta)=0$, $Z_{t+1}(\theta)=[Z_t(\theta)+\theta/\sqrt t-D_t]^+$ is a queue with decreasing inflow.
• $K(\theta,z)=\min\{t\ge0: z+\sum_{s=1}^t(\theta-D_s)\le0\}$ is the hitting time of $(-\infty,0]$ by the random walk started at $z$.

For $0<\rho'<m$, the proof uses $\tilde T=\lceil(m/\rho')^2\rceil$ and $\tilde K=\min\{t>\tilde T:Z_t(m)=0\}$.

Formalization targets

Goal: Theorem 8 (p. 13)

For every $T\ge1$ and every $\rho'$ with $0<\rho'<\min\{m,E[D_1]\}$,

$$\Lambda_2(T)\le\frac{\max\{b,h\}\,\bar y}{T}\Big\{\big\lceil(m/\rho')^2\big\rceil+E\Big[K\Big(\rho',\frac{2\sqrt2\,m^2}{\rho'}\Big)\Big]\Big\}+\frac{2hm\,E\big[|J_1(\rho')|^2\big]}{\sqrt T}.$$

The statement makes no moment assumption on demand. It is stated with the paper's explicit constants, and both expectations on the right may be infinite.

Milestones

1. Coupling (proof of Theorem 8, p. 13). For every demand path and every $t\ge1$, $y_t-\hat y_t\le Z_t(m)$.
2. Restart bound (p. 14). For $0<\rho'<m$, $E[\tilde K]\le\lceil(m/\rho')^2\rceil+E[K(\rho',2\sqrt2m^2/\rho')]$.
3. Claim (14) (p. 14, proved in Appendix E). For $0<\rho'<\min\{m,E[D_1]\}$, $\frac hT E\big[\sum_{t=\tilde K+1}^T Z_t(m)\big]\le 2hm\,E[|J_1(\rho')|^2]/\sqrt T$.
4. Lemma 9, corrected (p. 13). If $\theta<E[D_1]$, $E[D_1^4]<\infty$ and $z>0$, then $E[K(\theta,z)]\le1+\frac{2z}{E[D_1]-\theta}+\frac{8\pi^2E[(D_1-E[D_1])^4]}{(E[D_1]-\theta)^4}$.

Significance

The result. The cost of AIM relative to the newsvendor benchmark splits as $\Lambda_1(T)+\Lambda_2(T)$. Stochastic subgradient descent controls $\Lambda_1(T)$ for every $\gamma$, so Theorem 8 is the remaining step in showing that AIM converges at rate $O(1/\sqrt T)$ without any knowledge of a lower bound on mean demand. The first term of the bound is $O(1/T)$ whenever $E[K]$ is finite, and Lemma 9 gives that under a finite fourth moment. The second term is $O(1/\sqrt T)$ whenever $E[|J_1|^2]$ is finite, and the paper's Proposition 4 gives that under a finite sixth moment. The result therefore removes the one piece of prior information about demand, other than $\bar y$, that the non-perishable analysis needed.

Formalizing it. The paper's proof is complete and short, but it moves between expectations of random indices, pathwise couplings and renewal arguments, and the statements of Theorem 8 and Lemma 9 contain the slips recorded below. None of these results has a machine-checked proof. The mission produces a checked AIM recursion, a pathwise domination of excess inventory by a queue, and hitting-time and busy-period bounds for random walks with nonnegative i.i.d. decrements.

Difficulty

The argument behind Theorem 2 dominates $y_t-\hat y_t$ by a queue whose inflow $\rho/\sqrt t$ is below the mean demand. For large $\gamma$ the inflow $m/\sqrt t$ exceeds $E[D_1]$ in early periods, so the queue $Z(m)$ is unstable at first and its busy periods are not controlled by a stationary queue. A direct bound on $E[\sum_t Z_t(m)]$ through busy periods of $W(m)$ fails, because $W(m)$ may never empty when $m\ge E[D_1]$. The proof therefore separates a random initial stretch, which ends at the first time after $\tilde T$ that $Z(m)$ empties, from the remainder. The two parts are bounded by different processes. The random index $\tilde K$ sits inside the sums, so the expectations have to be handled with that dependence.

Formalization scope

• Demand uses the published definition CappedBaseStock_Model (DemandLaw, the i.i.d. path measure demandPathLaw). Its law has finite and strictly positive mean. The cost $Q$ and $y^{NV}$ are the published backorderCost and newsvendorLevel of LostSalesOrderUpTo.Asymptotic.Backorder. Both are reused, not redefined.
• The demand path is zero-based: the paper's $D_t$ is d (t-1). AIM is a deterministic recursion on the path, and $\hat y_t,y_t,x_t$ depend on $D_1,\dots,D_{t-1}$ only. Levels are real numbers, and $Q$ is evaluated at nonnegative levels.
• The conventions are $Z_1=W_1=0$ and $\tau_0=1$. The paper's own indexing ($Z_0=0$ in (7)) is undefined at $t=0$, and these are the conventions its proofs use.
• $K$, $|J_1|$ and $\tilde K$ take values in $[0,\infty]$, and $E[K]$, $E[|J_1|^2]$, $E[\tilde K]$ are Lebesgue integrals in $[0,\infty]$. Theorem 8 and Claim (14) are stated in $[0,\infty]$. A divergent expectation therefore makes a bound trivially true. It can never make a bound false or vacuous through a junk value $0$. $\Lambda_2(T)$ is a real expectation of a bounded integrand.
• Explicit readings of loose phrases: "for any choice of the parameter $\gamma$" means every $\gamma>0$. "Set $y_1=\hat y_1$ to any value in $[0,\bar y]$" means the statements hold for every such start. "With probability one" in the coupling is stated pathwise. $0<\rho'$ is added (the bound divides by $\rho'$), as are $h,b,\bar y>0$. In Claim (14) the random lower limit $\tilde K$ is read inside the expectation, as in (13) and Appendix E.
• Lemma 9 is false as printed: for $D\equiv1$, $\theta=0$, $z=1/4$ one has $K=1$ while the printed bound is $1/2$. The mission states it with an additive $1$, which is what the printed proof gives once the integers below $2z/(E[D_1]-\theta)$ are counted correctly.
• Ruled out: stating the goal about an arbitrary sequence of levels instead of the AIM recursion, taking $E[K]$ or $E[|J_1|^2]$ as real Bochner integrals (which are $0$ when the expectation diverges and would make the bound false), and dropping the newsvendor bound $y^{NV}\le\bar y$ from the goal.
• Welcome contributions: a reusable Lindley-recursion (see Asmussen 2003, Ch. III) and busy-period library (the inspection-paradox bound $E|J_{i(\theta,s)}(\theta)|\le E|J_1(\theta)|^2$, Lemma 13 of the paper), fourth-moment Markov bounds for sums of i.i.d. centred variables, and shift invariance of the i.i.d. path measure.

Selected references

• W. T. Huh and P. Rusmevichientong, A Nonparametric Asymptotic Analysis of Inventory Planning with Censored Demand, Mathematics of Operations Research 34(1):103–123, 2009. https://doi.org/10.1287/moor.1080.0355
• S. Asmussen, Applied Probability and Queues, 2nd ed., Springer, 2003. https://doi.org/10.1007/b97236

Motivation

A probability forecast is useful only when its stated frequencies bear a stable relation to outcomes. If a forecaster repeatedly announces a 70% chance of rain, calibration asks whether rain occurs on about 70% of those days. This is a minimal reliability requirement for probabilistic prediction, even though calibration alone does not rank every pair of forecasts by usefulness. Foster and Vohra study the difficulty of obtaining this property when the weather sequence is chosen in response to a forecaster's past behavior. A deterministic rule can be forced into a persistent calibration error; the article shows how randomized forecasts evade that obstruction when Nature sees past forecasts but cannot see the current random draw. Foster and Vohra, 1998.

The work sits at an intersection of sequential probability forecasting and repeated games. Its opponent can adapt to the whole observed history, including the forecaster's earlier random outcomes. The simultaneity of each round matters: before choosing that round's wet or dry outcome, Nature knows the distribution of the next forecast but not which forecast is realized. The paper's main result is about a specified forecasting rule constructed from regret balances, rather than merely the existence of some successful randomized strategy. Foster and Vohra, 1998, §§3, 5.

Timeline. Dawid (1982) proposed calibration as a criterion for sequential probability forecasts and showed that a coherent Bayesian expects to be calibrated (doi). Oakes (1985), with Dawid's accompanying comment, showed that no deterministic forecaster is calibrated against every outcome sequence: Nature may rain exactly when the forecast is at most $1/2$ (doi). Foster and Vohra circulated the present randomized construction from 1994 (received August 1994, published 1998); their 1997 Games and Economic Behavior paper used a calibrated forecaster built on the same pairwise-regret flow equations to reach correlated equilibria (doi). Hart and Mas-Colell (2000) later turned the same internal-regret quantities into regret matching (doi).

Setting

At round $s$, the outcome $X_s$ is $1$ for wet and $0$ for dry. The forecaster selects a probability from the finite grid $G_k=\{0,1/k,\ldots,1\}$, where $k$ is a positive integer. A forecast $p$ is represented by the binary probability vector $(1-p,p)$; the second coordinate is the forecast chance of rain. The forecaster chooses $i/k$ with probability $\mu_s^i$. The Brier loss of that possible forecast is $L_s^i=(X_s-i/k)^2$.

After $t$ rounds, $n_t(p)$ counts the realized forecasts equal to $p$, and $\rho_t(p)$ is the observed fraction of wet outcomes on those rounds. The quadratic calibration score is

$$C_t=\sum_{p\in G_k}\frac{n_t(p)}{t}\bigl(\rho_t(p)-p\bigr)^2.$$

A forecast never issued has zero count and contributes zero. The paper also uses a weighted calibration score $\widetilde C_t$, in which the realized indicator that $i/k$ was chosen is replaced by its conditional probability $\mu_s^i$. Its weighted count is $\widetilde n_t(i/k)=\sum_{s<t}\mu_s^i$, and its weighted wet frequency is $\widetilde\rho_t(i/k)=\sum_{s<t}\mu_s^i X_s/\widetilde n_t(i/k)$ when the denominator is positive.

For grid points $i/k$ and $j/k$, the pairwise regret $R_t^{i\to j}$ is the positive part of the cumulative weighted reduction in Brier loss that would result from replacing $i/k$ by $j/k$ on rounds weighted by $\mu_s^i$. The algorithm chooses its next distribution so that the regret flow out of each $i$ equals the flow into $i$:

$$\mu_s^i\sum_j R_{s-1}^{i\to j} =\sum_j\mu_s^j R_{s-1}^{j\to i}.$$

These equations use only regret from previous rounds. They specify a distribution after every possible history, including histories created by Nature's adaptive choices. Foster and Vohra, 1998, §5.

Formalization targets

Main theorem

The target is Theorem 1: for every $\varepsilon>0$, choose $k\ge1/\varepsilon^2$ and let the forecaster follow the regret-flow equations. Against every adaptive Nature, the realized score eventually satisfies

$$\Pr\{C_t<\varepsilon\}>1-\varepsilon.$$

The time after which the inequality holds may depend on the forecaster, Nature, and $\varepsilon$. The statement fixes the algorithm and the grid scale; a general existence theorem would leave out its central content. Foster and Vohra, 1998, Theorem 1 and §6 Corollary.

Supporting targets

The milestones record the source's attack path: solvability of the flow equations, a history-adapted forecaster satisfying them, the counting-process bounds and convergence of $C_t-\widetilde C_t$ in probability, the algebraic link between calibration and regret, the bound on the smoothed regret potential, and the deterministic bound on $\widetilde C_t$. Theorem 3's last constant is written as $(k+1)/(2\delta)$ and the corollary's horizon as $8k^2/\varepsilon^2$; the printed constants are inconsistent with the paper's $k+1$ grid points and its derived rate, respectively. The provenance and corrections are recorded with those milestones. Foster and Vohra, 1998, §6.

Significance

The result gives a concrete randomized forecaster whose realized empirical frequencies remain reliable even when outcomes react to past forecasts. The game model includes fixed outcome sequences as a special case, but its adaptive Nature can condition future choices on every earlier realized forecast and outcome. The theorem therefore identifies a particular sequential rule, its finite forecast grid, and the information boundary under which its guarantee holds. Foster and Vohra, 1998, §§3, 5–6.

The published Foster–Vohra 1997 formalization already supplies reusable definitions of finite probability vectors, history laws, pairwise regret, and calibration scores, together with a proved finite flow-conservation theorem. This mission extends that substrate to the 1998 paper's Brier-loss grid algorithm. Theorem 1 and its supporting results are proved on paper but not yet formalized; the earlier formal existence theorem for some calibrated forecaster does not establish this algorithm's guarantee, which is the content of the goal.

Difficulty

The weighted score $\widetilde C_t$ is controlled by quantities known from the chosen mixtures, while $C_t$ depends on the actual random draws. A direct deterministic bound on $C_t$ therefore does not follow from the regret equations. The gap requires a quantitative comparison of realized counts and weighted counts under an adaptive history law, followed by a passage from those count errors to the nonlinear calibration score. The regret itself has a positive-part kink, so its aggregate bound is stated through the paper's smoothed potential. Foster and Vohra, 1998, §6.

Formalization scope

The Lean model uses binary outcomes, $k+1$ grid indices Fin (k + 1), and histories ordered from oldest to newest. Rounds start at index $0$: the paper's $R_{s-1}$ in round $s$ is the regret over the preceding $s$ indices. Forecast and outcome are drawn independently conditional on the past by the published histLaw; Nature is any map from complete past histories to a probability distribution on the two outcomes. The forecast rule is likewise a map from histories to grid distributions. For each earlier round it reads only that round's prefix, so the current outcome cannot influence its mixture.

The goal uses the realized quadratic score calibScore2Hj h 1, whose second vector coordinate is the wet probability. The map $i\mapsto(1-i/k,i/k)$ is injective for $k>0$. The weighted score is a separate definition used in supporting results. A forecaster satisfying the flow equations is shown to exist by a milestone, so the goal's algorithm hypothesis has content. The statement covers adaptive Nature; replacing Nature by a fixed sequence or replacing $C_t$ by $\widetilde C_t$ would change the claim.

Every theorem requiring the grid has the explicit $k>0$ condition. Deterministic calibration bounds assume binary outcomes and probability-vector weights; the history-law theorems obtain these properties from Fin 2 and PMF. When a weighted count is zero, Lean's division convention gives weighted wet frequency $0$; nonnegative weights make its numerator zero as well. At horizon $0$, the weighted calibration score is $0$. The probability event is measured with the history law's outer measure in $\mathbb R_{\ge0}\cup\{\infty\}$. Reusable work includes finite-history martingale estimates, weighted calibration comparisons, and finite regret-potential bounds.

Selected references

• D. P. Foster and R. V. Vohra, Asymptotic calibration, Biometrika 85(2):379–390, 1998. DOI: 10.1093/biomet/85.2.379.
• A. P. Dawid, The well-calibrated Bayesian, Journal of the American Statistical Association 77:605–613, 1982. DOI: 10.1080/01621459.1982.10477856.
• D. Oakes, Self-calibrating priors do not exist, Journal of the American Statistical Association 80:339, 1985, with comments by A. P. Dawid (pp. 340–341) and M. Schervish (pp. 341–342). DOI: 10.1080/01621459.1985.10478117.
• D. P. Foster and R. V. Vohra, Calibrated learning and correlated equilibrium, Games and Economic Behavior 21:40–55, 1997. DOI: 10.1006/game.1997.0595.
• D. Blackwell, An analog of the minimax theorem for vector payoffs, Pacific Journal of Mathematics 6:1–8, 1956. DOI: 10.2140/pjm.1956.6.1.
• S. Hart and A. Mas-Colell, A simple adaptive procedure leading to correlated equilibrium, Econometrica 68:1127–1150, 2000. DOI: 10.1111/1468-0262.00153.