BEAVER: Ein effizienter deterministischer LLM-Verifizierer
BEAVER: An Efficient Deterministic LLM Verifier
December 5, 2025
papers.authors: Tarun Suresh, Nalin Wadhwa, Debangshu Banerjee, Gagandeep Singh
cs.AI
papers.abstract
Mit dem Übergang großer Sprachmodelle (LLMs) von Forschungsexemplaren zu Produktionssystemen benötigen Praktiker oft zuverlässige Methoden, um zu überprüfen, ob Modellausgaben erforderliche Randbedingungen erfüllen. Während stichprobenbasierte Schätzungen ein intuitives Verständnis des Modellverhaltens liefern, bieten sie keine soliden Garantien. Wir stellen BEAVER vor, den ersten praktischen Rahmen zur Berechnung deterministischer, solider Wahrscheinlichkeitsschranken für die Erfüllung von LLM-Randbedingungen. Für jede präfixgeschlossene semantische Bedingung erkundet BEAVER systematisch den Generierungsraum unter Verwendung neuartiger Trie- und Frontier-Datenstrukturen für Tokens und bewahrt in jeder Iteration nachweislich solide Schranken. Wir formalisieren das Verifikationsproblem, beweisen die Solidität unseres Ansatzes und evaluieren BEAVER an Aufgaben zur Korrektheitsverifikation, Privatsphärenverifikation und sicheren Codegenerierung über mehrere state-of-the-art LLMs hinweg. BEAVER erreicht 6- bis 8-mal engere Wahrscheinlichkeitsschranken und identifiziert im Vergleich zu Baseline-Methoden bei identischen Rechenbudgets 3- bis 4-mal mehr Hochrisikoinstanzen, was eine präzise Charakterisierung und Risikobewertung ermöglicht, die lockere Schranken oder empirische Evaluation nicht leisten können.
English
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.