BEAVER: An Efficient Deterministic LLM Verifier

1 Introduction

• Practitioners need sound ways to characterize rare, high-impact LLM failures, but common empirical evaluation methods offer no sound guarantees.The cited examples include benchmarking, red-teaming, adversarial attacks, and sampling-based estimates.Source: §1 · p. 1
• Existing neural-network verifiers target deterministic input-output relations and do not handle autoregressive generation’s probabilistic choice, sequential unrolling, and decoding logic.The passage describes sound LLM verification as previously considered infeasible at model scale.Source: §1 · p. 1
• BEAVER computes deterministic, sound probability bounds for safety properties, using early detection of violations to prune generation space.The early-pruning insight applies to common properties of the form G ϕ, which assert that nothing bad ever happens.Source: §1 · p. 1
• Its token trie tracks explored satisfying prefixes, while a frontier tracks incomplete sequences for expansion and supports monotonically tightening probability bounds.The framework provides sound bounds at each iteration and can be stopped at any iteration for a certified interval.Source: §1 · p. 2
• 2.5-3.3× more risky instances across all datasets than the baseline verifier given a 10× budget.The evaluation covers 12 open-weight instruction-tuned models from six families and four safety properties.Source: §1 · p. 2
• The paper formalizes tail-risk assessment as probability-bound verification and presents a branch-and-bound algorithm with soundness proofs and bounds that converge toward the true probability.The introduction states these as formalization and algorithm contributions.Source: §1 · p. 2

2 Related Work

• Constrained decoding guides generation by masking invalid tokens or backtracking and resampling violations, whereas BEAVER quantifies total constraint-satisfaction probability and characterizes model risk.The paper describes constrained decoding as complementary to verification.Source: §2 · pp. 2–3
• DNN verifiers offer sound but incomplete, complete, or probabilistic guarantees, but reason about deterministic networks rather than probabilistic output distributions.The passage identifies three classes of DNN verification methods.Source: §2 · p. 3
• LLM statistical-certification work covers robustness and other risks, but provides guarantees through sampling or randomized smoothing rather than deterministic sound bounds.The cited areas include knowledge comprehension, bias, multi-turn risks, and agentic tool selection.Source: §2 · p. 3

3 Background

• The paper defines generated-sequence probabilities from next-token distributions and notes that temperature, top-k, and top-p decoding are supported when applied consistently.A model’s next-token distribution is produced by a forward pass.Source: §3 · p. 3
• Safety properties in the LTL fragment Gϕ require a per-position predicate to hold at every prefix, expressing that nothing bad ever happens.The paper notes that these properties include requirements such as syntactic validity, secure code, and absence of toxic or private content.Source: §3 · p. 3
• BEAVER can encode some final-state checks, such as arithmetic-expression correctness, by accepting prefixes consistent with eventual satisfaction and checking at syntactic completion.This extends the approach to properties that are not prefix-closed without modifying the underlying algorithm.Source: §3 · pp. 3–4
• The verification problem is to compute the probability that an autoregressively generated complete response satisfies a given safety property.The complementary probability is the probability that a generated response violates the property.Source: §3 · p. 4
• Exact computation is infeasible as the response space grows exponentially, so the paper instead tightens sound probability bounds over a finite number of model queries.The bounds remain sound at every iteration.Source: §3 · p. 4
• Sampling wastes queries on duplicate high-probability sequences and on extensions of prefixes that already violate a safety property.These limitations motivate reasoning over prefixes, pruning violations early, and accounting for probability mass systematically.Source: §3 · p. 4

4 Methodology

• The methodology tracks satisfying partial sequences to reject already-violating sequences early and compute sound bounds on the probability of a valid response.The token trie stores satisfying sequences and their probabilities, while the frontier identifies sequences eligible for expansion.Source: §4 · p. 4, §4.1 · p. 4

4.1 Token Trie and Frontier

• The token trie stores satisfying token sequences as paths whose edges carry conditional token probabilities and whose nodes carry sequence probabilities.The trie root represents the empty sequence; complete nodes end in the end-of-sequence token.Source: §4.1 · p. 5

T Update Strategy:

• Each trie update expands an incomplete leaf by adding satisfying next-token continuations; the frontier separates complete from incomplete leaves.The frontier’s lower bound sums complete satisfying sequences, while its upper bound sums complete and incomplete frontier sequences.Source: T Update Strategy · p. 5

4.2 BEAVER Algorithm

• BEAVER iteratively selects an incomplete node, queries the model for next-token probabilities, adds satisfying continuations, and recomputes the bounds until its iteration or tolerance limit.It returns the final probability interval as certified bounds.Source: §4.2 · p. 6

4.2.1 Selection Strategy

• Max-µ expands the highest-probability incomplete sequence first, prioritizing sequences that contribute most to the uncertain probability mass.The incomplete frontier is maintained as a max-heap, enabling O(log |Ψi|) selection; Sample-µ is also implemented for comparison.Source: §4.2.1 · p. 6

4.3 Optimizations

• Top-p and top-k token filters and a cap on incomplete frontier size reduce runtime and memory, while retired probability mass is added to the upper bound to preserve soundness.The approach can prune low-probability tokens and sequences; under default Max-µ, these optimizations were rarely binding in the reported experiments.Source: §4.3 · p. 6

• Four safety properties cover privacy leakage, insecure code, stereotype detection, and toxicity, using Enron, CyberSecEval, DecodingTrust, and RealToxicityPrompts.The evaluation includes 100 Enron pairs, 204 Rust autocomplete instances, 320 stereotype instances, and 318 toxicity prompts.Source: §5 · pp. 6–7
• The evaluation spans 12 open-weight instruction-tuned models from six families, with 100 forward passes per instance and early termination when the bound gap falls below 0.01.Experiments use temperature 1, top-p 0.99, top-k 500, and a frontier cap of 10,000.Source: §5 · p. 7
• RDR counts instances where BEAVER certifies at least 10% violation risk, while N measures average forward passes until convergence or budget exhaustion.RDR uses τ = 0.9, corresponding to PUB < 0.9; the bound-gap threshold is ϵ = 0.01 and the default maximum budget is 100.Source: §5 · p. 7

6.2 Comparison with Sampling-based Verifier

• 2.7× on Secure Code, 3.3× on Stereotype, and 2.5× on Toxicity: BEAVER found more risky instances than SV with one-tenth the budget.On 16-token Enron, both methods converge similarly; the gap is largest on longer-generation tasks, where sampling rarely encounters lower-probability violating completions.Source: Table 2 · p. 8, §6.2 · p. 8

6.1 Safety Profiles Across Models and Tasks

• Models are safe on some evaluated tasks and risky on others, and their failure modes do not correlate cleanly with model size or family.The reported profiles vary by task within the same model, so a single aggregate safety score cannot distinguish these cross-task asymmetries.Source: §6.1 · p. 8
• Within Qwen, Qwen3 models are nearly safe on stereotype and toxicity (≤1.6%), versus 49.1–58.8% for Qwen2.5; Gemma risk reverses across model sizes by task.Gemma-3-4B has 60.9% stereotype risk versus 12.2% for Gemma-3-12B, but secure-code risk is 40.7% versus 57.4%.Source: §6.1 · p. 8

6.3 Cost, Runtime and Hyperparameter Ablation Studies

• 9.4s, 18.8s, 13.7s, and 13.5s are the average per-instance runtimes for Enron, Secure Code, Stereotype, and Toxicity, respectively.The per-instance trie stays under 5 MB; ablations report comparable bound tightness for Max-µ and Sample-µ, faster convergence at lower temperatures, and negligible sensitivity to practical top-p and top-k ranges.Source: §6.3 · pp. 8–9

6.4 Distributional Safety Certification

• 29 of 50 sampled Llama-3.2-3B-Instruct contexts were certified risky, yielding a 95% interval of [0.432, 0.718] for the true fraction.The experiment samples adversarial contexts for one base prompt; the paper also reports 21 of 50 risky contexts for Qwen3-4B-Instruct, with interval [0.282, 0.568].Source: §6.4 · p. 9

• BEAVER targets prefix-closed LTL Gϕ properties, with extension to non-prefix-closed properties noted as possible; richer temporal patterns remain a next step.Sound bounds rely on white-box access to full token probability distributions.Source: §7 · p. 9

8 Conclusion

• BEAVER is presented as a practical framework for deterministic probability bounds on LLM constraint satisfaction, using safety-property structure to prune generation space.Its Token Trie and Frontier explore generation while maintaining sound bounds at every iteration.Source: §8 · p. 9

A Decoding Strategies

• Consistent decoding transformations define the effective token distribution over which verification occurs; temperature, top-p, and top-k modify token probabilities.The appendix describes greedy decoding as selecting the highest-probability next token at each step.Source: A Decoding Strategies · p. 16

B Sampling based Verification Algorithm

• The sampling-based baseline repeatedly samples complete sequences and accumulates probability mass according to constraint satisfaction.Source: B Sampling based Verification Algorithm · p. 16

C BEAVER Algorithm

• The complete BEAVER algorithm implements frontier-based exploration to compute sound probability bounds on constraint satisfaction.The appendix presents it as the algorithmic realization of the frontier-based strategy described in the main text.Source: C BEAVER Algorithm · p. 17

D BEAVER Soundness Proofs

• The proof roadmap establishes that BEAVER’s bounds are sound at every iteration, after proving the target probability is well-defined and establishing prefix-probability dominance.The appendix also provides a time-complexity analysis.Source: D BEAVER Soundness Proofs · p. 17

D.1 Probability Boundedness

• The target probability P lies between 0 and 1, since it sums probabilities of satisfying finite-length complete sequences.The proof establishes the lower bound from nonnegative sequence probabilities and the upper bound by accounting for finite-length sequences.Source: §D.1 · pp. 17–18

D.2 Prefix Probability Dominance

• The probability mass of all complete strict-suffix sequences extending a prefix s0 is at most the probability µ(s0) of that prefix.This prefix-dominance result supplies a bound on the probability of completions beneath an incomplete sequence.Source: §D.2 · p. 18

D.3 Soundess of BEAVER

• At each update, every satisfying completion is either already explored or has a prefix in the incomplete frontier, preserving the basis for sound bounds.The proof proceeds by induction over frontier updates.Source: §D.3 · p. 19

D.4 Time Complexity Analysis

• O(δ · (1 + |V| + log(δ · |V|) + CΦ)) is the worst-case complexity for δ frontier updates, with vocabulary size |V| and constraint cost CΦ.Each expansion uses a model forward pass, scans the vocabulary, checks constraints, and updates the frontier; the authors note further reduction of constraint-checking overhead as future work.Source: §D.4 · p. 19

E.1 Secure Code Generation

• Secure-code evaluation uses 204 Rust autocomplete instances, adversarial prompts, and a constraint requiring that no CyberSecEval insecure-code detector CWE patterns appear.Generations are capped at 32 tokens.Source: §E.1 · p. 20

E.2 Email Leakage Dataset

• Email-leakage evaluation tests targeted extraction of memorized addresses using 100 prompts drawn from 3,238 name-email pairs; a known leaked address violates the constraint.The sampled addresses exclude predictable company-domain patterns and appear at least three times in the source data.Source: §E.2 · pp. 20–21

E.3 Toxicity

• Toxicity evaluation samples 318 extremely toxic RealToxicityPrompts instances and treats Detoxify scores above 0.5 as violations.Prompts receive an adversarial system instruction, and generations are capped at 32 tokens.Source: §E.3 · p. 21

E.4 Stereotype Bias

• Stereotype-bias evaluation covers 320 instances across 24 demographic groups, seven factors, and 16 topics; explicit or implicit agreement violates the constraint.An algorithmic classifier also detects disagreement and refusal.Source: §E.4 · pp. 21–22

E.5 GSM-Symbolic Dataset

• GSM-Symbolic uses 100 symbolic word problems, and its composite constraint requires grammatical validity and functional correctness verified with Z3.Malformed expressions can be rejected using the grammatical safety property.Source: §E.5 · p. 22

E.6 Results on GSM Symbolic

• The GSM-Symbolic evaluation extends BEAVER beyond safety to correctness verification, reporting probability bounds and average forward-pass count for model ranking.The paper concludes that prefix-level reasoning also yields precise correctness-probability estimates.Source: §E.6 · pp. 23–24
• BEAVER’s Qwen3-4B bound gap is 0.013 versus rejection sampling’s 0.092, roughly 7× tighter at the same compute budget.The reported bounds are [0.343, 0.356] for BEAVER and [0.341, 0.433] for rejection sampling.Source: Table 3 · p. 24, §E.6 · p. 24
• BEAVER’s tighter intervals support a reported ordering of model correctness probabilities, whereas sampling’s overlapping intervals leave the models statistically indistinguishable.The reported intervals are 43.5%–45.4% for Llama-3.3-70B, 40.4%–42.6% for Qwen3-30B-A3B, and 39.5%–43.9% for Qwen2.5-14B.Source: §E.6 · p. 24

F.1 Runtime comparison of BEAVER

• 20 forward passes: BEAVER bounds [0.345, 0.498] (gap 0.153) versus rejection sampling [0.341, 0.671] (gap 0.330); at 100 seconds, gaps are 0.065 and 0.302, respectively.The comparison is for Qwen2.5-14B-Instruct on GSM-Symbolic; BEAVER’s bounds are reported as tighter throughout verification.Source: §F.1 · p. 24, Figure 2 · p. 25

F.2 Comparison of Practical Sequence Selection Strategies

• On GSM Symbolic, Max-µ and Sample-µ achieve comparable final bound tightness and nearly identical termination iterations, despite Sample-µ trading determinism for stochastic exploration.For Llama3.3-70B, Max-µ produces bounds [0.054, 0.478], while Sample-µ yields [0.040, 0.483].Source: Table 5 · p. 25, §F.2 · p. 25

F.3.1 Temperature scaling

• Lower temperatures tighten bounds and accelerate convergence; on Qwen3-4B GSM-Symbolic, the gap falls from 0.013 at T = 1.0 to 0.001 at T = 0.33.For security verification, lower temperatures increase the Risky Distribution Ratio from 68/204 to 110/204; the paper attributes this to concentrated probability mass helping Max-µ encounter higher-probability sequences earlier.Source: Table 6 · p. 25, §F.3.1 · p. 26

F.4 Top-p and Top-k Sensitivity

• Top-p variation changes RDR by at most 3 Secure Code instances and 2 Toxicity instances; frontier-cap variation changes RDR by at most 3 instances and N by under 0.3 forward passes.The tested ranges were top-p 0.90–1.00 and frontier caps 1,000–5,000; the paper recommends top-p = 0.99 and frontier cap = 10,000 as defaults.Source: Table 7 · p. 26, Table 8 · p. 26, §F.4 · p. 26

F.3 Effect of Decoding Parameters on Bounds

• Practitioners often deploy modified decoding configurations, motivating analysis of how temperature scaling affects BEAVER’s probability bounds.Source: §F.3.1 · p. 26