BEAVER: Een Efficiënte Deterministische LLM-Verificateur
BEAVER: An Efficient Deterministic LLM Verifier
December 5, 2025
Auteurs: Tarun Suresh, Nalin Wadhwa, Debangshu Banerjee, Gagandeep Singh
cs.AI
Samenvatting
Naarmate grote taalmodellen (LLM's) de overgang maken van onderzoeksprototypes naar productiesystemen, hebben beoefenaars vaak behoefte aan betrouwbare methoden om te verifiëren dat modeluitvoeren aan vereiste beperkingen voldoen. Hoewel op steekproeven gebaseerde schattingen een indicatie geven van het modelgedrag, bieden zij geen sluitende garanties. Wij presenteren BEAVER, het eerste praktische raamwerk voor het berekenen van deterministische, sluitende waarschijnlijkheidsgrenzen voor de beperkingsvoldoening van LLM's. Gegeven een willekeurige prefix-gesloten semantische beperking, verkent BEAVER systematisch de gegenereerde ruimte met behulp van nieuwe gegevenstructuren zoals de token-trie en de frontier, waarbij bij elke iteratie bewezen sluitende grenzen worden aangehouden. Wij formaliseren het verificatieprobleem, bewijzen de sluitendheid van onze aanpak en evalueren BEAVER op taken voor correctheidsverificatie, privacyverificatie en veilige codegeneratie voor meerdere state-of-the-art LLM's. BEAVER bereikt 6 tot 8 keer smallere waarschijnlijkheidsgrenzen en identificeert 3 tot 4 keer meer hoog-risico gevallen in vergelijking met baseline-methoden onder identieke rekenbudgetten, waardoor een precieze karakterisering en risicobeoordeling mogelijk wordt die losse grenzen of empirische evaluatie niet kunnen bieden.
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.