論文の概要: Gym-saturation: an OpenAI Gym environment for saturation provers
- arxiv url: http://arxiv.org/abs/2203.04699v1
- Date: Wed, 9 Mar 2022 13:22:15 GMT
- ステータス: 処理完了
- システム内更新日: 2022-03-10 23:19:58.807662
- Title: Gym-saturation: an OpenAI Gym environment for saturation provers
- Title(参考訳): Gym-saturation:Saturation ProversのためのOpenAI Gym環境
- Authors: Boris Shminke
- Abstract要約: ジム飽和は、定理を証明できる強化学習(RL)エージェントのためのOpenAI Gym環境である。
ジム飽和は「ギヴン節」アルゴリズムを実装している(ヴァンパイアとEプロバーで使用されるものに似ている)
- 参考スコア(独自算出の注目度): 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: `gym-saturation` is an OpenAI Gym environment for reinforcement learning (RL)
agents capable of proving theorems. Currently, only theorems written in a
formal language of the Thousands of Problems for Theorem Provers (TPTP) library
in clausal normal form (CNF) are supported. `gym-saturation` implements the
'given clause' algorithm (similar to the one used in Vampire and E Prover).
Being written in Python, `gym-saturation` was inspired by PyRes. In contrast to
the monolithic architecture of a typical Automated Theorem Prover (ATP),
`gym-saturation` gives different agents opportunities to select clauses
themselves and train from their experience. Combined with a particular agent,
`gym-saturation` can work as an ATP. Even with a non trained agent based on
heuristics, `gym-saturation` can find refutations for 688 (of 8257) CNF
problems from TPTP v7.5.0.
- Abstract(参考訳): gm-saturationは、定理を証明できる強化学習(RL)エージェントのためのOpenAI Gym環境である。
現在、クローサル正規形(cnf)の定理プロバース(tptp)ライブラリの何千もの問題の形式言語で書かれた定理のみがサポートされている。
gym-saturationは'given clause'アルゴリズム(ヴァンパイアとe proverで使われるものと似ている)を実装している。
pythonで書かれた`gym-saturation`はpyresにインスパイアされた。
典型的な Automated Theorem Prover (ATP) のモノリシックなアーキテクチャとは対照的に, ‘gym-saturation’ は各エージェントに対して,自分自身で句を選択して経験からトレーニングする機会を提供する。
特定のエージェントと組み合わせることで、"gym-saturation"はATPとして機能する。
ヒューリスティックスに基づく訓練を受けていないエージェントであっても、"ジャム飽和"はTPTP v7.5.0から688(8257)のCNF問題に対する難題を見つけることができる。
関連論文リスト
- REFACTOR: Learning to Extract Theorems from Proofs [29.44286369265644]
我々は、REFACTORが、人間が証明を書くのに使用する定理の19.6%を抽出できることを示した。
新たに抽出された定理により,既存のMetaMathデータベースが構築可能であることを示す。
また、新理論データセットでトレーニングされた証明者が、より多くのテスト定理を証明し、最先端のベースラインを上回ることを実証する。
論文 参考訳(メタデータ) (2024-02-26T21:21:30Z) - MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [88.72298746872396]
MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。
5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。
我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
論文 参考訳(メタデータ) (2024-02-14T05:57:58Z) - ReFT: Reasoning with Reinforced Fine-Tuning [10.388069041382195]
本稿では,Reinforced Fine-Tuning (ReFT) というシンプルな手法を提案する。
ReFTはまずSFTを用いてモデルをウォームアップし,さらにオンライン強化学習,特に本論文のPPOアルゴリズムを用いる。
GSM8K、MathQA、SVAMPデータセットの実験では、ReFTがSFTを大幅に上回っている。
論文 参考訳(メタデータ) (2024-01-17T04:43:21Z) - Self-regulating Prompts: Foundational Model Adaptation without
Forgetting [112.66832145320434]
本稿では,PromptSRCと呼ばれる自己正規化フレームワークを提案する。
PromptSRCはタスク固有の汎用表現とタスクに依存しない汎用表現の両方に最適化するプロンプトを導く。
論文 参考訳(メタデータ) (2023-07-13T17:59:35Z) - TheoremQA: A Theorem-driven Question Answering dataset [100.39878559382694]
GPT-4のこれらの問題を解決する能力は非並列であり、Program-of-Thoughts Promptingの精度は51%である。
TheoremQAは、350の定理をカバーする800の高品質な質問を含むドメインの専門家によってキュレートされる。
論文 参考訳(メタデータ) (2023-05-21T17:51:35Z) - Comment on 'The operational foundations of PT-symmetric and
quasi-Hermitian quantum theory' [0.0]
著者の主な発見(つまり、QHQTが標準量子論を拡張しない)は、新しいものではないことを指摘した。
数学的に一貫した GPT のような理論は、すでに文献で利用可能である。
論文 参考訳(メタデータ) (2023-01-03T17:06:31Z) - Project proposal: A modular reinforcement learning based automated
theorem prover [0.0]
我々は独立したコンポーネントの強化学習証明を構築することを提案する。
我々は,Saturation Provers 用の OpenAI Gym 環境パッケージを $textttgym-saturation$ に追加の Vampire ベースの環境にコントリビュートする。
論文 参考訳(メタデータ) (2022-09-06T15:12:53Z) - Training a First-Order Theorem Prover from Synthetic Data [50.23600875138756]
自動定理証明に機械学習を適用する際の大きな課題は、トレーニングデータの不足である。
本稿では,人間のデータを公理によらずに,純粋に合成生成定理をトレーニングする手法を提案する。
私達の神経証明者は時間および検索のステップのこの総合的なデータで最先端のE-proverを上回っます。
論文 参考訳(メタデータ) (2021-03-05T17:01:34Z) - Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。
本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
論文 参考訳(メタデータ) (2020-09-07T19:50:10Z) - Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
我々は、定理証明器を訓練するために、定理と証明を自動的に合成するニューラルジェネレータを学習する。
実世界の課題に関する実験は、我々の手法による合成データが定理証明器を改善することを示した。
論文 参考訳(メタデータ) (2020-02-17T16:06:02Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。