論文の概要: Formally Verified Solution Methods for Infinite-Horizon Markov Decision
Processes
- arxiv url: http://arxiv.org/abs/2206.02169v1
- Date: Sun, 5 Jun 2022 13:03:34 GMT
- ステータス: 処理完了
- システム内更新日: 2022-06-07 16:56:23.195300
- Title: Formally Verified Solution Methods for Infinite-Horizon Markov Decision
Processes
- Title(参考訳): 無限水平マルコフ決定過程の形式的検証解法
- Authors: Maximilian Sch\"afeller and Mohammad Abdulaziz
- Abstract要約: 確率論の既存の形式化に基づいて、無限水平問題における期待される全報酬基準を解析する。
我々の発展はベルマン方程式を形式化し、最適なポリシーが存在する条件を与える。
我々のシステムは最先端のシステムと競合し、さらに性能も向上できることを示す。
- 参考スコア(独自算出の注目度): 7.538482310185133
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: We formally verify executable algorithms for solving Markov decision
processes (MDPs) in the interactive theorem prover Isabelle/HOL. We build on
existing formalizations of probability theory to analyze the expected total
reward criterion on infinite-horizon problems. Our developments formalize the
Bellman equation and give conditions under which optimal policies exist. Based
on this analysis, we verify dynamic programming algorithms to solve tabular
MDPs. We evaluate the formally verified implementations experimentally on
standard problems and show they are practical. Furthermore, we show that,
combined with efficient unverified implementations, our system can compete with
and even outperform state-of-the-art systems.
- Abstract(参考訳): 対話型定理証明器Isabelle/HOLにおいてマルコフ決定過程(MDP)を解くための実行可能なアルゴリズムを正式に検証する。
確率論の既存の定式化に基づき,無限ホライゾン問題に対する期待総報酬基準を解析する。
我々はベルマン方程式を定式化し, 最適政策が存在する条件を与える。
この分析に基づいて,表型MDPを解く動的プログラミングアルゴリズムを検証する。
標準化された実装を実験により評価し,実用性を示す。
さらに,効率的な非検証実装と組み合わせることで,最先端システムと競合し,性能を上回ることができることを示す。
関連論文リスト
- Online POMDP Planning with Anytime Deterministic Guarantees [11.157761902108692]
不確実性の下での計画は、部分的に観測可能なマルコフ決定プロセス(POMDP)を用いて数学的に定式化できる
POMDPの最適計画を見つけるには計算コストがかかり、小さなタスクにのみ適用可能である。
簡便な解と理論的に最適な解との決定論的関係を導出する。
論文 参考訳(メタデータ) (2023-10-03T04:40:38Z) - Making Linear MDPs Practical via Contrastive Representation Learning [101.75885788118131]
マルコフ決定過程(MDP)における次元性の呪いに、低ランク表現を利用することで対処することが一般的である。
本稿では,効率的な表現学習を可能にしつつ,正規化を自動的に保証する線形MDPの代替的定義について考察する。
いくつかのベンチマークにおいて、既存の最先端モデルベースおよびモデルフリーアルゴリズムよりも優れた性能を示す。
論文 参考訳(メタデータ) (2022-07-14T18:18:02Z) - Application-Driven Learning: A Closed-Loop Prediction and Optimization
Approach Applied to Dynamic Reserves and Demand Forecasting [62.997667081978825]
我々は、予測と意思決定のプロセスが統合され、協調最適化される新しいクローズドループフレームワークであるアプリケーション駆動学習を提案する。
提案手法は拡張性があり,標準のオープンループ手法よりも一貫して性能が向上することを示す。
論文 参考訳(メタデータ) (2021-02-26T02:43:28Z) - Identification of Unexpected Decisions in Partially Observable
Monte-Carlo Planning: a Rule-Based Approach [78.05638156687343]
本稿では,POMCPポリシーをトレースを検査して分析する手法を提案する。
提案手法は, 政策行動の局所的特性を探索し, 予期せぬ決定を識別する。
我々は,POMDPの標準ベンチマークであるTigerに対するアプローチと,移動ロボットナビゲーションに関する現実の問題を評価した。
論文 参考訳(メタデータ) (2020-12-23T15:09:28Z) - Stein Variational Model Predictive Control [130.60527864489168]
不確実性の下での意思決定は、現実の自律システムにとって極めて重要である。
モデル予測制御 (MPC) 法は, 複雑な分布を扱う場合, 適用範囲が限られている。
この枠組みが、挑戦的で非最適な制御問題における計画の成功に繋がることを示す。
論文 参考訳(メタデータ) (2020-11-15T22:36:59Z) - Logistic Q-Learning [87.00813469969167]
MDPにおける最適制御の正規化線形プログラミング定式化から導いた新しい強化学習アルゴリズムを提案する。
提案アルゴリズムの主な特徴は,広範に使用されているベルマン誤差の代わりとして理論的に音声として機能する,政策評価のための凸損失関数である。
論文 参考訳(メタデータ) (2020-10-21T17:14:31Z) - Partial Policy Iteration for L1-Robust Markov Decision Processes [13.555107578858307]
本稿では、ロバストなMDPの共通クラスを解くための新しい効率的なアルゴリズムについて述べる。
我々は、ロバストなMDPのための部分ポリシーイテレーション、新しい、効率的で柔軟な、一般的なポリシーイテレーションスキームを提案する。
実験結果から,提案手法は最先端手法よりも桁違いに高速であることが示唆された。
論文 参考訳(メタデータ) (2020-06-16T19:50:14Z) - Planning in Markov Decision Processes with Gap-Dependent Sample
Complexity [48.98199700043158]
マルコフ決定過程における計画のための新しいトラジェクトリに基づくモンテカルロ木探索アルゴリズム MDP-GapE を提案する。
我々は, MDP-GapE に要求される生成モデルに対する呼び出し回数の上限を証明し, 確率の高い準最適動作を同定する。
論文 参考訳(メタデータ) (2020-06-10T15:05:51Z) - Kernel Taylor-Based Value Function Approximation for Continuous-State
Markov Decision Processes [5.894659354028797]
我々は,カーネルベースのポリシー反復アルゴリズムを提案し,連続状態マルコフ決定過程(MDP)を解く。
提案手法は, 簡易計画シナリオと現実計画シナリオの両方において, 広範囲なシミュレーションにより検証した。
論文 参考訳(メタデータ) (2020-06-03T01:48:43Z) - Point-Based Methods for Model Checking in Partially Observable Markov
Decision Processes [36.07746952116073]
部分的に観測可能なマルコフ決定過程(POMDP)において線形時間論理式を満たすポリシーを合成する手法を提案する。
本稿では,所望の論理式を満たす最大確率を効率的に近似するために,ポイントベースの値反復法を提案する。
我々は,提案手法を大規模POMDPドメインに拡張し,その結果のポリシーの性能に強い拘束力を与えることを示した。
論文 参考訳(メタデータ) (2020-01-11T23:09:25Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。