BEAVER：効率的な決定論的大規模言語モデル検証器

要旨

大規模言語モデル（LLM）が研究プロトタイプから実用システムへ移行するにつれ、実務家はモデル出力が要求される制約を満たすことを検証する信頼性の高い手法を必要とすることが多い。サンプリングに基づく推定値はモデル挙動の直感を提供するが、確固たる保証は提供しない。本論文では、LLMの制約充足に関する確定的で健全な確率限界を計算する初の実用的フレームワークBEAVERを提案する。任意の接頭辞閉鎖された意味的制約が与えられた下で、BEAVERは新規のトークントライとフロンティアデータ構造を用いて生成空間を体系的に探索し、反復毎に数学的に健全な限界を維持する。我々は検証問題を形式化し、手法の健全性を証明し、複数の最先端LLMにおける正当性検証、プライバシー検証、セキュアコード生成タスクで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.

BEAVER：効率的な決定論的大規模言語モデル検証器

BEAVER: An Efficient Deterministic LLM Verifier

要旨

Support