論文の概要: 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を解く動的プログラミングアルゴリズムを検証する。 標準化された実装を実験により評価し,実用性を示す。 さらに,効率的な非検証実装と組み合わせることで,最先端システムと競合し,性能を上回ることができることを示す。

関連論文リスト

• On Policy Evaluation Algorithms in Distributional Reinforcement Learning [0.0]
  分散強化学習(DRL)による政策評価問題における未知の回帰分布を効率的に近似する新しいアルゴリズムのクラスを導入する。 提案したアルゴリズムの単純な例では、ワッサーシュタインとコルモゴロフ-スミルノフ距離の両方において誤差境界を証明する。 確率密度関数を持つ戻り分布の場合、アルゴリズムはこれらの密度を近似し、誤差境界は上限ノルム内で与えられる。
  論文  参考訳（メタデータ） (2024-07-19T10:06:01Z)
• Formally Verified Approximate Policy Iteration [11.602089225841633]
  形式化されたアルゴリズムが実行可能で検証可能な実装にどのように洗練されるかを示す。 実装は、その実行可能性を示すために、ベンチマーク問題で評価される。 この改良の一環として,線形プログラミングソリューションを認証する検証ソフトウェアを開発した。
  論文  参考訳（メタデータ） (2024-06-11T15:07:08Z)
• Online POMDP Planning with Anytime Deterministic Guarantees [11.157761902108692]
  不確実性の下での計画は、部分的に観測可能なマルコフ決定プロセス(POMDP)を用いて数学的に定式化できる POMDPの最適計画を見つけるには計算コストがかかり、小さなタスクにのみ適用可能である。 簡便な解と理論的に最適な解との決定論的関係を導出する。
  論文  参考訳（メタデータ） (2023-10-03T04:40:38Z)
• Provably Efficient UCB-type Algorithms For Learning Predictive State Representations [55.00359893021461]
  逐次決定問題は、予測状態表現(PSR)によってモデル化された低ランク構造が認められる場合、統計的に学習可能である 本稿では,推定モデルと実モデル間の全変動距離を上限とする新しいボーナス項を特徴とする,PSRに対する最初のUCB型アプローチを提案する。 PSRに対する既存のアプローチとは対照的に、UCB型アルゴリズムは計算的トラクタビリティ、最優先の準最適ポリシー、モデルの精度が保証される。
  論文  参考訳（メタデータ） (2023-07-01T18:35:21Z)
• Making Linear MDPs Practical via Contrastive Representation Learning [101.75885788118131]
  マルコフ決定過程(MDP)における次元性の呪いに、低ランク表現を利用することで対処することが一般的である。 本稿では,効率的な表現学習を可能にしつつ,正規化を自動的に保証する線形MDPの代替的定義について考察する。 いくつかのベンチマークにおいて、既存の最先端モデルベースおよびモデルフリーアルゴリズムよりも優れた性能を示す。
  論文  参考訳（メタデータ） (2022-07-14T18:18:02Z)
• 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)

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

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