提出首个高效确定性验证框架，精准识别大模型输出中的高风险情况。
BEAVER: An Efficient Deterministic LLM Verifier
- 基于新型数据结构系统遍历模型输出空间，保证每一步推导都可靠。
- 在12个开源大模型上验证，发现2-3倍更多高风险样本，仅需1/10算力。
- 适合关注模型安全、部署可靠性或需要可证明保障的研究者与工程师。
随着大语言模型从研究原型走向生产系统，从业者亟需可靠方法验证模型输出并评估尾部风险以确保安全部署。基于采样的估计虽能提供直观感受，但无法提供可信保障。本文提出 BEAVER，首个实用的确定性框架，用于计算大模型满足安全属性的严格概率边界。给定提示和任意安全属性，BEAVER 利用创新的 Token trie 与 Frontier 数据结构，系统探索模型输出空间，并在每轮迭代中维持可证明的严格边界。我们形式化了验证问题，证明了方法的正确性，并在12个开放权重的大模型上对4种安全属性进行了评估。BEAVER 发现的高风险实例比基线多2-3倍，同时仅消耗1/10的计算资源，揭示了传统宽松边界和随意评估所遗漏的尾部风险。
原文摘要 · Abstract (English)
As large language models (LLMs) transition from research prototypes to production systems, practitioners often need reliable methods to verify model outputs and characterize tail risk for safe deployment. While sampling-based estimates provide an ad-hoc intuition of model behavior, they offer no sound guarantees. We present BEAVER, the first practical framework for computing deterministic, sound probability bounds on LLM satisfaction of safety properties. Given a prompt & any safety property, BEAVER systematically explores the model output space using novel Token trie and Frontier data structures, maintaining provably sound bounds at every iteration. We formalize the verification problem, prove soundness of our approach, and evaluate BEAVER on 4 safety properties across 12 open-weight LLMs. BEAVER identifies 2-3x more risky instances compared to baselines while taking 1/10 of the compute budget, surfacing tail risks that loose bounds and ad-hoc evaluation misses.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。