論文の概要: Proving Theorems using Incremental Learning and Hindsight Experience Replay

• arxiv url: http://arxiv.org/abs/2112.10664v1
• Date: Mon, 20 Dec 2021 16:40:26 GMT
• ステータス: 処理完了
• システム内更新日: 2021-12-21 17:30:31.892632
• Title: Proving Theorems using Incremental Learning and Hindsight Experience Replay
• Title（参考訳）: インクリメンタル学習と後見経験リプレイを用いた定理の証明
• Authors: Eser Ayg\"un, Laurent Orseau, Ankit Anand, Xavier Glorot, Vlad Firoiu, Lei M. Zhang, Doina Precup and Shibl Mourad
• Abstract要約: 等式のない一階述語論理のドメイン固有プローバを学習するための一般的な漸進学習アルゴリズムを提案する。 我々は、証明が見つからない場合でも学べるように、後見経験の再生を定理証明に適用する。 我々は、この方法で訓練されたプローバーがTPTPデータセットの最先端の伝統的なプローバーにマッチし、時には超えることを示した。
• 参考スコア（独自算出の注目度）: 45.277067974919106
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Traditional automated theorem provers for first-order logic depend on speed-optimized search and many handcrafted heuristics that are designed to work best over a wide range of domains. Machine learning approaches in literature either depend on these traditional provers to bootstrap themselves or fall short on reaching comparable performance. In this paper, we propose a general incremental learning algorithm for training domain specific provers for first-order logic without equality, based only on a basic given-clause algorithm, but using a learned clause-scoring function. Clauses are represented as graphs and presented to transformer networks with spectral features. To address the sparsity and the initial lack of training data as well as the lack of a natural curriculum, we adapt hindsight experience replay to theorem proving, so as to be able to learn even when no proof can be found. We show that provers trained this way can match and sometimes surpass state-of-the-art traditional provers on the TPTP dataset in terms of both quantity and quality of the proofs.
• Abstract（参考訳）: 一階述語論理の伝統的な自動定理証明は、速度最適化された探索と、幅広い領域で最適に動作するように設計された多くの手作りのヒューリスティックに依存する。 文学における機械学習のアプローチは、これらの従来のプロバーの自己ブートストラップに依存するか、同等のパフォーマンスに達するのに不足している。 本稿では,基本条件付きアルゴリズムのみをベースとした一階述語論理の学習を行うための一般的な漸進的学習アルゴリズムを提案する。 節はグラフとして表現され、スペクトル特徴を持つトランスフォーマーネットワークに提示される。 自然カリキュラムの欠如に加えて,トレーニングデータのスパース性と初期欠如に対処するために,後見経験リプレイを定理証明に適用し,証明が見つからない場合でも学習できるようにする。 この方法で訓練されたプローバーは、証明の量と品質の両方の観点から、TPTPデータセット上の最先端の伝統的なプローバーにマッチし、時には超えることを示す。

関連論文リスト

• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)
• Learn from Failure: Fine-Tuning LLMs with Trial-and-Error Data for Intuitionistic Propositional Logic Proving [41.23045212775232]
  探索経路の失敗から学習する訓練モデルの利点を実証する。 既存のオープンソース定理証明データセットにそのような試行錯誤データが欠如しているにもかかわらず、直観論的命題論理定理のデータセットをキュレートする。 比較的短いトライアル・アンド・エラー情報(TrialMaster)で訓練されたモデルと、正しい経路でのみ訓練されたモデルを比較し、前者が低いトライアル探索でより目に見えない定理を解くことを発見した。
  論文  参考訳（メタデータ） (2024-04-10T23:01:45Z)
• ReFT: Reasoning with Reinforced Fine-Tuning [9.80361828538909]
  本稿では,Reinforced Fine-Tuning (ReFT) というシンプルな手法を提案する。 ReFTはまずSFTを用いてモデルをウォームアップし,さらにオンライン強化学習,特に本論文のPPOアルゴリズムを用いる。 GSM8K、MathQA、SVAMPデータセットの実験では、ReFTがSFTを大幅に上回っている。
  論文  参考訳（メタデータ） (2024-01-17T04:43:21Z)
• Learning to Guide a Saturation-Based Theorem Prover [9.228237801323042]
  TRAILは、ニューラルネットワーク内で証明される飽和に基づく定理の中核要素を特徴付ける、深い学習に基づく定理証明のアプローチである。 我々の知る限りでは、TRAILは最先端の伝統的な定理証明器の性能を超える最初の強化学習に基づくアプローチである。
  論文  参考訳（メタデータ） (2021-06-07T18:35:57Z)
• Training a First-Order Theorem Prover from Synthetic Data [50.23600875138756]
  自動定理証明に機械学習を適用する際の大きな課題は、トレーニングデータの不足である。 本稿では,人間のデータを公理によらずに,純粋に合成生成定理をトレーニングする手法を提案する。 私達の神経証明者は時間および検索のステップのこの総合的なデータで最先端のE-proverを上回っます。
  論文  参考訳（メタデータ） (2021-03-05T17:01:34Z)
• Multi-Agent Reinforcement Learning with Temporal Logic Specifications [65.79056365594654]
  本研究では,時間論理仕様を満たすための学習課題を,未知の環境下でエージェントのグループで検討する。 我々は、時間論理仕様のための最初のマルチエージェント強化学習手法を開発した。 主アルゴリズムの正確性と収束性を保証する。
  論文  参考訳（メタデータ） (2021-02-01T01:13:03Z)
• Learning Reasoning Strategies in End-to-End Differentiable Proving [50.9791149533921]
  条件付き定理プローバーは勾配に基づく最適化により最適規則選択戦略を学習する。 条件付き定理プローサは拡張性があり、CLUTRRデータセット上で最先端の結果が得られることを示す。
  論文  参考訳（メタデータ） (2020-07-13T16:22:14Z)
• Learning to Prove from Synthetic Theorems [41.74768503409581]
  自動定理証明に機械学習を適用する上での大きな課題は、トレーニングデータの不足である。 本稿では,一組の公理から生成される合成定理による学習に依存するアプローチを提案する。 このような定理が自動証明器の訓練に利用でき、学習された証明器が人間の生成した定理にうまく移行できることが示される。
  論文  参考訳（メタデータ） (2020-06-19T17:48:09Z)
• Distance-Based Regularisation of Deep Networks for Fine-Tuning [116.71288796019809]
  我々は,仮説クラスを,初期訓練前の重みを中心にした小さな球面に制約するアルゴリズムを開発した。 実験的な評価は、我々のアルゴリズムがうまく機能していることを示し、理論的な結果を裏付けるものである。
  論文  参考訳（メタデータ） (2020-02-19T16:00:47Z)
• An Experimental Study of Formula Embeddings for Automated Theorem Proving in First-Order Logic [13.633012068936894]
  本研究では,一般的なグラフベースエンコーディングを持つ現行システムに適用されるパターンベースの埋め込みについて,実験的に比較する。 実験により、より複雑なグラフベースの埋め込みにより、より単純な実行時の符号化方式の利点が打ち消されることが示された。
  論文  参考訳（メタデータ） (2020-02-02T16:07:15Z)

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

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