論文の概要: Agentproof: Static Verification of Agent Workflow Graphs
- arxiv url: http://arxiv.org/abs/2603.20356v1
- Date: Fri, 20 Mar 2026 13:56:20 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-03-24 19:11:38.862915
- Title: Agentproof: Static Verification of Agent Workflow Graphs
- Title（参考訳）: Agentproof: エージェントワークフローグラフの静的検証
- Abstract要約: エージェントフレームワークは、ツール使用の振る舞いを明示的なワークフローグラフとしてエンコードする傾向にある。
本稿では,4つの主要なエージェントフレームワークから統合抽象グラフモデルを自動的に抽出するAgentproofを提案する。
汎用的なモデルチェッカーとは異なり、Agentproofは手動モデリングを必要としない。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Agent frameworks increasingly encode tool-using behavior as explicit workflow graphs, yet safety enforcement remains a runtime concern. These frameworks expose analyzable graph structure through their APIs, enabling pre-deployment static verification of safety properties that runtime guardrails can only check reactively. This paper presents Agentproof, a system that automatically extracts a unified abstract graph model from four major agent frameworks (LangGraph, CrewAI, AutoGen, Google ADK), applies six structural checks with witness trace generation, and evaluates temporal safety policies via a DSL compiled to deterministic finite automata, both statically through a graph x DFA product construction and at runtime over event traces. Unlike general-purpose model checkers, Agentproof requires no manual modeling. In a curated benchmark of 18 author-constructed workflows, 27% of the benchmark contain structural defects (dead-end nodes, unreachable exits) and 55% violate a human-gate policy when enforced, distinct categories that prior work conflates. All 15 temporal policies defined fit within the seven-form DSL fragment, and verification completes in sub-second time for graphs up to 5,000 nodes. The corpus serves as a reproducible benchmark for evaluating static verification tools rather than as a prevalence study; defect rates reflect tool detection capability on a targeted benchmark, not base rates in production systems. Nonetheless, static graph verification complements runtime guardrails by catching topology-level defects that runtime tools miss unless the offending path is exercised.
- Abstract（参考訳）: エージェントフレームワークは、ツール使用の振る舞いを明示的なワークフローグラフとしてエンコードする傾向にある。
これらのフレームワークは分析可能なグラフ構造をAPIを通じて公開し、ランタイムガードレールがリアクティブにチェックできない安全特性の事前デプロイによる静的検証を可能にする。
本稿では,4つの主要なエージェントフレームワーク(LangGraph,CrewAI,AutoGen,Google ADK)から統合抽象グラフモデルを自動的に抽出するシステムであるAgentproofを提案する。
汎用的なモデルチェッカーとは異なり、Agentproofは手動モデリングを必要としない。
著者が構築した18のワークフローのキュレートされたベンチマークでは、ベンチマークの27%が構造上の欠陥(デッドエンドノード、到達不能な出口)を含んでおり、55%が強制された場合、以前の作業が混在する別のカテゴリに違反している。
15の時間ポリシーはすべて7フォームのDSLフラグメントに適合し、検証は5000ノードまでのグラフで秒以下の時間で完了する。
コーパスは、一般的な調査としてではなく、静的検証ツールを評価するための再現可能なベンチマークとして機能する。
それでも静的グラフ検証は,実行時のツールが見逃すトポロジレベルの欠陥をキャッチして,実行時のガードレールを補完するものだ。
関連論文リスト
- Automating Attack Graph Construction for Agentic Pentesting. Towards Neuro-Symbolic Vulnerability Hunting [0.0]
スキャナ出力に接地した論理的アタックグラフは、明示的で監査可能なアタックパス推論を提供する。
MulVALのようなシンボリックフレームワークを現代のセキュリティやエージェントパイプラインに統合するには、スキャナのエビデンスを初期事実に翻訳する必要がある。
本稿では、この相互運用性問題に対処し、Webセキュリティケーススタディにおけるその実現可能性を示す半自動パイプラインを提案する。
論文 参考訳（メタデータ） (2026-09-14T13:13:54Z) - Formal Verification of Agentic Systems over Operational Data [59.98246281888422]
大規模言語モデル(LLM)によって駆動されるエージェントシステムは、永続的な運用データを扱う現実世界にますます展開されている。
既存のアプローチはそのようなシステムレベルの保証を提供していません。
本稿では, 1 つの LLM とツールオーケストレーションハーネスからなるエージェントシステムのリレーショナル操作データに対する検証について述べる。
論文 参考訳（メタデータ） (2026-08-04T13:01:30Z) - ScrambleToolBench: Agents Search Exhaustively Even When Their Own Map Points to the Next Step [74.83535434786145]
ScrambleToolBenchは,行動推論の分離を目的とした対話型端末ベンチマークである。
このベンチマークでは、エージェントがテストとエラーのインタラクションを通じて、隠されたツールの振る舞いを明らかにする必要がある。
現状の言語モデルに対する我々の評価は、初期発見が成功しても頑健な適応にはならないことを示している。
論文 参考訳（メタデータ） (2026-08-03T15:07:46Z) - PhyAgentOS: A Self-Evolving Operating System for Embodied Agents with Decoupled Cognitive Planning and Physical Execution [49.776611937968]
我々は、スケジューリング、検証、メモリ、ベンチマーク、安全性をシステムレベルのサービスとして提供するPhyAgentOSを紹介します。
セッション中心のセッションは、スケジューリング、互換性、監督された実行、エビデンス収集、受け入れの最小単位として、アクションではなくセッションを扱う。
SessionVerifierは、実行終了とセマンティックタスク完了を、成功、失敗、または再計画のエビデンスに基づいて判断する。
ベンチマークはデプロイメントセッションと検証パスを再利用するので、結果は実際の実行に遡る。
論文 参考訳（メタデータ） (2026-07-18T04:46:53Z) - ClawForge: Generating Executable Interactive Benchmarks for Command-Line Agents [59.626170560327274]
textbfClawForgeは、ステートコンフリクト下で実行可能なコマンドラインカテゴリのためのジェネレータベースのベンチマークフレームワークである。
私たちはこのフレームワークをClawForge-Bench(17のシナリオ、6の能力カテゴリ)としてインスタンス化します。
論文 参考訳（メタデータ） (2026-05-13T21:34:08Z) - Willful Disobedience: Automatically Detecting Failures in Agentic Traces [2.2365938060262356]
AgentPexはエージェントトレースを体系的に評価するAIツールである。
エージェントプロンプトとシステム命令から振る舞いルールを抽出し、これらの仕様を使用してコンプライアンスのトレースを自動的に評価する。
我々は、通信、小売、航空会社の顧客サービスにおいて、AgentPexを2ベンチから424のトレースで評価した。
論文 参考訳（メタデータ） (2026-03-25T00:33:39Z) - Dynamic analysis enhances issue resolution [53.50448142467294]
DAIRA(Dynamic Analysis-enhanced Issue Resolution Agent)は、エージェントの推論サイクルに動的解析を組み込む自動修復フレームワークである。
テストトレース駆動の方法論によって駆動されるDAIRAは、軽量モニタを使用して重要なランタイムデータを抽出する。
Gemini 3 Flash Previewを使用すると、DAIRAは新たな最先端(SOTA)パフォーマンスを確立し、SWE-bench Verifiedデータセットで79.4%の解像度を達成する。
論文 参考訳（メタデータ） (2026-03-23T14:48:54Z) - An End-to-End Framework for Functionality-Embedded Provenance Graph Construction and Threat Interpretation [2.0740117800511215]
Auto-Provは、証明グラフベースの異常検出のためのエンドツーエンドフレームワークである。
ログの型をクラスタ化し、プロファイランスエッジとエンティティレベルの情報を効率的に抽出する。
システムレベルの機能コンテキストを、既知および未確認のシステムエンティティの両方に対して推論する。
安定して解釈可能な攻撃サマリーを生成し、システムの進化の下では堅牢である。
論文 参考訳（メタデータ） (2026-03-17T19:40:05Z) - AgentProcessBench: Diagnosing Step-Level Process Quality in Tool-Using Agents [50.481033105867205]
我々はAgentProcessBenchを紹介した。AgentProcessBenchは、現実的なツール拡張トラジェクトリにおけるステップレベルの有効性を評価するための最初のベンチマークである。
ベンチマークは、1,000の多様な軌跡と8,509の人間ラベル付きステップアノテーションと89.1%のアノテーション間合意で構成されている。
探索をキャプチャする3つのラベリングスキームと、ラベルのあいまいさを減らすためのエラー伝搬ルールを備えている。
論文 参考訳（メタデータ） (2026-03-15T16:13:58Z) - FP-Predictor - False Positive Prediction for Static Analysis Reports [5.4164223824711755]
この研究は、静的アプリケーションセキュリティテスト(SAST)レポートを真で偽陽性と予測するために設計されたグラフ畳み込みネットワーク(GCN)モデルを示す。
このモデルは静的解析結果から構築されたコードプロパティグラフ(CPG)を利用して、コード内の構造的および意味的な関係をキャプチャする。
CryptoAPI-Benchベンチマークの評価では、このモデルの実用性を示し、全体の精度は96.6%に達した。
論文 参考訳（メタデータ） (2026-03-11T09:05:39Z) - GraphBit: A Graph-based Agentic Framework for Non-Linear Agent Orchestration [34.588097323063074]
GraphBitは、明示的に決定的に有向非巡回グラフ(DAG)として定義するエンジンオーケストレーションフレームワークである。
インシデントオーケストレーションとは異なり、GraphBitのエージェントは型付き関数として動作し、Rustベースのエンジンはルーティング、状態遷移、ツール呼び出しを制御し、監査性を保証する。
一時的なスクラッチスペース、構造化状態、外部コネクタで構成される3層メモリアーキテクチャは、ステージ間でコンテキストを分離し、長時間実行中のパイプラインにおける推論を低下させるカスケードコンテキストを防止する。
論文 参考訳（メタデータ） (2026-03-08T18:32:28Z) - ESAA: Event Sourcing for Autonomous Agents in LLM-Based Software Engineering [0.0]
本稿では,ESAA(Event Sourcing for Autonomous Agents)アーキテクチャについて述べる。
アーキテクチャは、イベントソーシングパターンにインスパイアされた、認知意図とプロジェクトの状態突然変異を分離する。
2つのケーススタディは、アーキテクチャを検証し、単一エージェントのシナリオを超えたアーキテクチャのスケーラビリティの実証的な証拠を提供する。
論文 参考訳（メタデータ） (2026-02-26T16:45:59Z) - CaMeLs Can Use Computers Too: System-level Security for Computer Use Agents [60.98294016925157]
AIエージェントは、悪意のあるコンテンツがエージェントの行動をハイジャックして認証情報を盗んだり、金銭的損失を引き起こすような、インジェクション攻撃に弱い。
CUAのためのシングルショットプランニングでは、信頼できるプランナーが、潜在的に悪意のあるコンテンツを観察する前に、条件付きブランチで完全な実行グラフを生成する。
このアーキテクチャ分離は命令インジェクションを効果的に防止するが、ブランチステアリング攻撃を防ぐには追加の対策が必要であることを示す。
論文 参考訳（メタデータ） (2026-01-14T23:06:35Z) - BackdoorAgent: A Unified Framework for Backdoor Attacks on LLM-based Agents [58.83028403414688]
大規模言語モデル(LLM)エージェントは、計画、メモリ、ツールの使用を組み合わせた多段階ワークフローを通じてタスクを実行する。
エージェントワークフローの特定のステージに注入されたバックドアトリガーは、複数の中間状態を通して持続し、下流出力に悪影響を及ぼす可能性がある。
LLMエージェントにおけるバックドア脅威を統一したエージェント中心のビューを提供するモジュールおよびステージアウェアフレームワークである textbfBackdoorAgent を提案する。
論文 参考訳（メタデータ） (2026-01-08T03:49:39Z) - AgentArmor: Enforcing Program Analysis on Agent Runtime Trace to Defend Against Prompt Injection [14.522205401511727]
大きな言語モデル(LLM)エージェントは、自然言語推論と外部ツールの実行を組み合わせることで、さまざまな問題を解決するための強力な新しいパラダイムを提供する。
本研究では,エージェントランタイムトレースを解析可能なセマンティクスを用いた構造化プログラムとして扱う新しい知見を提案する。
本稿では,エージェントトレースをグラフ中間表現に基づく構造化プログラム依存表現に変換するプログラム解析フレームワークであるAgentArmorを提案する。
論文 参考訳（メタデータ） (2025-08-02T07:59:34Z) - DRIFT: Dynamic Rule-Based Defense with Injection Isolation for Securing LLM Agents [52.92354372596197]
大規模言語モデル(LLM)は、強力な推論と計画能力のため、エージェントシステムの中心となってきています。
この相互作用は、外部ソースからの悪意のある入力がエージェントの振る舞いを誤解させる可能性がある、インジェクション攻撃のリスクも引き起こす。
本稿では,信頼に値するエージェントシステムのための動的ルールベースの分離フレームワークを提案する。
論文 参考訳（メタデータ） (2025-06-13T05:01:09Z) - SOPBench: Evaluating Language Agents at Following Standard Operating Procedures and Constraints [59.645885492637845]
SOPBenchは、各サービス固有のSOPコードプログラムを実行可能な関数の有向グラフに変換する評価パイプラインである。
提案手法では,各サービス固有のSOPコードプログラムを実行可能関数の有向グラフに変換し,自然言語SOP記述に基づいてこれらの関数を呼び出しなければならない。
我々は18の先行モデルを評価し、上位モデルでさえタスクが困難であることを示す。
論文 参考訳（メタデータ） (2025-03-11T17:53:02Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。