BEAVER: Um Verificador Determinístico Eficiente para LLM
BEAVER: An Efficient Deterministic LLM Verifier
December 5, 2025
Autores: Tarun Suresh, Nalin Wadhwa, Debangshu Banerjee, Gagandeep Singh
cs.AI
Resumo
À medida que os modelos de linguagem de grande escala (LLMs) transitam de protótipos de pesquisa para sistemas de produção, os profissionais frequentemente necessitam de métodos confiáveis para verificar se as saídas dos modelos satisfazem as restrições exigidas. Embora as estimativas baseadas em amostragem forneçam uma intuição do comportamento do modelo, elas não oferecem garantias sólidas. Apresentamos o BEAVER, o primeiro quadro prático para calcular limites de probabilidade determinísticos e sólidos sobre a satisfação de restrições em LLMs. Dada qualquer restrição semântica com prefixo fechado, o BEAVER explora sistematicamente o espaço de geração utilizando novas estruturas de dados de trie de tokens e fronteira, mantendo limites comprovadamente sólidos a cada iteração. Formalizamos o problema de verificação, provamos a solidez da nossa abordagem e avaliamos o BEAVER em tarefas de verificação de correção, verificação de privacidade e geração de código seguro em vários LLMs de última geração. O BEAVER alcança limites de probabilidade 6 a 8 vezes mais restritos e identifica 3 a 4 vezes mais instâncias de alto risco em comparação com métodos de base sob orçamentos computacionais idênticos, permitindo uma caracterização precisa e uma avaliação de riscos que limites frouxos ou avaliação empírica não podem fornecer.
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.