論文の概要: Practical Runtime Enforcement of First-Order Temporal Requirements

• arxiv url: http://arxiv.org/abs/2610.04611v1
• Date: Sat, 03 Oct 2026 15:52:08 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-11 18:24:02.619529
• Title: Practical Runtime Enforcement of First-Order Temporal Requirements
• Title（参考訳）: 第一段階の時間要件の実践的実行方法
• Abstract要約: ますます増加するコンプライアンスの世界では、現実世界のシステムは何百もの要件に従わなければならない。 複雑なポリシーをサポートする既存の実行メカニズムは、プロダクションソフトウェアでは遅すぎることが多い。 複雑な時間的要求を強制する効率的なアルゴリズムとツールを導入し、その性能を実証する。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by-nc-sa/4.0/
• Abstract: Runtime enforcers observe a system's behavior and exert control over it to ensure that the system always adheres to its requirements. Many natural requirements not only formulate restrictions on the system's present behavior, but also impose obligations on its future behavior; for instance, agentic security may require personal data collected during a run to be erased by some deadline. In an ever-growing compliance landscape, real-world systems may be subject to hundreds of such requirements. However, existing enforcement mechanisms supporting complex policies are often too slow for production software; instead, developers may resort to non-temporal access control mechanisms and ad-hoc instrumentation, but these scale poorly with requirement complexity. To address this problem, we introduce an efficient algorithm and tool for enforcing complex temporal requirements and demonstrate its performance. Specifically, we identify a fragment of Metric First-Order Temporal Logic (MFOTL) that can be enforced with low runtime complexity while supporting a rich family of practically relevant requirements, including obligations. We then design an enforcement algorithm for this fragment and implement it in EnfFlash, a novel tool that enforces requirements with latency up to 44x lower than EnfGuard, the previous state-of-the-art enforcer, on standard benchmarks, and up to three orders of magnitude lower on security policies for LLM agents. This performance is achieved by compiling requirements into imperative programs that we efficiently interpret. We evaluate EnfFlash both standalone, on existing benchmarks, and integrated in web applications as an enforcement backend. We demonstrate that it can enforce a substantial 400-line MFOTL formula specifying the GDPR on a social network while adding under 15 ms to each page view, which is sufficient for most interactive and real-time applications.
• Abstract（参考訳）: 実行時執行者はシステムの振る舞いを観察し、システムの要求に常に従うように制御する。 多くの自然条件は、システムの現在の動作に制限を定めているだけでなく、将来の動作にも義務を課している。 ますます増加するコンプライアンスの世界では、現実世界のシステムは何百もの要件に従わなければならない。 しかし、複雑なポリシーをサポートする既存の実行メカニズムは、プロダクションソフトウェアでは遅すぎる場合が多い。代わりに、開発者は、時間的でないアクセス制御機構やアドホックなインスツルメンテーションに頼ることができるが、これらのスケールは要件の複雑さに乏しい。 この問題に対処するために、複雑な時間的要求を強制する効率的なアルゴリズムとツールを導入し、その性能を実証する。 具体的には,MFOTL(Metric First-Order Temporal Logic)の断片を,義務を含む実用的な要件の豊富なファミリーをサポートしながら,実行時の複雑性を低く抑えることができる。 次に、このフラグメントの強制アルゴリズムを設計し、それをEnfFlashで実装します。これは、従来の最先端の執行機関であるEnfGuardよりも44倍低いレイテンシで要求を強制する新しいツールです。 この性能は、我々が効率的に解釈する命令型プログラムに要求をコンパイルすることで達成される。 既存のベンチマークでEnfFlashを評価し、実行バックエンドとしてWebアプリケーションに統合します。 各ページビューに15ミリ秒以下を追加しながら、ソーシャルネットワーク上でGDPRを指定する400行のMFOTL公式を強制できることを示し、ほとんどのインタラクティブでリアルタイムなアプリケーションに十分である。

関連論文リスト

• Tractable Reinforcement Learning for Full Class of Signal Temporal Logic Specifications Using Spatiotemporal Tube Reward [1.8619748472447968]
  本稿では,未知の力学と厳密なアクチュエータ制限の下で動作するロボットシステムの制御問題に対処する。 Signal Temporal Logic (STL) を用いたこれらの高レベル仕様を示す。 時空間管(STT)の幾何学的特性を利用した時空間強化学習フレームワークを提案する。
  論文  参考訳（メタデータ） (2026-09-23T17:03:00Z)
• Formal Verification of Agentic Systems over Operational Data [59.98246281888422]
  大規模言語モデル(LLM)によって駆動されるエージェントシステムは、永続的な運用データを扱う現実世界にますます展開されている。 既存のアプローチはそのようなシステムレベルの保証を提供していません。 本稿では, 1 つの LLM とツールオーケストレーションハーネスからなるエージェントシステムのリレーショナル操作データに対する検証について述べる。
  論文  参考訳（メタデータ） (2026-08-04T13:01:30Z)
• Ethical Hyper-Velocity (EHV): A Provably Deterministic Governance-Aware JIT Compiler Architecture for Agentic Systems [0.0]
  Ethical Hyper-VeCRは、実行時にAIガバナンスポリシーを正式な検証するためのフレームワークである。 EHVは、ガバナンス対応のJust-In-TimeJITコンパイラを介して、ポリシー実行ポイント(PEP)を推論パイプラインにリロケーションする。 O(1)の実施によって、デプロイメントのベロシティとガバナンスの間の従来のトレードオフを排除し、ガバナンスをO(days)からO(1)に還元できることを示す。
  論文  参考訳（メタデータ） (2026-05-18T06:15:51Z)
• HIPO: Instruction Hierarchy via Constrained Reinforcement Learning [57.40686733111483]
  textscHIPOは、制約付きマルコフ決定プロセスとしてHIFを定式化する新しいアライメントフレームワークである。 textscHIPOはシステムプロンプトを単に入力コンテキストから厳密なアルゴリズム境界まで高める。
  論文  参考訳（メタデータ） (2026-03-17T06:12:41Z)
• Evaluating Implicit Regulatory Compliance in LLM Tool Invocation via Logic-Guided Synthesis [18.51135049856393]
  我々は,非構造化規則を線形時間論理託に変換するフレームワークであるLogiSafetyGenを導入し,論理誘導ファジングを用いて,有効かつ安全クリティカルなトレースを合成する。 このフレームワーク上に構築したLogiSafetyBenchは,LLMが機能目標と遅延コンプライアンスルールの両方を満たすPythonプログラムを生成するために必要な,240の人間認証タスクからなるベンチマークである。 13種類のSOTA (State-of-the-art) LLMの評価により、より優れた機能的正当性を達成したにもかかわらず、安全よりもタスク完了を優先し、非準拠な振る舞いをもたらすことが判明した。
  論文  参考訳（メタデータ） (2026-01-13T03:55:18Z)
• Reinforcement learning with timed constraints for robotics motion planning [0.5436465344481877]
  本稿では,マルコフ決定プロセス (MDP) と部分観測可能なマルコフ決定プロセス (POMDP) の両方でポリシーを合成するための統一されたオートマトンベースのフレームワークを提案する。 単純だが表現力のある報酬構造は、時間的正しさを強制し、さらなるパフォーマンス目標を許容する。 その結果、提案フレームワークは、遷移条件下で厳密な時間制約を満たすポリシーを一貫して学習し、より大きな状態空間にスケールし、部分的に観測可能な環境において有効であることを実証した。
  論文  参考訳（メタデータ） (2025-12-31T19:43:44Z)
• Analyzing and Internalizing Complex Policy Documents for LLM Agents [53.14898416858099]
  大規模言語モデル(LLM)ベースのエージェントシステムは、多様なビジネスルールをコードするコンテキスト内ポリシー文書に依存している。 これは、パフォーマンスを保ちながら、ポリシー文書をモデルプリエントに組み込む内部化手法の開発を動機付けます。 CC-Genは4つのレベルにまたがる制御可能な複雑度を持つエージェントベンチマークジェネレータである。
  論文  参考訳（メタデータ） (2025-10-13T16:30:07Z)
• DRIFT: Dynamic Rule-Based Defense with Injection Isolation for Securing LLM Agents [52.92354372596197]
  大規模言語モデル(LLM)は、強力な推論と計画能力のため、エージェントシステムの中心となってきています。 この相互作用は、外部ソースからの悪意のある入力がエージェントの振る舞いを誤解させる可能性がある、インジェクション攻撃のリスクも引き起こす。 本稿では,信頼に値するエージェントシステムのための動的ルールベースの分離フレームワークを提案する。
  論文  参考訳（メタデータ） (2025-06-13T05:01:09Z)
• AGENTIF: Benchmarking Instruction Following of Large Language Models in Agentic Scenarios [51.46347732659174]
  LLM(Large Language Models)は、現実世界のエージェントアプリケーションにおいて高度な機能を示す。 AgentIFは、エージェントシナリオでLLM命令に従う能力を体系的に評価する最初のベンチマークである。
  論文  参考訳（メタデータ） (2025-05-22T17:31:10Z)
• Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic [4.60607942851373]
  システム実行から形式仕様を自動合成する問題を考察する。 時間論理式を合成するための古典的なアプローチの多くは、公式のサイズを最小化することを目的としている。 我々は,この概念を定式化し,有界な外見を持つ簡潔な公式を合成する学習アルゴリズムを考案する。
  論文  参考訳（メタデータ） (2023-10-26T14:13:15Z)
• Certified Reinforcement Learning with Logic Guidance [78.2286146954051]
  線形時間論理(LTL)を用いて未知の連続状態/動作マルコフ決定過程(MDP)のゴールを定式化できるモデルフリーなRLアルゴリズムを提案する。 このアルゴリズムは、トレースが仕様を最大確率で満たす制御ポリシーを合成することが保証される。
  論文  参考訳（メタデータ） (2019-02-02T20:09:32Z)

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

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