論文の概要: Learning to Prove Theorems by Learning to Generate Theorems
- arxiv url: http://arxiv.org/abs/2002.07019v2
- Date: Fri, 30 Oct 2020 04:33:04 GMT
- ステータス: 処理完了
- システム内更新日: 2022-12-31 11:41:08.883408
- Title: Learning to Prove Theorems by Learning to Generate Theorems
- Title(参考訳): 定理生成の学習による定理証明の学習
- Authors: Mingzhe Wang, Jia Deng
- Abstract要約: 我々は、定理証明器を訓練するために、定理と証明を自動的に合成するニューラルジェネレータを学習する。
実世界の課題に関する実験は、我々の手法による合成データが定理証明器を改善することを示した。
- 参考スコア(独自算出の注目度): 71.46963489866596
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: We consider the task of automated theorem proving, a key AI task. Deep
learning has shown promise for training theorem provers, but there are limited
human-written theorems and proofs available for supervised learning. To address
this limitation, we propose to learn a neural generator that automatically
synthesizes theorems and proofs for the purpose of training a theorem prover.
Experiments on real-world tasks demonstrate that synthetic data from our
approach improves the theorem prover and advances the state of the art of
automated theorem proving in Metamath. Code is available at
https://github.com/princeton-vl/MetaGen.
- Abstract(参考訳): 我々は、AIの重要な課題である自動定理証明の課題を考える。
深層学習は、トレーニング定理証明者にとって有望であるが、教師付き学習に利用可能な人間による定理や証明は限られている。
この制限に対処するため,定理証明器を訓練するために,定理と証明を自動的に合成するニューラルジェネレータを提案する。
実世界の課題に関する実験は、この手法による合成データが定理証明器を改良し、メタ数学における自動定理証明技術の進歩を示すものである。
コードはhttps://github.com/princeton-vl/MetaGenで入手できる。
関連論文リスト
- REFACTOR: Learning to Extract Theorems from Proofs [29.44286369265644]
我々は、REFACTORが、人間が証明を書くのに使用する定理の19.6%を抽出できることを示した。
新たに抽出された定理により,既存のMetaMathデータベースが構築可能であることを示す。
また、新理論データセットでトレーニングされた証明者が、より多くのテスト定理を証明し、最先端のベースラインを上回ることを実証する。
論文 参考訳(メタデータ) (2024-02-26T21:21:30Z) - Graph2Tac: Learning Hierarchical Representations of Math Concepts in
Theorem proving [0.6990493129893112]
AIエージェントが新しい定理を証明しているとき、その定理に関連する数学的概念や補題のほとんどは、トレーニング中に一度も見られなかったかもしれない。
これは、Coqプロジェクトの多種多様なライブラリを持ち、それぞれ独自の定義、補題、さらにはそれらの補題を証明するために使用されるカスタム戦術の手順を持つCoq証明アシスタントに特に当てはまる。
私たちは、Coqにおける機械学習のために、新しい大規模でグラフベースのデータセットを活用することで、この目標に向かっています。
論文 参考訳(メタデータ) (2024-01-05T18:52:09Z) - LEGO-Prover: Neural Theorem Proving with Growing Libraries [86.1191481712352]
LEGO-Prover では,証明された補題を含むスキルライブラリを,定理証明に使用される LLM の能力を高めるためのスキルとして活用する。
LEGO-Proverは、証明をモジュール的に構築することにより、ライブラリから取得した既存のスキルを活用し、証明プロセス中に新しいスキルを作成することができる。
我々のアブレーション研究は、これらの新たなスキルが定理の証明に役立つことを示唆し、47.1%から50.4%に改善した。
論文 参考訳(メタデータ) (2023-10-01T12:47:59Z) - TheoremQA: A Theorem-driven Question Answering dataset [100.39878559382694]
GPT-4のこれらの問題を解決する能力は非並列であり、Program-of-Thoughts Promptingの精度は51%である。
TheoremQAは、350の定理をカバーする800の高品質な質問を含むドメインの専門家によってキュレートされる。
論文 参考訳(メタデータ) (2023-05-21T17:51:35Z) - NaturalProver: Grounded Mathematical Proof Generation with Language
Models [84.2064569475095]
自然数理言語における定理証明は、数学の進歩と教育において中心的な役割を果たす。
本研究では,背景参照を条件づけて証明を生成する言語モデルであるNaturalProverを開発する。
NaturalProverは、短い(2-6ステップ)証明を必要とするいくつかの定理を証明でき、40%の時間で正しいと評価された次のステップの提案を提供することができる。
論文 参考訳(メタデータ) (2022-05-25T17:01:18Z) - 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) - Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。
本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
論文 参考訳(メタデータ) (2020-09-07T19:50:10Z) - Learning to Prove from Synthetic Theorems [41.74768503409581]
自動定理証明に機械学習を適用する上での大きな課題は、トレーニングデータの不足である。
本稿では,一組の公理から生成される合成定理による学習に依存するアプローチを提案する。
このような定理が自動証明器の訓練に利用でき、学習された証明器が人間の生成した定理にうまく移行できることが示される。
論文 参考訳(メタデータ) (2020-06-19T17:48:09Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。