論文の概要: LTL Verification of Memoryful Neural Agents

• arxiv url: http://arxiv.org/abs/2503.02512v1
• Date: Tue, 04 Mar 2025 11:20:19 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-03-05 19:20:58.601645
• Title: LTL Verification of Memoryful Neural Agents
• Title（参考訳）: 記憶型ニューラルエージェントのLTL検証
• Authors: Mehran Hosseini, Alessio Lomuscio, Nicola Paoletti,
• Abstract要約: 本稿では,LTL(Linear Temporal Logic)仕様に対して,MN-MAS(Memoryful Neural Multi-Agent Systems)を検証するためのフレームワークを提案する。 MN-MASの例としては、フィードフォワードとリカレントニューラルネットワークに基づくマルチエージェントシステムや状態空間モデルがある。
• 参考スコア（独自算出の注目度）: 16.353043979615496
• License:
• Abstract: We present a framework for verifying Memoryful Neural Multi-Agent Systems (MN-MAS) against full Linear Temporal Logic (LTL) specifications. In MN-MAS, agents interact with a non-deterministic, partially observable environment. Examples of MN-MAS include multi-agent systems based on feed-forward and recurrent neural networks or state-space models. Different from previous approaches, we support the verification of both bounded and unbounded LTL specifications. We leverage well-established bounded model checking techniques, including lasso search and invariant synthesis, to reduce the verification problem to that of constraint solving. To solve these constraints, we develop efficient methods based on bound propagation, mixed-integer linear programming, and adaptive splitting. We evaluate the effectiveness of our algorithms in single and multi-agent environments from the Gymnasium and PettingZoo libraries, verifying unbounded specifications for the first time and improving the verification time for bounded specifications by an order of magnitude compared to the SoA.
• Abstract（参考訳）: 本稿では,LTL(Linear Temporal Logic)仕様に対して,MN-MAS(Memoryful Neural Multi-Agent Systems)を検証するためのフレームワークを提案する。 MN-MASでは、エージェントは非決定論的で部分的に観察可能な環境と相互作用する。 MN-MASの例としては、フィードフォワードとリカレントニューラルネットワークに基づくマルチエージェントシステムや状態空間モデルがある。 従来のアプローチとは異なり、我々は有界LTL仕様と非有界LTL仕様の両方の検証をサポートする。 我々は、ラッソ探索や不変合成を含む確立された境界モデル検査技術を活用し、検証問題を制約解に還元する。 これらの制約を解決するために,有界伝播,混合整数線形プログラミング,適応分割に基づく効率的な手法を開発した。 我々は,GymnasiumライブラリとPettingZooライブラリの単一およびマルチエージェント環境におけるアルゴリズムの有効性を評価し,非有界仕様の検証を初めて行い,SoAと比較し,有界仕様の検証時間を格段に改善した。

関連論文リスト

• A Learned Proximal Alternating Minimization Algorithm and Its Induced Network for a Class of Two-block Nonconvex and Nonsmooth Optimization [4.975853671529418]
  本研究では,学習可能な2ブロック非平滑問題の解法として,一般学習型交互最小化アルゴリズムLPAMを提案する。 提案するLPAM-netはパラメータ効率が高く,いくつかの最先端手法と比較して良好な性能を示す。
  論文  参考訳（メタデータ） (2024-11-10T02:02:32Z)
• Collision Avoidance Verification of Multiagent Systems with Learned Policies [9.550601011551024]
  本稿では,マルチエージェントフィードバックループ(MA-NFL)の衝突回避特性を検証するための後方到達性に基づくアプローチを提案する。 私たちは多くの不確実性を説明しており、現実のシナリオとよく一致しています。 提案アルゴリズムは,MA-NFLの衝突回避アルゴリズムを模倣するエージェントを用いて,衝突回避特性を検証できることを示す。
  論文  参考訳（メタデータ） (2024-03-05T20:36:26Z)
• Amortizing intractable inference in large language models [56.92471123778389]
  難治性後部分布のサンプルとして, 償却ベイズ推定を用いる。 我々は,LLMファインチューニングの分散マッチングパラダイムが,最大習熟の代替となることを実証的に実証した。 重要な応用として、チェーン・オブ・ソート推論を潜在変数モデリング問題として解釈する。
  論文  参考訳（メタデータ） (2023-10-06T16:36:08Z)
• Optimization Guarantees of Unfolded ISTA and ADMM Networks With Smooth Soft-Thresholding [57.71603937699949]
  我々は,学習エポックの数の増加とともに,ほぼゼロに近いトレーニング損失を達成するための最適化保証について検討した。 トレーニングサンプル数に対する閾値は,ネットワーク幅の増加とともに増加することを示す。
  論文  参考訳（メタデータ） (2023-09-12T13:03:47Z)
• Symmetric Tensor Networks for Generative Modeling and Constrained Combinatorial Optimization [72.41480594026815]
  ポートフォリオ最適化からロジスティクスに至るまで、制約付き最適化問題は業界に多い。 これらの問題の解決における主要な障害の1つは、有効な検索空間を制限する非自明なハード制約の存在である。 本研究では、Ax=bという形の任意の整数値等式制約をU(1)対称ネットワーク(TN)に直接エンコードし、それらの適用性を量子に着想を得た生成モデルとして活用する。
  論文  参考訳（メタデータ） (2022-11-16T18:59:54Z)
• Verifying Quantized Neural Networks using SMT-Based Model Checking [2.38142799291692]
  インクリメンタルモデルチェック(IMC)と満足度変調理論(SMT)を用いたシンボリック検証フレームワークの開発と評価を行った。 浮動小数点演算と不動小数点演算の両方で実装されたANNの安全な挙動を保証できる。 小規模から中規模のANNの場合、我々の手法は検証のほとんどを数分で完了します。
  論文  参考訳（メタデータ） (2021-06-10T18:27:45Z)
• Neural Network-based Control for Multi-Agent Systems from Spatio-Temporal Specifications [0.757024681220677]
  仕様言語としてSTREL(Spatio-Temporal Reach and Escape Logic)を使用します。 STREL仕様を用いた制御合成問題のマッピングを行い,勾配法と勾配法の組み合わせによる解法を提案する。 我々はオフライン最適化の結果を用いてニューラルネットワークをトレーニングし、制御が現在の状態を入力する機械学習技術を開発した。
  論文  参考訳（メタデータ） (2021-04-06T18:08:09Z)
• Incremental Verification of Fixed-Point Implementations of Neural Networks [0.19573380763700707]
  インクリメンタル境界モデル検査(BMC)、満足度変調理論(SMT)、不変推論を用いた新しいシンボル検証フレームワークの開発と評価を行った。 提案手法は,異なる入力画像を考慮した21の試験事例の85.8%,カバー手法に関連する特性の100%を検証・生成することができた。
  論文  参考訳（メタデータ） (2020-12-21T10:03:44Z)
• Adaptive Subcarrier, Parameter, and Power Allocation for Partitioned Edge Learning Over Broadband Channels [69.18343801164741]
  パーティショニングエッジ学習(PARTEL)は、無線ネットワークにおいてよく知られた分散学習手法であるパラメータサーバトレーニングを実装している。 本稿では、いくつかの補助変数を導入してParticleELを用いてトレーニングできるディープニューラルネットワーク(DNN)モデルについて考察する。
  論文  参考訳（メタデータ） (2020-10-08T15:27:50Z)
• Statistical control for spatio-temporal MEG/EEG source imaging with desparsified multi-task Lasso [102.84915019938413]
  脳磁図(MEG)や脳電図(EEG)のような非侵襲的手法は、非侵襲的手法を約束する。 ソースローカライゼーション(ソースイメージング)の問題は、しかしながら、高次元の統計的推測問題を引き起こす。 この問題に対処するために,分離されたマルチタスクラッソ(ecd-MTLasso)のアンサンブルを提案する。
  論文  参考訳（メタデータ） (2020-09-29T21:17:16Z)
• Communication-Efficient Distributed Stochastic AUC Maximization with Deep Neural Networks [50.42141893913188]
  本稿では,ニューラルネットワークを用いた大規模AUCのための分散変数について検討する。 我々のモデルは通信ラウンドをはるかに少なくし、理論上はまだ多くの通信ラウンドを必要としています。 いくつかのデータセットに対する実験は、我々の理論の有効性を示し、我々の理論を裏付けるものである。
  論文  参考訳（メタデータ） (2020-05-05T18:08:23Z)

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

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