論文の概要: Training a First-Order Theorem Prover from Synthetic Data
- arxiv url: http://arxiv.org/abs/2103.03798v1
- Date: Fri, 5 Mar 2021 17:01:34 GMT
- ステータス: 処理完了
- システム内更新日: 2021-03-08 14:53:14.590940
- Title: Training a First-Order Theorem Prover from Synthetic Data
- Title（参考訳）: 合成データによる第一次定理証明の訓練
- Authors: Vlad Firoiu, Eser Aygun, Ankit Anand, Zafarali Ahmed, Xavier Glorot,
Laurent Orseau, Lei Zhang, Doina Precup, Shibl Mourad
- Abstract要約: 自動定理証明に機械学習を適用する際の大きな課題は、トレーニングデータの不足である。
本稿では,人間のデータを公理によらずに,純粋に合成生成定理をトレーニングする手法を提案する。
私達の神経証明者は時間および検索のステップのこの総合的なデータで最先端のE-proverを上回っます。
- 参考スコア（独自算出の注目度）: 50.23600875138756
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: A major challenge in applying machine learning to automated theorem proving
is the scarcity of training data, which is a key ingredient in training
successful deep learning models. To tackle this problem, we propose an approach
that relies on training purely with synthetically generated theorems, without
any human data aside from axioms. We use these theorems to train a
neurally-guided saturation-based prover. Our neural prover outperforms the
state-of-the-art E-prover on this synthetic data in both time and search steps,
and shows significant transfer to the unseen human-written theorems from the
TPTP library, where it solves 72\% of first-order problems without equality.
- Abstract（参考訳）: 機械学習を自動定理証明に適用する上での大きな課題は、ディープラーニングモデルを成功させる上で重要な要素であるトレーニングデータの不足である。
この問題に取り組むために,我々は,人間のデータを公理以外に使わずに,純粋に合成生成定理をトレーニングする手法を提案する。
これらの定理を使用して、神経誘導飽和ベースの証明者を訓練する。
私たちのニューラルネットワークは、この合成データにおける最先端のE-proverを時間と検索の両方のステップで上回っており、TPTPライブラリから見えない人間の記述定理に有意な移行を示しており、一階問題の72\%を平等に解決します。
関連論文リスト
- Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。
マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。
その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
論文 参考訳（メタデータ） (2024-10-21T08:04:21Z) - Training Nonlinear Transformers for Chain-of-Thought Inference: A Theoretical Generalization Analysis [82.51626700527837]
チェーン・オブ・シフト(Chain-of-shift, CoT)は、複数の中間ステップを持つ例を用いてクエリを増強することにより、大規模言語モデルの推論能力を実現する効率的な手法である。
CoT の理論的成功にもかかわらず、CoT が成立しても正確な一般化が得られないことを示す。
論文 参考訳（メタデータ） (2024-10-03T03:12:51Z) - How does unlabeled data improve generalization in self-training? A
one-hidden-layer theoretical analysis [93.37576644429578]
この研究は、既知の反復的自己学習パラダイムに関する最初の理論的分析を確立する。
トレーニング収束と一般化能力の両面で、ラベルなしデータの利点を実証する。
また、浅部ニューラルネットワークから深部ニューラルネットワークへの実験は、我々の確立した自己学習に関する理論的知見の正しさを正当化するものである。
論文 参考訳（メタデータ） (2022-01-21T02:16:52Z) - Graph Contrastive Pre-training for Effective Theorem Reasoning [6.721845345130468]
既存の手法は、人間の専門家による証明から深層ニューラルネットワークに基づくモデルを学ぶことによって、戦術予測の有望な結果を示す。
本稿では,定理証明のための表現学習の改善に着目した新しい拡張であるNeuroTacticを提案する。
論文 参考訳（メタデータ） (2021-08-24T16:14:54Z) - Proof Artifact Co-training for Theorem Proving with Language Models [4.934817254755007]
PACT(bf Proof bf Artifact bf Co-bf Training)は、カーネルレベルのコトレーニング用証明項から自己教師付きデータを抽出する一般的な手法である。
我々は、Transformer言語モデルによって駆動されるニューラル定理証明器でリーンを計測し、PACTがテスト定理の保留組における成功率を証明する定理を32%から48%に改善することを示す。
論文 参考訳（メタデータ） (2021-02-11T18:59:24Z) - The Gaussian equivalence of generative models for learning with shallow
neural networks [30.47878306277163]
本研究では,事前学習した生成モデルから得られたデータに基づいて学習したニューラルネットワークの性能について検討する。
この等価性を裏付ける厳密で解析的で数値的な証拠を3本提供します。
これらの結果は、現実的なデータを持つ機械学習モデルの理論研究への有効な道を開く。
論文 参考訳（メタデータ） (2020-06-25T21:20:09Z) - Learning to Prove from Synthetic Theorems [41.74768503409581]
自動定理証明に機械学習を適用する上での大きな課題は、トレーニングデータの不足である。
本稿では,一組の公理から生成される合成定理による学習に依存するアプローチを提案する。
このような定理が自動証明器の訓練に利用でき、学習された証明器が人間の生成した定理にうまく移行できることが示される。
論文 参考訳（メタデータ） (2020-06-19T17:48:09Z) - Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
我々は、定理証明器を訓練するために、定理と証明を自動的に合成するニューラルジェネレータを学習する。
実世界の課題に関する実験は、我々の手法による合成データが定理証明器を改善することを示した。
論文 参考訳（メタデータ） (2020-02-17T16:06:02Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。