論文の概要: 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問題に対する難題を見つけることができる。

関連論文リスト

• Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically [29.908878832382523]
  本稿では,自動検証/評価を可能にする形式言語による証明記述能力の向上に焦点をあてる。 我々は、定理に直接関係する補題がテスト時の定理証明者に与えられないより自然な設定で作業する。 我々は、モデルが定理を補題に分解し、補題を証明し、補題を用いて定理を証明することを奨励するRLベースの訓練アルゴリズムを設計する。
  論文  参考訳（メタデータ） (2024-11-04T05:57:40Z)
• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。 マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。 その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
  論文  参考訳（メタデータ） (2024-10-21T08:04:21Z)
• ATG: Benchmarking Automated Theorem Generation for Generative Language Models [83.93978859348313]
  人間はより広範に複雑な数学的結果を探求するために新しい定理を開発することができる。 現在の生成言語モデル(LM)は、定理の自動証明において著しく改善されている。 本稿では,エージェントが価値ある(あるいは新しい)定理を自動生成できるかどうかを評価する自動定理生成ベンチマークを提案する。
  論文  参考訳（メタデータ） (2024-05-05T02:06:37Z)
• 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)
• 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)
• Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
  我々は、定理証明器を訓練するために、定理と証明を自動的に合成するニューラルジェネレータを学習する。 実世界の課題に関する実験は、我々の手法による合成データが定理証明器を改善することを示した。
  論文  参考訳（メタデータ） (2020-02-17T16:06:02Z)

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

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