[2512.05439] BEAVER: An Efficient Deterministic LLM Verifier

Computer Science > Artificial Intelligence arXiv:2512.05439 (cs) [Submitted on 5 Dec 2025 (v1), last revised 7 May 2026 (this version, v2)] Title:BEAVER: An Efficient Deterministic LLM Verifier Authors:Tarun Suresh, Nalin Wadhwa, Debangshu Banerjee, Gagandeep Singh View a PDF of the paper titled BEAVER: An Efficient Deterministic LLM Verifier, by Tarun Suresh and 3 other authors View PDF HTML (experimental) 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. Subjects: Artificial Intelligence (cs.AI); Formal Languages and Automata Theory (cs.FL) Cite as: ar...