Optimization

Motivation

One-dimensional bin packing asks for the fewest unit-capacity bins that hold a given list of items with sizes in $(0,1)$. Deciding whether two bins suffice is NP-hard (it contains the partition problem), so no polynomial-time algorithm guarantees a ratio below $3/2$ unless P = NP. The natural question is therefore asymptotic: how small can the additive error $A(I) - OPT(I)$ be made, as a function of the optimum $OPT(I)$?

• 1974: D. S. Johnson, A. Demers, J. D. Ullman, M. R. Garey and R. L. Graham analysed First Fit and First Fit Decreasing, with asymptotic ratios $17/10$ and $11/9$ (SIAM J. Comput. 3(4)).
• 1981: W. Fernandez de la Vega and G. S. Lueker gave an asymptotic approximation scheme: for every $\varepsilon > 0$, $(1+\varepsilon)\,OPT(I) + 1$ bins in linear time (Combinatorica 1).
• 1982: N. Karmarkar and R. M. Karp replaced the multiplicative error by an additive one: $OPT(I) + O(\log^2 OPT(I))$ bins in polynomial time (Proc. 23rd FOCS). This mission formalizes that bound.
• 2017: R. Hoberg and T. Rothvoss improved the additive error to $O(\log OPT)$ (SODA 2017). Whether $OPT(I) + O(1)$ is achievable remains open.

Its main device, geometric grouping followed by rounding a linear program over bin configurations, recurs in later additive results and in cutting-stock problems.

Setting

An instance $I$ is a finite multiset of piece sizes in the open interval $(0,1)$. Write $n(I)$ for the number of pieces, $m(I)$ for the number of distinct sizes, $SIZE(I)$ for the total size and $a(I)$ for the smallest size. A packing is a multiset of bins whose union is $I$ and in each of which the sizes sum to at most $1$; its cost is the number of bins, and $OPT(I)$ is the least cost.

A configuration is a nonempty multiset of sizes occurring in $I$ that fits in one bin. The fractional bin-packing problem is the linear program

$$(I)\qquad \min\ \mathbf 1\cdot x\quad\text{s.t.}\quad x \ge 0,\quad Ax \ge b,$$

with one variable $x_j$ per configuration, where $A_{tj}$ counts the pieces of size $t$ in configuration $j$ and $b_t$ the pieces of size $t$ in $I$. Its value is $LIN(I)$. A basic feasible solution is an extreme point of the feasible region.

Geometric grouping with parameter $k$ sorts the pieces in non-increasing order and cuts them into consecutive groups $G_1, G_2, \dots, G_q$, each the shortest run of pieces of total size at least $k$. Within each group $G_i$ ($i \ge 2$) only as many of the largest pieces as $G_{i-1}$ has are kept; they are rounded up to the largest size in $G_i$, giving $G_i'$. The rounded pieces form $J$, and $G_1$ together with the unrounded leftovers $\Delta G_i$ form $J'$.

ALGORITHM 2 with a positive integer $k$ and a positive real $g$:

1. Eliminate all pieces of size $\le g$.
2. While $SIZE > 1 + \frac{1}{1-1/k}\ln\frac1g$: group the current instance into $J, J'$; pack $J'$ in at most $2k[2 + \ln\frac1g]$ bins; obtain a basic feasible solution $x$ of the LP of $J$ with cost at most $LIN(J)+1$; open $\lfloor x_j\rfloor$ bins of each configuration $j$, fill them with pieces, and delete the pieces so packed.
3. Pack the remaining pieces in at most $2 + \frac{2}{1-1/k}\ln\frac1g$ bins.
4. Reinsert the eliminated pieces, using a new bin only when necessary.

Its cost on $I$ is written $A(I)$.

Formalization targets

Goal: Theorem 4 with explicit constants

For every instance $I$ with $SIZE(I) \ge 2$, every packing that ALGORITHM 2 with $k=2$ and $g = 1/SIZE(I)$ can output is a packing of $I$ with

$$A(I) \le OPT(I) + \bigl(1 + \log_2 OPT(I)\bigr)\bigl(9 + 4\ln OPT(I)\bigr) + 2 + 4\ln OPT(I).$$

This is the paper's $A(I) \le OPT(I) + O(\log^2 OPT(I))$, with the constants that its proof yields.

The general bound for ALGORITHM 2

For integers $k \ge 2$, $0 < g \le \tfrac12$ and $SIZE(I) \ge 1$:

$$A(I) \le \max\Bigl\{(1+2g)\,OPT(I) + 1,\ OPT(I) + \Bigl[1 + \frac{\ln SIZE(I)}{\ln k}\Bigr]\Bigl[1 + 4k + 2k\ln\frac1g\Bigr] + 2 + \frac{2}{1-\frac1k}\ln\frac1g\Bigr\}.$$

Milestones

In attack order: Lemmas 1–3; Theorem 2 (items 1–3, the bound on $J'$, item 4 corrected); the per-iteration shrinking of $SIZE$; the bound on the number $t$ of iterations; the telescoping of $LIN$; the bin count after Step 3; the general bound.

Significance

The bound gives a polynomial-time algorithm whose additive error is polylogarithmic in the optimum, hence a fully polynomial asymptotic approximation scheme ($O(\log^2 OPT) = o(OPT)$). Varying $k$ and $g$ trades running time for error, as the paper notes after Theorem 4. The scheme of solving the rounded LP, keeping its integer part and re-grouping the residual is reused by later additive results, including the $O(\log OPT)$ bound of Hoberg and Rothvoss.

The result has been proved since 1982. No machine-checked proof of it, or of any bin-packing approximation guarantee of this kind, is known to exist in Lean or Mathlib. The mission produces a formal version whose hypotheses and constants are explicit. It also corrects two printed statements whose published forms are false: Theorem 2, item 4, and the chain of inequalities in the analysis that relies on it. The corrections are disclosed in the statements.

Difficulty

Rounding a single LP solution does not suffice. A basic solution of the configuration LP has at most $m$ fractional variables, and after rounding down, the leftover pieces form an instance of size at most $m(J)$. With linear grouping that leftover is of order $1/\varepsilon^2$ and costs a constant factor. The difficulty is making the residual shrink geometrically. Geometric grouping must produce an instance $J$ with $m(J) \le SIZE/k + O(\ln(1/g))$ distinct sizes while discarding only $O(k\ln(1/g))$ in $J'$. The residual must then be re-grouped and re-solved. Each step must be accounted for simultaneously in $SIZE$, $LIN$ and $OPT$, with an additive loss per iteration; the harmonic-sum estimate behind $SIZE(J')$ and the telescoping of $LIN$ across iterations carry most of the weight.

Formalization scope

• Model. An instance is a Multiset ℝ with sizes in the open interval $(0,1)$; real sizes generalize the paper's rationals, and the interval is open because a group of size at least $k$ must contain more than $k$ pieces. Packings are Multiset (Multiset ℝ). $OPT$ and $LIN$ are infima over nonempty sets. LP solutions are finitely supported functions on configurations; "basic" means extreme point.
• Subroutine contract. The Fractional Bin-Packing procedure is modelled only by its stated output: any basic feasible solution of cost at most $LIN(J)+1$. The ellipsoid method of §6 is not modelled.
• Runs. ALGORITHM 2 is a relation Alg2Run k g I P, witnessed by a trace. Every bound holds for every run: every admissible subroutine output, every packing at Steps 2 and 3 within the prescribed counts, every choice of pieces for the principal bins (which must fill every available slot), and every order of the Step 4 insertion. A separate well-definedness item states that a run exists, so the bounds are not vacuous.
• Explicit constants. $O(\log^2 OPT(I))$ in Theorem 4 is replaced by $(1+\log_2 OPT)(9 + 4\ln OPT) + 2 + 4\ln OPT$. The asymptotic threshold is made explicit as $SIZE(I) \ge 2$. $\ln$ is Real.log and $\log_2$ is Real.logb 2.
• Corrected statements. The last group of geometric grouping may fall short of $k$, which the paper ignores. For it, $\Delta G_q$ consists of the $\max(0, l_q - l_{q-1})$ smallest pieces. Theorem 2, item 4 is stated as $m(J) \le SIZE(J)/k + \ln(1/a(I)) + 1$; the printed version without $+1$ fails for $I = \{0.95, 0.95, 0.95, 0.9\}$, $k = 2$. Theorem 2 is stated for integers $k \ge 2$, which its proof needs. The iteration bound is stated for $t \ge 1$ and for the instance after Step 1.
• Out of scope. Running times, polynomiality, the function $T(m,n)$, the number of subroutine calls, §6, ALGORITHM 3 and Theorem 5.
• Ruling out trivial versions. "There exists a packing with at most $OPT(I) + \dots$ bins" is trivially true and is not the goal. The goal bounds every output of the algorithm, and the existence item shows that outputs exist.

Contributions welcome: milestone proofs; a harmonic-sum bound $\sum_{j=a}^{b} 1/j \le \ln\frac{b}{a-1}$; extreme-point facts for $\{x \ge 0 : Ax \ge b\}$ (at most as many nonzero coordinates as rows; an optimal extreme point exists), reusable beyond bin packing; monotonicity of $LIN$ and $OPT$ under the piecewise order.

Selected references

• N. Karmarkar, R. M. Karp, An Efficient Approximation Scheme for the One-Dimensional Bin-Packing Problem, Proc. 23rd Annual Symposium on Foundations of Computer Science (SFCS 1982), IEEE, pp. 312–320, 1982. https://doi.org/10.1109/SFCS.1982.61
• W. Fernandez de la Vega, G. S. Lueker, Bin packing can be solved within 1 + ε in linear time, Combinatorica 1(4), 349–355, 1981. https://doi.org/10.1007/BF02579456
• D. S. Johnson, A. Demers, J. D. Ullman, M. R. Garey, R. L. Graham, Worst-case performance bounds for simple one-dimensional packing algorithms, SIAM J. Comput. 3(4), 299–325, 1974. https://doi.org/10.1137/0203025
• R. Hoberg, T. Rothvoss, A Logarithmic Additive Integrality Gap for Bin Packing, Proc. 28th ACM-SIAM SODA, 2616–2625, 2017. https://doi.org/10.1137/1.9781611974782.172

Motivation

Algorithmic mechanism design asks for algorithms whose inputs are held by self-interested parties. Each party reports its private data, the algorithm computes an outcome, and payments are arranged so that no party gains by misreporting. Nisan and Ronen introduced the field in Algorithmic Mechanism Design (Games Econ. Behav. 35, 2001). Their running example is task scheduling on unrelated machines: $k$ tasks are distributed among $n$ machines owned by different agents, each agent knows only its own processing times, and the designer wants to minimize the make-span.

Without incentives the problem is classical: minimizing make-span on unrelated machines is NP-hard and admits a polynomial 2-approximation (Lenstra, Shmoys, Tardos, 1990). With selfish agents the question changes: which approximation ratios can a truthful mechanism guarantee? This mission formalizes the paper's upper bound, the MinWork mechanism, which is the benchmark every later lower bound for truthful scheduling is compared with.

Timeline.

• 1961: Vickrey introduces the second-price auction (J. Finance 16).
• 1971–1973: Clarke and Groves generalize it to the VCG family of truthful mechanisms for utilitarian objectives (Groves, Econometrica 41, 1973).
• 1999/2001: Nisan and Ronen show MinWork is a strongly truthful $n$-approximation, and that no truthful mechanism beats ratio 2.
• 2007: Christodoulou, Koutsoupias and Vidali raise the deterministic lower bound to $1+\sqrt2$ for $n \ge 3$; Koutsoupias and Vidali later raise it to $1+\varphi \approx 2.618$.
• 2023: Christodoulou, Koutsoupias and Kovács prove the Nisan–Ronen conjecture: no deterministic truthful mechanism achieves a ratio below $n$ (STOC 2023, arXiv:2301.11905), so MinWork is optimal among deterministic truthful mechanisms.

Setting

There are $n$ agents and $k$ tasks. Agent $i$'s type is the vector $t^i = (t^i_1,\dots,t^i_k)$ of positive times, $t^i_j > 0$ being the time agent $i$ needs to perform task $j$. A type vector is $t = (t^1,\dots,t^n)$. An allocation $x$ sends each task $j$ to one agent; $x^i$ is the set of tasks agent $i$ receives. The make-span of $x$ is

$$g(x,t) = \max_{i} \sum_{j \in x^i} t^i_j ,$$

and agent $i$'s valuation is $v^i(x,t^i) = -\sum_{j \in x^i} t^i_j$.

A direct mechanism asks every agent to declare a type, computes an allocation $x(d)$ from the declared vector $d$, and hands agent $i$ a payment $p^i(d)$. Agent $i$'s utility is $p^i(d) + v^i(x(d), t^i)$, with $t^i$ its true type. The mechanism is truthful if declaring $t^i$ maximizes agent $i$'s utility for every declaration of the others, and strongly truthful if truth-telling is the only such dominant strategy. An allocation rule is a $c$-approximation if $g(x(t),t) \le c \cdot g(y,t)$ for every type vector $t$ and every allocation $y$.

The MinWork mechanism allocates each task to an agent with minimal declared time for it, breaking ties arbitrarily. For each task it wins, an agent receives the second-best declared time $\min_{i' \ne i} d^{i'}_j$:

$$p^i(d) = \sum_{j \in x^i(d)} \min_{i' \neq i} d^{i'}_j .$$

The Lean development uses the same names: load, makespan, IsTruthful, IsStronglyTruthful, IsApprox, IsMinWorkAlloc, secondBest, minTime, minWorkPay.

Formalization targets

Goal: Theorem 4.1

For $n \ge 2$ and every MinWork allocation rule $x$ with payments $p$ as above,

$$(x,p)\ \text{is strongly truthful} \quad\text{and}\quad g(x(t),t) \le n \cdot g(y,t)\ \ \text{for all positive } t \text{ and all allocations } y .$$

Milestones

1. Theorem 3.1 (Groves): a VGC mechanism is truthful. This is an existing platform theorem, used as a reference.
2. MinWork belongs to the VGC family. Its allocation maximizes $\sum_i v^i(t^i,x)$, and its payment is $\sum_{i'\ne i} v^{i'}(t^{i'},x(t)) + h^{-i}$ with $h^{-i} = \sum_j \min_{i'\ne i} t^{i'}_j$.
3. Claim 4.2: MinWork is strongly truthful.
4. $g(x(t),t) \le \sum_{j} \min_i t^i_j$.
5. $g(y,t) \ge \frac1n \sum_j \min_i t^i_j$ for every allocation $y$.
6. Claim 4.3: MinWork is an $n$-approximation.

Significance

The theorem gives the first positive result for truthful scheduling: a mechanism that is truthful in the strongest sense and is within a factor $n$ of optimal, whatever the tie-breaking rule. Every lower bound in the paper (Theorems 4.6, 4.10 and 4.12) and in the later literature measures itself against this ratio. Since the 2023 resolution of the Nisan–Ronen conjecture, the ratio $n$ is known to be tight for deterministic truthful mechanisms.

The result is proved in the paper; it is not known to be formalized in any proof assistant. The platform already has Groves' theorem in an abstract form (AGT.vcg_incentive_compatible). This mission connects that abstract statement to a concrete combinatorial mechanism, and it adds the strict part of strong truthfulness for any number of tasks and agents, which the paper proves only for one task and two agents. The vocabulary (make-span over unrelated machines, direct scheduling mechanisms, strong truthfulness) is shared with the seven later missions of this series.

Difficulty

Truthfulness follows from Groves' theorem once MinWork is identified as a VGC mechanism. The identification requires the payment identity at every declared vector and under every tie-breaking rule, including ties at the winning time. The main difficulty is the strict part of strong truthfulness. A misreport that differs from the truth only on one task must still be shown to lose strictly for some declarations of the others. Those declarations must stay positive, and on every other task they must leave the outcome unchanged. The paper's proof covers only one task and two agents and leaves the general case as "similar". Its printed inequality also has the two utilities in the wrong order (see below), so it cannot be transcribed directly.

Formalization scope

• Agents are Fin n and tasks are Fin k. An allocation is a function Fin k → Fin n, and an agent may receive no task. Types are positive reals, and every truthfulness and approximation quantifier ranges over positive true types, positive misreports and positive declarations of the others.
• Payments are handed to the agent, so utility is the payment minus the true time spent. Payments are computed from the declared vector, never from true types.
• The allocation rule is a parameter satisfying the MinWork specification (IsMinWorkAlloc). Every result holds for every tie-breaking rule, including rules that depend on the whole declared vector. No particular argmin is fixed.
• $n \ge 2$ is a hypothesis of the goal and of the truthfulness items: with a single agent the paper's second-best minimum is undefined. The approximation items need only $n \ge 1$. There is no hypothesis on $k$.
• The make-span and both minima are Finset.sup' / Finset.inf' over nonempty finite sets, so they are true maxima and minima with no default values.
• Strong truthfulness is formalized as truthfulness plus: every misreport $d^i \ne t^i$ is strictly worse than the truth for some positive declarations of the others. Given truthfulness this is equivalent to Definition 5. A formalization that states only that truth-telling is dominant, or proves strictness only for single-task instances, does not meet the goal. Neither does an existential ratio in place of $n$.
• Printed slip: in the proof of Claim 4.2 (p. 177) the case $d^i > t^i$ reads "the utility for agent $i$ is $t^i - d^i < 0$, instead of 0 in the case of truth-telling". With the Definition 11 payments the misreporting agent loses the task (utility 0), and the truthful agent wins it with utility $d^{3-i} - t^i > 0$. The milestone text keeps the paper's words; the Lean statements assert what the argument establishes.
• Out of scope: running time ("polynomial time"), and the paper's general revelation-principle framework (Proposition 2.1).
• Welcome contributions: proofs of the milestones, and a reusable lemma connecting the local VGC milestone to AGT.vcg_incentive_compatible.

Selected references

• N. Nisan, A. Ronen, Algorithmic Mechanism Design, Games and Economic Behavior 35 (2001) 166–196. https://doi.org/10.1006/game.1999.0790
• T. Groves, Incentives in Teams, Econometrica 41 (1973) 617–631. https://doi.org/10.2307/1914085
• W. Vickrey, Counterspeculation, Auctions, and Competitive Sealed Tenders, Journal of Finance 16 (1961) 8–37. https://doi.org/10.1111/j.1540-6261.1961.tb02789.x
• J. K. Lenstra, D. B. Shmoys, É. Tardos, Approximation algorithms for scheduling unrelated parallel machines, Mathematical Programming 46 (1990) 259–271. https://doi.org/10.1007/BF01585745
• G. Christodoulou, E. Koutsoupias, A. Kovács, A Proof of the Nisan-Ronen Conjecture, STOC 2023. https://arxiv.org/abs/2301.11905

Motivation

Column generation solves linear programs with far too many variables to list: one works with a small subset $J' \subseteq J$ of the columns, the restricted master problem (RMP), and adds columns of negative reduced cost as a pricing problem finds them (Lübbecke and Desrosiers 2005, §2.1). Many integer programs from vehicle routing, crew scheduling and crew pairing are reformulated so that the master problem is a set-partitioning problem: every row (a customer, a flight leg, a task) must be covered by exactly one selected column (a route, a pairing, a schedule). The linear relaxation of such a master is solved by column generation, and an integer solution is then sought by branch-and-price, branch-and-bound with column generation at every node.

Branching in branch-and-price is not free. Fixing a master variable $\lambda_j$ to $0$ does not stop the pricing problem from regenerating the same column, and handling that complicates the pricing problem. The rule that avoids this for set partitioning goes back to Ryan and Foster (1981): branch on a pair of rows, requiring them to be covered either by the same column or by two different columns. Both requirements are constraints the pricing problem can respect directly. Lübbecke and Desrosiers call it "the most common scheme in conjunction with column generation" (§7.3, p. 1020) and state the proposition that makes it well defined as their Proposition 3.

Timeline:

• 1981: Ryan and Foster introduce the pair-of-rows branching rule for set partitioning in crew scheduling.
• 1998: the branch-and-price survey of Barnhart et al. (1998) presents the rule as the branching scheme for set-partitioning masters.
• 2005: Lübbecke and Desrosiers state it as Proposition 3 of their survey, attributing it to Ryan and Foster without proof.

Setting

Rows are indexed by $\{1, \dots, m\}$ and columns by a finite set $J'$. A matrix $A = (a_{rj}) \in \{0,1\}^{m \times |J'|}$ has every entry equal to $0$ or $1$; column $j$ covers row $r$ when $a_{rj} = 1$. The set-partitioning system of the RMP's linear relaxation is

$$A\lambda = \mathbf 1, \qquad \lambda \ge \mathbf 0, \qquad \lambda \in \mathbb R^{J'} .$$

A vector $\lambda$ is a basic feasible solution of this system when it satisfies all its constraints and, among the constraints active at $\lambda$ (the $m$ equality rows, and the constraints $\lambda_j \ge 0$ with $\lambda_j = 0$), there are $|J'|$ linearly independent ones. Equivalently, $\lambda$ is feasible and the columns of $A$ in the support of $\lambda$ are linearly independent. A solution is fractional when it is not a $0/1$ vector, $\lambda \notin \{0,1\}^{|J'|}$.

For two rows $r, s$ the Ryan–Foster quantity is $\sum_{j \in J'} a_{rj} a_{sj} \lambda_j$, written pairCover A lam r s in Lean: the total weight on the columns that cover both rows. For $r = s$ it is the row sum, equal to $1$ on every feasible $\lambda$.

Formalization targets

Goal: Proposition 3 (p. 1020)

For every $0/1$ matrix $A$ and every fractional basic feasible solution $\lambda$ of $A\lambda = \mathbf 1$, $\lambda \ge \mathbf 0$,

$$\exists\, r, s \in \{1, \dots, m\}: \qquad 0 < \sum_{j \in J'} a_{rj}\, a_{sj}\, \lambda_j < 1 .$$

The two rows are automatically distinct. The statement concerns every fractional basic solution, not only an optimal one, and no cost vector enters it.

Milestone: the branches keep every integer solution (§7.3, p. 1020)

For every $0/1$ solution $\lambda \in \{0,1\}^{|J'|}$ of $A\lambda = \mathbf 1$ and every pair of rows $r, s$,

$$\sum_{j \in J'} a_{rj}\, a_{sj}\, \lambda_j \in \{0, 1\} .$$

This is the paper's requirement that "integer solutions remain intact" (p. 1019), specialised to the two branches "$= 1$" and "$= 0$" of the paragraph after Proposition 3.

Significance

Proposition 3 is what makes Ryan–Foster branching a valid branching scheme in the sense of §7.3: the current fractional solution violates both branches for the chosen pair, so it is excluded from both children, while by the milestone every integer solution survives in one of them. The same pair-of-rows idea underlies branching in bin packing, graph colouring, vehicle routing and crew scheduling codes, where it is used because both branches translate into constraints on the pricing problem rather than on individual master variables.

The paper states the result and refers its proof to Ryan and Foster (1981); no machine-checked version of the proposition is known. This mission produces a formal statement tied to a standard, representation-aware definition of basic solutions (Bertsimas–Tsitsiklis Definition 2.9, already on the platform) and, once proved, a verified lemma that any formal development of branch-and-price for set partitioning can cite.

Difficulty

An argument that uses only feasibility and a fractional coordinate cannot work. Without basicness the claim is false: with one row and two identical columns, $A = [1\ 1]$, the vector $\lambda = (\tfrac12, \tfrac12)$ is feasible and fractional, yet the only pair of rows is $r = s$, whose quantity is $1$. The difficulty is to turn basicness, a linear-algebra condition, into a combinatorial statement about which rows the fractional columns cover. A set-partitioning matrix need not have full row rank, so the familiar description of basic solutions through an invertible basis matrix is not available in general.

Formalization scope

• Rows are Fin m and columns Fin n, so $J'$ is identified with $\{0, \dots, n-1\}$. $A$ is a real matrix Matrix (Fin m) (Fin n) ℝ with the hypothesis IsZeroOneMatrix A (every entry $0$ or $1$); $\lambda$ is lam : Fin n → ℝ, since λ is a Lean keyword. Columns are $0/1$ vectors; the equivalent reading as subsets of the rows is only prose.
• "Basic solution" is not defined in the paper. It is read as Bertsimas–Tsitsiklis Definition 2.9 for the standard-form constraint family: LinearOptimization.IsBasicFeasibleSolution (LinearOptimization.stdFormSystem A (fun _ => 1)) lam, from the platform definitions BasicSolution and ActiveConstraints. This definition needs no full-row-rank assumption, which a set-partitioning matrix need not satisfy, and it is not replaced by an ad hoc support condition.
• Typo correction. The paper writes "i.e., $\lambda \notin \{0,1\}^m$". Since $\lambda$ has one coordinate per column, the statement reads it as $\lambda \notin \{0,1\}^{|J'|}$: ¬ IsZeroOneVector lam.
• The rows $r, s$ range over all of $\{1, \dots, m\}$, including $r = s$, as on the page; no distinctness is assumed or required.
• "Fractional basic solution" is any such solution, not the RMP optimum; no costs or optimality hypothesis enter.
• The milestone reads the paragraph after Proposition 3, together with the validity requirement "integer solutions remain intact" (p. 1019), as the dichotomy for all $0/1$ solutions of $A\lambda = \mathbf 1$. The sentence about transferring the branching information to the pricing problem is not formalized.
• Edge cases: for $m = 0$ basicness forces $\lambda = 0$, and for $n = 0$ the vector is empty; in both cases no fractional basic solution exists and the goal is vacuous, as on the page.
• A trivializing formalization is ruled out: dropping basicness makes the goal false (the $[1\ 1]$ example above), dropping the $0/1$ hypothesis on $A$ changes the meaning of the quantity, and replacing "fractional basic" by an unsatisfiable hypothesis would make it empty; the hypotheses are satisfied, for instance, by three rows, the columns $\{1,2\}, \{2,3\}, \{1,3\}$ and $\lambda = (\tfrac12, \tfrac12, \tfrac12)$.

A complete development needs linear-algebra facts about basic solutions of standard-form systems without a rank assumption (support columns linearly independent), which are reusable beyond this mission. Contributions welcome: that characterization as a lemma, and proofs of the milestone and of the goal.

Selected references

• M. E. Lübbecke and J. Desrosiers, Selected Topics in Column Generation, Operations Research 53(6):1007–1023, 2005. https://doi.org/10.1287/opre.1050.0234
• D. M. Ryan and B. A. Foster, An integer programming approach to scheduling, in A. Wren (ed.), Computer Scheduling of Public Transport, North-Holland, 1981, pp. 269–280.
• C. Barnhart, E. L. Johnson, G. L. Nemhauser, M. W. P. Savelsbergh and P. H. Vance, Branch-and-Price: Column Generation for Solving Huge Integer Programs, Operations Research 46(3):316–329, 1998. https://doi.org/10.1287/opre.46.3.316
• D. Bertsimas and J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Definition 2.9.

Motivation

Many optimization problems in engineering, simulation-based design and machine learning give access only to function values: the objective is the output of a simulator or a black-box program, and its gradient is unavailable or too expensive. Derivative-free (or zeroth-order) methods address this setting. Nesterov and Spokoiny (Found. Comput. Math. 17 (2017)) showed that a very simple oracle, the finite difference of $f$ along a random Gaussian direction, can replace the gradient in standard first-order schemes at the price of a factor depending only on the dimension. Their analysis became the reference point for later work on zeroth-order stochastic optimization and on gradient-free methods in reinforcement learning and adversarial attacks.

This mission covers Section 6 of the paper: the accelerated random method $\mathcal{FG}_\mu$ and its rate, Theorem 9. It is the third mission of a series; the first covers random search for nonsmooth problems (Theorem 6), the second the random gradient method for smooth problems (Theorem 8).

Setting

Let $E$ be a real inner product space of dimension $n \ge 2$ with norm $\|\cdot\|$ (the paper's space with operator $B$ is $E$ with the inner product $\langle Bx, y\rangle$). Let $u$ be a standard Gaussian vector in $E$, and write $\mathbb E_u$ for expectation over $u$.

The objective $f : E \to \mathbb R$ is differentiable with Lipschitz gradient, $\|\nabla f(x) - \nabla f(y)\| \le L_1\|x - y\|$ with $L_1 > 0$, and strongly convex with parameter $\tau \ge 0$:

$$f(y) \ge f(x) + \langle\nabla f(x), y - x\rangle + \tfrac{\tau}{2}\|y - x\|^2 .$$

The value $\tau = 0$ is allowed (plain convexity). The condition number is $\kappa = \tau/L_1$. The problem $f^* = \min_{x \in E} f(x)$ is assumed solvable, with minimizer $x^*$.

For $\mu \ge 0$ the Gaussian approximation is $f_\mu(x) = \mathbb E_u f(x + \mu u)$, and the random gradient-free oracle is

$$B^{-1}g_\mu(x) = \frac{f(x + \mu u) - f(x)}{\mu}\,u \quad (\mu > 0), \qquad B^{-1}g_0(x) = \langle\nabla f(x), u\rangle\,u .$$

The paper (p. 548) sets $\theta_n = 1/(16(n+1)^2L_1(f))$ and $h_n = 1/(4(n+4)L_1(f))$. This mission uses $\theta_n = 1/(16(n+4)^2L_1)$; the reason is given under Formalization scope. Method $\mathcal{FG}_\mu$ (Eq. (60)) chooses $x_0 \in E$, $v_0 = x_0$ and $\gamma_0 > 0$ with $\gamma_0 \ge \tau$, and at every iteration $k \ge 0$:

1. computes $\alpha_k > 0$ with $\theta_n^{-1}\alpha_k^2 = (1 - \alpha_k)\gamma_k + \alpha_k\tau \equiv \gamma_{k+1}$;
2. sets $\lambda_k = \alpha_k\tau/\gamma_{k+1}$, $\beta_k = \alpha_k\gamma_k/(\gamma_k + \alpha_k\tau)$ and $y_k = (1-\beta_k)x_k + \beta_k v_k$;
3. draws a fresh Gaussian direction $u_k$, independent of the past, and computes $g_\mu(y_k)$;
4. sets $x_{k+1} = y_k - h_n B^{-1}g_\mu(y_k)$ and $v_{k+1} = (1-\lambda_k)v_k + \lambda_k y_k - (\theta_n/\alpha_k)B^{-1}g_\mu(y_k)$.

Write $\phi_k = \mathbb E f(x_k)$ (expectation over $u_0, \dots, u_{k-1}$), $\psi_k = \prod_{i=0}^{k-1}(1-\alpha_i)$ and $C_k = 1 + \sum_{i=1}^{k-1}\prod_{j=k-i}^{k-1}(1-\alpha_j)$ for $k \ge 1$, with $\psi_0 = 1$ and $C_0 = 0$ (p. 550).

Formalization targets

Goal: Theorem 9 (p. 549)

For all $k \ge 0$,

$$\phi_k - f^* \le \psi_k\Big[f(x_0) - f(x^*) + \frac{\gamma_0}{2}\|x_0 - x^*\|^2\Big] + \mu^2 L_1\Big(n + \frac{3(n+8)}{16}C_k\Big), \tag{62}$$

where

$$\psi_k \le \min\Big\{\Big(1 - \frac{\kappa^{1/2}}{4(n+4)}\Big)^k,\ \Big(1 + \frac{k}{8(n+4)}\sqrt{\frac{\gamma_0}{L_1}}\Big)^{-2}\Big\}, \qquad C_k \le \min\Big\{k,\ \frac{4(n+4)}{\kappa^{1/2}}\Big\}.$$

The two regimes are a rate $O(n^2/k^2)$ for convex $f$ and a linear rate with ratio $1 - \kappa^{1/2}/(4(n+4))$ for strongly convex $f$, both up to a bias proportional to $\mu^2$.

Milestones

In attack order: Lemma 1 (Gaussian moments, (16)–(17)); Theorem 3.1 (the bound (32) on the second moment of $g_0$); Theorem 1's (19), $|f_\mu - f| \le \frac{\mu^2}{2}L_1 n$; Eq. (12), $L_1(f_\mu) \le L_1(f)$; Lemma 5, the bound (37) on $\mathbb E_u\|g_\mu(x)\|_*^2$ in terms of $\nabla f_\mu(x)$; Eq. (21), $\nabla f_\mu = \mathbb E_u g_\mu$; and Eq. (11), $f_\mu \ge f$ for convex $f$.

Significance

Theorem 9 shows that the $n$-fold slowdown of gradient-free methods relative to their gradient counterparts survives acceleration: $\mathcal{FG}_\mu$ reaches accuracy $\epsilon$ in $O(n L_1^{1/2}R/\epsilon^{1/2})$ iterations for convex $f$, against $O(nL_1R^2/\epsilon)$ for the non-accelerated random gradient method. The analysis also quantifies how small the finite-difference step $\mu$ must be for this to hold. The result is used as the baseline accelerated zeroth-order rate in later work.

The theorem is proved in the paper. As far as is known it has not been machine-checked, and Mathlib has no Gaussian smoothing, no random gradient-free oracle and no analysis of an accelerated method driven by random directions. A formal proof also settles the constant question raised by the printed $\theta_n$ (see below).

Difficulty

The deterministic fast gradient method is analysed by an estimate-sequence argument in which the gradient step is exact. Here the step uses $g_\mu(y_k)$, which is an unbiased estimate of $\nabla f_\mu(y_k)$ and not of $\nabla f(y_k)$, and whose second moment is of order $n\|\nabla f_\mu\|^2$ plus a bias term. The step size and the coupling parameter $\theta_n$ must absorb this second moment, and the argument must be run for $f_\mu$ rather than $f$. The estimate sequence then has to be passed through expectations over the history $u_0, \dots, u_{k-1}$, which requires the independence of $u_k$ from $x_k, v_k, y_k$ and integrability of every quantity involved. Transporting the result from $f_\mu$ back to $f$ uses (11) and (19), and requires that $f_\mu$ inherits strong convexity with the same parameter $\tau$, a fact the paper uses without stating it.

Formalization scope

$E$ is an arbitrary finite-dimensional real inner product space (InnerProductSpace ℝ E, FiniteDimensional ℝ E, Borel measurable), $n$ is Module.finrank ℝ E, and the Gaussian is Mathlib's stdGaussian E. The operator $B$ is absorbed into the inner product, so $\nabla f$ is gradient f and $B^{-1}g_\mu$ is $\frac{f(x+\mu u)-f(x)}{\mu}u$. This is not a restriction to $B = I$ on $\mathbb R^n$. All expectations are Bochner integrals; under the hypotheses every integrand is integrable, so no integrability hypothesis is added.

The run is a structure over a probability space $(\Omega, \mathbb P)$: directions $u_k$ that are measurable, mutually independent (iIndepFun) and standard Gaussian; deterministic sequences $\gamma, \alpha$ satisfying step a) as equations; and random points $x_k, v_k$ satisfying steps b)–d) for every outcome. The smoothing parameter satisfies $\mu \ge 0$, and at $\mu = 0$ the oracle is $g_0$. The goal pins $\theta = 1/(16(n+4)^2L_1)$ and $h = 1/(4(n+4)L_1)$. $\psi_k$ and $C_k$ are definitions computed from $\alpha$.

The constant $\theta_n$. The paper prints $\theta_n = \frac{1}{16(n+1)^2L_1(f)}$. The proof (pp. 549–550) needs $\frac{h_n}{4(n+4)} - \frac{h_n^2L_1}{2} = \frac{1}{32(n+4)^2L_1} = \frac{\theta_n}{2}$, $\alpha_k \ge [\tau\theta_n]^{1/2} = \frac{\kappa^{1/2}}{4(n+4)}$ and $\theta_n^{1/2} = \frac{1}{4(n+4)L_1^{1/2}}$, which hold only with $(n+4)$. With the printed value $\theta_n$ is larger than the first inequality allows, and the argument does not go through. The mission therefore states Theorem 9 with $\theta_n = \frac{1}{16(n+4)^2L_1}$; all other constants are as printed.

Two trivializing formalizations are ruled out. First, the bound $C_k \le 4(n+4)/\kappa^{1/2}$ carries the hypothesis $\tau > 0$: at $\tau = 0$ the paper's value is $+\infty$, while Lean's division by zero would turn it into $C_k \le 0$, which is false. $\psi_k$ and $C_k$ are definitions from the run, not free variables that only satisfy the bounds. Second, the oracle is the random finite difference along i.i.d. standard Gaussian directions, not the exact gradient (which would give Nesterov's deterministic method) and not an arbitrary direction sequence.

A complete development needs Gaussian integration by parts in an inner product space, moment bounds for $\|u\|$, differentiation under the integral sign for $f_\mu$, and conditional expectation along an i.i.d. sequence. The smoothing layer (Lemma 1, (11), (12), (19), (21), (32), (37)) is reusable for any zeroth-order method, and contributions of these components as separate lemmas are welcome.

Selected references

• Yu. Nesterov, V. Spokoiny, Random Gradient-Free Minimization of Convex Functions, Foundations of Computational Mathematics 17(2):527–566, 2017. https://doi.org/10.1007/s10208-015-9296-2
• Yu. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004 (Lemma 2.2.4 and Section 2.2.1, the estimate-sequence analysis the proof of Theorem 9 follows). https://doi.org/10.1007/978-1-4419-8853-9

Motivation

Many optimization problems in engineering, simulation-based design and machine learning give access to the objective only through its values: the function is computed by a black-box code, and derivatives are unavailable or too expensive to program. Zeroth-order (derivative-free) methods address this setting. Classical derivative-free methods (pattern search, Nelder–Mead, model-based trust regions) come with weak or no global complexity guarantees for convex problems.

Nesterov and Spokoiny (Found. Comput. Math. 17 (2017) 527–566) showed that replacing the gradient by a finite difference along a random Gaussian direction yields methods whose expected complexity is that of the corresponding gradient method multiplied by a factor proportional to the dimension. Their paper is a standard reference for zeroth-order convex optimization and for Gaussian smoothing, and its oracle and analysis are reused in bandit convex optimization, zeroth-order stochastic optimization (e.g. Ghadimi–Lan 2013) and derivative-free reinforcement learning.

This mission concerns Section 5 of the paper: the random gradient method $\mathcal{RG}_\mu$ for smooth convex functions and its linear rate for strongly convex ones.

Setting

Let $E$ be a real inner product space of finite dimension $n$, with norm $\|\cdot\|$. (The paper works with a space carrying an operator $B = B^* \succ 0$ and norm $\|x\| = \langle Bx, x\rangle^{1/2}$; choosing $\langle B\cdot,\cdot\rangle$ as the inner product gives exactly this setting, and the dual norm $\|\cdot\|_*$ becomes the norm of the Riesz representative.)

A function $f : E \to \mathbb R$ belongs to $C^{1,1}(E)$ with constant $L_1$ if it is differentiable and $\|\nabla f(x) - \nabla f(y)\| \le L_1\|x - y\|$ for all $x, y$. It is strongly convex with parameter $\tau > 0$ if $f(y) \ge f(x) + \langle \nabla f(x), y - x\rangle + \frac{\tau}{2}\|y-x\|^2$ for all $x, y$.

Let $u$ be a standard Gaussian vector of $E$ (coordinates in any orthonormal basis are independent $N(0,1)$). The Gaussian approximation of $f$ with parameter $\mu \ge 0$ is $f_\mu(x) = \mathbb E_u f(x + \mu u)$, and the moments are $M_p = \mathbb E_u\|u\|^p$. The random gradient-free oracle returns, for a sampled direction $u$,

$$B^{-1}g_\mu(x) = \frac{f(x+\mu u) - f(x)}{\mu}\, u \quad (\mu > 0), \qquad B^{-1}g_0(x) = f'(x,u)\, u,$$

and the symmetric oracle is $B^{-1}\hat g_\mu(x) = \frac{f(x+\mu u) - f(x - \mu u)}{2\mu}u$.

Consider $f^* = \min_{x\in E} f(x)$ for a convex $f \in C^{1,1}(E)$, assumed solvable with a minimizer $x^*$, and $n \ge 2$. The random gradient method $\mathcal{RG}_\mu$ (Eq. (54), p. 546) is:

Method $\mathcal{RG}_\mu$: Choose $x_0 \in E$. Iteration $k \ge 0$. a). Generate $u_k$ and corresponding $g_\mu(x_k)$. b). Compute $x_{k+1} = x_k - hB^{-1}g_\mu(x_k)$.

The directions $u_0, u_1, \dots$ are independent standard Gaussian vectors, and $\phi_k = \mathbb E f(x_k)$ (with $\phi_0 = f(x_0)$).

Formalization targets

Goal: Theorem 8 (p. 546)

With step size $h = \frac{1}{4(n+4)L_1}$ and any $\mu \ge 0$, for every $N \ge 0$,

$$\frac{1}{N+1}\sum_{k=0}^{N}(\phi_k - f^*) \le \frac{4(n+4)L_1\|x_0-x^*\|^2}{N+1} + \frac{9\mu^2(n+4)^2L_1}{25},$$

and, if $f$ is strongly convex with parameter $\tau > 0$, then with $\delta_\mu = \frac{18\mu^2(n+4)^2}{25\tau}L_1$,

$$\phi_N - f^* \le \frac12 L_1\left[\delta_\mu + \left(1 - \frac{\tau}{8(n+4)L_1}\right)^{N}\big(\|x_0-x^*\|^2 - \delta_\mu\big)\right].$$

Both bounds are one theorem with one proof in the paper, so the goal states their conjunction, with every constant as printed.

Milestones

The milestones are the results the paper's proof of Theorem 8 rests on, in attack order:

1. Lemma 1 (p. 534): $M_p \le n^{p/2}$ for $p \in [0,2]$ and $n^{p/2} \le M_p \le (p+n)^{p/2}$ for $p \ge 2$.
2. Theorem 3.1, (32) (p. 537): $\mathbb E_u\|g_0(x)\|_*^2 \le (n+4)\|\nabla f(x)\|_*^2$ at a point of differentiability.
3. Theorem 4.2, (35) (p. 538): $\mathbb E_u\|g_\mu(x)\|_*^2 \le \frac{\mu^2}{2}L_1^2(n+6)^3 + 2(n+4)\|\nabla f(x)\|_*^2$, and the same with $\frac{\mu^2}{8}$ for $\hat g_\mu$.
4. Eq. (21) (pp. 534–535): for $\mu > 0$, $f_\mu$ is differentiable with $\nabla f_\mu(x) = \mathbb E_u B^{-1}g_\mu(x)$.
5. Eq. (25) (p. 535): $\mathbb E_u \langle\nabla f(x), u\rangle u = \nabla f(x)$, the $\mu = 0$ counterpart.
6. Convexity of $f_\mu$ (p. 533) and Eq. (11): $f \le f_\mu$ for convex $f$.
7. Theorem 1, (19) (p. 534): $|f_\mu(x) - f(x)| \le \frac{\mu^2}{2}L_1 n$.

Significance

The result. Theorem 8 shows that a method using two function values per iteration reaches accuracy $\epsilon$ on a smooth convex problem in $O(\frac{n}{\epsilon}L_1\|x_0 - x^*\|^2)$ iterations, and in $O(\frac{nL_1}{\tau}\ln\frac{L_1\|x_0-x^*\|^2}{\epsilon})$ iterations under strong convexity, provided $\mu$ is small enough. This is $n$ times the complexity of the deterministic gradient method, which is the natural price for replacing an $n$-dimensional gradient by one directional estimate. The strongly convex bound makes explicit the bias floor $\frac12 L_1\delta_\mu$ caused by the finite-difference step, and shows that it vanishes for the limiting method $\mathcal{RG}_0$.

Formalizing it. The result is proved in the paper; nothing here is open. To our knowledge none of it has a machine-checked proof. A formalization produces a reusable Gaussian-smoothing layer on Mathlib's stdGaussian (moments of the Gaussian norm, differentiation of $f_\mu$ under the integral, variance bounds of random oracles) and a complete expected-complexity proof of a randomized first-order method, in which the probabilistic structure (independent directions, iterates depending only on past directions, tower property) has to be handled explicitly.

Difficulty

The deterministic part of the argument is the textbook analysis of gradient descent. The difficulty is in the Gaussian facts it uses. The obvious bound on the oracle's second moment, $\mathbb E\langle\nabla f(x),u\rangle^2\|u\|^2 \le \|\nabla f(x)\|^2 M_4 \le (n+4)^2\|\nabla f(x)\|^2$, loses a factor of $n$ and would give a quadratic dependence on dimension; the $(n+4)$ of (32) needs a sharper computation. The moment bounds of Lemma 1 for non-integer $p$ and the differentiation under the integral in (21) are measure-theoretic steps that Mathlib does not package. Finally, the step from per-iteration inequalities to bounds on $\phi_k$ requires conditioning on the past directions, which must be set up on a probability space carrying the whole sequence $u_0, u_1, \dots$.

Formalization scope

$E$ is an arbitrary finite-dimensional real inner product space with MeasurableSpace and BorelSpace, $n$ is Module.finrank ℝ E, and $\nabla f$ is Mathlib's gradient. Expectations over $u$ are Bochner integrals against ProbabilityTheory.stdGaussian E. A run of $\mathcal{RG}_\mu$ lives on a probability space $(\Omega, P)$: measurable directions $u_k$, jointly independent (iIndepFun) with law stdGaussian E, iterates with $x_0$ deterministic and the update holding for every $k$ and outcome. $\phi_k$ is ∫ ω, f (x k ω) ∂P. The oracle is defined by cases, with $f'(x,u)u$ at $\mu = 0$ ($f'(x,u)$ the one-sided directional derivative of Eq. (23), a Filter.limUnder, which equals fderiv ℝ f x u for differentiable $f$), so the goal covers every $\mu \ge 0$ as the paper claims. $L_1$ and $\tau$ are any constants satisfying the defining inequalities. The standing assumptions of Section 5 (convexity, a global minimizer $x^*$, $n \ge 2$) and $L_1 > 0$ are explicit hypotheses; $n \ge 2$ is needed for the constant $9/25$.

A trivializing formalization is ruled out: the oracle is the random finite difference along i.i.d. standard Gaussian directions, not the true gradient (which would be deterministic gradient descent), and every expectation in the statements is of a quantity that is integrable under the stated hypotheses, so no bound holds through a junk value of a non-integrable integral.

A complete development needs Gaussian moment computations in finite dimension, differentiation under the integral sign for $f_\mu$, the variance bounds of the oracles, and a conditional-expectation argument for the iteration. The smoothing layer is reusable for the companion missions on random search for nonsmooth problems and on the accelerated random method, and for other zeroth-order methods. Contributions of any of the milestones, of general Gaussian-integrability lemmas, or of alternative proofs are welcome.

Selected references

• Yu. Nesterov, V. Spokoiny, Random Gradient-Free Minimization of Convex Functions, Foundations of Computational Mathematics 17(2):527–566, 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):2341–2368, 2013. https://doi.org/10.1137/120880811
• Yu. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9

Motivation

Many optimization problems in engineering, simulation-based design and machine learning give access to the values of an objective function but not to its gradient: the function is computed by a black-box program, by a simulator, or by a model whose derivatives are unavailable or too expensive. Zeroth-order (or derivative-free) methods use only function values. Classical direct-search methods of this kind usually come without complexity bounds.

Nesterov and Spokoiny (Found. Comput. Math. 17 (2017) 527–566) showed that a very simple randomized scheme has explicit, dimension-dependent worst-case complexity bounds. The idea is to replace the gradient by a finite difference of $f$ along a random Gaussian direction. The resulting oracle is an unbiased estimate of the gradient of a smoothed version of $f$. Their analysis is the reference point for the later literature on zeroth-order stochastic optimization, bandit convex optimization and gradient-free training.

This mission covers the paper's result for nonsmooth convex problems over a closed convex set: the projected random search method $\mathcal{RS}_\mu$ and its convergence bound, Theorem 6.

Setting

Let $E$ be a real inner product space of finite dimension $n$, with norm $\|\cdot\|$. (The paper works with a space carrying a positive definite operator $B$ and the norm $\langle Bx, x\rangle^{1/2}$. This is the same thing as an arbitrary finite-dimensional inner product space, with $B$ encoding the inner product, and the development is written in that generality.)

A function $f : E \to \mathbb R$ is Lipschitz continuous with constant $L_0 \ge 0$ if $|f(x) - f(y)| \le L_0 \|x - y\|$ for all $x, y$. The paper calls this class $C^{0,0}(E)$ and writes $L_0(f)$ for the constant.

Let $u$ be a standard Gaussian vector in $E$: its coordinates in any orthonormal basis are independent $N(0,1)$ variables. For $\mu \ge 0$ the Gaussian smoothing of $f$ is

$$f_\mu(x) = \mathbb E_u\, f(x + \mu u),$$

and the Gaussian moments are $M_p = \mathbb E_u \|u\|^p$.

For $\mu > 0$ the random gradient-free oracle at $x$ draws $u$ and returns the vector

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

It costs two function values.

The problem is

$$f^* = \min_{x \in Q} f(x),$$

where $Q \subseteq E$ is closed and convex, $f$ is convex and Lipschitz, and $x^* \in Q$ is a minimizer. With $\pi_Q$ the Euclidean projection onto $Q$, positive steps $h_0, h_1, \ldots$ and a starting point $x_0 \in Q$, the random search method $\mathcal{RS}_\mu$ iterates

$$x_{k+1} = \pi_Q\big(x_k - h_k\, g_\mu(x_k)\big),$$

drawing a fresh independent Gaussian direction $u_k$ at every iteration. The iterates are random. Write $\phi_k = \mathbb E f(x_k)$ and $S_N = \sum_{k=0}^N h_k$.

Formalization targets

Goal: Theorem 6

For every $N \ge 0$,

$$\frac{1}{S_N}\sum_{k=0}^{N} h_k(\phi_k - f^*) \le \mu L_0\, n^{1/2} + \frac{1}{S_N}\left[\frac12\|x_0 - x^*\|^2 + \frac{(n+4)^2}{2} L_0^2 \sum_{k=0}^{N} h_k^2\right].$$

The step sizes, the smoothing parameter and the horizon are left free, so every step-size rule in the paper follows from this one inequality. The constants are the paper's.

Milestones

The facts about smoothing and the oracle on which the goal rests, in the paper's order:

1. Lemma 1: $M_p \le n^{p/2}$ for $p \in [0,2]$ and $n^{p/2} \le M_p \le (p+n)^{p/2}$ for $p \ge 2$.
2. Theorem 1 (18): $|f_\mu(x) - f(x)| \le \mu L_0 n^{1/2}$.
3. Convexity of $f_\mu$ for convex $f$.
4. Eq. (11): $f_\mu \ge f$ for convex $f$.
5. Eq. (21): $\nabla f_\mu(x) = \mathbb E_u\, g_\mu(x)$ for $\mu > 0$.
6. Theorem 4.1 (34): $\mathbb E_u \|g_\mu(x)\|^2 \le L_0^2 (n+4)^2$.
7. Theorem 2 ($\mu \ge 0$): $f(y) \ge f(x) - \mu L_0 n^{1/2} + \langle \nabla f_\mu(x), y - x\rangle$ for all $y$, where at $\mu = 0$ the vector is the limiting $\nabla f_0(x) = \mathbb E_u[f'(x,u)\,u]$ of Eq. (24).

Significance

Theorem 6 shows that a method using only function values, with no subgradient, solves nonsmooth convex problems with the classical projected-subgradient guarantee. Two things change: $L_0^2$ is multiplied by $(n+4)^2$, and a bias $\mu L_0 n^{1/2}$ appears, which can be made as small as desired. With suitable $\mu$, $h_k$ and $N$ an $\epsilon$-accurate expected value is reached in $O(n^2 L_0^2 R^2/\epsilon^2)$ oracle calls. The factor $n^2$ quantifies the cost of not having gradients. The same analysis carries over to stochastic objectives (the paper's Theorem 7).

The results are proved in the paper. As far as is known, none of them has a machine-checked proof. The mission produces a Lean development of Gaussian smoothing on an arbitrary finite-dimensional inner product space: the moment bounds, the approximation, convexity and gradient identities, and the oracle variance bound. On top of it sits the full convergence theorem for a randomized projected method, stated for the actual random process rather than for an idealized expectation recursion. The smoothing layer is reusable: the same facts underlie the smooth and accelerated random methods of the same paper and most Gaussian-smoothing analyses in zeroth-order optimization.

Difficulty

A plain subgradient analysis does not apply. The vector $g_\mu(x_k)$ is not a subgradient of $f$, nor an unbiased estimate of one. It is an unbiased estimate of the gradient of a different function, $f_\mu$, and its second moment grows with the dimension. The argument therefore has to move between $f$ and $f_\mu$ at exactly the right places, using properties of $f_\mu$ that hold for every nonsmooth Lipschitz $f$.

Those properties are genuinely analytic. Differentiating $f_\mu$ requires differentiating a Gaussian integral of a function that need not be differentiable. The moment bounds need estimates of $\mathbb E\|u\|^p$ for real $p$. In the probabilistic part, $x_k$ depends on $u_0, \ldots, u_{k-1}$, and each one-step estimate has to be integrated using the independence of $u_k$ from the past. Mathlib provides the standard Gaussian measure and independence, but no Gaussian smoothing, no projection onto convex sets and no conditional-expectation argument for this kind of recursion.

Formalization scope

The space is E with [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E], and $n$ is Module.finrank ℝ E. No lower bound on $n$ is assumed. The Gaussian is ProbabilityTheory.stdGaussian E, and expectations are Bochner integrals against it. $f_\mu$ is the definition smoothing, $M_p$ is moment (with real exponent Real.rpow), and $g_\mu$ is oracle.

The projection is the relation IsMetricProjection Q y z ($z \in Q$ and $z$ is a nearest point of $Q$ to $y$). The run is the predicate IsRandomSearchRun: directions $u_k : \Omega \to E$ on a probability space $(\Omega, P)$, measurable, mutually independent (iIndepFun) and each with law stdGaussian E; a deterministic $x_0 \in Q$; and the update above for every $k$ and every outcome.

$\phi_k$ is $\int f(x_k)\,dP$. The Lipschitz constant $L_0 \ge 0$ is any constant satisfying the Lipschitz inequality. It is an explicit hypothesis, because the paper's bound uses $L_0(f)$, which presupposes $f \in C^{0,0}(E)$. The smoothing parameter satisfies $\mu > 0$ and every step satisfies $h_k > 0$.

Two trivializing formalizations are ruled out. First, an expectation of a non-integrable function would be $0$ as a Bochner integral; Lipschitz continuity of $f$ makes every expectation in the mission integrable, and no statement relies on the junk value. Second, a run whose directions are not independent standard Gaussians, or whose update uses a subgradient instead of the finite difference, is a different theorem (the projected subgradient method). The run predicate fixes the paper's process exactly. A run exists for every closed $Q$ containing $x_0$ (on the countable product of Gaussians), so the goal is not vacuous.

A complete development needs:

• Gaussian integration by parts, or differentiation under the integral, for Lipschitz integrands;
• moment estimates for the standard Gaussian norm;
• existence and nonexpansiveness of projections onto closed convex sets;
• an expectation argument for the random recursion.

The smoothing lemmas, the moment bounds and the projection facts are reusable beyond this mission. Contributions are welcome at every level: proofs of the milestones, general lemmas about stdGaussian and projections, and alternative proofs of Lemma 1 (for example through the chi distribution).

Selected references

• Yu. Nesterov, V. Spokoiny, Random Gradient-Free Minimization of Convex Functions, Foundations of Computational Mathematics 17(2):527–566, 2017. https://doi.org/10.1007/s10208-015-9296-2
• Yu. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9
• A. D. Flaxman, A. T. Kalai, H. B. McMahan, Online convex optimization in the bandit setting: gradient descent without a gradient, SODA 2005. https://arxiv.org/abs/cs/0408007
• J. C. Duchi, M. I. Jordan, M. J. Wainwright, A. Wibisono, Optimal rates for zero-order convex optimization: the power of two function evaluations, IEEE Trans. Inf. Theory 61(5):2788–2806, 2015. https://arxiv.org/abs/1312.2139