BEAVER: Un Verificatore LLM Deterministico Efficiente
BEAVER: An Efficient Deterministic LLM Verifier
December 5, 2025
Autori: Tarun Suresh, Nalin Wadhwa, Debangshu Banerjee, Gagandeep Singh
cs.AI
Abstract
Con il passaggio dei grandi modelli linguistici (LLM) da prototipi di ricerca a sistemi di produzione, i professionisti necessitano spesso di metodi affidabili per verificare che gli output del modello soddisfino i vincoli richiesti. Sebbene le stime basate sul campionamento forniscano un'intuizione del comportamento del modello, non offrono garanzie solide. Presentiamo BEAVER, il primo framework pratico per calcolare limiti di probabilità deterministici e solidi sulla soddisfazione dei vincoli per gli LLM. Dato un qualsiasi vincolo semantico chiuso rispetto al prefisso, BEAVER esplora sistematicamente lo spazio di generazione utilizzando nuove strutture di dati basate su trie di token e frontiere, mantenendo limiti provabilmente solidi a ogni iterazione. Formalizziamo il problema della verifica, dimostriamo la solidità del nostro approccio e valutiamo BEAVER su compiti di verifica della correttezza, verifica della privacy e generazione di codice sicuro su molteplici LLM all'avanguardia. BEAVER ottiene limiti di probabilità da 6 a 8 volte più stretti e identifica da 3 a 4 volte più istanze ad alto rischio rispetto ai metodi baseline con budget computazionali identici, consentendo una caratterizzazione precisa e una valutazione del rischio che limiti approssimativi o valutazioni empiriche non possono fornire.
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.