Source-linked AI summary
A Constant-Competitive Algorithm for Dynamic Mixture-of-Experts Serving
Ian D'Ambrosio
TL;DR
Dynamic Mixture-of-Experts serving has an open randomized competitive-ratio order for its integral primal problem. This paper reduces reciprocal service costs to positive-body chasing and proves a constant randomized ratio, with a machine-checked Lean 4 proof.
Problem
The randomized competitive ratio for the integral primal problem remained open because the prior lower-bound construction applied only to an auxiliary dual.
Method
The paper uses finite tangent approximations, geometrically shrinking positive resets, and balanced projection to reduce reciprocal service costs to positive-body chasing with covering sparsity two.
Results
E[ALG] ≤ 10CPB · OPT + (5CPB + 2)k + 16, yielding CRrand(k) = Θ(1) with a multiplicative constant independent of m, k, and the horizon.
Takeaways & Limitations
The asymptotic randomized integral competitive ratio is constant for arbitrary numbers of experts under the fixed-sequence convention.
Takeaways & Limitations
The theorem does not determine the best numerical constant, deterministic integral ratio, or ratio against an adaptive adversary.
Abstract
from arXiv · showhide
Huang, Lou, and Xiao introduced Dynamic Mixture-of-Experts Serving and gave an O(sqrt(log k))-competitive randomized algorithm for its integral primal problem, where k is the number of replica GPUs beyond the mandatory copy of each expert. Their matching lower barrier applies to an auxiliary dual and leaves the primal order open. We prove that the randomized primal competitive ratio is in fact Theta(1) for arbitrary numbers of experts. The upper bound reduces reciprocal-max service costs to chasing positive bodies with covering row sparsity two. A finite tangent envelope approximates each reciprocal epigraph within a constant factor, summable positive resets convert accumulated service into movement, and a nonexpansive balanced projection removes the positive-body algorithm's resource augmentation. Combining the resulting fractional path with Lazy Threshold Rounding gives E[ALG] <= 10 C_PB OPT + (5 C_PB + 2) k + 16, where C_PB is the absolute constant from Chasing Positive Bodies at resource augmentation one and covering sparsity two. The full reduction, rounding composition, and quantified main theorem are machine-checked in Lean 4 relative to exact formal interfaces for the two cited source theorems. Deterministic rational controls and a fresh independent replay accompany the formal proof.
1 Introduction
The introduction establishes that Dynamic MoE serving has a constant randomized competitive ratio, improving on the prior O(√log k) integral-primal guarantee. It reduces reciprocal service costs to positive-body chasing, resolves finite-tangent and projection obstacles, and formally verifies the reduction and rounding.
- Main result: Constant randomized competitive ratio is proved for the primal Dynamic MoE serving problem, whereas prior work established O(√log k).The earlier Ω(√log k) lower-bound construction applies to an offset-Fenchel-dual maximization problem.
- Reduction: The reduction uses a finite positive-polyhedral inner approximation of each reciprocal epigraph and invokes the positive-body chasing theorem.The construction addresses the reciprocal epigraph’s continuum of tangents and the cited theorem’s finite-matrix requirement.
- Rounding: The deterministic fractional path is converted online into an exact integral allocation with no expected movement loss and at most a factor-three service loss.This conversion uses the Lazy Threshold Rounding lemma of Huang, Lou, and Xiao.
- Verification: Lean 4 formalizes and verifies every new MoE bridge, including tangent construction, reset feasibility, movement comparison, exact-budget projection, service charging, rounding, and constant assembly.The two published ingredients are treated as explicit source interfaces audited against pinned source archives, and an independent referee reproduced 24 tests.
2 Model and main result
For m experts and k replica GPUs, the model evaluates causal randomized integral algorithms on fixed finite workload sequences with horizon-independent additive terms. The main theorem gives E[ALG] ≤ 10CPB · OPT + (5CPB + 2)k + 16, with a multiplicative constant independent of m, k, and the horizon, implying CRrand(k) = Θ(1).
- Model and objective: The model fixes m ≥1 experts and k ≥1 replica GPUs, with an integral initial state supplied as part of each instance.OPT is defined over integral paths for a fixed finite workload sequence under the oblivious-adversary convention.
- Model and objective: CRrand(k) is the infimum multiplicative factor for causal randomized integral algorithms with an additive term depending on m and k but not the horizon.The guarantee must hold for every m ≥1, every integral initial state, and every fixed finite workload sequence.
- Reduction: Capacity scaling increases reciprocal service cost by at most a factor two when capacity is halved while retaining at least half of every coordinate.The service-cost epigraph separates into height-and-coordinate constraints, so tangent discretization preserves covering-row support d = 2.
- Main result: E[ALG] ≤10CPB · OPT +(5CPB + 2)k + 16.CPB is the absolute constant from the cited positive-bodies theorem at resource augmentation ϵ = 1 and maximum covering-row support d = 2.
- Main result: The multiplicative constant is independent of m, k, and the horizon, and CRrand(k) = Θ(1).Scaling an equal-workload one-round instance makes the additive constant negligible, while every realized online path is feasible offline.
3 Two source theorems
This section records the two source consequences used by the reduction: an absolute-constant positive-body chaser at covering sparsity two, and Lazy Threshold Rounding for exact-budget fractional MoE paths. Together, they provide the movement guarantee and integral rounding interface needed later.
- Positive-body chasing: At ϵ = 1 and d = 2, Positive-Body Chasing yields an absolute movement factor CPB with exact covering constraints and packing right-hand sides doubled.The underlying guarantee is O(ϵ^-1 log(d/ϵ))-competitive, with packing violation factor 1 + ϵ.
- Lazy Threshold Rounding: Lazy Threshold Rounding applies online to any exact-budget fractional MoE path and produces integral exact-budget states from the given integral initial state.It uses one shared set of random thresholds over all rounds.
- Lazy Threshold Rounding: Using the same thresholds across consecutive prefixes gives the corresponding expected path-movement bound.The source implements each rounding step greedily in polynomial time.
4 A finite positive approximation to reciprocal service
The reciprocal service function is approximated by a finite maximum of tangent functions over an integer grid. This envelope preserves the reciprocal value within a 3/4 factor and yields positive covering rows of sparsity two.
- Finite tangent envelope: p = ⌈1 + u⌉ lies in {1, ..., 2k + 1} and supplies the 3/4 approximation.For q = 1 + u, q ≤ p < 2q, so q/p ∈ (1/2, 1].
- Finite tangent envelope: 3/4 ≤ H_r(u) / (r / (1 + u)) ≤ 1 for 0 ≤ u ≤ 2k.The finite envelope is H_r(u) = max_{1≤p≤2k+1} L_{r,p}(u).
- Positive covering reduction: Each tangent inequality becomes a positive covering row with support size at most two.Coordinates with r = 0 require no row, or may use a vacuous zero-coefficient row with zero right-hand side.
- Grid choices: O(log(k + 1)) rows per expert suffice with a geometric grid, while the formal reduction uses the integer grid.Both envelope lemmas are machine-checked.
5 The event/reset reduction
The reduction presents a causal event/reset construction whose normalized covering rows have positive right-hand sides and support at most two. A balanced projection preserves nonnegativity and total mass while controlling movement from the initial state.
- Event/reset construction: The reset is processed after the round-t action and before the next request, preserving causality; normalized packing rows have positive right-hand sides, event rows support at most two, and both bodies are nonempty.The construction sets δ0 := 0 for the initial accounting convention.
- Event/reset construction: The positive-body chaser runs with ϵ = 1, representing its event point as (ut, st) and the following reset height as bt.
- Balanced projection: The balanced projection produces nonnegative coordinates and total mass k.The proof derives ρ(u) ≥ 0 and obtains the total-mass statement by summing the projection formula.
- Movement accounting: 16/3 bounds the summed error terms when δt = 1 for t ≥ 1.
- Balanced projection: The balanced projection is nonexpansive, while the first projected state can be at distance at most 2k from the supplied integral x0.The bound uses the diameter of the exact simplex.
6 Comparison with the MoE optimum
The comparison applies the positive-body theorem to an optimal MoE comparator path by lifting event and reset states into feasible body points. Lazy Threshold Rounding then yields the stated constant-competitive bound with a horizon-independent additive term.
- Comparator-path lifting: An integral comparator path is lifted by using (y_t, h_t) at event times and (y_t, 0) at reset times.The tangent-underestimator identity makes the event point feasible, and the reset point is feasible as well.
- Positive-body comparison: Applying the positive-body theorem to an optimal MoE path supplies the fractional comparison bound.
- Rounding and final bound: The additive term is independent of the horizon, and the construction depends only on revealed requests and one initial rounding seed.
7 Formal and executable verification
The section formalizes the new Dynamic MoE implications in Lean 4.32.2 and validates them through an executable replay. It states an explicit 10C_PB upper-bound factor while treating the cited CPB and HLX results as checked primitive premises rather than reproving them.
- Formal development: 10C_PB is the explicit factor in the main DynamicMoeMain.dynamicMoe upper-bound declaration.The proof also formalizes the CPB-compatible body condition and telescopes HLX’s per-step expected movement inequality.
- Formal development: Lean reports only propext, Classical.choice, and Quot.sound as standard axioms for every audited declaration.
- Formal boundary: The development proves new Dynamic MoE implications from exact CPB and HLX consequences, while pinned source archives and theorem-bearing members are SHA-256 checked before replay.It does not reprove the complete CPB or HLX papers.
- Executable replay: 24 tests pass, and a fresh independent process reproduces the exact-control and formal-packet artifact hashes.The exact control covers rational tangent-envelope, reset-charge, budget-map, movement-normalization, and offline dynamic-program tests, including a corrupted-movement negative control.
8 Scope and open directions
The theorem resolves the asymptotic randomized integral ratio under the fixed-sequence convention, while leaving several quantitative and adversarial questions open. The section also identifies a geometric-grid improvement and an exact-real-number issue in the reset schedule.
- Scope: The theorem resolves the asymptotic randomized integral ratio under the fixed-sequence convention.
- Open directions: The best numerical constant, deterministic integral competitive ratio, and ratio against an adaptive adversary remain undetermined.
- Efficiency: O(m log(k + 1)) covering rows per event replace the concrete integer grid’s O(mk) rows without changing the proof.The geometric grid is noted after Lemma 2.
- Implementation: The reset schedule uses exact real numbers, leaving replacement by another positive summable schedule as an implementation direction.