Evergreen: Efficient Claim Verification for Semantic Aggregates

論文「Evergreen: Efficient Claim Verification for Semantic Aggregates」の詳細な技術的サマリーを以下に示します。

1. 問題定義

セマンティッククエリ処理エンジン（例：Snowflake Cortex AISQL）の台頭により、セマンティック集約はプリミティブな演算子となりました。これにより、大規模言語モデル（LLM）は、タプルの関係性を自然言語の要約や集約値に削減することが可能になります。しかし、これらの LLM によって生成された集約値には、基盤となるデータに根拠のない幻覚的な主張（例：実際はそうではないのに「レビューの大多数は肯定的である」など）が含まれることがよくあります。

これらの主張を検証することは、以下の 4 つの主要な要因により困難です。

1. 規模: 関係性は LLM のコンテキストウィンドウを超えることが多く（数千件のレビュー＝数十万トークン）、処理が困難です。
2. 複雑性: 主張には量化子（すべて、いくつか、大多数）、グループ化、およびグループ間比較が含まれており、セマンティック推論（テキストの理解）とシンボリック推論（カウント/比較）の両方が必要となります。
3. コスト: 総当たり的な検証には、すべてのタプルに対して LLM を呼び出す必要があり、これは過度に高価で遅延を伴います。
4. 説明可能性: ユーザーは、単なる「真/偽」の二値判断ではなく、信頼を得るための引用（証拠）を必要とします。

既存のアプローチはこの課題を包括的に解決できていません。LLM-as-a-judge手法は大規模なコンテキストでは失敗し、*Retrieval-Augmented Generation (RAG)*は独立したタプルにわたる量化された主張に対して困難を抱え、Program-based LLMは最適化の負担を LLM に転嫁することで、最適ではないパフォーマンスをもたらします。

2. 手法：Evergreen システム

Evergreen は、主張の検証をセマンティッククエリ処理タスクとして再定義します。LLM に主張を「チェック」させる代わりに、Evergreen は主張を宣言的なセマンティック検証クエリにコンパイルし、クエリエンジンによって実行します。

A. 主張の分解とコンパイル

1. 分解: LLM が自然言語による集約値を原子的主張に分解し、元のコンテキストを使用して曖昧な参照（例：代名詞）を解決します。
2. 論理的マッピング: 主張は論理構造にマッピングされます。
   • 存在量化/全称量化: $\exists t, \forall t$
   • 基数/比例: $\exists \ge k, \exists \ge \rho$
   • 順序/ネスト: グループのランキングまたはネストされた量化子（例：「すべての場所に 2 件以上の苦情がある」）。
3. クエリ生成: 主張は、標準的な関係演算子（filter, map, aggregate）とセマンティック演算子（プロンプトベースの LLM 呼び出し）を使用した DataFrame 風 API にコンパイルされます。
   • filter(prompt): セマンティックフィルタリング。
   • map(prompt): セマンティック属性の抽出。
   • aggregate: 量化子にマッピングされます（例：bool_or $\to$ $\exists$, count_if $\to$ 基数）。

B. 検証を考慮した最適化

Evergreen は、正しさを維持しつつ LLM 呼び出しを最小化するための特定の最適化を導入します。

1. 早期停止: クエリエンジンはイテレータモデルを使用します。
   • $\exists$（例：「いくつか」）の場合、1 つの証拠が見つかり次第停止します。
   • $\forall$（例：「すべて」）の場合、1 つの反例が見つかり次第停止します。
   • 基数/比例の主張の場合、比較ロジックをプッシュダウンし、残りのタプルに関係なく閾値が数学的に決定された時点で停止します。
2. 関連性ソート: 早期停止を効果的にするため、タプルは関連性によって事前にソートされます。LLM が主張のロジックに基づいて検索クエリを生成し、タプルは埋め込み類似性とキーワードマッチングによってランク付けされます。これにより、「証拠」がストリームの早期に現れるようにします。
3. 信頼度シーケンス（CS）による推定: 早期停止が不可能な場合（例：全称主張が真であることを検証する場合）、Evergreen はAnytime-Valid Confidence Sequencesを使用します。古典的な信頼区間とは異なり、CS は誤り率を増大させることなく継続的な監視を可能にします。システムは、信頼区間が主張が真または偽であることが高い確率で証明された時点でサンプリングを停止します。
4. 汎用最適化:
   • 演算子融合: 複数のセマンティック演算子（例：filter + map）を、タプルあたりの単一の LLM 呼び出しに結合します。
   • 類似性フィルタリング: LLM を呼び出す前に、埋め込みを用いた軽量な事前フィルタで明らかに無関係なタプルを破棄します。
   • プロンプトキャッシング: 異なる主張間で同一のプロンプトに対する LLM の応答を再利用します。

C. セミリング由来による引用

説明を提供するために、Evergreen は引用をデータ由来として扱います。これは第一階述語論理のためのセミリング由来を利用します。

• 各タプルには、主張の式を満たすかどうかを示すトークンが注釈付けられます。
• システムは、結果を正当化する最小のトークンセット（単項式）を導出します。
• 主張が真の場合、証拠の最小セットを返します。偽の場合、反例の最小セットを返します。これにより、説明は簡潔かつ数学的に根拠のあるものになります。

3. 主な貢献

1. 論理的定式化: セマンティック集約における一般的な主張タイプを特定し、それらを明確に定義された論理構造（存在量化、全称量化、基数、比例、順序、ネスト）にマッピングしました。
2. 宣言的コンパイル: 自然言語の主張を宣言的なセマンティック検証クエリにコンパイルする方法を実証し、最適化の負担を LLM からクエリエンジンへ移行させました。
3. 新規最適化: 早期停止、関連性ソート、信頼度シーケンス推定など、検証固有の手法を導入し、コストと遅延を劇的に削減しました。
4. 形式的由来: セミリング由来を適用し、検証結果に対する最小の説明としての引用を形式化しました。
5. 包括的な評価: 実世界の飲食店レビューデータセット上の 16 種類の多様な主張を用いたベンチマークを構築し、システムを評価しました。

4. 実験結果

システムは、3 つの Yelp データセット（それぞれ 1.6k〜1.8k タプル）において、以下のベースラインに対して評価されました：LLM-as-a-judge（base_rm）、Retrieval-Augmented Agent（rag_agent）、および最適化されていない Evergreen（evg_unopt）。

• 品質対コスト:
  • 強力な LLM: 強力な LLM（Opus）を使用した Evergreen は、F1 = 1.00（完全な検証）を達成し、最適化されていないバージョンと比較してコストを3.2 倍、遅延を4.0 倍削減しました。
  • 弱い LLM: 弱い LLM（Llama 8B）を使用した Evergreen は、強い LLM-as-a-judge ベースライン（Opus）よりも F1 スコアで上回りました（0.89 対 0.82）。コストは48 倍低く、遅延は2.3 倍低かったです。
  • RAG エージェントとの比較: 弱い LLM を使用した場合、Evergreen は RAG エージェントの品質と同等かそれ以上であり、コストは63 倍低く、遅延は4.2 倍低かったです。
• アブレーション研究:
  • 早期停止が最も重要な最適化であり、コスト/遅延を6.7 倍削減しました。
  • 推定（CS）とプロンプトキャッシングは、2 倍〜2.7 倍の節約を提供しました。
  • 最適化を無効化すると一般的にパフォーマンスが大幅に低下し、ニューロシンボリックアプローチの必要性が証明されました。
• ロバスト性: より弱いモデルであっても、Evergreen は高い由来精度（0.84〜0.99）を維持し、提供された引用が信頼できることを保証しました。

5. 意義

Evergreen は、セマンティックデータシステムが信頼性を扱う方法において重要な転換点を表しています。

• ニューロシンボリックの相乗効果: LLM のセマンティック理解と、データベースクエリエンジンの厳密な最適化および論理的推論を効果的に組み合わせます。
• スケーラビリティ: 現在、生産環境のデータ分析における LLM の信頼性のある使用を妨げている「コンテキストウィンドウ」と「コスト」のボトルネックを解決します。
• 信頼性: 数学的に根拠のある最小の引用を提供することで、「ブラックボックス」的な LLM 出力を超え、セマンティック集約を監査可能で企業利用に信頼性のあるものにします。
• 将来の方向性: データベースシステムが LLM によって生成された洞察の正確性を自動的に強制する「セマンティック整合性制約」への道を開きます。

要約すると、Evergreen は、主張の検証をクエリ最適化問題として扱うことで、システムが現在の最先端の LLM ベースのアプローチのコストと遅延の一部分で、完全またはほぼ完全な検証品質を達成できることを実証しています。