Fugu-MT 論文翻訳(概要): Formally Verified Approximate Policy Iteration

論文の概要: Formally Verified Approximate Policy Iteration

arxiv url: http://arxiv.org/abs/2406.07340v1
Date: Tue, 11 Jun 2024 15:07:08 GMT
ステータス: 処理完了
システム内更新日: 2024-06-12 15:24:54.396025
Title: Formally Verified Approximate Policy Iteration
Title（参考訳）: 形式的に検証された近似ポリシーイテレーション
Authors: Maximilian Schäffeler, Mohammad Abdulaziz,
Abstract要約: 形式化されたアルゴリズムが実行可能で検証可能な実装にどのように洗練されるかを示す。実装は、その実行可能性を示すために、ベンチマーク問題で評価される。この改良の一環として,線形プログラミングソリューションを認証する検証ソフトウェアを開発した。
参考スコア（独自算出の注目度）: 11.602089225841633
License: http://creativecommons.org/licenses/by/4.0/
Abstract: We formally verify an algorithm for approximate policy iteration on Factored Markov Decision Processes using the interactive theorem prover Isabelle/HOL. Next, we show how the formalized algorithm can be refined to an executable, verified implementation. The implementation is evaluated on benchmark problems to show its practicability. As part of the refinement, we develop verified software to certify Linear Programming solutions. The algorithm builds on a diverse library of formalized mathematics and pushes existing methodologies for interactive theorem provers to the limits. We discuss the process of the verification project and the modifications to the algorithm needed for formal verification.
Abstract（参考訳）: 対話型定理証明器Isabelle/HOLを用いてマルコフ決定過程の近似ポリシー反復のアルゴリズムを正式に検証する。次に,形式化されたアルゴリズムを,実行可能かつ検証可能な実装に改良する方法を示す。実装は、その実行可能性を示すために、ベンチマーク問題で評価される。この改良の一環として,線形プログラミングソリューションを認証する検証ソフトウェアを開発した。このアルゴリズムは、形式化された数学の多種多様なライブラリの上に構築され、インタラクティブな定理証明者のための既存の方法論を限界まで押し上げる。本稿では,検証プロジェクトのプロセスと,形式検証に必要なアルゴリズムの変更について論じる。

関連論文リスト

Improving LLM Reasoning through Scaling Inference Computation with Collaborative Verification [52.095460362197336]
大規模言語モデル(LLM)は一貫性と正確な推論に苦しむ。 LLMは、主に正しいソリューションに基づいて訓練され、エラーを検出して学習する能力を減らす。本稿では,CoT(Chain-of-Thought)とPoT(Program-of-Thought)を組み合わせた新しい協調手法を提案する。
論文参考訳（メタデータ） (2024-10-05T05:21:48Z)
Bisimulation Learning [55.859538562698496]
我々は、大きな、潜在的に無限の状態空間を持つ状態遷移系の有限バイシミュレートを計算する。提案手法は,実際に行われている他の最先端ツールよりも高速な検証結果が得られる。
論文参考訳（メタデータ） (2024-05-24T17:11:27Z)
Automatic Program Instrumentation for Automatic Verification (Extended Technical Report) [0.0]
帰納的検証とソフトウェアモデルチェックでは、特定の仕様言語構造を扱うことが問題となる。本稿では,様々なアドホックなアプローチを仮定する統一検証パラダイムとして,インスツルメンテーションを提案する。我々は,プログラムのアグリゲーションによる検証に適したMonoCeraツールにアプローチを実装した。
論文参考訳（メタデータ） (2023-05-26T14:55:35Z)
FastDiagP: An Algorithm for Parallelized Direct Diagnosis [64.65251961564606]
FastDiagは、競合を事前に決定せずに診断計算をサポートする典型的な直接診断アルゴリズムである。本稿では,投機的プログラミングのアイデアに基づく新しいアルゴリズムであるFastDiagPを提案する。このメカニズムは、高速な回答で一貫性チェックを提供し、アルゴリズムのランタイムパフォーマンスを高めるのに役立つ。
論文参考訳（メタデータ） (2023-05-11T16:26:23Z)
Making Linear MDPs Practical via Contrastive Representation Learning [101.75885788118131]
マルコフ決定過程(MDP)における次元性の呪いに、低ランク表現を利用することで対処することが一般的である。本稿では,効率的な表現学習を可能にしつつ,正規化を自動的に保証する線形MDPの代替的定義について考察する。いくつかのベンチマークにおいて、既存の最先端モデルベースおよびモデルフリーアルゴリズムよりも優れた性能を示す。
論文参考訳（メタデータ） (2022-07-14T18:18:02Z)
Formally Verified Solution Methods for Infinite-Horizon Markov Decision Processes [7.538482310185133]
確率論の既存の形式化に基づいて、無限水平問題における期待される全報酬基準を解析する。我々の発展はベルマン方程式を形式化し、最適なポリシーが存在する条件を与える。我々のシステムは最先端のシステムと競合し、さらに性能も向上できることを示す。
論文参考訳（メタデータ） (2022-06-05T13:03:34Z)
Formal Semantics and Formally Verified Validation for Temporal Planning [7.538482310185133]
時間計画のための簡潔で簡潔な意味論を提示する。このセマンティクスは対話型定理証明器 Isabelle/HOL の論理で開発・形式化されている。我々はこれらのセマンティクスから時間計画のための検証アルゴリズムを導き、Isabelle/HOLの形式的証明を用いて、この検証アルゴリズムが我々のセマンティクスを実装していることを示す。
論文参考訳（メタデータ） (2022-03-25T12:04:03Z)
Counterfactual Explanations in Sequential Decision Making Under Uncertainty [27.763369810430653]
本研究では, 逐次的意思決定プロセスにおいて, 対実的説明を求める手法を開発した。我々の問題定式化において、反実的説明は、少なくとも k 個の作用において異なる作用の別の列を特定する。提案アルゴリズムは,不確実性の下での意思決定の促進に有用な洞察を与えることができることを示す。
論文参考訳（メタデータ） (2021-07-06T17:38:19Z)
Modularity in Reinforcement Learning via Algorithmic Independence in Credit Assignment [79.5678820246642]
提案手法は, 事前決定の順序に対して, スパース変化のみを必要とする伝達問題に対して, 政策段階の手法よりも, より標本効率が高いことを示す。我々は最近提案された社会的意思決定の枠組みをマルコフ決定プロセスよりもよりきめ細かい形式主義として一般化する。
論文参考訳（メタデータ） (2021-06-28T21:29:13Z)
Information Theoretic Meta Learning with Gaussian Processes [74.54485310507336]
情報理論の概念,すなわち相互情報と情報のボトルネックを用いてメタ学習を定式化する。相互情報に対する変分近似を用いることで、メタ学習のための汎用的かつトラクタブルな枠組みを導出する。
論文参考訳（メタデータ） (2020-09-07T16:47:30Z)
Verification and Validation of Convex Optimization Algorithms for Model Predictive Control [1.5322124183968633]
本稿では,凸最適化アルゴリズムであるEllipsoid法とそのコード実装の形式的検証について述べる。これらのコードプロパティと証明の適用性と制限も提示される。数値安定性の制御に使用できるアルゴリズムの修正について述べる。
論文参考訳（メタデータ） (2020-05-26T09:18:14Z)

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