BEAVER: An Efficient Deterministic LLM Verifier
Not on the map. Why?
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.
Key facts. Cited by 2 papers in the map (data through 7 Oct 2026). Builds on 39 of its 80 references that are in the map. First posted on arXiv 5 Dec 2025.
Builds on
39 of 80 references.
References · 39
- 2021Training Verifiers to Solve Math Word Problemscited by 9,743
- 2023Universal and Transferable Adversarial Attacks on Aligned Language Modelscited by 2,914
- 2019The Curious Case of Neural Text Degenerationcited by 2,881
- 2019Certified Adversarial Robustness via Randomized Smoothingcited by 1,324
- 2020RealToxicityPrompts: Evaluating Neural Toxic Degeneration in Language Modelscited by 1,235
- 2022Red Teaming Language Models with Language Modelscited by 983
- 2024GSM-Symbolic: Understanding the Limitations of Mathematical Reasoning in Large Language Modelscited by 533
- 2023DecodingTrust: A Comprehensive Assessment of Trustworthiness in GPT Modelscited by 505
- 2025Phi-4-Mini Technical Report: Compact yet Powerful Multimodal Language Models via Mixture-of-LoRAscited by 491
- 2018Efficient Neural Network Robustness Certification with General Activation Functionscited by 439
- 2023Catastrophic Jailbreak of Open-source LLMs via Exploiting Generationcited by 439
- 2023Certifying LLM Safety against Adversarial Promptingcited by 248
27 more
- 2017Formal Verification of Piece-Wise Linear Feed-Forward Neural Networkscited by 241
- 2021Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verificationcited by 224
- 2022Are Large Pre-Trained Language Models Leaking Your Personal Information?cited by 195
- 2023Efficient Guided Generation for Large Language Modelscited by 192
- 2020Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifierscited by 183
- 2018Efficient Formal Safety Analysis of Neural Networkscited by 165
- 2019Branch and Bound for Piecewise Linear Neural Network Verificationcited by 138
- 2023Purple Llama CyberSecEval: A Secure Coding Benchmark for Language Modelscited by 130
- 2018Strong mixed-integer programming formulations for trained neural networkscited by 115
- 2022General Cutting Planes for Bound-Propagation-Based Neural Network Verificationcited by 102
- 2024Guiding LLMs The Right Way: Fast, Non-Invasive Constrained Generationcited by 99
- 2022Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Boundcited by 92
- 2022Certified Training: Small Boxes are All You Needcited by 51
- 2025CRANE: Reasoning with constrained LLM generationcited by 38
- 2021A Review of Formal Methods applied to Machine Learningcited by 33
- 2024IterGen: Iterative Semantic-aware Structured LLM Generation with Backtrackingcited by 28
- 2023Expressive Losses for Verified Robustness via Convex Combinationscited by 23
- 2022Double Sampling Randomized Smoothingcited by 22
- 2020Fast Geometric Projections for Local Robustness Certificationcited by 21
- 2025Code Researcher: Deep Research Agent for Large Systems Code and Commit Historycited by 19
- 2021Make Sure You're Unsure: A Framework for Verifying Probabilistic Specificationscited by 18
- 2023Incremental Verification of Neural Networkscited by 14
- 2024NLP Verification: Towards a General Methodology for Certifying Robustnesscited by 14
- 2023Incremental Randomized Smoothing Certificationcited by 12
- 2025Shh, don't say that! Domain Certification in LLMscited by 7
- 2023Interpreting Robustness Proofs of Deep Neural Networkscited by 3
- 2020The Enron Corpus: Where the Email Bodies are Buried?cited by 2
Built on by
Citing papers per year: 2026: 2.
2 papers.