論文の概要: Methods for Formal Verification of Agent Skills: Three Layers Toward a Mechanically Checkable Capability-Containment Proof
- arxiv url: http://arxiv.org/abs/2605.23951v1
- Date: Sat, 09 May 2026 19:27:38 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-06-01 02:55:42.969625
- Title: Methods for Formal Verification of Agent Skills: Three Layers Toward a Mechanically Checkable Capability-Containment Proof
- Title（参考訳）: エージェントスキルの形式的検証方法:機械的に確認可能な能力証明に向けての3つの層
- Authors: Alfredo Metere,
- Abstract要約: LLM駆動のランタイムによってどのようにスキルが消費されるかに忠実なスキル行動に関する正確なセマンティクスを提供します。
本稿では,定式化や定式化によるスキル向上を両立させる構成可能な3つの手法を提案する。
これら3つのメソッドに加えて、バンドルプロデューサと再チェッカーは、オープンソースエンクロードフレームワークのゼロ依存JavaScriptモジュールとして出荷される。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: The companion paper introduced a four-level verification lattice on agent-skill manifests (unverified, declared, tested, formal) and left the top level aspirational. This paper closes that gap. We give a precise semantics for skill behaviour faithful to how a skill is consumed by an LLM-driven runtime (a deterministic script-side reachable through a non-deterministic LLM-side), state the verification problem as a capability-containment property over that semantics, and present three composable methods that together raise a skill from declared or tested to formal: (1) sound static capability-containment analysis of the script-side via abstract interpretation over a small effect lattice; (2) a refinement type system for tool-call envelopes that mechanically rejects any call whose statically-inferred capability is not in the manifest's declared set; (3) SMT-bounded model checking against the parent paper's biconditional correctness criterion, with the bound chosen so any counter-example fitting the runtime's transaction-buffer horizon is exhibited as a concrete trace. We prove the three layers composed soundly cover the parent paper's threat model modulo a single residual (the LLM's freedom to refuse to act) that the parent paper's runtime biconditional catches at session boundary. The methods reuse existing well-engineered tools (Z3, Semgrep, CodeQL, refinement-type checkers, mechanised proof assistants) rather than asking operators to build new ones, and the proof-carrying artifact extends the existing SKILL.md convention. All three methods plus the bundle producer and re-checker ship as zero-dependency JavaScript modules in the open-source enclawed framework (https://github.com/metereconsulting/enclawed; project page https://www.enclawed.com/), with 53 unit tests and an end-to-end CLI demo on a sample skill.
- Abstract（参考訳）: 共用論文ではエージェントスキルマニフェスト(未検証、宣言、テスト、フォーマル)に4段階の検証格子を導入し、トップレベルの仮定を残した。
この論文はそのギャップを埋める。
LLM駆動型ランタイム(非決定論的LCM側で到達可能な決定論的スクリプト側)がいかにスキルを消費するかに忠実なスキルのセマンティクスを提示し、そのセマンティクス上での検証問題を機能完備性として記述し、そのセマンティクス上で宣言されたまたはテストされたスキルを形式的に引き上げる3つの構成可能なメソッドを提示する。
我々は,親紙の脅威モデルを構成する3つの層が,親紙のランタイムバイコンディショナルがセッション境界でキャッチする単一残差(LLMの動作を拒否する自由)を変調することを示した。
これらのメソッドは、演算子に新しいツールを構築するように求めるのではなく、既存のよく設計されたツール(Z3、Semgrep、CodeQL、精細化型チェッカー、機械化された証明アシスタント)を再利用し、証明するアーティファクトは既存のSKILL.md規約を拡張している。
オープンソースフレームワーク(https://github.com/metereconsulting/enclawed; project page https://www.enclawed.com/)では、53のユニットテストと、サンプルスキルに関するエンドツーエンドのCLIデモが提供されている。
関連論文リスト
- AgentSecBench: Measuring Prompt Injection, Privacy Leakage, and Tool-Use Integrity in LLM Agents [0.2864713389096699]
本稿では,AgentSecBenchを,この問題に対する正式なセキュリティフレームワークの実証的なインスタンス化として紹介する。
3つのゲーム・インストラクション・インテリジェンス・インテリジェンス・インテリジェンス・インテリジェンス・インテリジェンス・インテリジェンス・インテリジェンス・インテリジェンス(英語版)・インテリジェンス・インテリジェンス・インテリジェンス・インテリジェンス・インテリジェンス(英語版)・インテリジェンス・インテリジェンス・インテリジェンス・インテリジェンス・インテリジェンス・インテリジェンス・インテリジェンス(英語版)を定めている。
これは、承認された観察と能力に対するプロジェクションとしてのアプリケーションポリシーを表し、プロジェクションの即時アノテーションとプロジェクションの強化を区別し、敵のアドバンテージと、防衛が生成前に関連するモデル可視チャネルを閉鎖するかどうかを計測する。
論文 参考訳（メタデータ） (2026-05-25T18:53:22Z) - PRIMA: Operational Patterns for Resilient Multi-Agent Research with Verifiable Identity and Convergent Feedback [0.0]
PRIMAは、複数時間にわたる協調型マルチエージェント研究システムとして運用されている。
主なコントリビューションは、生存可能な障害モードのための3つの運用パターンである。
グラフ同型ケーススタディは、生成されたアーティファクトのアーキテクチャ的クレームを根拠にしている。
論文 参考訳（メタデータ） (2026-05-23T23:27:46Z) - Agentic Model Checking [12.832868209928039]
本稿では,LLMエージェントと境界モデルチェックバックエンドを結合するパラダイムを提案する。
我々は、BMC-Agentのアプローチをインスタンス化し、CとRustのLLM生成カーネルおよびコンパイラコード上で評価する。
論文 参考訳（メタデータ） (2026-05-20T17:25:52Z) - Securing LLM Agents Need Intent-to-Execution Integrity [49.490963596514185]
我々は, LLMエージェントの確保には, エージェントの実行がユーザの意図を忠実に反映した場合に規定するエンドツーエンドの正当性を定義する必要があると主張している。
LLMエージェントはコンパイラと構造的に類似しており、セキュリティ違反はユーザ意図を保存しない誤った実行に対応する。
emphTool整合性、emph命令整合性、emphJudgment整合性、emphData整合性。
論文 参考訳（メタデータ） (2026-05-16T12:53:31Z) - Proof-Carrying Certificates for LLM Pipelines: A Trust-Boundary Architecture [0.0]
本稿では,大規模言語モデルを取り巻く決定論的構造化計算を検証するためのフレームワークを提案する。
リーン4の信頼境界アーキテクチャを,現代的なLLMパイプラインの汎用インターフェースに拡張しています。
論文 参考訳（メタデータ） (2026-05-13T12:01:41Z) - Skills as Verifiable Artifacts: A Trust Schema and a Biconditional Correctness Criterion for Human-in-the-Loop Agent Runtimes [0.0]
私たちは、スキルが検証されるまで、信頼されたコードであると主張する。
スキル検証がなければ、ループ内の人間ゲートは、あらゆる不可逆呼び出しに発射されなければならない。
すべてのスキルマニフェストに明確な検証レベルを含む信頼スキーマを提供します。
論文 参考訳（メタデータ） (2026-05-01T05:53:05Z) - Rethinking Testing for LLM Applications: Characteristics, Challenges, and a Lightweight Interaction Protocol [83.83217247686402]
大言語モデル(LLM)は、単純なテキストジェネレータから、検索強化、ツール呼び出し、マルチターンインタラクションを統合する複雑なソフトウェアシステムへと進化してきた。
その固有の非決定主義、ダイナミズム、文脈依存は品質保証に根本的な課題をもたらす。
本稿では,LLMアプリケーションを3層アーキテクチャに分解する: textbftextitSystem Shell Layer, textbftextitPrompt Orchestration Layer, textbftextitLLM Inference Core。
論文 参考訳（メタデータ） (2025-08-28T13:00:28Z) - Towards Copyright Protection for Knowledge Bases of Retrieval-augmented Language Models via Reasoning [58.57194301645823]
大規模言語モデル(LLM)は、現実のパーソナライズされたアプリケーションにますます統合されている。
RAGで使用される知識基盤の貴重かつしばしばプロプライエタリな性質は、敵による不正使用のリスクをもたらす。
これらの知識基盤を保護するための透かし技術として一般化できる既存の方法は、一般的に毒やバックドア攻撃を含む。
我々は、無害な」知識基盤の著作権保護の名称を提案する。
論文 参考訳（メタデータ） (2025-02-10T09:15:56Z) - Factcheck-Bench: Fine-Grained Evaluation Benchmark for Automatic Fact-checkers [121.53749383203792]
本稿では,大規模言語モデル (LLM) 生成応答の事実性に注釈を付けるための総合的なエンドツーエンドソリューションを提案する。
オープンドメインの文書レベルの事実性ベンチマークを,クレーム,文,文書の3段階の粒度で構築する。
予備実験によると、FacTool、FactScore、Perplexityは虚偽の主張を識別するのに苦労している。
論文 参考訳（メタデータ） (2023-11-15T14:41:57Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。