Technical Summary: BEAVER – An Efficient Deterministic LLM Verifier

1. Problem Statement

As Large Language Models (LLMs) transition from research prototypes to production systems, practitioners face the critical challenge of characterizing "tail risk"—rare but high-impact failures such as leaking private information, generating insecure code, or producing toxic content. Current deployment practices rely almost exclusively on ad-hoc empirical methods, including benchmarking, red-teaming, and sampling-based estimates. While these methods offer intuition, they provide no sound guarantees regarding model behavior.

The core difficulty in verifying LLMs lies in their nature as auto-regressive models that induce a probability distribution over output sequences rather than producing a single deterministic output. Existing neural network verifiers target deterministic input-output relations and cannot handle the combination of probabilistic choice, sequential unrolling, and decoding logic specific to autoregressive generation. Consequently, sound verification of LLMs has been considered infeasible due to model scale and the exponential growth of the output space.

2. Methodology

The paper presents BEAVER, the first practical framework for computing deterministic, sound probability bounds on LLM satisfaction of safety properties. The approach is grounded in the observation that many safety properties follow the Linear Temporal Logic (LTL) form $G\phi$ (asserting "nothing bad ever happens"). For such properties, violations can be detected early, allowing for aggressive pruning of the generation space.

Core Data Structures

BEAVER utilizes two novel data structures to explore the output space systematically:

1. Token Trie ($T$): A prefix tree that tracks all explored sequences satisfying the safety constraint $\Phi$. Each node represents a token sequence $s$ with its associated probability $\mu(s)$. The trie only stores sequences that satisfy the prefix-closed property of $\Phi$.
2. Frontier ($\Psi$): A set of leaf nodes in the Token Trie, split into:
   • $\Psi_c$: Complete sequences (ending with <eos>).
   • $\Psi_i$: Incomplete sequences eligible for expansion.

Algorithm: Branch-and-Bound

BEAVER employs a branch-and-bound algorithm to iteratively tighten the probability bounds $[P_{LB}, P_{UB}]$ for the probability $P$ that a generated response satisfies $\Phi$:

• Initialization: The trie starts with the root (empty sequence). $P_{LB} = 0$ and $P_{UB} = 1$.
• Selection: An incomplete node $n[x]$ is selected from the frontier (typically using a greedy Max-$\mu$ heuristic to prioritize high-probability sequences).
• Expansion: The model is queried for next-token probabilities $P_M(\cdot | p \cdot x)$. Valid continuations $x \cdot t$ that satisfy $\Phi$ are added to the trie.
• Update: The bounds are recomputed:
  • $P_{LB}$ is the sum of probabilities of all complete, satisfying sequences in $\Psi_c$.
  • $P_{UB}$ is the sum of probabilities of all sequences in $\Psi_i \cup \Psi_c$, plus a Pruned Mass Accumulator ($M_p$).
• Soundness: If low-probability tokens or sequences are pruned (e.g., via top-$p$ or top-$k$ filters) to ensure scalability, their cumulative probability mass is added to $M_p$. This ensures $P_{UB}$ remains a valid upper bound ($P_{LB} \le P \le P_{UB}$) at every iteration, regardless of pruning.

The algorithm terminates when a maximum budget of forward passes is reached or when the gap $P_{UB} - P_{LB}$ falls below a tolerance $\epsilon$.

3. Key Contributions

1. Formalization: The authors formalize LLM tail-risk assessment as a verification problem, computing probability bounds for safety properties of the form $G\phi$. They introduce the Token Trie and Frontier data structures to enable sound bound computation.
2. BEAVER Algorithm: A novel branch-and-bound verification algorithm with formal soundness proofs. It produces valid probability intervals at every iteration that converge toward the true probability.
3. Empirical Validation: The framework is evaluated on 12 open-weight instruction-tuned models (across Llama, Qwen, Gemma, Phi, OLMo, and Mistral families) and four safety properties:
   • Privacy leakage (Enron email dataset).
   • Insecure code generation (CyberSecEval).
   • Stereotype bias (DecodingTrust).
   • Toxicity (RealToxicityPrompts).

4. Results

The evaluation demonstrates that BEAVER significantly outperforms sampling-based baselines in both efficiency and risk detection:

• Risk Detection: BEAVER identifies 2.5 to 3.3 times more risky instances than a sampling-based verifier (SV), even when operating with 1/10th of the compute budget (100 forward passes vs. ~1000 for SV).
• Tail Risk Surfacing: BEAVER certifies non-trivial tail risk (violation probability $\ge 10\%$) on a substantial fraction of prompts that ad-hoc evaluation declares safe.
• Task-Dependent Profiles: The results reveal that risk profiles are highly task-dependent and do not correlate cleanly with model size. For example, Qwen3-4B shows high risk in privacy and code security but is safe on toxicity, whereas Gemma-3-4B shows the inverse pattern.
• Efficiency: BEAVER converges to tight bounds ($\epsilon=0.01$) in modest wall-clock time (e.g., ~9.4s for Enron, ~18.8s for Secure Code) with memory footprints under 5MB per instance.
• Distributional Certification: The paper demonstrates that per-prompt guarantees can be composed with statistical techniques (Clopper-Pearson) to provide distributional safety guarantees over large input spaces, a capability not offered by existing evaluation methods.

5. Significance and Claims

The paper claims that deterministic verification of LLM behavior is both feasible and practical for real-world deployment. By moving beyond ad-hoc sampling, BEAVER enables principled risk assessment that can surface tail risks invisible to single-number safety scores.

The authors emphasize that their approach provides sound guarantees rather than statistical estimates. This is critical for safety-critical scenarios where a 10% violation rate could translate to thousands of unsafe outputs in production. The framework establishes that LLM tail risk can be characterized soundly and tractably, offering a rigorous alternative to current empirical evaluation methods.

Limitations: The current framework targets prefix-closed safety properties ($G\phi$), though it admits extension to non-prefix-closed properties. It relies on white-box access to full token probability distributions and uses heuristics (Max-$\mu$) for selection, which the authors note could be improved with learned value functions for harder specifications.