🤖 AI

BEAVER: An Efficient Deterministic LLM Verifier

本論文は、LLM の安全性特性に対する決定論的かつ健全な確率境界を効率的に計算するためにトークントライとフロンティアデータ構造を採用する新たなフレームワーク「BEAVER」を導入し、計算コストの断片でサンプリングベースのベースラインよりもはるかに多くのリスクのあるインスタンスを特定することで、それらを凌駕する性能を示す。

原著者： Tarun Suresh, Nalin Wadhwa, Debangshu Banerjee, Gagandeep Singh

公開日 2026-05-11

📖 1 分で読めます☕ さくっと読める

CC BY 4.0

原著者： Tarun Suresh, Nalin Wadhwa, Debangshu Banerjee, Gagandeep Singh

原論文は CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) でライセンスされています。 ✨ これは以下の論文のAI生成解説です。著者が執筆または承認したものではありません。技術的な正確性については原論文を参照してください。免責事項の全文を読む

非常に賢く創造的なロボットが物語、コード、またはメールを書くことを想像してください。あなたはこう知りたいはずです。「このロボットに質問を投げかけたら、秘密のパスワードを漏らすやウイルスを作成するなど、危険なことを言う確率はどれくらいか？」

現在、人々はこれを解決するために、同じ質問をロボットに千回繰り返し、失敗した回数を数えることで答えようとしています。これは、藁の山から針を見つけるために、盲目的に藁を掴み取るようなものです。針を見逃したり、同じ藁の束を何度も掴み取ったりする可能性があります。これは遅く、費用がかかり、藁の山が安全であるという「保証」も与えてくれません。

「BEAVER」は、このゲームを変える新しいツールです。盲目的に掴み取る代わりに、質問をする前に可能な答えの全図書館を地図化する「超整理された司書」のように機能します。

以下に、簡単な比喩を用いてその仕組みを説明します。

1. 「可能性の樹」（トークントライ）

ロボットの答えが木のように成長すると想像してください。

幹はあなたの質問です。
枝は、ロボットが言うかもしれない最初の数語です。
葉は、最終的な完全な文です。

ほとんどのツールは、一つの枝を選んでその先まで進むだけです。しかし、BEAVER は木全体を見渡します。ロボットが取りうるすべての経路の地図を作成します。

2. 「安全ガード」（フロンティア）

BEAVER には特別なルールがあります。「もし枝が危険そうに見えたら、即座に切り捨てる」というものです。

ロボットが漏洩や有毒な侮辱につながる単語を入力し始めると、BEAVER は文のその冒頭でそれを察知します。
その文を完成させる時間を無駄にしません。「止まれ！この経路は危険だ」と言い、その枝を木から剪定します。
これは、パーティの警備員が、誰かが VIP ルームに入り込んで騒ぎを起こすのを待つのではなく、怪しい人物が入室しようとした瞬間に阻止するのと同じです。

3. 「賢い探検家」（ブランチ・アンド・バウンド）

BEAVER はすべての枝をランダムにチェックするわけではありません。「Max-µ」という賢い戦略を使用します。

枝にはそれぞれ異なる「重み」（確率）があると想像してください。ある経路は非常に起こりやすく、他の経路は稀です。
BEAVER は常に最も重く、最も起こりやすい経路を最初にチェックします。
これらの経路をチェックするにつれて、進行中のスコアを維持します。
- 「安全スコア」（下限）： 木の一部が確実に安全である割合はどれくらいか？
- 「最悪ケーススコア」（上限）： すべての葉をチェックしていなくても、木の一部が危険である可能性がある割合はどれくらいか？

4. 結果：「安全証明書」

「おそらく大丈夫だろう」といった漠然とした推測ではなく、BEAVER は数学的な保証を提供します。

例えば、「少なくとも 90% の答えは安全であると 100% 確信しており、多くても 10% しか危険である可能性はない」と言います。
さらに良いことに、これは従来の「盲目的な推測」手法よりもはるかに高速に実行されます。論文によると、BEAVER は従来の手法よりも2.5 倍から 3 倍多くの危険な例を発見しながら、必要なコンピュータパワーは10 分の 1で済みます。

なぜこれが重要なのか

この論文では、BEAVER を Llama、Qwen、Gemma などの 12 種類の異なる AI モデルと、4 種類の安全性テストで検証しました。

プライバシー： メールアドレスを漏らすか？
セキュリティ： 脆弱なコードを作成するか？
バイアス： ステレオタイプを使用するか？
毒性： 失礼または有害か？

結果、異なるモデルは異なる「性格」を持つことが示されました。あるモデルは数学は得意だが秘密保持は不得意かもしれません。別のモデルは礼儀正しいが、悪いコードを書くかもしれません。BEAVER は、他の手法が見逃すこうした特定の弱点を特定できます。

要約すると： BEAVER は、AI が失敗する可能性のあるすべての経路を体系的に探索し、危険な経路を早期に遮断し、時間と費用を節約しながら、他の手法では見逃してしまうリスクを特定する、正確で数学的に証明された安全性レポートを提供するツールです。

技術的サマリー：BEAVER – 効率的な決定論的 LLM 検証器

1. 問題定義

大規模言語モデル（LLM）が研究プロトタイプから本番システムへ移行するにつれ、実務家は「テールリスク」（個人情報漏洩、安全でないコードの生成、有害コンテンツの作成など、稀だが高影響な失敗）を特定するという重大な課題に直面しています。現在の展開慣行は、ベンチマーク、レッドチーム、サンプリングに基づく推定などのアドホックな経験的手法にほぼ完全に依存しています。これらの手法は直観を提供しますが、モデルの動作に関する確実な保証は提供しません。

LLM の検証における核心的な難しさは、それらが出力シーケンス上の確率分布を誘起する自己回帰モデルであり、単一の決定論的出力を生成するわけではないという性質にあります。既存のニューラルネットワーク検証器は決定論的な入力 - 出力関係を対象としており、自己回帰生成に特有の確率的選択、逐次展開、デコーディング論理の組み合わせを処理できません。その結果、モデルの規模と出力空間の指数関数的な増大により、LLM の確実な検証は不可能であると考えられてきました。

2. 手法

本論文は、LLM が安全性属性を満たすことに対する決定論的かつ確実な確率境界を計算する初の実用的フレームワークであるBEAVERを提示します。このアプローチは、多くの安全性属性が線形時相論理（LTL）形式 $G\phi$ （「決して悪いことが起こらない」ことを主張）に従うという観察に基づいています。そのような属性の場合、違反は早期に検出可能であり、生成空間の積極的な剪定を可能にします。

核心的なデータ構造

BEAVER は、出力空間を体系的に探索するために 2 つの新しいデータ構造を利用します：

トークントライ ( $T$ ): 安全性制約 $\Phi$ を満たすすべての探索済みシーケンスを追跡する接頭辞木です。各ノードは、関連する確率 $\mu(s)$ を持つトークンシーケンス $s$ を表します。トライは、 $\Phi$ の接頭辞閉包の性質を満たすシーケンスのみを格納します。
フロンティア ( $\Psi$ ): トークントライの葉ノードの集合であり、以下に分割されます：
- $\Psi_c$ : 完了シーケンス（<eos> で終了）。
- $\Psi_i$ : 展開対象の不完全シーケンス。

アルゴリズム：ブランチ・アンド・バウンド

BEAVER は、生成された応答が $\Phi$ を満たす確率 $P$ に対する確率境界 $[P_{LB}, P_{UB}]$ を反復的に絞り込むブランチ・アンド・バウンドアルゴリズムを採用します：

初期化: トライはルート（空シーケンス）から開始されます。 $P_{LB} = 0$ 、 $P_{UB} = 1$ とします。
選択: フロンティアから不完全ノード $n[x]$ が選択されます（通常、高確率シーケンスを優先する貪欲なMax- $\mu$ ヒューリスティックを使用します）。
展開: モデルに次のトークンの確率 $P_M(\cdot | p \cdot x)$ を問い合わせます。 $\Phi$ を満たす有効な継続 $x \cdot t$ がトライに追加されます。
更新: 境界が再計算されます：
- $P_{LB}$ は、 $\Psi_c$ 内のすべての完了かつ満足シーケンスの確率の合計です。
- $P_{UB}$ は、 $\Psi_i \cup \Psi_c$ 内のすべてのシーケンスの確率の合計に、剪定質量アキュムレータ ( $M_p$ ) を加えた値です。
確実性: スケーラビリティを確保するために低確率のトークンやシーケンスが剪定された場合（例：top- $p$ または top- $k$ フィルタを介して）、それらの累積確率質量が $M_p$ に加算されます。これにより、剪定の有無にかかわらず、すべての反復において $P_{UB}$ が有効な上限 ( $P_{LB} \le P \le P_{UB}$ ) として維持されます。

アルゴリズムは、最大フォワードパス予算に達したか、またはギャップ $P_{UB} - P_{LB}$ が許容誤差 $\epsilon$ 未満になったときに終了します。

3. 主要な貢献

定式化: 著者らは、LLM のテールリスク評価を $G\phi$ 形式の安全性属性に対する確率境界を計算する検証問題として定式化しました。確実な境界計算を可能にするために、トークントライとフロンティアのデータ構造を導入しました。
BEAVER アルゴリズム: 形式的な確実性証明を備えた新しいブランチ・アンド・バウンド検証アルゴリズムです。これは、真の確率に収束するすべての反復において有効な確率区間を生成します。
経験的検証: このフレームワークは、12 のオープンウェイト指示チューニングモデル（Llama、Qwen、Gemma、Phi、OLMo、Mistral の各ファミリーにまたがる）と4 つの安全性属性で評価されました：
- プライバシー漏洩（Enron メールデータセット）。
- 安全でないコード生成（CyberSecEval）。
- 偏見ステレオタイプ（DecodingTrust）。
- 毒性（RealToxicityPrompts）。

4. 結果

評価により、BEAVER が効率性とリスク検出の両面でサンプリングベースのベースラインを大幅に上回ることが示されました：

リスク検出: BEAVER は、計算予算の1/10（SV 対 1000 回程度のフォワードパスに対し、100 回）で動作する場合でも、サンプリングベースの検証器（SV）よりも2.5 倍から 3.3 倍多いリスク事例を特定します。
テールリスクの表面化: BEAVER は、アドホック評価が安全と宣言するプロンプトの相当な割合において、非自明なテールリスク（違反確率 $\ge 10\%$ ）を証明します。
タスク依存プロファイル: 結果は、リスクプロファイルがタスクに強く依存し、モデルサイズとは明確に相関しないことを明らかにしています。例えば、Qwen3-4B はプライバシーとコードセキュリティにおいて高いリスクを示しますが、毒性については安全であるのに対し、Gemma-3-4B は逆のパターンを示します。
効率性: BEAVER は、 modest なウォールクロック時間（例：Enron で約 9.4 秒、Secure Code で約 18.8 秒）で tight な境界（ $\epsilon=0.01$ ）に収束し、インスタンスあたりのメモリ使用量は 5MB 未満です。
分布的保証: 本論文は、プロンプトごとの保証を統計的手法（Clopper-Pearson）と組み合わせることで、既存の評価手法では提供されていない大規模入力空間に対する分布的安全性保証を提供できることを実証しています。

5. 意義と主張

本論文は、LLM の動作の決定論的検証が、実世界での展開において可能かつ実用的であると主張しています。アドホックなサンプリングを超えて移動することで、BEAVER は単一の数値の安全性スコアでは見えないテールリスクを表面化できる、原理的なリスク評価を可能にします。

著者らは、彼らのアプローチが統計的推定ではなく確実な保証を提供することを強調しています。これは、10% の違反率が本番環境で数千の安全でない出力に転化しうる、安全性が重要なシナリオにおいて重要です。このフレームワークは、LLM のテールリスクを確実かつ実用的に特徴づけることが可能であることを確立し、現在の経験的評価手法に対する厳密な代替案を提供しています。

限界: 現在のフレームワークは接頭辞閉安全性属性（ $G\phi$ ）を対象としていますが、非接頭辞閉属性への拡張も認めています。これは、完全なトークン確率分布へのホワイトボックスアクセスに依存し、選択にはヒューリスティック（Max- $\mu$ ）を使用します。著者らは、より困難な仕様に対しては学習された値関数によって改善可能であると指摘しています。