Efficient Deterministic LLM Verification with Branch and Bound

As large language models (LLMs) transition from research prototypes to production systems, practitioners need reliable ways to verify model outputs before they are deployed. While sampling-based estimates provide an ad-hoc intuition of model behavior, they offer no sound guarantees. We present BEAVER, the first practi- cal framework for computing deterministic, sound probability bounds on LLM constraint satisfaction. Given a prompt and a constraint, BEAVER systematically explores the model’s output distribution using a token trie and a frontier, maintain- ing provably sound bounds at every iteration. We formalize the LLM verification problem, prove that BEAVER’s bounds are sound and that its selection strategy Max-μ is optimal for verification upto any tolerance. On 3 important safety tasks across 5 popular LLMs, BEAVER certifies up to 7.6× more prompts as risky than a sampling-based verifier while using fewer forward passes, and its per-prompt bounds extend to statistical certificates over distributions of prompts.