# BEAVER: An Efficient Deterministic LLM Verifier

arXiv: https://arxiv.org/abs/2512.05439 · HTML: https://mlsanity.com/paper/2512.05439/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 39 of its 80 references that are in the map.
- First posted on arXiv 5 Dec 2025.

## Builds on (most cited first, 30 of 39)

- [Training Verifiers to Solve Math Word Problems](https://mlsanity.com/paper/2110.14168/) (2021)
- [Universal and Transferable Adversarial Attacks on Aligned Language Models](https://mlsanity.com/paper/2307.15043/) (2023)
- [The Curious Case of Neural Text Degeneration](https://mlsanity.com/paper/1904.09751/) (2019)
- [Certified Adversarial Robustness via Randomized Smoothing](https://mlsanity.com/paper/1902.02918/) (2019)
- [RealToxicityPrompts: Evaluating Neural Toxic Degeneration in Language Models](https://mlsanity.com/paper/2009.11462/) (2020)
- [Red Teaming Language Models with Language Models](https://mlsanity.com/paper/2202.03286/) (2022)
- [GSM-Symbolic: Understanding the Limitations of Mathematical Reasoning in Large Language Models](https://mlsanity.com/paper/2410.05229/) (2024)
- [Phi-4-Mini Technical Report: Compact yet Powerful Multimodal Language Models via Mixture-of-LoRAs](https://mlsanity.com/paper/2503.01743/) (2025)
- [DecodingTrust: A Comprehensive Assessment of Trustworthiness in GPT Models](https://mlsanity.com/paper/2306.11698/) (2023)
- [Catastrophic Jailbreak of Open-source LLMs via Exploiting Generation](https://mlsanity.com/paper/2310.06987/) (2023)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Certifying LLM Safety against Adversarial Prompting](https://mlsanity.com/paper/2309.02705/) (2023)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification](https://mlsanity.com/paper/2103.06624/) (2021)
- [Are Large Pre-Trained Language Models Leaking Your Personal Information?](https://mlsanity.com/paper/2205.12628/) (2022)
- [Efficient Guided Generation for Large Language Models](https://mlsanity.com/paper/2307.09702/) (2023)
- [Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers](https://mlsanity.com/paper/2011.13824/) (2020)
- [Efficient Formal Safety Analysis of Neural Networks](https://mlsanity.com/paper/1809.08098/) (2018)
- [Branch and Bound for Piecewise Linear Neural Network Verification](https://mlsanity.com/paper/1909.06588/) (2019)
- [Purple Llama CyberSecEval: A Secure Coding Benchmark for Language Models](https://mlsanity.com/paper/2312.04724/) (2023)
- [Strong mixed-integer programming formulations for trained neural networks](https://mlsanity.com/paper/1811.08359/) (2018)
- [General Cutting Planes for Bound-Propagation-Based Neural Network Verification](https://mlsanity.com/paper/2208.05740/) (2022)
- [Guiding LLMs The Right Way: Fast, Non-Invasive Constrained Generation](https://mlsanity.com/paper/2403.06988/) (2024)
- [Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Bound](https://mlsanity.com/paper/2205.00263/) (2022)
- [Certified Training: Small Boxes are All You Need](https://mlsanity.com/paper/2210.04871/) (2022)
- [CRANE: Reasoning with constrained LLM generation](https://mlsanity.com/paper/2502.09061/) (2025)
- [A Review of Formal Methods applied to Machine Learning](https://mlsanity.com/paper/2104.02466/) (2021)
- [IterGen: Iterative Semantic-aware Structured LLM Generation with Backtracking](https://mlsanity.com/paper/2410.07295/) (2024)
- [Expressive Losses for Verified Robustness via Convex Combinations](https://mlsanity.com/paper/2305.13991/) (2023)
- [Double Sampling Randomized Smoothing](https://mlsanity.com/paper/2206.07912/) (2022)

## Built on by (most cited first, 2 of 2)

- [Decoding as Optimisation on the Probability Simplex: From Top-K to Top-P (Nucleus) to Best-of-K Samplers](https://mlsanity.com/paper/2602.18292/) (2026)
- [SymboUQ: Symbolic Uncertainty Quantification for Spatial Reasoning in LLMs](https://mlsanity.com/paper/2608.00417/) (2026)

## Abstract (arXiv)

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.