Vosti：大语言模型确定性推理的形式化规范、实现与验证

研究团队提出了大语言模型确定性推理的形式化规范，并构建了经过形式化验证的推理引擎 Vosti。针对 vLLM 与 SGLang 确定性模式在部分执行变化下仍出现 logits 差异的问题，Vosti 结合 Verus 证明与 Triton 分析器实现了逐位一致的 logits 输出。在重 decode 负载下，Vosti 实现了媲美 vLLM batch-invariant 模式的性能。