論文の概要: Project proposal: A modular reinforcement learning based automated
theorem prover
- arxiv url: http://arxiv.org/abs/2209.02562v1
- Date: Tue, 6 Sep 2022 15:12:53 GMT
- ステータス: 処理完了
- システム内更新日: 2022-09-07 13:50:55.703246
- Title: Project proposal: A modular reinforcement learning based automated
theorem prover
- Title(参考訳): プロジェクト提案:モジュラー強化学習に基づく自動定理証明器
- Authors: Boris Shminke
- Abstract要約: 我々は独立したコンポーネントの強化学習証明を構築することを提案する。
我々は,Saturation Provers 用の OpenAI Gym 環境パッケージを $textttgym-saturation$ に追加の Vampire ベースの環境にコントリビュートする。
- 参考スコア(独自算出の注目度): 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: We propose to build a reinforcement learning prover of independent
components: a deductive system (an environment), the proof state representation
(how an agent sees the environment), and an agent training algorithm. To that
purpose, we contribute an additional Vampire-based environment to
$\texttt{gym-saturation}$ package of OpenAI Gym environments for saturation
provers. We demonstrate a prototype of using $\texttt{gym-saturation}$ together
with a popular reinforcement learning framework (Ray $\texttt{RLlib}$).
Finally, we discuss our plans for completing this work in progress to a
competitive automated theorem prover.
- Abstract(参考訳): 提案手法は,推論システム(環境),証明状態表現(エージェントが環境をどのように見ているか),エージェントトレーニングアルゴリズムといった,独立したコンポーネントの強化学習証明器を構築することを目的とする。
その目的のために、飽和プロデューサのためのOpenAI Gym環境パッケージの$\texttt{gym-saturation}$に、Vampireベースの環境を追加提供します。
一般的な強化学習フレームワーク(Ray $\texttt{RLlib}$)と一緒に$\texttt{gym-saturation}$を使用するプロトタイプを実演する。
最後に,本研究の完成に向けての計画について,競合する自動定理証明者に向けて議論する。
関連論文リスト
- Inertial Confinement Fusion Forecasting via LLMs [49.954202788661156]
本研究では,従来の貯水池計算パラダイムとLarge Language Models(LLM)の新たな統合である$textbfFusion-LLM$を紹介する。
本研究では, 核融合特異的プロンプトを付加した$textitLLM-anchored Reservoir$を提案し, インロジョン中の熱電子ダイナミクスの正確な予測を可能にする。
また、物理実験に基づく最初の$textttICF$ベンチマークである$textbfFusion4AI$も提示し、プラズマ物理学研究における新しいアイデアの育成を目的としている。
論文 参考訳(メタデータ) (2024-07-15T05:46:44Z) - Jointly Training and Pruning CNNs via Learnable Agent Guidance and Alignment [69.33930972652594]
本稿では,CNNモデルの重みと構造的プーン構造を協調的に学習するための新しい構造的プルーニング手法を提案する。
本手法の中核となる要素は強化学習(RL)エージェントであり,その動作がCNNモデルの階層のプルーニング比を決定する。
我々は,モデルの重みとエージェントのポリシーを反復的に訓練し,共同訓練と刈り取りを行う。
論文 参考訳(メタデータ) (2024-03-28T15:22:29Z) - gym-saturation: Gymnasium environments for saturation provers (System
description) [0.0]
VampireとiProverの2つの異なるプロバーで使用例を提供しています。
環境ラッパーが証明器をマルチアームバンディットに類似した問題に変換する方法を示す。
論文 参考訳(メタデータ) (2023-09-16T15:25:39Z) - Unifying Language Learning Paradigms [96.35981503087567]
データセットやセットアップ全体にわたって普遍的に有効である事前学習モデルのための統一的なフレームワークを提案する。
本研究では, 事前学習対象を相互に配置し, 異なる対象間の補間を効果的に行う方法を示す。
また,テキスト内学習において,ゼロショットSuperGLUEで175B GPT-3,ワンショット要約でT5-XXLの性能を3倍に向上させた。
論文 参考訳(メタデータ) (2022-05-10T19:32:20Z) - Efficiently Training On-Policy Actor-Critic Networks in Robotic Deep
Reinforcement Learning with Demonstration-like Sampled Exploration [7.930709072852582]
本稿では,アクター批判アルゴリズムに基づく実証から学ぶための一般的なフレームワークを提案する。
我々は,Mujocoの4つの標準ベンチマーク環境と,自設計の2つのロボット環境について実験を行った。
論文 参考訳(メタデータ) (2021-09-27T12:42:05Z) - MEPG: A Minimalist Ensemble Policy Gradient Framework for Deep
Reinforcement Learning [26.349085280990657]
本稿では,資源消費問題を解決するために,新しい単純なアンサンブル・ディープRLアルゴリズムを提案する。
我々は、最小限のアンサンブル一貫性を持つベルマン更新を導入したアンダーラインミニマリスト underlineEnsemble underlinePolicy underlineGradient framework (MEPG)を提案する。
論文 参考訳(メタデータ) (2021-09-22T07:30:52Z) - DRILL-- Deep Reinforcement Learning for Refinement Operators in
$\mathcal{ALC}$ [1.9036571490366496]
本稿では,畳み込み型Q-ラーニングモデルを用いた新しいクラス表現学習手法DRILLを提案する。
そのアーキテクチャにより、DRILLは標準ハードウェア上で1秒で103ドル以上のクラス表現の期待値の累積的な将来の報酬を計算することができる。
論文 参考訳(メタデータ) (2021-06-29T12:57:45Z) - PsiPhi-Learning: Reinforcement Learning with Demonstrations using
Successor Features and Inverse Temporal Difference Learning [102.36450942613091]
時間差学習(ITD)と呼ばれる逆強化学習アルゴリズムを提案する。
Psi Phi$-learningと呼ばれるデモで強化学習のための新しいアルゴリズムに到達し、オンライン環境の相互作用から学習とITDをシームレスに統合する方法を示します。
論文 参考訳(メタデータ) (2021-02-24T21:12:09Z) - A Generic and Model-Agnostic Exemplar Synthetization Framework for
Explainable AI [29.243901669124515]
我々は、説明可能なAIに焦点をあて、入力例を合成するための新しい汎用的でモデルに依存しないフレームワークを提案する。
我々は、データ生成の先行として機能する生成モデルを使用し、新しい進化戦略を用いて、その潜在空間をトラバースする。
私たちのフレームワークはモデルに依存しませんが、私たちが説明しようとしている機械学習モデルはブラックボックスです。
論文 参考訳(メタデータ) (2020-06-06T15:46:48Z) - A Model-driven Deep Neural Network for Single Image Rain Removal [52.787356046951494]
完全解釈可能なネットワーク構造を持つモデル駆動型ディープニューラルネットワークを提案する。
雨を表現するための畳み込み辞書学習機構に基づいて,新しい単一画像デレーニングモデルを提案する。
すべてのレインカーネルとオペレータは自動的に抽出され、レイン層とクリーンなバックグラウンド層の両方の特徴を忠実に特徴付けることができる。
論文 参考訳(メタデータ) (2020-05-04T09:13:25Z) - Budget Learning via Bracketing [50.085728094234476]
予算学習の問題は、学習者の目標として、雲の使用を最小限に抑えつつ、精度の明確な損失を被ることである。
本稿ではブラケットの概念を用いてBL問題に対する新しい定式化を提案する。
我々は、実世界のデータセットに関する我々の理論を実証的に検証し、事前ゲーティングに基づく手法よりも優れた性能を示す。
論文 参考訳(メタデータ) (2020-04-14T04:38:14Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。