論文の概要: Non-Deterministic Planning for Hyperproperty Verification
- arxiv url: http://arxiv.org/abs/2405.13488v1
- Date: Wed, 22 May 2024 09:57:49 GMT
- ステータス: 処理完了
- システム内更新日: 2024-05-25 00:45:22.971315
- Title: Non-Deterministic Planning for Hyperproperty Verification
- Title（参考訳）: ハイパープロパティ検証のための非決定論的計画法
- Authors: Raven Beutner, Bernd Finkbeiner,
- Abstract要約: 提案手法は,ハイパープロパティの自動検証に強力な中間言語を提供することを示す。
本稿では,HyperLTL検証問題に対して,非決定論的マルチエージェント計画インスタンスを構築するアルゴリズムを提案する。
提案手法は,HyperLTLの大きな断片に対して,従来のFOND,あるいはPOND計画問題に対応していることを示す。
- 参考スコア（独自算出の注目度）: 4.726777092009553
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Non-deterministic planning aims to find a policy that achieves a given objective in an environment where actions have uncertain effects, and the agent - potentially - only observes parts of the current state. Hyperproperties are properties that relate multiple paths of a system and can, e.g., capture security and information-flow policies. Popular logics for expressing temporal hyperproperties - such as HyperLTL - extend LTL by offering selective quantification over executions of a system. In this paper, we show that planning offers a powerful intermediate language for the automated verification of hyperproperties. Concretely, we present an algorithm that, given a HyperLTL verification problem, constructs a non-deterministic multi-agent planning instance (in the form of a QDec-POMDP) that, when admitting a plan, implies the satisfaction of the verification problem. We show that for large fragments of HyperLTL, the resulting planning instance corresponds to a classical, FOND, or POND planning problem. We implement our encoding in a prototype verification tool and report on encouraging experimental results.
- Abstract（参考訳）: 非決定論的計画(英語版)は、行動が不確実な環境において所定の目的を達成する政策を見つけることを目的としており、エージェントが(潜在的に)現在の状態の一部だけを観察することを目的としている。
ハイパープロパティは、システムの複数のパスに関連するプロパティであり、例えば、セキュリティと情報フローポリシーをキャプチャできる。
HyperLTLのような時間的ハイパープロパティを表現する一般的なロジックは、システムの実行に対して選択的な定量化を提供することでLTLを拡張する。
本稿では,ハイパープロパティの自動検証において,計画が強力な中間言語を提供することを示す。
具体的には,ハイパーLTL検証問題を前提として,非決定論的マルチエージェント計画インスタンス(QDec-POMDPの形式で)を構築するアルゴリズムを提案する。
提案手法は,HyperLTLの大きな断片に対して,従来のFOND,あるいはPOND計画問題に対応していることを示す。
プロトタイプ検証ツールに符号化を実装し,実験結果を報告する。
関連論文リスト
- Ask-before-Plan: Proactive Language Agents for Real-World Planning [68.08024918064503]
プロアクティブエージェントプランニングでは、ユーザエージェントの会話とエージェント環境のインタラクションに基づいて、言語エージェントが明確化のニーズを予測する必要がある。
本稿では,明確化,実行,計画の3つのエージェントからなる新しいマルチエージェントフレームワーク,Clarification-Execution-Planning(textttCEP)を提案する。
論文 参考訳（メタデータ） (2024-06-18T14:07:28Z) - Unlocking Large Language Model's Planning Capabilities with Maximum Diversity Fine-tuning [10.704716790096498]
大規模言語モデル(LLM)は、技術やシステム設計の推進によって達成された、目覚ましいタスク解決能力を示している。
本稿では,LLMの計画能力に及ぼす微調整の影響について検討する。
計画領域におけるファインチューニングのサンプル効率を向上させるために,MDFT(Maximum Diversity Fine-Tuning)戦略を提案する。
論文 参考訳（メタデータ） (2024-06-15T03:06:14Z) - Testing and Understanding Erroneous Planning in LLM Agents through Synthesized User Inputs [12.412286518773028]
大規模言語モデル(LLM)は、幅広いタスクを解くのに有効であることを示した。
LLMは、特にタスクが複雑で長期計画を必要とする場合、誤った計画を立てる傾向がある。
提案するPDoctorは,LLMエージェントをテストし,それらの誤った計画を理解するための新しいアプローチである。
論文 参考訳（メタデータ） (2024-04-27T08:56:45Z) - KnowAgent: Knowledge-Augmented Planning for LLM-Based Agents [54.09074527006576]
大規模言語モデル(LLM)は複雑な推論タスクにおいて大きな可能性を証明していますが、より高度な課題に取り組むには不十分です。
この不適切さは、主に言語エージェントのアクション知識が組み込まれていないことに起因する。
我々は、明示的な行動知識を取り入れることで、LLMの計画能力を高めるために設計された新しいアプローチであるKnowAgentを紹介する。
論文 参考訳（メタデータ） (2024-03-05T16:39:12Z) - Learning Logic Specifications for Policy Guidance in POMDPs: an
Inductive Logic Programming Approach [57.788675205519986]
我々は任意の解法によって生成されるPOMDP実行から高品質なトレースを学習する。
我々は、データと時間効率のIndu Logic Programming(ILP)を利用して、解釈可能な信念に基づくポリシー仕様を生成する。
ASP(Answer Set Programming)で表現された学習は、ニューラルネットワークよりも優れた性能を示し、より少ない計算時間で最適な手作りタスクに類似していることを示す。
論文 参考訳（メタデータ） (2024-02-29T15:36:01Z) - AutoGPT+P: Affordance-based Task Planning with Large Language Models [6.848986296339031]
AutoGPT+Pは、余裕に基づくシーン表現と計画システムを組み合わせたシステムである。
提案手法は,現在最先端のLCM計画手法であるSayCanの81%の成功率を超え,98%の成功率を達成した。
論文 参考訳（メタデータ） (2024-02-16T16:00:50Z) - Entropy-Regularized Token-Level Policy Optimization for Language Agent Reinforcement [67.1393112206885]
大規模言語モデル(LLM)は、対話的な意思決定タスクにおいてインテリジェントなエージェントとして期待されている。
本稿では,トークンレベルでのLLMの最適化に適したエントロピー拡張RL法である,エントロピー正規化トークンレベル最適化(ETPO)を導入する。
我々は,データサイエンスコード生成を多段階対話型タスクのシリーズとしてモデル化したシミュレーション環境におけるETPOの有効性を評価する。
論文 参考訳（メタデータ） (2024-02-09T07:45:26Z) - Embodied Task Planning with Large Language Models [86.63533340293361]
本研究では,現場制約を考慮した地上計画のための具体的タスクにおけるTAsk Planing Agent (TaPA)を提案する。
推論の際には,オープンボキャブラリオブジェクト検出器を様々な場所で収集された多視点RGB画像に拡張することにより,シーン内の物体を検出する。
実験の結果,我々のTaPAフレームワークから生成されたプランは,LLaVAやGPT-3.5よりも大きなマージンで高い成功率が得られることがわかった。
論文 参考訳（メタデータ） (2023-07-04T17:58:25Z) - AdaPlanner: Adaptive Planning from Feedback with Language Models [56.367020818139665]
大規模言語モデル(LLM)は、最近、シーケンシャルな意思決定タスクの自律的エージェントとして機能する可能性を実証している。
本研究では,LLMエージェントが環境フィードバックに応じて自己生成計画を適応的に改善することのできるクローズドループアプローチであるAdaPlannerを提案する。
幻覚を緩和するために,様々なタスク,環境,エージェント機能にまたがる計画生成を容易にするコードスタイルのLCMプロンプト構造を開発した。
論文 参考訳（メタデータ） (2023-05-26T05:52:27Z) - On the Complexity of Rational Verification [5.230352342979224]
合理的検証とは、同時マルチエージェントシステムの時間論理特性が保持する問題を指す。
合理的な検証の複雑さは仕様によって大幅に低減できることを示す。
平均支払ユーティリティ関数によって与えられるプレイヤーの目標を考慮した場合、合理的な検証のための改善された結果を提供する。
論文 参考訳（メタデータ） (2022-07-06T12:56:22Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。