🤖 AI

BEAVER: An Efficient Deterministic LLM Verifier

本文介绍了BEAVER，这是一个新颖的框架，它利用Token前缀树和前沿数据结构，高效地计算大语言模型安全属性的确定性且可靠的概率边界，通过以计算预算的一小部分识别出显著更多的风险实例，从而超越了基于采样的基线方法。

原作者： Tarun Suresh, Nalin Wadhwa, Debangshu Banerjee, Gagandeep Singh

发布于 2026-05-11

📖 1 分钟阅读☕ 轻松阅读

原作者： Tarun Suresh, Nalin Wadhwa, Debangshu Banerjee, Gagandeep Singh

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一下，你拥有一个非常聪明、富有创造力的机器人，它能撰写故事、代码或电子邮件。你想知道：“如果我向这个机器人提问，它说出危险内容的概率有多大？比如泄露秘密密码或编写病毒？”

目前，人们尝试通过让机器人重复回答同一问题一千次，并统计其出错的次数来回答这个问题。这就像试图通过盲目地抓取 handfuls 干草来从干草堆中寻找一根针。你可能会错过那根针，或者反复抓取同一把干草。这种方法既缓慢又昂贵，而且无法向你保证干草堆是安全的。

BEAVER 是一款改变游戏规则的新工具。它不再盲目地抓取 handfuls 干草，而是像一位超级有条理的图书管理员，在你提问之前，就绘制出所有可能答案的完整地图。

以下是其工作原理，使用简单的类比说明：

1. “可能性之树”（Token Trie）

想象机器人的回答像一棵树一样生长。

树干是你的问题。
树枝是机器人可能说出的前几个词。
树叶是最终完整的句子。

大多数工具只选择一条树枝并走到尽头。然而，BEAVER 会审视整棵树。它构建了机器人可能采取的所有路径的地图。

2. “安全守卫”（Frontier）

BEAVER 有一条特殊规则：“如果某条树枝开始显得危险，立即将其剪除。”

如果机器人开始输入一个可能导致泄露或有毒侮辱的词语，BEAVER 会在句子开头就立刻发现它。
它不会浪费时间完成那个句子。它会说：“停！这条路径是坏的”，并将该树枝从树上剪掉。
这就像派对上的保安，一旦某人看起来可疑就阻止其进入 VIP 室，而不是等到他们已经在里面制造麻烦时才行动。

3. “智能探索者”（Branch and Bound）

BEAVER 并非随机检查每一条树枝。它采用一种称为"Max-µ"的智能策略。

想象每条树枝都有不同的“权重”（概率）。某些路径发生的可能性很高，而其他路径则很罕见。
BEAVER 总是优先检查最重、最可能发生的路径。
在检查这些路径时，它会持续计算得分：
- “安全得分”（下界）： 有多少树的部分是绝对安全的？
- “最坏情况得分”（上界）： 即使我们尚未检查每一片树叶，有多少树的部分可能是危险的？

4. 结果：“安全证书”

BEAVER 不会给你一个模糊的猜测，比如“大概没问题”，而是给你一个数学保证。

它可能会说：“我们 100% 确定至少 90% 的答案是安全的，最多 10% 可能是危险的。”
更棒的是，它完成这一点的速度比旧的“盲目猜测”方法快得多。论文显示，BEAVER 发现的危险示例数量是旧方法的2.5 到 3 倍，而仅使用了十分之一的计算机算力。

为什么这很重要

论文在 12 种不同的 AI 模型（如 Llama、Qwen 和 Gemma）以及四种安全测试类型上测试了 BEAVER：

隐私： 它会泄露电子邮件地址吗？
安全： 它会编写不安全的代码吗？
偏见： 它会使用刻板印象吗？
毒性： 它会粗鲁或有害吗？

结果表明，不同模型具有不同的“个性”。一个模型可能在数学方面很出色，但在保守秘密方面却很差。另一个模型可能很有礼貌，但会编写糟糕的代码。BEAVER 能够发现其他方法遗漏的这些具体弱点。

简而言之： BEAVER 是一种系统性地探索 AI 可能失败的每一种方式的工具，它尽早切断危险路径，并提供精确的、经数学证明的安全报告，从而节省时间和金钱，同时发现其他方法完全遗漏的风险。

技术摘要：BEAVER——一种高效的确定性大语言模型验证器

1. 问题陈述

随着大语言模型（LLMs）从研究原型转向生产系统，从业者面临着刻画“尾部风险”的关键挑战——即罕见但影响巨大的故障，例如泄露私人信息、生成不安全代码或产生有害内容。当前的部署实践几乎完全依赖临时的经验方法，包括基准测试、红队测试和基于采样的估计。虽然这些方法提供了直观认识，但它们无法提供关于模型行为的可靠保证。

验证大语言模型的核心难点在于其作为自回归模型的本质：它们诱导输出序列上的概率分布，而非产生单一的确定性输出。现有的神经网络验证器针对确定性的输入 - 输出关系，无法处理自回归生成中特有的概率选择、序列展开和解码逻辑的组合。因此，由于模型规模庞大以及输出空间的指数级增长，大语言模型的可靠验证一直被认为不可行。

2. 方法论

本文提出了BEAVER，这是首个用于计算大语言模型满足安全属性确定性、可靠概率界限的实用框架。该方法基于以下观察：许多安全属性遵循线性时序逻辑（LTL）形式 $G\phi$ （断言“坏事永远不会发生”）。对于此类属性，违规情况可被早期检测，从而允许对生成空间进行激进剪枝。

核心数据结构

BEAVER 利用两种新颖的数据结构来系统地探索输出空间：

Token 字典树（ $T$ ）：一棵前缀树，用于跟踪所有满足安全约束 $\Phi$ 的已探索序列。每个节点代表一个令牌序列 $s$ 及其关联概率 $\mu(s)$ 。该字典树仅存储满足 $\Phi$ 的前缀闭包性质的序列。
前沿集（ $\Psi$ ）：Token 字典树中叶节点的集合，分为：
- $\Psi_c$ ：完整序列（以 <eos> 结尾）。
- $\Psi_i$ ：可被扩展的不完整序列。

算法：分支定界

BEAVER 采用分支定界算法，迭代地收紧生成响应满足 $\Phi$ 的概率 $P$ 的概率界限 $[P_{LB}, P_{UB}]$ ：

初始化：字典树从根节点（空序列）开始。 $P_{LB} = 0$ 且 $P_{UB} = 1$ 。
选择：从前沿集中选择一个不完整节点 $n[x]$ （通常使用贪婪的Max- $\mu$ 启发式方法，优先处理高概率序列）。
扩展：查询模型以获取下一个令牌的概率 $P_M(\cdot | p \cdot x)$ 。将满足 $\Phi$ 的有效延续 $x \cdot t$ 添加到字典树中。
更新：重新计算界限：
- $P_{LB}$ 是 $\Psi_c$ 中所有完整且满足条件的序列的概率之和。
- $P_{UB}$ 是 $\Psi_i \cup \Psi_c$ 中所有序列的概率之和，加上剪枝质量累加器（ $M_p$ ）。
可靠性：如果为了确保可扩展性而剪枝了低概率令牌或序列（例如通过 top- $p$ 或 top- $k$ 过滤器），则将其累积概率质量添加到 $M_p$ 中。这确保了无论是否进行剪枝， $P_{UB}$ 在每次迭代中始终是有效的上界（ $P_{LB} \le P \le P_{UB}$ ）。

当达到最大前向传递预算，或差距 $P_{UB} - P_{LB}$ 低于容差 $\epsilon$ 时，算法终止。

3. 主要贡献

形式化：作者将大语言模型尾部风险评估形式化为一个验证问题，计算形式为 $G\phi$ 的安全属性的概率界限。他们引入了 Token 字典树和前沿集数据结构，以实现可靠界限的计算。
BEAVER 算法：一种具有形式化可靠性证明的新型分支定界验证算法。它在每次迭代中产生有效的概率区间，并收敛至真实概率。
实证验证：该框架在12 个开源指令微调模型（涵盖 Llama、Qwen、Gemma、Phi、OLMo 和 Mistral 系列）和四个安全属性上进行了评估：
- 隐私泄露（Enron 电子邮件数据集）。
- 不安全代码生成（CyberSecEval）。
- 刻板印象偏见（DecodingTrust）。
- 毒性（RealToxicityPrompts）。

4. 结果

评估表明，BEAVER 在效率和风险检测方面显著优于基于采样的基线：

风险检测：即使计算预算仅为基于采样的验证器（SV）的1/10（100 次前向传递对比 SV 的约 1000 次），BEAVER 识别出的风险实例数量也是 SV 的 2.5 到 3.3 倍。
尾部风险显现：BEAVER 证实了相当一部分被临时评估宣布为安全的提示词中存在非平凡的尾部风险（违规概率 $\ge 10\%$ ）。
任务依赖概况：结果显示风险概况高度依赖于任务，且与模型规模没有清晰的关联。例如，Qwen3-4B 在隐私和代码安全方面表现出高风险，但在毒性方面是安全的；而 Gemma-3-4B 则呈现出相反的模式。
效率：BEAVER 在适中的挂钟时间内收敛至紧密界限（ $\epsilon=0.01$ ）（例如，Enron 约 9.4 秒，安全代码约 18.8 秒），每个实例的内存占用低于 5MB。
分布认证：本文证明了可以将每提示词保证与统计技术（Clopper-Pearson）相结合，以提供针对大型输入空间的分布安全保证，这是现有评估方法所不具备的能力。

5. 意义与主张

本文主张，大语言模型行为的确定性验证对于实际部署既是可行的也是实用的。通过超越临时的采样，BEAVER 实现了原则性的风险评估，能够揭示单一数值安全评分无法察觉的尾部风险。

作者强调，他们的方法提供的是可靠保证而非统计估计。这对于安全关键场景至关重要，因为 10% 的违规率在生产环境中可能转化为数千个不安全输出。该框架确立了大语言模型尾部风险可以被可靠且可行地刻画，为当前的经验评估方法提供了严谨的替代方案。

局限性：当前框架针对前缀闭包安全属性（ $G\phi$ ），尽管它允许扩展至非前缀闭包属性。它依赖于对完整令牌概率分布的白盒访问，并使用启发式方法（Max- $\mu$ ）进行选择，作者指出这可以通过针对更复杂规范的习得价值函数加以改进。