Vosti：确定性 LLM 推理的规范、实现与验证

📌 One-Sentence Summary

本文介绍了 Vosti，这是一种经过形式化验证的推理引擎，旨在确保在不同执行变体下 LLM 输出 logits 达到位级完全一致。

📝 Summary

当前的 LLM 推理系统使用了批处理、Prompt 分块和 KV-cache 管理等多种优化手段，这些可能导致非确定性输出。作者形式化了确定性 LLM 推理——即要求固定配置和初始采样器状态能够产生位级相同的结果。为了实现这一点，他们提出了 Vosti，该引擎将算子选择与运行时状态解耦，并使用形式化验证（Verus 和 Triton）证明调度和分页 KV-cache 操作不会改变输出 logits。

💡 Main Points

确定性 LLM 推理标准的形式化定义

他们定义了在固定模型和部署下，具有相同 prompt 和采样器状态的请求必须产生位级相同的结果。

现有的生产模式如 vLLM 和 SGLang 缺乏形式化系统规范

测试表明，即使是目前生产环境中的“确定性”模式，在某些执行变体下也会产生不同的 logits。

Vosti 通过解耦选择来实现确定性

它独立于运行时引擎状态选择算子，并将缓存的 KV 值与逻辑 token 前缀绑定。

通过 Verus 和 Triton 分析器提供形式化验证

通过 Verus 的证明确保了调度/KV-cache 的安全性，同时通过分析器证明了跨布局的输出是位级等等的。

💬 Key Quotes

我们形式化了确定性 LLM 推理：在固定模型和部署配置下，具有相同 prompt 和初始采样器状态的请求在不同执行的对应输出位置上产生位级相同的 logits。

Vosti 独立于运行时引擎状态选择算子，并将缓存的 KV 值与其逻辑 token 前缀绑定。

📊 Article Meta

AI Screening： 87

Source： Hacker News - Newest: "LLM"

Author： matt_d

Category： 人工智能

Language： 英文

Read Time： 2 min

Word Count： 323

Tags：

AI 与智能应用 , 形式化验证 , AI 工程 , LLM 推理优化 , LLM 推理