BEAVER : Un vérificateur déterministe et efficace pour les grands modèles de langage
BEAVER: An Efficient Deterministic LLM Verifier
December 5, 2025
papers.authors: Tarun Suresh, Nalin Wadhwa, Debangshu Banerjee, Gagandeep Singh
cs.AI
papers.abstract
Alors que les grands modèles de langage (LLM) passent du statut de prototypes de recherche à celui de systèmes en production, les praticiens ont souvent besoin de méthodes fiables pour vérifier que les sorties des modèles satisfont aux contraintes requises. Si les estimations par échantillonnage donnent une intuition du comportement du modèle, elles n'offrent aucune garantie formelle. Nous présentons BEAVER, le premier cadre pratique pour calculer des bornes de probabilité déterministes et formelles sur la satisfaction des contraintes par les LLM. Étant donnée une contrainte sémantique fermée par préfixe, BEAVER explore systématiquement l'espace de génération en utilisant de nouvelles structures de données basées sur un trie de tokens et une frontière, tout en maintenant des bornes prouvablement formelles à chaque itération. Nous formalisons le problème de vérification, prouvons la validité de notre approche et évaluons BEAVER sur des tâches de vérification de la correction, de vérification de la confidentialité et de génération de code sécurisé avec plusieurs LLM de pointe. BEAVER obtient des bornes de probabilité 6 à 8 fois plus serrées et identifie 3 à 4 fois plus d'instances à haut risque que les méthodes de référence, pour un budget de calcul identique, permettant une caractérisation précise et une évaluation des risques que les bornes larges ou l'évaluation empirique ne peuvent fournir.
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.