論文の概要: CertRL: Formalizing Convergence Proofs for Value and Policy Iteration in Coq

• arxiv url: http://arxiv.org/abs/2009.11403v2
• Date: Tue, 15 Dec 2020 19:39:30 GMT
• ステータス: 処理完了
• システム内更新日: 2022-10-15 16:46:42.921268
• Title: CertRL: Formalizing Convergence Proofs for Value and Policy Iteration in Coq
• Title（参考訳）: certrl: coqにおける価値と政策イテレーションの収束証明の形式化
• Authors: Koundinya Vajjha, Avraham Shinnar, Vasily Pestun, Barry Trager, Nathan Fulton
• Abstract要約: 強化学習アルゴリズムは,長期報酬を最適化することにより,確率的環境における逐次的意思決定問題を解決する。 本稿では、有限状態マルコフ決定過程に対する値とポリシーの反復という、2つの正準強化学習アルゴリズムの形式化を開発する。 CertRLライブラリは、Markov決定プロセスと強化学習アルゴリズムに関する特性を証明するための一般的なフレームワークを提供する。
• 参考スコア（独自算出の注目度）: 1.154957229836278
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Reinforcement learning algorithms solve sequential decision-making problems in probabilistic environments by optimizing for long-term reward. The desire to use reinforcement learning in safety-critical settings inspires a recent line of work on formally constrained reinforcement learning; however, these methods place the implementation of the learning algorithm in their Trusted Computing Base. The crucial correctness property of these implementations is a guarantee that the learning algorithm converges to an optimal policy. This paper begins the work of closing this gap by developing a Coq formalization of two canonical reinforcement learning algorithms: value and policy iteration for finite state Markov decision processes. The central results are a formalization of Bellman's optimality principle and its proof, which uses a contraction property of Bellman optimality operator to establish that a sequence converges in the infinite horizon limit. The CertRL development exemplifies how the Giry monad and mechanized metric coinduction streamline optimality proofs for reinforcement learning algorithms. The CertRL library provides a general framework for proving properties about Markov decision processes and reinforcement learning algorithms, paving the way for further work on formalization of reinforcement learning algorithms.
• Abstract（参考訳）: 強化学習アルゴリズムは長期報酬を最適化することで確率的環境における逐次意思決定問題を解決する。 安全クリティカルな環境で強化学習を利用するという欲求は、公式に制約された強化学習に関する最近の取り組みを刺激するが、これらの手法は信頼されたコンピューティング基盤に学習アルゴリズムを実装する。 これらの実装の重要な正確性は、学習アルゴリズムが最適なポリシーに収束する保証である。 本稿では,このギャップを埋める作業として,有限状態マルコフ決定過程に対する値とポリシーの反復という,2つの正準強化学習アルゴリズムのCoq形式化を開発する。 中心となる結果はベルマンの最適性原理とその証明の形式化であり、ベルマン最適性作用素の縮約性を用いて、列が無限大地平線極限に収束することを示す。 certrlの開発は、強化学習アルゴリズムに対するgiry monadと機械化されたメートル法推論の合理性証明の例である。 CertRLライブラリは、マルコフ決定プロセスと強化学習アルゴリズムに関する特性を証明するための一般的なフレームワークを提供する。

関連論文リスト

• Safe Reinforcement Learning for Constrained Markov Decision Processes with Stochastic Stopping Time [0.6554326244334868]
  安全制約付きマルコフ決定過程に対するオンライン強化学習アルゴリズムを提案する。 学習方針は高い信頼を持って安全であることを示す。 また、プロキシセットと呼ばれる状態空間のサブセットを定義することで、効率的な探索を実現することができることを示す。
  論文  参考訳（メタデータ） (2024-03-23T20:22:30Z)
• Regularized Q-Learning with Linear Function Approximation [2.765106384328772]
  線形汎関数近似を用いた正規化Q-ラーニングの2段階最適化について検討する。 特定の仮定の下では、提案アルゴリズムはマルコフ雑音の存在下で定常点に収束することを示す。
  論文  参考訳（メタデータ） (2024-01-26T20:45:40Z)
• Maximum-Likelihood Inverse Reinforcement Learning with Finite-Time Guarantees [56.848265937921354]
  逆強化学習(IRL)は報酬関数と関連する最適ポリシーを回復することを目的としている。 IRLの多くのアルゴリズムは本質的にネスト構造を持つ。 我々は、報酬推定精度を損なわないIRLのための新しいシングルループアルゴリズムを開発した。
  論文  参考訳（メタデータ） (2022-10-04T17:13:45Z)
• Stochastic convex optimization for provably efficient apprenticeship learning [1.0609815608017066]
  コスト関数が不明な大規模マルコフ決定プロセス(MDP)について検討する。 擬似学習の課題に対処するために凸最適化ツールを用いており、これは、限られた専門家による実証からポリシーを学習するものである。
  論文  参考訳（メタデータ） (2021-12-31T19:47:57Z)
• Formalising the Foundations of Discrete Reinforcement Learning in Isabelle/HOL [0.0]
  我々は、動的プログラミングに必要な基礎と、そのようなプロセスに対する強化学習エージェントの使用に焦点を当てる。 我々は、割引係数が1以下であるような、普遍的に最適な政策の存在を証明している。 最後に、値反復とポリシーアルゴリズムが有限時間で機能することを証明し、それぞれにエプシロン最適化と完全最適ポリシーを生成する。
  論文  参考訳（メタデータ） (2021-12-11T14:38:36Z)
• A Boosting Approach to Reinforcement Learning [59.46285581748018]
  複雑度が状態数に依存しない意思決定プロセスにおける強化学習のための効率的なアルゴリズムについて検討する。 このような弱い学習手法の精度を向上させることができる効率的なアルゴリズムを提供する。
  論文  参考訳（メタデータ） (2021-08-22T16:00:45Z)
• Uniform-PAC Bounds for Reinforcement Learning with Linear Function Approximation [92.3161051419884]
  線形関数近似を用いた強化学習について検討する。 既存のアルゴリズムは、高い確率的後悔と/またはおよそ正当性(PAC)サンプルの複雑さの保証しか持たない。 我々はFLUTEと呼ばれる新しいアルゴリズムを提案し、高い確率で最適ポリシーへの均一PAC収束を享受する。
  論文  参考訳（メタデータ） (2021-06-22T08:48:56Z)
• Policy Mirror Descent for Regularized Reinforcement Learning: A Generalized Framework with Linear Convergence [60.20076757208645]
  本稿では,正規化RLを解くためのGPMDアルゴリズムを提案する。 我々は,このアルゴリズムが次元自由な方法で,全範囲の学習率に線形に収束することを実証した。
  論文  参考訳（メタデータ） (2021-05-24T02:21:34Z)
• Logistic Q-Learning [87.00813469969167]
  MDPにおける最適制御の正規化線形プログラミング定式化から導いた新しい強化学習アルゴリズムを提案する。 提案アルゴリズムの主な特徴は,広範に使用されているベルマン誤差の代わりとして理論的に音声として機能する,政策評価のための凸損失関数である。
  論文  参考訳（メタデータ） (2020-10-21T17:14:31Z)
• Constrained Combinatorial Optimization with Reinforcement Learning [0.30938904602244344]
  本稿では,RL(Deep Reinforcement Learning)を用いた制約付き最適化問題に対処する枠組みを提案する。 我々は、その定式化における制約に対処するために、Neural Combinatorial Optimization(NCO)理論を拡張した。 その文脈では、ソリューションは環境との相互作用に基づいて反復的に構築されます。
  論文  参考訳（メタデータ） (2020-06-22T03:13:07Z)
• A Distributional Analysis of Sampling-Based Reinforcement Learning Algorithms [67.67377846416106]
  定常ステップサイズに対する強化学習アルゴリズムの理論解析に対する分布的アプローチを提案する。 本稿では,TD($lambda$)や$Q$-Learningのような値ベースの手法が,関数の分布空間で制約のある更新ルールを持つことを示す。
  論文  参考訳（メタデータ） (2020-03-27T05:13:29Z)

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

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