論文の概要: Containment Verification: AI Safety Guarantees Independent of Alignment

• arxiv url: http://arxiv.org/abs/2605.09045v1
• Date: Sat, 09 May 2026 16:36:45 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-12 23:28:50.042573
• Title: Containment Verification: AI Safety Guarantees Independent of Alignment
• Title（参考訳）: 囲い込み検証:AIの安全保証はアライメントとは無関係
• Abstract要約: 本稿では,エージェントフレームワーク自体の安全性を保証する封じ込め検証を導入する。 ハボックオラクルセマンティクスの下では、AIは型付きアクション空間全体にわたって制約のないオラクルとしてモデル化される。 モデル付き境界イベント、アクション引数、状態上で表現される境界強化性については、普遍的な保証を証明します。
• 参考スコア（独自算出の注目度）: 13.629487815782355
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Agentic frameworks are the software layer through which AI agents act in the world. Existing safety methods intervene on the model and therefore remain conditional on unverifiable properties of learned behavior. We introduce containment verification, which locates safety guarantees in the agentic framework itself. Under havoc oracle semantics, the AI is modeled as an unconstrained oracle ranging over the entire typed action space, and the verified containment layer must enforce the boundary policy for every possible AI output. For boundary-enforceable properties, expressed over modeled boundary events, action arguments, and state, we prove a universal guarantee by forward-simulation refinement and mechanize it in Dafny. We instantiate the paradigm by verifying PocketFlow, a minimalist agentic LLM framework, and use an agentic synthesis pipeline to generate the specification, operational model, and refinement proof under an information barrier against tautological specifications. To our knowledge, this is the first deductive formal verification of an agentic framework, and its guarantee is invariant to model capability over the modeled typed action boundary.
• Abstract（参考訳）: エージェントフレームワークは、AIエージェントが世界で行動するソフトウェアレイヤである。 既存の安全手法はモデルに介入するので、学習行動の検証不可能な性質について条件付きのままである。 本稿では,エージェントフレームワーク自体の安全性を保証する封じ込め検証を導入する。 ハボックオラクルセマンティクスの下では、AIは型付きアクション空間全体にわたって制約のないオラクルとしてモデル化され、検証された封じ込め層はAI出力のすべての境界ポリシーを強制しなければならない。 モデル付き境界事象、行動論、状態上で表現される境界エンフォースブルな性質に対して、前方シミュレーションの洗練により普遍的な保証を証明し、ダフニーでそれを機械化する。 我々は,最小限のエージェント LLM フレームワークである PocketFlow を検証してパラダイムをインスタンス化し,エージェント合成パイプラインを用いて,触覚的仕様に対する情報バリアの下で仕様,操作モデル,精製証明を生成する。 我々の知る限り、これはエージェント・フレームワークの導出的形式的検証としては初めてであり、その保証はモデル化された型付きアクション・バウンダリのモデル能力に不変である。

関連論文リスト

• Formal Verification of Agentic Systems over Operational Data [59.98246281888422]
  大規模言語モデル(LLM)によって駆動されるエージェントシステムは、永続的な運用データを扱う現実世界にますます展開されている。 既存のアプローチはそのようなシステムレベルの保証を提供していません。 本稿では, 1 つの LLM とツールオーケストレーションハーネスからなるエージェントシステムのリレーショナル操作データに対する検証について述べる。
  論文  参考訳（メタデータ） (2026-08-04T13:01:30Z)
• Adversarial Attacks in Multi-Agent LLM Pipelines: Unveiling Structural Vulnerabilities in Agentic AI Architectures [4.053243845971823]
  マルチエージェントLLMパイプラインは、特殊な言語モデルエージェントを構造化し、中間出力をエージェント間で渡して複雑なタスクを解決する。 この設計では、単一のエージェント設定にないセキュリティギャップが導入されている。 この脆弱性は、エージェント間の境界を越える際に、データの明示的な検証を強制するセキュリティプリミティブである境界検証の欠如に起因している、と私たちは主張する。
  論文  参考訳（メタデータ） (2026-08-01T15:35:58Z)
• Operational Hallucination and Safety Drift in AI Agents [0.3823356975862005]
  ツール使用自律エージェントのプランナーとして機能する大規模言語モデル(LLM)は、マルチターン実行における動的信頼性のリスクを導入する。 本稿では,複数のLLM(Safety Drift)とOperational Hallucination(Operational Hallucination)の2つの障害モードを実証的に特徴付ける。 本稿では、インテント-アクション整合性チェック、状態追跡、強制終了プリミティブを組み込んだ、軽量でプラグ&プレイのアーキテクチャ青写真であるAction-Aware Supervision Layerを提案する。
  論文  参考訳（メタデータ） (2026-07-20T17:01:50Z)
• Provably Secure Agent Guardrail [89.79561918065122]
  既存の防衛アーキテクチャは経験的セマンティックガードレールと確率論的大モデル調整器に依存している。 本稿では,論理的推論の基本的制約に基づくエージェントのための新しいセキュリティパラダイムを提案する。
  論文  参考訳（メタデータ） (2026-05-28T02:12:41Z)
• From CRUD to Autonomous Agents: Formal Validation and Zero-Trust Security for Semantic Gateways in AI-Native Enterprise Systems [0.0]
  本稿では,モデルコンテキストプロトコル(MCP)が管理するセマンティックゲートウェイの設計,形式検証,実証評価を提案する。 ゲートウェイは、エンタプライズAPIをセマンティックサーフェスとして再構成する。 このアーキテクチャでは、事前に推論されたセマンティックファイアウォール、決定論的ツールレベルRBAC、アウトオブバンドの暗号化人間対ループの承認を含む3層ゼロトラストセキュリティモデルが導入されている。
  論文  参考訳（メタデータ） (2026-04-28T12:25:06Z)
• CORA: Conformal Risk-Controlled Agents for Safeguarded Mobile GUI Automation [68.53387633351484]
  有害な行為に対する統計的保証を提供するポスト・ポリティクス・プレアクション保護フレームワークであるCORA(Conformal Risk-control GUI Agent)を提案する。 CORAは、安全を選択的行動実行として再定義する:我々は、提案されたステップごとに行動条件リスクを推定するためにガーディアンモデルを訓練する。 このパラダイムを厳格に評価するために、ステップレベルのハーモラベルを持つモバイル安全違反の新しいベンチマークであるPhone-Harmを紹介する。
  論文  参考訳（メタデータ） (2026-04-10T09:41:21Z)
• BarrierSteer: LLM Safety via Learning Barrier Steering [83.12893815611052]
  BarrierSteerは、学習した非線形安全性制約を直接モデルの潜在表現空間に埋め込むことで、安全性を形式化する新しいフレームワークである。 BarrierSteerは、敵の成功率を大幅に低下させ、安全でない世代を減少させ、既存の手法より優れていることを示す。
  論文  参考訳（メタデータ） (2026-02-23T18:19:46Z)
• Agentic Problem Frames: A Systematic Approach to Engineering Reliable Domain Agents [0.0]
  大きな言語モデル(LLM)は、自律的なエージェントへと進化していますが、現在の"フレームワークレス"な開発は、あいまいな自然言語に基づいています。 本研究では,内部モデルインテリジェンスからエージェントと環境間の構造的相互作用に焦点を移すシステム工学フレームワークであるエージェント問題フレーム(APF)を提案する。
  論文  参考訳（メタデータ） (2026-02-22T06:32:32Z)
• Steering Externalities: Benign Activation Steering Unintentionally Increases Jailbreak Risk for Large Language Models [62.16655896700062]
  活性化ステアリングは大規模言語モデル(LLM)の有用性を高める技術である 重要かつ過度に調査された安全リスクを無意識に導入することを示します。 実験によると、これらの介入は強制乗算器として機能し、ジェイルブレイクに新たな脆弱性を発生させ、標準ベンチマークで攻撃成功率を80%以上向上させる。
  論文  参考訳（メタデータ） (2026-02-03T12:32:35Z)
• GAVEL: Towards rule-based safety through activation monitoring [2.337566423505956]
  大規模言語モデル(LLM)は、有害な行動を検出し予防するために、アクティベーションベースの監視とペアになってきています。 既存のアクティベーション安全性アプローチ、幅広い誤用データセットのトレーニング、精度の低下、柔軟性の制限、解釈可能性の欠如。 本稿では,サイバーセキュリティにおけるルール共有プラクティスにインスパイアされた,ルールベースのアクティベーション安全という新たなパラダイムを紹介する。
  論文  参考訳（メタデータ） (2026-01-27T16:31:39Z)
• CaMeLs Can Use Computers Too: System-level Security for Computer Use Agents [60.98294016925157]
  AIエージェントは、悪意のあるコンテンツがエージェントの行動をハイジャックして認証情報を盗んだり、金銭的損失を引き起こすような、インジェクション攻撃に弱い。 CUAのためのシングルショットプランニングでは、信頼できるプランナーが、潜在的に悪意のあるコンテンツを観察する前に、条件付きブランチで完全な実行グラフを生成する。 このアーキテクチャ分離は命令インジェクションを効果的に防止するが、ブランチステアリング攻撃を防ぐには追加の対策が必要であることを示す。
  論文  参考訳（メタデータ） (2026-01-14T23:06:35Z)
• Towards Verifiably Safe Tool Use for LLM Agents [53.55621104327779]
  大規模言語モデル(LLM)ベースのAIエージェントは、データソース、API、検索エンジン、コードサンドボックス、さらにはその他のエージェントなどのツールへのアクセスを可能にすることで、機能を拡張する。 LLMは意図しないツールインタラクションを起動し、機密データを漏洩したり、クリティカルレコードを上書きしたりするリスクを発生させる。 モデルベースセーフガードのようなリスクを軽減するための現在のアプローチは、エージェントの信頼性を高めるが、システムの安全性を保証することはできない。
  論文  参考訳（メタデータ） (2026-01-12T21:31:38Z)
• AI Bill of Materials and Beyond: Systematizing Security Assurance through the AI Risk Scanning (AIRS) Framework [31.261980405052938]
  人工知能(AI)システムの保証は、ソフトウェアサプライチェーンセキュリティ、敵機械学習、ガバナンスドキュメントに分散している。 本稿では,AI保証の運用を目的とした脅威モデルに基づくエビデンス発生フレームワークであるAI Risk Scanning(AIRS)フレームワークを紹介する。
  論文  参考訳（メタデータ） (2025-11-16T16:10:38Z)
• AgentGuard: Runtime Verification of AI Agents [1.14219428942199]
  AgentGuardは、エージェントAIシステムの実行時検証のためのフレームワークである。 動的確率保証(Dynamic Probabilistic Assurance)と呼ばれる新しいパラダイムを通じて、継続的な量的保証を提供する。
  論文  参考訳（メタデータ） (2025-09-28T13:08:50Z)
• Advancing Neural Network Verification through Hierarchical Safety Abstract Interpretation [52.626086874715284]
  我々は、安全でない出力の階層構造を検証する抽象的DNN検証と呼ばれる新しい問題定式化を導入する。 出力到達可能な集合に関する抽象的解釈と推論を活用することにより,形式的検証プロセスにおいて,複数の安全性レベルを評価することができる。 我々の貢献には、新しい抽象的安全性の定式化と既存のアプローチとの関係を理論的に探求することが含まれる。
  論文  参考訳（メタデータ） (2025-05-08T13:29:46Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。