Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2512.05439 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866914541375324160 |
|---|---|
| author | Suresh, Tarun Wadhwa, Nalin Banerjee, Debangshu Singh, Gagandeep |
| author_facet | Suresh, Tarun Wadhwa, Nalin Banerjee, Debangshu Singh, Gagandeep |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2512_05439 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | BEAVER: An Efficient Deterministic LLM Verifier Suresh, Tarun Wadhwa, Nalin Banerjee, Debangshu Singh, Gagandeep Artificial Intelligence Formal Languages and Automata Theory 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. |
| title | BEAVER: An Efficient Deterministic LLM Verifier |
| topic | Artificial Intelligence Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2512.05439 |