BEAVER: Un Verificador Determinista y Eficiente para Modelos de Lenguaje Grandes

BEAVER: An Efficient Deterministic LLM Verifier

December 5, 2025

Autores: Tarun Suresh, Nalin Wadhwa, Debangshu Banerjee, Gagandeep Singh

cs.AI

Resumen

A medida que los grandes modelos de lenguaje (LLM) transitan de prototipos de investigación a sistemas de producción, los profesionales a menudo necesitan métodos confiables para verificar que las salidas del modelo satisfacen las restricciones requeridas. Si bien las estimaciones basadas en muestreo ofrecen una intuición del comportamiento del modelo, no proporcionan garantías sólidas. Presentamos BEAVER, el primer marco práctico para calcular cotas de probabilidad deterministas y sólidas sobre el cumplimiento de restricciones en LLM. Dada cualquier restricción semántica cerrada por prefijos, BEAVER explora sistemáticamente el espacio de generación utilizando nuevas estructuras de datos de trie de tokens y frontera, manteniendo cotas demostrablemente sólidas en cada iteración. Formalizamos el problema de verificación, demostramos la solidez de nuestro enfoque y evaluamos BEAVER en tareas de verificación de corrección, verificación de privacidad y generación de código seguro en múltiples LLM de última generación. BEAVER logra cotas de probabilidad de 6 a 8 veces más ajustadas e identifica de 3 a 4 veces más instancias de alto riesgo en comparación con métodos base bajo idénticos presupuestos computacionales, permitiendo una caracterización precisa y una evaluación de riesgos que las cotas laxas o la evaluación empírica no pueden proporcionar.

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.