BEAVER: An Efficient Deterministic LLM Verifier

TL;DR

BEAVER is a practical framework that provides deterministic, sound probability bounds for verifying safety properties of large language models, improving detection of risky outputs efficiently.

Contribution

It introduces novel Token trie and Frontier data structures for systematic exploration, enabling sound bounds and better risk detection compared to baselines.

Findings

BEAVER identifies 2-3x more risky instances than baselines.

It operates at 1/10 of the compute budget of existing methods.

BEAVER effectively surfaces tail risks missed by other evaluation approaches.

Abstract

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.