🤖 AI

SENTINEL: A Multi-Level Formal Framework for Safety Evaluation of Foundation Model-based Embodied Agents

SENTINELは、意味論、計画、および軌跡の各レベルにおいて、形式的な時相論理仕様に対する意味理解、計画、および実行を体系的に検証することにより、基盤モデルベースの身体化エージェントの物理的安全性を保証する、新しいマルチレベルの形式的フレームワークである。

原著者： Simon Sinong Zhan, Philip Wang, Yao Liu, Yiyan Peng, Zinan Wang, Qineng Wang, Zhian Ruan, Xiangyu Shi, Xinyu Cao, Frank Yang, Zhenyang Ni, Kangrui Wang, Ruohan Zhang, Huajie Shao, Manling Li, Qi Zhu

公開日 2026-07-22

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

CC BY 4.0

原著者： Simon Sinong Zhan, Philip Wang, Yao Liu, Yiyan Peng, Zinan Wang, Qineng Wang, Zhian Ruan, Xiangyu Shi, Xinyu Cao, Frank Yang, Zhenyang Ni, Kangrui Wang, Ruohan Zhang, Huajie Shao, Manling Li, Qi Zhu

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

あなたは、家のお手伝いをするために、新しいロボットに教育を行っているところだと想像してください。あなたは、サンドイッチを作らせたり、部屋を片付けさせたり、あるいは単にコップ一杯の水を差し出させたりしたいと考えています。これは、「エンボディド・エージェント（身体性を持つエージェント）」という、現実世界（または仮想世界）を見て、考え、動くことができるロボットの世界です。あなたの曖昧な指示を理解できるほど賢くするために、科学者たちは、人間がこれまでに書いたほぼすべての文章を学習した、巨大で超スマートな脳のような「基盤モデル」を彼らに与えています。しかし、ここに落とし穴があります。ロボットが賢いからといって、それが安全であるとは限らないのです。超知能を持つロボットは、あなたに飲み物を持ってくるための最短ルートを見つけ出すかもしれませんが、もしそのロボットが「ノートパソコンの横に水を注ぐのが良くないこと」を理解していなければ、ショートを引き起こしてしまうかもしれません。大きな疑問は、科学者たちが投げかけている問いです。「どうすれば、この賢いロボットたちが、助けようとする過程で、誤って家を焼き払ったり、私たちの持ち物を壊したりしないようにできるのか？」

ここで、SENTINELと呼ばれる新しいフレームワークが登場します。SENTINELを、ロボットの脳に対する、非常に厳格で超論理的な「安全検査官」だと考えてください。単にロボットに「これは安全だと思いますか？」と聞くのではなく（それは、子供に屋根から飛び降りても大丈夫だと思うか聞くようなものです。なぜなら、彼らは重力を理解していないかもしれないからです）、SENTINELは「時相論理（temporal logic）」という特別な「数学の言語」を使用します。この言語は、何が起こるべきか、何が起こってはならないか、そしてどのような順序で起こるべきかを正確に記述する、一連の破れないルールのセットのようなものです。例えば、「火に注意して」と言う代わりに、SENTINELは「もしコンロがオンであれば、紙は決してコンロから1メートル以内にあってはならない」というルールを記述します。

研究者たちは、空港の3層のセキュリティ・チェックポイントのような、ロボットの安全性を3つの異なる段階でチェックするテストシステムを構築しました。第一に、**セマンティック・レベル（意味レベル）**では、ロボットが与えられた安全ルールを実際に理解しているかどうかを確認します。ロボットは、あなたの言葉（「漂白剤とアンモニアを混ぜるな」）を正しい数学的ルールに翻訳できましたか？第二に、**プラン・レベル（計画レベル）**では、ロボットが動き出す前の「ToDoリスト」を確認します。もし計画が「電子レンジをオンにし、次に金属のスプーンを中に入れる」となっていたら、SENTINELは、生徒がテスト用紙を提出する前に間違いを見つける教師のように、このミスを即座に察知します。最後に、**トラジェクトリー・レベル（軌跡レベル）**では、シミュレーション内でロボットが実際にタスクを実行する様子を観察します。たとえ計画自体は問題なく見えても、ロボットの腕が大きく振れすぎて花瓶を倒してしまったかもしれません。SENTINELは、リアルタイムで何も問題が起きないよう、ロボットの動作という「映画」全体を見守ります。

実験において、チームはデジタル上のキッチンやリビングルームにいる仮想ロボットに対してこのシステムをテストしました。その結果、強力で大きなAIモデルは「どのように」タスクを行うかを考えるのには優れていますが、これらの厳格な数学的ルールでチェックされない限り、安全性の詳細を見落としがちであることが分かりました。SENTINELが、ロボットに対して「なぜその計画が安全ではないのか」について具体的なフィードバックを与えたとき（例えば、金属のスプーンが電子レンジに入れられようとしている正確な瞬間を指摘するなど）、ロボットは、単に別のAIから「それは安全ではない」と言われるよりも、ずっと上手く間違いを修正して学習することができました。この研究は、ロボットを真に安全な助手にするためには、推測から脱却し、ロボットの思考プロセスのあらゆるステップにおいて、これらの精密な数学的安全性チェックを使用する必要があることを示唆しています。それは単に賢いことではなく、慎重であることであり、SENTINELはロボットにその両方を教えるためのツールなのです。

技術要約: SENTINEL

問題提起

基礎モデル（Foundation Models: FMs）の身体性を持つエージェントへの統合は、プランニングや人間との相互作用における能力を拡大させた一方で、安全性のリスクを増大させている。FMベースのエージェントに対する既存の評価ベンチマークは、主にタスク完了メトリクス（例：成功率）に焦点を当てており、物理的な危険を単なるタスク失敗として扱うことが多く、独立した安全性違反として扱わない。現在の安全性評価手法は、ヒューリスティックなルールや主観的なFMベースの判定器（LLM-as-Judge）に大きく依存しており、これらは厳密な定義を欠いており、エージェントのパイプラインにおける異なる段階（意味論的な誤解、不安全なプラン生成、または不安全な物理的実行）で発生する失敗を区別できていない。さらに、これらの手法は、どのレベルで安全性違反が起因しているのかを特定することができない。

手法

著者らは、SENTINEL（Safety EvaluatioN framework with Temporal logics for INterpretable Embodied foundation modeL-based agents）を提案する。これは、物理的な安全性を時相論理仕様に接地させるマルチレベルの形式的フレームワークである。本フレームワークはシミュレーション環境（VirtualHomeおよびAI2-THOR）内で動作し、エージェントを以下の3つの進行的なレベルで評価する。

1. 形式的安全仕様

SENTINELは、自然言語の安全性制約を時相論理式、具体的には線形時相論理（LTL）および計算樹論理（CTL）へとエンコードする。

状態不変量（State Invariants）: すべての時刻において不安全な状態を禁止する制約（例：衝突回避のための $G(\neg p)$ ）。
順序制約（Ordering Constraints）: 適切なアクションのシーケンスを強制する制約（例：「最終的に電源を切る」のための $G(p \to F q)$ ）。
分類: 安全性ルールは状態不変量と順序制約に分類され、シミュレーション内のオブジェクト特性から導出された原子命題にマッピングされる。

2. マルチレベル評価パイプライン

本フレームワークは、失敗を段階的にフィルタリングし、違反を特定するための3段階のパイプラインを採用している。

意味論レベルの評価（Semantic-Level Evaluation）:
- 目的: 自然言語の安全性要件を形式的なLTL式へと翻訳するFMの能力を評価する。
- 手法: エージェントに安全性制約をプロンプトとして与え、候補となるLTL式を生成させる。これらは、構文チェックおよび意味論的等価性検証（Büchiオートマトンと言語包含関係による）を用いて、グラウンドトゥルース（正解）のLTL仕様と比較される。
- 出力: 構文エラー、意味論的な非等価性、および解釈の成功に関するメトリクス。
プランレベルの評価（Plan-Level Evaluation）:
- 目的: 実行前に、高レベルのアクションプランおよびサブゴールをLTL制約に対して検証する。
- 手法: エージェントは高レベルのプラン（マイルストーン・サブゴール）を生成する。このプランは、不安全な記号的順序や欠落した前提条件を検出するためにLTL式に対してチェックされる。アクション空間内でのプランの実行可能性を検証するために、幅優先探索（BFS）が使用される。
- 出力: タスク目標は満たすものの、安全性制約に違反する不安全なプランの特定。
軌跡レベルの評価（Trajectory-Level Evaluation）:
- **目的、分岐する結果や環境のダイナミクスを考慮して、プランの物理的な実行を評価する。
- 手法: 高レベルのプランに基づき、シミュレータから複数の実行軌跡をサンプリングする。これらの軌跡は計算樹（Computation Tree） ( $T$ ) に統合される。分岐時間の特性を評価するために、LTLからCTLへと安全性要件がリフトアップされる。
- 検証: CTLモデルチェッカーが、ツリーに対して特性（例：「すべてのパスが常に $\phi$ を満たす」ための $AG \phi$ ）を検証する。
- 出力: 実行依存の違反の検出、および反例パス（失敗の原因となる特定の状態やシーケンス）の生成。

3. フィードバック駆動型のリファインメント

SENTINELは、軌跡レベルのチェック中に生成された反例を利用して、エージェントに検証可能なフィードバックを提供する。このフィードバックループにより、エージェントは基礎となるエージェントアーキテクチャを変更することなく、安全性を向上させるためにプランを反復的に洗練させることが可能となる。

主な貢献

形式的かつ解釈可能な安全性仕様: 本研究は、直感的な安全性要件をLTLおよびCTLに接地させることで、ヒューリスティックな判断ではなく、明示的な分類（状態不変量、時間的依存関係）と形式的検証を可能にする。
統一されたマルチレベル形式安全性評価: SENTINELは、意味論的解釈、プラン生成、および物理的実行の全過程にわたって、安全性を段階的に形式的に評価する初のフレームワークである。この設計により、失敗を特定の段階（理解、推論、または実行）へと局所化できる。
クロスレベルの経験的分析: 著者らは、タスクに安全性に焦点を当てた要件を追加した上で、VirtualHomeおよびAI2-THORにSENTINELを適用している。彼らは、安全性違反が異なるレベル（例：意味論的な誤解 vs 低レベルのコントローラーエラー）から生じることを示し、形式的評価がタスク成功のみに焦点を当てたベンチマークでは見えない失敗モードを露呈させることを実証している。

実験結果

著者らは、複数のクローズドソースモデル（GPT-5, Claude-Opus, Gemini）およびオープンソースモデル（DeepSeek, Qwen, Mistral, Llama）、ならびに視覚言語モデル（VLM）を評価した。

意味論レベル: 大規模なモデルは、小規模なオープンソースモデルと比較して、自然言語からLTLへの翻訳において著しく高い性能を示した。しかし、強力なモデルであっても、グローバルな禁止事項と比較して、条件付きの禁止事項には苦戦した。
プランレベル: 意味論的等価率が高いモデルは、一般にプランレベルで高い安全性率を維持した。しかし、明示的な安全性ガイダンス（LTLプロンプト）を追加しても安全性メトリクスは改善されたが、すべての違反を排除することはできなかった。
軌跡レベル:
- LLM vs VLM: VLMベースのエージェントは、視覚的な接地が物理的な危険の検出を助けるため、テキストのみのLLMよりも高い安全性率を達成した。しかし、VLMはしばしばタスク成功率が低くなる傾向があり、これは安全性と能力のトレードオフを示唆している。
- 実行失敗: プランレベルから軌跡レベルの結果にかけて、「成功かつ安全（Success & Safety）」の著しい低下が観察された。これは、多くの失敗が低レベルのアクション引数やコントローラーにおける安全性メカニズムの欠如に起因していることを示唆している。
安全性向上: リファインメントループの実験において、SENTINELの検証可能な反例フィードバックは、LLM-as-Judgeのベースラインよりも大幅に大きな安全性メトリクスの改善（約2倍の改善）をもたらした一方で、同等のタスク成功率の向上を維持した。分析によれば、LLM-as-Judgeベースラインは真に不安全な軌跡を見逃すことが多く（ある研究では83%の見逃し率）、SENTINELの形式的チェックの方が信頼性が高いことが示された。
効率性: 統合された計算樹に対するCTLベースの検証は、独立したLTLチェックよりも効率的であることが判明した。この高速化は、軌跡の数が増えるにつれて顕著になった。

意義と主張

本論文は、SENTINELが、基礎モデルベースの身体性エージェントの安全性を体系的に評価するための厳密な基盤を提供すると主張している。ヒューリスティックまたは主観的な判断を超えて、本フレームワークは以下を提供する：

局所化: 安全性の失敗が、指示の誤解、不安全なプランの生成、またはアクションの不安全な実行のいずれに起因するかを特定する能力。
実行可能なフィードバック: リファインメントループを通じて意味のある安全性向上を駆動できる、検証可能な反例の生成。
スケーラビリティ: サンプリングされた計算樹に対するCTLの使用は、複雑な物理環境における完全な状態モデルチェックの実現不可能性に対し、実用的なトレードオフを提供し、スケーラブルな経験的違反検出を実現する。

著者らは、SENTINELはサンプリングされた軌跡から組み立てられた有限の計算樹に基づいて動作するため、認定された検証ではなく経験的な検出を提供するものであると強調している。サンプル数が不十分な場合に違反が見逃される可能性は残るが、このアプローチは統計的モデルチェックに近いものであり、ブラックボックスである基礎モデルの性質と物理環境の複雑さを考慮すると、必要不可欠なものであると主張している。本フレームワークは、検証可能な安全性ベンチマークおよび安全性に配慮した強化学習報酬への一歩として提示されている。