BEAVER: An Efficient Deterministic LLM Verifier

• URL: http://arxiv.org/abs/2512.05439v1
• Date: Fri, 05 Dec 2025 05:34:06 GMT
• Title: BEAVER: An Efficient Deterministic LLM Verifier
• Authors: Tarun Suresh, Nalin Wadhwa, Debangshu Banerjee, Gagandeep Singh,
• Abstract summary: We present BEAVER, the first practical framework for computing deterministic, sound probability bounds on large language models.<n>We formalize the verification problem, prove soundness of our approach, and evaluate BEAVER on correctness verification, privacy verification and secure code generation tasks.
• Score: 11.949243456810263
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: As large language models (LLMs) transition from research prototypes to production systems, practitioners often need reliable methods to verify that model outputs satisfy required constraints. While sampling-based estimates provide an intuition of model behavior, they offer no sound guarantees. We present BEAVER, the first practical framework for computing deterministic, sound probability bounds on LLM constraint satisfaction. Given any prefix-closed semantic constraint, BEAVER systematically explores the generation 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 correctness verification, privacy verification and secure code generation tasks across multiple state of the art LLMs. BEAVER achieves 6 to 8 times tighter probability bounds and identifies 3 to 4 times more high risk instances compared to baseline methods under identical computational budgets, enabling precise characterization and risk assessment that loose bounds or empirical evaluation cannot provide.

Related papers

• Towards Anytime-Valid Statistical Watermarking [63.02116925616554]
  We develop the first e-value-based watermarking framework, Anchored E-Watermarking, that unifies optimal sampling with anytime-valid inference.<n>Our framework can significantly enhance sample efficiency, reducing the average token budget required for detection by 13-15% relative to state-of-the-art baselines.
  arXiv  Detail & Related papers  (2026-02-19T18:32:26Z)
• Fact-Checking with Large Language Models via Probabilistic Certainty and Consistency [7.806516365113592]
  Large language models (LLMs) are increasingly used in applications requiring factual accuracy.<n>While fact-checking can mitigate these errors, existing methods typically retrieve external evidence indiscriminately.<n>We introduce Probabilistic Certainty and Consistency (PCC), a framework that estimates factual confidence.
  arXiv  Detail & Related papers  (2026-01-05T21:57:41Z)
• Random-Set Large Language Models [4.308457163593758]
  Large Language Models (LLMs) are known to produce very high-quality tests and responses to our queries.<n>But how much can we trust this generated text?<n>We propose a novel Random-Set Large Language Model (RSLLM) approach which predicts finite random sets (belief functions) over the token space.
  arXiv  Detail & Related papers  (2025-04-25T05:25:27Z)
• Fast Controlled Generation from Language Models with Adaptive Weighted Rejection Sampling [90.86991492288487]
  evaluating constraint on every token can be prohibitively expensive.<n> LCD can distort the global distribution over strings, sampling tokens based only on local information.<n>We show that our approach is superior to state-of-the-art baselines.
  arXiv  Detail & Related papers  (2025-04-07T18:30:18Z)
• Assessing Correctness in LLM-Based Code Generation via Uncertainty Estimation [0.0]
  We explore uncertainty estimation as a proxy for correctness in LLM-generated code.<n>We adapt two state-of-the-art techniques from natural language generation to the domain of code generation.<n>Our findings indicate a strong correlation between the uncertainty computed through these techniques and correctness.
  arXiv  Detail & Related papers  (2025-02-17T10:03:01Z)
• Unconditional Truthfulness: Learning Unconditional Uncertainty of Large Language Models [104.55763564037831]
  We train a regression model that leverages attention maps, probabilities on the current generation step, and recurrently computed uncertainty scores from previously generated tokens.<n>Our evaluation shows that the proposed method is highly effective for selective generation, achieving substantial improvements over rivaling unsupervised and supervised approaches.
  arXiv  Detail & Related papers  (2024-08-20T09:42:26Z)
• ConU: Conformal Uncertainty in Large Language Models with Correctness Coverage Guarantees [68.33498595506941]
  We introduce a novel uncertainty measure based on self-consistency theory. We then develop a conformal uncertainty criterion by integrating the uncertainty condition aligned with correctness into the CP algorithm. Empirical evaluations indicate that our uncertainty measure outperforms prior state-of-the-art methods.
  arXiv  Detail & Related papers  (2024-06-29T17:33:07Z)
• Cycles of Thought: Measuring LLM Confidence through Stable Explanations [53.15438489398938]
  Large language models (LLMs) can reach and even surpass human-level accuracy on a variety of benchmarks, but their overconfidence in incorrect responses is still a well-documented failure mode. We propose a framework for measuring an LLM's uncertainty with respect to the distribution of generated explanations for an answer.
  arXiv  Detail & Related papers  (2024-06-05T16:35:30Z)
• Data-Driven Distributionally Robust Safety Verification Using Barrier Certificates and Conditional Mean Embeddings [0.24578723416255752]
  We develop scalable formal verification algorithms without shifting the problem to unrealistic assumptions. In a pursuit of developing scalable formal verification algorithms without shifting the problem to unrealistic assumptions, we employ the concept of barrier certificates. We show how to solve the resulting program efficiently using sum-of-squares optimization and a Gaussian process envelope.
  arXiv  Detail & Related papers  (2024-03-15T17:32:02Z)
• Self-Evaluation Improves Selective Generation in Large Language Models [54.003992911447696]
  We reformulate open-ended generation tasks into token-level prediction tasks. We instruct an LLM to self-evaluate its answers. We benchmark a range of scoring methods based on self-evaluation.
  arXiv  Detail & Related papers  (2023-12-14T19:09:22Z)
• Decomposing Uncertainty for Large Language Models through Input Clarification Ensembling [69.83976050879318]
  In large language models (LLMs), identifying sources of uncertainty is an important step toward improving reliability, trustworthiness, and interpretability. In this paper, we introduce an uncertainty decomposition framework for LLMs, called input clarification ensembling. Our approach generates a set of clarifications for the input, feeds them into an LLM, and ensembles the corresponding predictions.
  arXiv  Detail & Related papers  (2023-11-15T05:58:35Z)
• Learning with Safety Constraints: Sample Complexity of Reinforcement Learning for Constrained MDPs [13.922754427601491]
  We characterize the relationship between safety constraints and the number of samples needed to ensure a desired level of accuracy. Our main finding is that compared to the best known bounds of the unconstrained regime, the sample of constrained RL algorithms are increased by a factor that is logarithmic in the number of constraints.
  arXiv  Detail & Related papers  (2020-08-01T18:17:08Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.