BEAVER: Эффективный детерминированный верификатор больших языковых моделей
BEAVER: An Efficient Deterministic LLM Verifier
December 5, 2025
Авторы: Tarun Suresh, Nalin Wadhwa, Debangshu Banerjee, Gagandeep Singh
cs.AI
Аннотация
По мере перехода больших языковых моделей (БЯМ) от исследовательских прототипов к промышленным системам, практикам часто требуются надежные методы для проверки соответствия выходных данных модели заданным ограничениям. Хотя оценки на основе сэмплирования дают интуитивное представление о поведении модели, они не предоставляют строгих гарантий. Мы представляем BEAVER — первую практическую систему для вычисления детерминированных, строгих вероятностных границ удовлетворения ограничений БЯМ. Для любого семантического ограничения, замкнутого относительно префиксов, BEAVER систематически исследует пространство генераций, используя новые структуры данных — префиксное дерево (trie) и границу (frontier), — сохраняя доказуемо строгие границы на каждой итерации. Мы формализуем задачу верификации, доказываем строгость нашего подхода и оцениваем BEAVER на задачах верификации корректности, проверки конфиденциальности и генерации безопасного кода для нескольких современных БЯМ. BEAVER обеспечивает в 6–8 раз более точные вероятностные границы и выявляет в 3–4 раза больше случаев высокого риска по сравнению с базовыми методами при одинаковых вычислительных затратах, что позволяет проводить точную характеристику и оценку рисков, недоступные для грубых границ или эмпирической оценки.
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.