論文の概要: MizAR 60 for Mizar 50
- arxiv url: http://arxiv.org/abs/2303.06686v1
- Date: Sun, 12 Mar 2023 15:13:05 GMT
- ステータス: 処理完了
- システム内更新日: 2023-03-14 17:28:10.522481
- Title: MizAR 60 for Mizar 50
- Title(参考訳): MizAR 60 for Mizar 50
- Authors: Jan Jakub\r{u}v, Karel Chvalovsk\'y, Zarathustra Goertzel, Cezary
Kaliszyk, Mirek Ol\v{s}\'ak, Bartosz Piotrowski, Stephan Schulz, Martin Suda,
Josef Urban
- Abstract要約: ハンマー設定でミザール定理の約60%を自動証明するAI/TPシステムを開発した。
また、自動プローバーが人間の記述したMizar証明で用いられる前提のみを使用することで助けられる場合、自動的なMizar定理の75%を自動で証明する。
- 参考スコア(独自算出の注目度): 3.2322198481646867
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: As a present to Mizar on its 50th anniversary, we develop an AI/TP system
that automatically proves about 60\% of the Mizar theorems in the hammer
setting. We also automatically prove 75\% of the Mizar theorems when the
automated provers are helped by using only the premises used in the
human-written Mizar proofs. We describe the methods and large-scale experiments
leading to these results. This includes in particular the E and Vampire
provers, their ENIGMA and Deepire learning modifications, a number of
learning-based premise selection methods, and the incremental loop that
interleaves growing a corpus of millions of ATP proofs with training
increasingly strong AI/TP systems on them. We also present a selection of Mizar
problems that were proved automatically.
- Abstract(参考訳): ミザール50周年記念として,ハンマー設定におけるミザーの定理の約60%を自動で証明するai/tpシステムを開発した。
また、自動プローバーが人間の記述したMizar証明で用いられる前提のみを使用することで助けられる場合、ミザーの定理の75%を自動で証明する。
これらの結果につながる手法と大規模実験について述べる。
具体的には、Eとヴァンパイアのプローバー、ENIGMAとDeepireの学習修正、学習ベースの前提選択方法、そして、ますます強力なAI/TPシステムをトレーニングすることで数百万のATP証明を成長させるインクリメンタルループが含まれる。
また、自動的に証明されたミザー問題の選択も提示する。
関連論文リスト
- Enhancing Neural Theorem Proving through Data Augmentation and Dynamic
Sampling Method [1.8130068086063336]
本稿では,定理証明のための新しい動的サンプリング手法であるDS-Proverを紹介する。
単純化と書き直しの戦術を複数の前提で1つの前提で戦術に分解することで、トレーニングデータセットを強化します。
ProofNetデータセットでは14.2%の最先端パフォーマンス(Pass@1)、MiniF2Fでは29.8%のパフォーマンスを実現しています。
論文 参考訳(メタデータ) (2023-12-20T09:55:21Z) - Multistage Collaborative Knowledge Distillation from a Large Language
Model for Semi-Supervised Sequence Generation [63.26957760031662]
本研究は半教師付きシーケンス生成タスクについて検討し,いくつかのラベル付き例ではモデルを微調整するには不十分である。
数発の試薬で抽出した学生モデルは、教師よりも一般的に一般化できるという発見を提示する。
論文 参考訳(メタデータ) (2023-11-15T01:28:28Z) - AutoMix: Automatically Mixing Language Models [63.911984598567834]
大規模言語モデル(LLM)が、クラウドAPIプロバイダからさまざまなサイズと構成で利用可能になった。
本稿では,より小さなLMからの出力の近似精度に基づいて,クエリを大規模LMに戦略的にルーティングする手法であるAutoMixを提案する。
論文 参考訳(メタデータ) (2023-10-19T17:57:39Z) - LEGO-Prover: Neural Theorem Proving with Growing Libraries [86.1191481712352]
LEGO-Prover では,証明された補題を含むスキルライブラリを,定理証明に使用される LLM の能力を高めるためのスキルとして活用する。
LEGO-Proverは、証明をモジュール的に構築することにより、ライブラリから取得した既存のスキルを活用し、証明プロセス中に新しいスキルを作成することができる。
我々のアブレーション研究は、これらの新たなスキルが定理の証明に役立つことを示唆し、47.1%から50.4%に改善した。
論文 参考訳(メタデータ) (2023-10-01T12:47:59Z) - HyperTree Proof Search for Neural Theorem Proving [14.677400513932852]
本稿では,変圧器を用いた自動定理証明のためのオンライン学習手順を提案する。
我々のモデルは、オンライントレーニングを通じて以前の証明検索から学習し、トレーニング分布から遠く離れた領域に一般化することができる。
HTPSだけでは、アノテートされた証明に基づいて訓練されたモデルがメタマス定理の65.4%を証明し、GPT-fにより56.5%の先行状態を著しく上回ることを示した。
論文 参考訳(メタデータ) (2022-05-23T17:49:55Z) - Sequence-level self-learning with multiple hypotheses [53.04725240411895]
我々は、自動音声認識(ASR)のためのアテンションベースシーケンス・ツー・シーケンス(seq2seq)モデルを用いた新しい自己学習手法を開発した。
従来の教師なし学習手法とは対照的に,我々はEmphmulti-task Learning(MTL)フレームワークを採用する。
実験の結果,本手法は,英語データのみを用いてトレーニングしたベースラインモデルと比較して,英文音声データのWERを14.55%から10.36%に削減できることがわかった。
論文 参考訳(メタデータ) (2021-12-10T20:47:58Z) - Learning Equational Theorem Proving [2.8784416089703955]
深層強化学習環境下で証明された方程式定理を学習するための最短解イミテーション学習(3SIL)を開発した。
自己学習されたモデルは、準群論におけるトップオープン予想の1つによって生じる問題を証明する上で、最先端のパフォーマンスを達成する。
論文 参考訳(メタデータ) (2021-02-10T16:33:07Z) - Vampire With a Brain Is a Good ITP Hammer [0.0]
我々は,効率のよい神経誘導による飽和手順の強化により,完全なMizarライブラリ上でのハンティングにおけるヴァンパイアの性能を向上させる。
節の論理的内容を考慮した従来のニューラルメソッドと比較して、これはニューラルガイダンスの大きなリアルタイム高速化につながる。
得られたシステムは、優れた学習能力を示し、Mizarライブラリ上で最先端のパフォーマンスを達成する。
論文 参考訳(メタデータ) (2021-02-06T07:24:53Z) - Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。
本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
論文 参考訳(メタデータ) (2020-09-07T19:50:10Z) - Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
我々は、定理証明器を訓練するために、定理と証明を自動的に合成するニューラルジェネレータを学習する。
実世界の課題に関する実験は、我々の手法による合成データが定理証明器を改善することを示した。
論文 参考訳(メタデータ) (2020-02-17T16:06:02Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。