Fugu-MT 論文翻訳(概要): Learning to Guide a Saturation-Based Theorem Prover

論文の概要: Learning to Guide a Saturation-Based Theorem Prover

arxiv url: http://arxiv.org/abs/2106.03906v1
Date: Mon, 7 Jun 2021 18:35:57 GMT
ステータス: 処理完了
システム内更新日: 2021-06-09 15:45:06.903772
Title: Learning to Guide a Saturation-Based Theorem Prover
Title（参考訳）: Saturation-based Theorem Prover の学習
Authors: Ibrahim Abdelaziz, Maxwell Crouse, Bassem Makni, Vernon Austil, Cristina Cornelio, Shajith Ikbal, Pavan Kapanipathi, Ndivhuwo Makondo, Kavitha Srinivas, Michael Witbrock, Achille Fokoue
Abstract要約: TRAILは、ニューラルネットワーク内で証明される飽和に基づく定理の中核要素を特徴付ける、深い学習に基づく定理証明のアプローチである。我々の知る限りでは、TRAILは最先端の伝統的な定理証明器の性能を超える最初の強化学習に基づくアプローチである。
参考スコア（独自算出の注目度）: 9.228237801323042
License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
Abstract: Traditional automated theorem provers have relied on manually tuned heuristics to guide how they perform proof search. Recently, however, there has been a surge of interest in the design of learning mechanisms that can be integrated into theorem provers to improve their performance automatically. In this work, we introduce TRAIL, a deep learning-based approach to theorem proving that characterizes core elements of saturation-based theorem proving within a neural framework. TRAIL leverages (a) an effective graph neural network for representing logical formulas, (b) a novel neural representation of the state of a saturation-based theorem prover in terms of processed clauses and available actions, and (c) a novel representation of the inference selection process as an attention-based action policy. We show through a systematic analysis that these components allow TRAIL to significantly outperform previous reinforcement learning-based theorem provers on two standard benchmark datasets (up to 36% more theorems proved). In addition, to the best of our knowledge, TRAIL is the first reinforcement learning-based approach to exceed the performance of a state-of-the-art traditional theorem prover on a standard theorem proving benchmark (solving up to 17% more problems).
Abstract（参考訳）: 従来の自動定理プローバーは、証明探索の実行方法を手動で調整したヒューリスティックに頼っている。しかし、近年、定理プロバーに統合して自動的に性能を向上させる学習機構の設計への関心が高まっている。本研究では、ニューラルネットワーク内での飽和に基づく定理のコア要素を特徴付ける、深層学習に基づく定理証明手法であるTRAILを紹介する。 TRAILは(a)論理式を表現する効果的なグラフニューラルネットワーク、(b)処理された節と利用可能なアクションの観点から飽和ベースの定理証明器の状態を示す新しい神経表現、(c)注意に基づくアクションポリシーとして推論選択プロセスの新たな表現を利用する。提案手法は, TRAILが2つの標準ベンチマークデータセットにおいて, 従来の強化学習に基づく定理証明を著しく上回り, 最大36%の定理を証明できることを示す。さらに、私たちの知る限りでは、TRAILは標準的な定理証明ベンチマーク(最大17%以上の問題を解く)における最先端の伝統的な定理証明器の性能を超える最初の強化学習ベースのアプローチである。

関連論文リスト

Graph Stochastic Neural Process for Inductive Few-shot Knowledge Graph Completion [63.68647582680998]
I-FKGC(inductive few-shot knowledge graph completion)と呼ばれる課題に焦点をあてる。帰納的推論(inductive reasoning)の概念に着想を得て,I-FKGCを帰納的推論問題とした。本稿では,仮説の連成分布をモデル化したニューラルプロセスに基づく仮説抽出器を提案する。第2のモジュールでは、この仮説に基づいて、クエリセットのトリプルが抽出された仮説と一致するかどうかをテストするグラフアテンションベースの予測器を提案する。
論文参考訳（メタデータ） (2024-08-03T13:37:40Z)
Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
論文参考訳（メタデータ） (2024-07-14T01:43:07Z)
Towards a General Framework for Continual Learning with Pre-training [55.88910947643436]
本稿では,事前学習を用いた逐次到着タスクの連続学習のための一般的な枠組みを提案する。我々はその目的を,タスク内予測,タスク同一性推論,タスク適応予測という3つの階層的構成要素に分解する。本稿では,パラメータ効率細調整(PEFT)技術と表現統計量を用いて,これらのコンポーネントを明示的に最適化する革新的な手法を提案する。
論文参考訳（メタデータ） (2023-10-21T02:03:38Z)
Neural Theorem Provers Delineating Search Area Using RNN [2.462063246087401]
一般化EMベースの手法を用いてニューラル定理の計算効率を継続的に向上するRNNNTP法を提案する。関係生成装置を効果的に、かつ、解釈可能に訓練し、トレーニングの進展に応じて全体モデルを実行することができ、計算効率も大幅に向上する。
論文参考訳（メタデータ） (2022-03-14T10:44:11Z)
Proving Theorems using Incremental Learning and Hindsight Experience Replay [45.277067974919106]
等式のない一階述語論理のドメイン固有プローバを学習するための一般的な漸進学習アルゴリズムを提案する。我々は、証明が見つからない場合でも学べるように、後見経験の再生を定理証明に適用する。我々は、この方法で訓練されたプローバーがTPTPデータセットの最先端の伝統的なプローバーにマッチし、時には超えることを示した。
論文参考訳（メタデータ） (2021-12-20T16:40:26Z)
Graph Contrastive Pre-training for Effective Theorem Reasoning [6.721845345130468]
既存の手法は、人間の専門家による証明から深層ニューラルネットワークに基づくモデルを学ぶことによって、戦術予測の有望な結果を示す。本稿では,定理証明のための表現学習の改善に着目した新しい拡張であるNeuroTacticを提案する。
論文参考訳（メタデータ） (2021-08-24T16:14:54Z)
Training a First-Order Theorem Prover from Synthetic Data [50.23600875138756]
自動定理証明に機械学習を適用する際の大きな課題は、トレーニングデータの不足である。本稿では,人間のデータを公理によらずに,純粋に合成生成定理をトレーニングする手法を提案する。私達の神経証明者は時間および検索のステップのこの総合的なデータで最先端のE-proverを上回っます。
論文参考訳（メタデータ） (2021-03-05T17:01:34Z)
Reinforcement Learning with External Knowledge by using Logical Neural Networks [67.46162586940905]
論理ニューラルネットワーク(LNN)と呼ばれる最近のニューラルシンボリックフレームワークは、ニューラルネットワークとシンボリックロジックの両方のキープロパティを同時に提供することができる。外部知識ソースからのモデルフリー強化学習を可能にする統合手法を提案する。
論文参考訳（メタデータ） (2021-03-03T12:34:59Z)
TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning [6.764610878007278]
深層強化学習を用いた対話型定理証明(ITP)の新しい手法を提案する。我々は、各状態が潜在的な導出経路の集合を表すマルコフ決定プロセス(MDP)としてITPのプロセスを定式化する。このフレームワークは、人間の専門家を使ったアプローチに匹敵するパフォーマンスを提供する。
論文参考訳（メタデータ） (2021-02-19T06:08:39Z)
Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
我々は、定理証明器を訓練するために、定理と証明を自動的に合成するニューラルジェネレータを学習する。実世界の課題に関する実験は、我々の手法による合成データが定理証明器を改善することを示した。
論文参考訳（メタデータ） (2020-02-17T16:06:02Z)
An Experimental Study of Formula Embeddings for Automated Theorem Proving in First-Order Logic [13.633012068936894]
本研究では,一般的なグラフベースエンコーディングを持つ現行システムに適用されるパターンベースの埋め込みについて,実験的に比較する。実験により、より複雑なグラフベースの埋め込みにより、より単純な実行時の符号化方式の利点が打ち消されることが示された。
論文参考訳（メタデータ） (2020-02-02T16:07:15Z)

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

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