AI 中文总结
该研究针对全在线KV缓存调度问题，通过构造困难实例得到确定性竞争比下界，利用均匀因果串行策略得到上界，在Lean 4中完成机器验证，证明其竞争比为紧线性的Θ(n)。
AI 中文摘要
Jaillet等人提出了一种在不断增长的KV缓存内存约束下对非抢占式大语言模型（LLM）请求进行批处理的全在线模型。对于总端到端延迟，他们证明了每个确定性算法的竞争比为Ω(√n)，而基础的顺序上界为n。我们消除了这一差距。设R_det(n,M)为内存M下恰好n个请求的最优确定性竞争比，令R_det(n)=sup_M R_det(n,M)。对于每个n≥2，我们证明(n-1)/12 ≤ R_det(n) ≤ n，因此R_det(n)=Θ(n)。下界构造了一个内存占满的长请求，观察其确定性启动时间后，在长请求运行中途释放n-1个宽单令牌请求。没有短请求能与长请求重叠，而事后调度会在有用时以相反顺序运行两组请求。该困难实例使用显式固定内存M=2(n-1)n。上界由均匀因果串行策略实现。精确模型、因果性论证、两个比较器分支及量词顺序均在Lean 4中完成机器验证，证明附带精确有限控制与重放命令。
英文摘要
Jaillet et al. introduced a fully online model for batching nonpreemptive LLM requests under a growing KV-cache memory constraint. For total end-to-end latency they proved that every deterministic algorithm has competitive ratio Omega(sqrt(n)), while the elementary sequential upper bound is n. We close this gap. Let R_det(n,M) be the optimal deterministic ratio for exactly n requests at memory M, and let R_det(n)=sup_M R_det(n,M). For every n >= 2 we prove (n-1)/12 <= R_det(n) <= n, so R_det(n)=Theta(n). The lower bound releases one memory-filling long request, observes its deterministic start time, and then releases n-1 wide one-token requests halfway through the long run. No short request can overlap the long one, whereas a hindsight schedule runs the two groups in the opposite order when useful. The hard instance uses the explicit fixed memory M=2(n-1)n. The upper bound is achieved by a uniform causal serial policy. The exact model, causality argument, both comparator branches, and quantifier order are machine-checked in Lean 4. Exact finite controls and replay commands accompany the proof.
Comments6 pages. The exact fully online model, fixed-memory-before-scheduler quantifier order, serial upper bound, and wide-short lower bound are checked in Lean 4. A separate reproducibility archive contains pinned-source bootstraps, exact finite controls, formal proofs, tests, and canonical SHA-256 manifests
