論文の概要: Adversarial Robustness Verification and Attack Synthesis in Stochastic
Systems
- arxiv url: http://arxiv.org/abs/2110.02125v1
- Date: Tue, 5 Oct 2021 15:52:47 GMT
- ステータス: 処理完了
- システム内更新日: 2021-10-06 13:53:45.744393
- Title: Adversarial Robustness Verification and Attack Synthesis in Stochastic
Systems
- Title(参考訳): 確率系における逆ロバスト性検証と攻撃合成
- Authors: Lisa Oakley, Alina Oprea, Stavros Tripakis
- Abstract要約: 我々は、離散時間マルコフ連鎖(DTMC)として定義されるシステムにおける対向的堅牢性のための公式な枠組みを開発する。
我々は、元の遷移確率の周囲に$varepsilon$ボールで制約された、敵がシステム遷移を摂動できる脅威モデルのクラスを概説する。
- 参考スコア(独自算出の注目度): 8.833548357664606
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Probabilistic model checking is a useful technique for specifying and
verifying properties of stochastic systems including randomized protocols and
the theoretical underpinnings of reinforcement learning models. However, these
methods rely on the assumed structure and probabilities of certain system
transitions. These assumptions may be incorrect, and may even be violated in
the event that an adversary gains control of some or all components in the
system.
In this paper, motivated by research in adversarial machine learning on
adversarial examples, we develop a formal framework for adversarial robustness
in systems defined as discrete time Markov chains (DTMCs), and extend to
include deterministic, memoryless policies acting in Markov decision processes
(MDPs). Our framework includes a flexible approach for specifying several
adversarial models with different capabilities to manipulate the system. We
outline a class of threat models under which adversaries can perturb system
transitions, constrained by an $\varepsilon$ ball around the original
transition probabilities and define four specific instances of this threat
model.
We define three main DTMC adversarial robustness problems and present two
optimization-based solutions, leveraging traditional and parametric
probabilistic model checking techniques. We then evaluate our solutions on two
stochastic protocols and a collection of GridWorld case studies, which model an
agent acting in an environment described as an MDP. We find that the parametric
solution results in fast computation for small parameter spaces. In the case of
less restrictive (stronger) adversaries, the number of parameters increases,
and directly computing property satisfaction probabilities is more scalable. We
demonstrate the usefulness of our definitions and solutions by comparing system
outcomes over various properties, threat models, and case studies.
- Abstract(参考訳): 確率モデル検査は、ランダム化されたプロトコルや強化学習モデルの理論的基礎を含む確率システムの特性の特定と検証に有用な手法である。
しかし、これらの手法は、あるシステム遷移の仮定された構造と確率に依存する。
これらの仮定は誤りであり、敵がシステム内の一部のまたはすべてのコンポーネントを制御できる場合にさえ違反する可能性がある。
本稿では,敵対的機械学習の研究に動機づけられ,離散時間マルコフ連鎖 (dtmcs) として定義されるシステムにおいて,敵対的ロバストネスの形式的枠組みを開発し,マルコフ決定プロセス (mdps) に作用する決定論的かつメモリレスなポリシーを含むように拡張する。
我々のフレームワークは、システムを操作するための異なる機能を持つ複数の敵モデルを指定する柔軟なアプローチを含んでいる。
本論文では,元の遷移確率を囲む$\varepsilon$ ballで制約されたシステム遷移を摂動可能な脅威モデルのクラスを概説し,この脅威モデルの4つの特定のインスタンスを定義する。
我々は,3つの主要なdtmc逆ロバスト性問題を定義し,従来型およびパラメトリック確率モデルチェック手法を活用した2つの最適化ベースソリューションを提案する。
次に,2つの確率的プロトコルとGridWorldケーススタディの集合を用いて,MDPとして記述された環境下で作用するエージェントをモデル化する。
パラメトリック解は小さなパラメータ空間に対する高速な計算をもたらす。
制約の少ない(強弱な)敵の場合、パラメータの数が増加し、直接計算される特性満足度はよりスケーラブルである。
さまざまな特性,脅威モデル,ケーススタディに対するシステム結果を比較することで,定義とソリューションの有用性を示す。
関連論文リスト
- Learning Controlled Stochastic Differential Equations [61.82896036131116]
本研究では,非一様拡散を伴う連続多次元非線形微分方程式のドリフト係数と拡散係数の両方を推定する新しい手法を提案する。
我々は、(L2)、(Linfty)の有限サンプル境界や、係数の正則性に適応する学習率を持つリスクメトリクスを含む、強力な理論的保証を提供する。
当社のメソッドはオープンソースPythonライブラリとして利用可能です。
論文 参考訳(メタデータ) (2024-11-04T11:09:58Z) - Correct-by-Construction Control for Stochastic and Uncertain Dynamical
Models via Formal Abstractions [44.99833362998488]
我々は、様々なモデリングの前提の下でこの問題を解決するために使用できる抽象フレームワークを開発する。
我々は、与えられた仕様を満たすための保証とともに、iMDPの最適ポリシーを計算するために最先端の検証技術を使用します。
そして、このポリシーを構築によって、これらの保証が動的モデルに受け継がれるフィードバックコントローラに改良できることを示します。
論文 参考訳(メタデータ) (2023-11-16T11:03:54Z) - Robust Control for Dynamical Systems With Non-Gaussian Noise via Formal
Abstractions [59.605246463200736]
雑音分布の明示的な表現に依存しない新しい制御器合成法を提案する。
まず、連続制御系を有限状態モデルに抽象化し、離散状態間の確率的遷移によってノイズを捕捉する。
我々は最先端の検証技術を用いてマルコフ決定プロセスの間隔を保証し、これらの保証が元の制御システムに受け継がれるコントローラを演算する。
論文 参考訳(メタデータ) (2023-01-04T10:40:30Z) - Formal Controller Synthesis for Markov Jump Linear Systems with
Uncertain Dynamics [64.72260320446158]
マルコフジャンプ線形系に対する制御器の合成法を提案する。
本手法は,MJLSの離散(モードジャンピング)と連続(確率線形)の両方の挙動を捉える有限状態抽象化に基づいている。
本手法を複数の現実的なベンチマーク問題,特に温度制御と航空機の配送問題に適用する。
論文 参考訳(メタデータ) (2022-12-01T17:36:30Z) - Online Probabilistic Model Identification using Adaptive Recursive MCMC [8.465242072268019]
適応再帰的マルコフ連鎖モンテカルロ法(ARMCMC)を提案する。
モデルパラメータの確率密度関数全体を計算しながら、従来のオンライン手法の欠点を解消する。
本研究では,ソフト曲げアクチュエータとハント・クロスリー動的モデルを用いてパラメータ推定を行った。
論文 参考訳(メタデータ) (2022-10-23T02:06:48Z) - Probabilities Are Not Enough: Formal Controller Synthesis for Stochastic
Dynamical Models with Epistemic Uncertainty [68.00748155945047]
複雑な力学系のモデルにおける不確実性を捉えることは、安全なコントローラの設計に不可欠である。
いくつかのアプローチでは、安全と到達可能性に関する時間的仕様を満たすポリシーを形式的な抽象化を用いて合成する。
我々の貢献は、ノイズ、不確実なパラメータ、外乱を含む連続状態モデルに対する新しい抽象的制御法である。
論文 参考訳(メタデータ) (2022-10-12T07:57:03Z) - Sample Complexity of Robust Reinforcement Learning with a Generative
Model [0.0]
本稿では,モデルに基づく強化学習(RL)アルゴリズムを提案する。
我々は,全変動距離,カイ二乗発散,KL発散の3種類の不確実性集合を考察した。
この結果に加えて,ロバストポリシの利点に関する公式な分析的議論も提示する。
論文 参考訳(メタデータ) (2021-12-02T18:55:51Z) - Stein Variational Model Predictive Control [130.60527864489168]
不確実性の下での意思決定は、現実の自律システムにとって極めて重要である。
モデル予測制御 (MPC) 法は, 複雑な分布を扱う場合, 適用範囲が限られている。
この枠組みが、挑戦的で非最適な制御問題における計画の成功に繋がることを示す。
論文 参考訳(メタデータ) (2020-11-15T22:36:59Z) - A Hamiltonian Monte Carlo Method for Probabilistic Adversarial Attack
and Learning [122.49765136434353]
本稿では,HMCAM (Acumulated Momentum) を用いたハミルトニアンモンテカルロ法を提案する。
また, 対数的対数的対数的学習(Contrastive Adversarial Training, CAT)と呼ばれる新たな生成法を提案し, 対数的例の平衡分布にアプローチする。
いくつかの自然画像データセットと実用システムに関する定量的および定性的な解析により、提案アルゴリズムの優位性が確認された。
論文 参考訳(メタデータ) (2020-10-15T16:07:26Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。