論文の概要: Learning to Prove from Synthetic Theorems
- arxiv url: http://arxiv.org/abs/2006.11259v1
- Date: Fri, 19 Jun 2020 17:48:09 GMT
- ステータス: 処理完了
- システム内更新日: 2022-11-19 05:16:13.758288
- Title: Learning to Prove from Synthetic Theorems
- Title（参考訳）: 合成定理から証明する学習
- Authors: Eser Ayg\"un, Zafarali Ahmed, Ankit Anand, Vlad Firoiu, Xavier Glorot,
Laurent Orseau, Doina Precup, Shibl Mourad
- Abstract要約: 自動定理証明に機械学習を適用する上での大きな課題は、トレーニングデータの不足である。
本稿では,一組の公理から生成される合成定理による学習に依存するアプローチを提案する。
このような定理が自動証明器の訓練に利用でき、学習された証明器が人間の生成した定理にうまく移行できることが示される。
- 参考スコア（独自算出の注目度）: 41.74768503409581
- 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 with synthetic theorems, generated from a set of
axioms. We show that such theorems can be used to train an automated prover and
that the learned prover transfers successfully to human-generated theorems. We
demonstrate that a prover trained exclusively on synthetic theorems can solve a
substantial fraction of problems in TPTP, a benchmark dataset that is used to
compare state-of-the-art heuristic provers. Our approach outperforms a model
trained on human-generated problems in most axiom sets, thereby showing the
promise of using synthetic data for this task.
- Abstract（参考訳）: 自動定理証明に機械学習を適用する上での大きな課題は、トレーニングデータの不足である。
この問題に対処するために,一組の公理から生成される合成定理による訓練に依存するアプローチを提案する。
このような定理は自動証明器の訓練に利用でき、学習された証明器は人間の生成した定理にうまく移行できることを示す。
合成定理のみを専門とする証明器は,最先端のヒューリスティックな証明器を比較するために用いられるベンチマークデータセットであるTPTPにおいて,かなりの数の問題を解くことができることを示す。
提案手法は,ほとんどの公理集合において人間が生成する問題に対して学習したモデルよりも優れており,このタスクに合成データを使用することの期待を示す。
関連論文リスト
- 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) - Discovering Interpretable Physical Models using Symbolic Regression and
Discrete Exterior Calculus [55.2480439325792]
本稿では,記号回帰(SR)と離散指数計算(DEC)を組み合わせて物理モデルの自動発見を行うフレームワークを提案する。
DECは、SRの物理問題への最先端の応用を越えている、場の理論の離散的な類似に対して、ビルディングブロックを提供する。
実験データから連続体物理の3つのモデルを再発見し,本手法の有効性を実証する。
論文 参考訳（メタデータ） (2023-10-10T13:23:05Z) - 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) - 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) - Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。
本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
論文 参考訳（メタデータ） (2020-09-07T19:50:10Z) - IsarStep: a Benchmark for High-level Mathematical Reasoning [20.96474618260995]
本稿では,高レベルな数学的推論のためのベンチマークを提案し,ニューラルシークエンス・ツー・シーケンスモデルの推論能力について検討する。
我々は、人間の専門家が定理証明器で記述した最大の証明のリポジトリから、非合成データセットを構築した。
論文 参考訳（メタデータ） (2020-06-13T21:09:23Z) - Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
我々は、定理証明器を訓練するために、定理と証明を自動的に合成するニューラルジェネレータを学習する。
実世界の課題に関する実験は、我々の手法による合成データが定理証明器を改善することを示した。
論文 参考訳（メタデータ） (2020-02-17T16:06:02Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。