技術的概要：MANTRA – SMT 検証済みコンプライアンスベンチマークの合成

問題定義

ツールを利用する大規模言語モデル（LLM）エージェントは、企業運営、医療、旅行予約などの重要な分野でますます展開されており、その行動は厳格な手順マニュアルに準拠する必要があります。これらのエージェントを評価する際の根本的な課題は、入力と出力の間の「ミスマッチ」です。手順規則は通常、人間の解釈のために構造化されていない自然言語で記述される一方、エージェントの行動はツールの呼び出しのシーケンス（実行トレース）として現れます。

既存の評価手法は以下の重大な限界を有しています：

• 手動構築：手作業によるベンチマークの作成は高品質ですが、大規模で複雑なマニュアルや新しい分野には拡張できません。
• LLM ベースのジャッジ：展開は容易ですが、これらのジャッジは長い実行トレースにわたって厳格な時間的制約、事前条件、および禁止された行動を確実に強制することに苦しみ、信頼性の低い評価につながります。
• 結果のみ評価：多くのベンチマークは最終状態のみをチェックし、エージェントが非準拠の手順経路を通じて正しい結果に到達したかどうかを検出できません。

自然言語マニュアルから決定論的かつ機械的に検証可能な採点を提供する、スケーラブルで再現性のあるトレースレベルのコンプライアンスベンチマークを自動的に生成する方法が不足しています。

手法：MANTRA フレームワーク

MANTRA（MANual-to-Test-tRAnslation）は、自然言語の手順ドキュメントとツールスキーマからコンプライアンスベンチマークを自動的に合成するように設計されたフレームワークです。これは、LLM 生成と形式検証を組み合わせた 3 段階のパイプラインを通じて動作します。

1. ドキュメント取り込みとシナリオ生成

• 依存グラフ構築：システムは手順マニュアル（$D$）を取り込み、ノードがコンテンツチャンク（例：段落）を表し、エッジが階層的および参照関係を表す依存グラフ（$G_D$）を構築します。
• カバレッジ駆動サンプリング：タスクの複雑さを制御し、広範なカバレッジを確保するために、MANTRA は $G_D$ から部分グラフ（$G_{DS}$）をサンプリングします。小さく密な部分グラフは単純なシナリオを生み出し、より大きく疎に接続された部分グラフは複数の規則に関与する複雑なシナリオを誘発します。
• ツールの関連性とシナリオ合成：各サンプルに対して、LLM が関連するツール（$T_S$）を識別し、具体的なシナリオ（$\lambda$）を生成します。各シナリオには、自然言語プロンプト（$p_\lambda$）と変数の評価値が含まれます。これには、エージェントを誘導するためにプロンプトで明示される内部状態変数（例：「リクエストは保留中」）も含まれます。

2. チェック生成とワールドモデル作成

コンプライアンスを決定論的に評価するために、MANTRA は各シナリオに対して 2 つの独立したアーティファクトを生成します：

• トレースレベルチェック（$C_\lambda$）：LLM は、必要なツール呼び出し、禁止された呼び出し、および時間的順序（例：check_inventory は assign_warehouse_picker より前に実行されなければならない）を指定するブールチェックのセットを生成します。これらのチェックは具体的な引数値でグラウンディングされます。
• 記号的ワールドモデル（$W_S$）：独立して、LLM は手順規則を状態遷移システムとして表現するワールドモデルを生成します。このモデルは、状態変数、ツールの事前条件、および事後条件を定義する型付きドメイン固有言語（DSL）で表現されます。この抽象化により、複雑な手順ロジックのコンパクトな表現が可能になります。

3. SMT ソルバーによる相互検証

MANTRA の核心的な革新は、生成されたチェックとワールドモデルを相互検証するために充足可能性モジュロ理論（SMT）ソルバー（具体的には Z3）を使用することです。

• 有界モデルチェッキング：$C_\lambda$ と $W_S$ の両方が、トレースホライズン $h$ 上の有界 SMT エンコーディング（$b\Phi_h$）にコンパイルされます。
• 競合検索：システムは 2 種類の不一致を検索します：
  1. 前方競合：チェックを満たすがワールドモデルに違反するトレース（チェックが弱すぎるか、モデルが過度に制限的であることを示す）。
  2. 後方競合：ワールドモデルを満たすが特定のチェックに違反するトレース（チェックが過度に制限的であることを示す）。
• 構造化修復ループ：競合が見つかった場合、MANTRA は修復ループを採用します：
  • ワールドモデル解決：同じサンプルからの複数のシナリオが競合を共有する場合、LLM はワールドモデルに対する共有修復（例：欠落した事前条件の追加）を提案します。
  • チェック解決：競合が解消されない場合、システムは個々のシナリオに対する特定のチェックを特定し、修復します。
  • 決定論的編集：修復は、正当性を保証する型付き編集言語を介して適用され、その後再コンパイルおよび再検証が行われます。
• 人間ループ内：自動化された修復が一定数の反復後に失敗した場合、システムは構造化された人間によるレビューのためにシナリオをフラグ付けし、レビューアーが曖昧さを手動で解決できるようにします。

主要な貢献

1. 自動化パイプライン：自然言語マニュアルとツールスキーマを、制御可能なタスクの難易度と決定論的採点を備えた機械検証可能なベンチマークに変換する完全自動化パイプライン。
2. 2 つのアーティファクト定式化：SMT ソルビングを介して相互検証されるトレースレベルチェックと記号的ワールドモデルの分離。これにより、ベンチマークが受け入れられる前に不一致を自動的に特定および修復でき、人間の介入を最小限に抑えます。
3. ベンチマークスイート：6 つの分野（運営、Sneaky Sasquatch、キャビン安全、小売、航空会社、通信）にわたる 285 の多様なタスクを含む新しいベンチマークスイートの作成。これらのタスクは、最小限の人的努力で最大約 16,000 語の 148 個のツールを持つ手順マニュアルに拡張可能です。
4. 詳細な失敗分析：このフレームワークは、欠落した呼び出し、順序違反、および禁止された行動を区別するエージェントの失敗モードの詳細なデバッグを可能にするトレースレベルチェックを提供します。

結果と評価

著者は、6 つの異なる LLM エージェントを使用して MANTRA フレームワークと生成されたベンチマークを評価しました。

• 検証効率：SMT ベースの相互検証は、生成されたテストケースの大部分を自動的に正常に検証しました。例えば、「運営」分野では、前方および後方改良ラウンドの後、66 件中 63 件の生成されたケースが検証されました。
• エージェントのパフォーマンス：評価により、現在の LLM エージェントは手順コンプライアンスに苦戦していることが明らかになりました。成功率は分野によって大きく異なり、「小売」と「航空会社」（$\tau$-Bench 由来）はドキュメントの長さではなく複雑なツールの使用により特に困難であることが判明しました。
• 失敗モード分析：10,895 件の失敗したチェックの分析により、失敗の 76% が「必要な呼び出しの欠落（義務付けられたツールのスキップ）」または「アンカーの欠落（順序条項の前提条件を実行しないこと）」によるものであることが示されました。
  • 支配的な失敗パターンは「早すぎる書き込み」であり、エージェントは必要な読み取りスタイルのルックアップを実行する前に書き込みスタイルのツールを呼び出しました。
  • モデル Qwen3.6:36B は、「読み取り後に書き込み」という厳格な習慣を維持することで、特に航空会社および小売分野で優れたパフォーマンスを示し、これらの分野で 0% の早すぎる書き込み率を達成しました。
• 既存のベンチマークとの比較：手動構築または LM ジャッジに依存する既存のベンチマークとは異なり、MANTRA は最小限の人的努力で大規模な非構造化ドキュメントや新しい分野に拡張可能な決定論的かつトレースレベルの評価を提供します。

意義と主張

この論文は、ツールを利用するエージェントのためのスケーラブルで信頼性の高いベンチマークを作成するために、自動化されたベンチマーク生成と形式的に根拠のある検証手法を組み合わせる MANTRA の実現可能性を証明していると主張しています。

• 信頼性：SMT ソルバーを使用してチェックをワールドモデルに対して相互検証することで、MANTRA は LLM の幻覚から生じる可能性のある論理的な不一致からベンチマークを解放し、LLM-as-a-judge アプローチと比較して評価結果に対するより高い信頼性を提供します。
• スケーラビリティ：このフレームワークは、手動ベンチマーク作成のスケーラビリティのボトルネックに対処し、任意の分野にわたる複雑な現実世界の手順マニュアル（最大 50 ページ以上）に対するエージェントの評価を可能にします。
• デバッグ機能：トレースレベルチェックの粒度により、研究者は単純な合格/不合格指標を超えて、前提条件のルックアップをスキップする傾向など、エージェント推論における特定の構造的失敗を理解できるようになります。

著者は、MANTRA を安全な行動の単独の保証としてではなく、コンプライアンスが重要な設定でより信頼性の高い AI システムを開発するための重要な構成要素として位置づけており、機械学習と形式検証の間のギャップを埋めています。