动态混合专家服务的常竞争比算法
A Deterministic Constant-Competitive Algorithm for Dynamic Mixture-of-Experts Serving
浏览论文内容
中文总结 AI 辅助
针对动态混合专家服务问题，本文证明其随机原始算法竞争比为Θ(1)，给出含量化界的算法，结果在Lean 4中完成机器验证。
中文摘要 AI 辅助
Huang、Lou和Xiao提出了动态混合专家服务（Dynamic Mixture-of-Experts Serving），并针对其原始积分问题给出了竞争比为O(√log k)的随机算法，其中k是每个专家强制副本之外的GPU副本数量。他们的匹配下界适用于辅助对偶问题，而原始问题的竞争比阶数仍未确定。我们证明，对于任意数量的专家，随机原始算法的竞争比实际上为Θ(1)。该上界将倒数最大服务成本简化为用行稀疏度为2的覆盖算法追踪正体。有限切线包络以常数因子近似每个倒数上境图，可求和的正重置将累积服务转化为移动，非扩张平衡投影消除了正体算法的资源增强。将得到的分数路径与惰性阈值舍入（Lazy Threshold Rounding）结合，可得E[ALG] ≤ 10 C_PB OPT + (5 C_PB + 2) k + 16，其中C_PB是资源增强为1且覆盖稀疏度为2时，来自追踪正体（Chasing Positive Bodies）的绝对常数。完整的归约、舍入组合及量化主定理已在Lean 4中相对于两个引用源定理的精确形式化接口进行了机器验证，形式化证明伴随确定性有理控制和全新独立重放。
英文摘要
Dynamic Mixture-of-Experts Serving allocates k replica GPUs among m experts as workloads change. At each round, the online algorithm sees the current workload, chooses integral replica counts, and pays bottleneck service cost plus replica movement. It does not know future workloads. Huang, Lou, and Xiao gave an O(sqrt(log k))-competitive randomized algorithm for this problem. We prove a deterministic O(1)-competitive algorithm. For every number of experts and every k>=1, the algorithm satisfies ALG_det <= 10 C_PB OPT + (5 C_PB + 8) k + 16, where C_PB is the absolute constant from Chasing Positive Bodies at resource augmentation one and covering sparsity two. Consequently, CR_det(k)<=10 C_PB for every k>=1, so CR_det(k)=Theta(1). The multiplicative factor does not depend on the number of experts, replica budget, horizon, or workload values. Thus randomization is not needed for the asymptotic guarantee. The proof has two layers. A finite tangent envelope, summable positive resets, and a nonexpansive balanced projection reduce reciprocal-max service costs to a deterministic exact-budget fractional path. A new deterministic rounding theorem converts every such path to integral allocations with service distortion three and movement bounded by the fractional movement plus 6k. The complete reduction, rounding theorem, causal composition, and quantified main theorem are machine-checked in Lean 4 relative to the positive-body result as the sole scientific source premise. The theorem concerns the allocation model above. It does not include network topology, shared-edge congestion, or routing decisions.
发表机构
- Nth Research Collective（Nth研究集体）
机构由 AI 辅助整理，请以论文原文为准。
