論文の概要: ETAS: An Effect-Typed Language for Agent Systems
- arxiv url: http://arxiv.org/abs/2607.17780v1
- Date: Mon, 20 Jul 2026 10:11:53 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-07-21 18:48:37.587708
- Title: ETAS: An Effect-Typed Language for Agent Systems
- Title（参考訳）: ETAS:エージェントシステムのためのエフェクト型言語
- Abstract要約: ETASはエージェントシステムのためのプログラミング言語である。
モデル支援エージェント、ツールコール、プロンプト、型付きメモリ、人間の承認、ポリシー、実行トレースをセマンティックプログラム要素として扱う。
- 参考スコア（独自算出の注目度）: 3.1440390119576676
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: ETAS is a programming language for agent systems that treats model-backed agents, tool calls, prompts, typed memory, human approvals, policies, and execution traces as semantic program elements rather than library conventions. It separates deterministic computation from agentic nondeterminism and externally visible actions while preserving a direct programming style. We present the core design of ETAS. Its static semantics assigns ordinary types through spec conformance and tracks each computation with two behavioral indices: an escaping effect row and a persistent abstraction of the typed action trace it may request. Specs form a terminating compile-time constraint calculus: type specs provide evidence for polymorphism and resource facts, callable specs constrain function and stage shapes, and trace specs express allow, deny, and temporal constraints. Typing checks requested traces against compiled monitors and emits residual obligations when dynamic resources preclude a complete static proof. The dynamic semantics distinguish requested, handled, denied, and committed events; handlers interpret typed actions without making their requests invisible to authorization or audit. We formalize a core calculus and state preservation, progress, type/effect soundness, handler trace-transparency, and policy safety. We also implement ETAS in Rust with a command-line interface, typed HIR checks, effect and policy diagnostics, handler checks, and trace-aware execution hooks. ETAS provides a programming-language foundation for reasoning about authorization, nondeterminism, recovery, and audit evidence before and during agent execution.
- Abstract（参考訳）: ETASは、モデル支援エージェント、ツールコール、プロンプト、型付きメモリ、人間の承認、ポリシー、実行トレースを、ライブラリの規約ではなくセマンティックなプログラム要素として扱うエージェントシステムのためのプログラミング言語である。
決定論的計算をエージェント的非決定主義と分離し、直接プログラミングスタイルを保ちながら外部から見えるアクションを分離する。
本稿では ETAS のコア設計について述べる。
その静的セマンティクスは、仕様適合性を通じて通常の型を割り当て、各計算を2つの行動指標(エスケープエフェクト行と、要求される可能性のある型付きアクショントレースの永続的な抽象化)で追跡する。
型仕様は多型やリソース事実、呼び出し可能な仕様制約関数とステージ形状、トレース仕様は許容、拒否、時間的制約を表す。
タイピングは、要求されたトレースをコンパイルされたモニタに対してチェックし、動的リソースが完全な静的な証明を妨げたときに、残りの義務を発行する。
動的セマンティクスは、要求された、処理された、拒否された、コミットされたイベントを区別する。
我々は、コア計算と状態保存、進行、タイプ/エフェクトの音性、ハンドラトレースの透明性、およびポリシーの安全性を定式化する。
Rustでは、コマンドラインインターフェース、型付きHIRチェック、エフェクトとポリシの診断、ハンドラチェック、トレース対応実行フックなど、ETASも実装しています。
ETASは、承認、非決定主義、回復、エージェント実行前後の証拠の監査に関する推論のためのプログラミング言語基盤を提供する。
関連論文リスト
- From Natural Language Policies to Executable Obligations: A Verification Harness for Dependable In-Car LLM Agents [0.5352699766206808]
我々は,CAR-bench Track1への参入であるAgentGuardUtilを紹介した。
各会話で出荷される自然言語ポリシーは、ポリシー毎に1度、型付きマシンチェック可能なルールにコンパイルされる。
決定論的義務エンジンは、これらのルールをライブツールの結果と、ドラフト自体のシミュレーション後状態に対して解釈する。
論文 参考訳（メタデータ） (2026-08-24T14:06:21Z) - Formal Verification of Agentic Systems over Operational Data [59.98246281888422]
大規模言語モデル(LLM)によって駆動されるエージェントシステムは、永続的な運用データを扱う現実世界にますます展開されている。
既存のアプローチはそのようなシステムレベルの保証を提供していません。
本稿では, 1 つの LLM とツールオーケストレーションハーネスからなるエージェントシステムのリレーショナル操作データに対する検証について述べる。
論文 参考訳（メタデータ） (2026-08-04T13:01:30Z) - 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) - TTHE: Test-Time Harness Evolution [50.26245555541721]
既存のアプローチでは、デプロイ前、トレーニング前、あるいはテスト時に凍結される固定されたエージェントワークフローの開発データを最適化する。
我々は、エージェントがテスト入力で生成するラベルのない実行トレースのみを使用して、評価自体にハーネスを最適化できるかどうかを問う。
評価中、TTHEは候補ハーネスの人口を維持し、それらの実行トレースの理由をエージェントプロジェクタを通じてそれらを洗練する。
その後、審査員は実行元プロキシ信号から改善されたハーネスをコミットし、選択したプログラムは継続してその後の入力を統治する。
論文 参考訳（メタデータ） (2026-07-09T05:53:39Z) - VIGIL: Runtime Enforcement of Behavioral Specifications in AI Agent Skills [13.980239249972819]
VIGILはエージェントシステムのためのエンドツーエンドのランタイム実行フレームワークである。
エージェントの実際の実行トレースを、スキル仕様、オペレータ定義制約、複数のスキルにまたがるグローバルルールから、行動ポリシーに対してチェックする。
95%以上のリコールと偽陽性率で政策違反を検出する。
論文 参考訳（メタデータ） (2026-06-25T01:58:44Z) - A Physical Agentic Loop for Language-Guided Grasping with Execution-State Monitoring [5.437966695589128]
我々は、接地された実行状態上で動作する有界な実施エージェントとして言語誘導の把握を再構築する。
未修正の学習操作プリミティブをラップする物理エージェントループを導入する。
眼内カメラD405を用いた移動マニピュレータのループを検証した。
論文 参考訳（メタデータ） (2026-04-08T08:01:35Z) - 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) - Agentproof: Static Verification of Agent Workflow Graphs [0.0]
エージェントフレームワークは、ツール使用の振る舞いを明示的なワークフローグラフとしてエンコードする傾向にある。
本稿では,4つの主要なエージェントフレームワークから統合抽象グラフモデルを自動的に抽出するAgentproofを提案する。
汎用的なモデルチェッカーとは異なり、Agentproofは手動モデリングを必要としない。
論文 参考訳（メタデータ） (2026-03-20T13:56:20Z) - TriCEGAR: A Trace-Driven Abstraction Mechanism for Agentic AI [5.1181001367075]
TriCEGARはトレース駆動の抽象化メカニズムで、実行ログから状態構築を自動化する。
タイプされたエージェントライフサイクルイベントをキャプチャし、トレースから抽象化を構築するフレームワークネイティブ実装について説明する。
また, 走行確率が異常検出をガードレール信号として有効にする方法も示す。
論文 参考訳（メタデータ） (2026-01-30T14:01:47Z) - Deriving Character Logic from Storyline as Codified Decision Trees [67.01182739162142]
ロールプレイング(RP)エージェントは、さまざまな物語の文脈で一貫して行動するために行動プロファイルに依存する。
大規模物語データから実行可能かつ解釈可能な決定構造を誘導するデータ駆動型フレームワークであるCDT(Condified Decision Trees)を提案する。
論文 参考訳（メタデータ） (2026-01-15T05:12:43Z) - DRIFT: Dynamic Rule-Based Defense with Injection Isolation for Securing LLM Agents [52.92354372596197]
大規模言語モデル(LLM)は、強力な推論と計画能力のため、エージェントシステムの中心となってきています。
この相互作用は、外部ソースからの悪意のある入力がエージェントの振る舞いを誤解させる可能性がある、インジェクション攻撃のリスクも引き起こす。
本稿では,信頼に値するエージェントシステムのための動的ルールベースの分離フレームワークを提案する。
論文 参考訳（メタデータ） (2025-06-13T05:01:09Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。