Fugu-MT 論文翻訳(概要): MizAR 60 for Mizar 50

論文の概要: 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証明を成長させるインクリメンタルループが含まれる。また、自動的に証明されたミザー問題の選択も提示する。

関連論文リスト

Proof Automation with Large Language Models [6.587933406842906]
大規模言語モデル(LLM)は、自然言語で非公式な証明を自動的に生成する可能性を示している。本稿では,まず LLM に初期証明を生成することを促し,次に目標とする記号法を利用して低レベルの問題を反復的に修復する,新しい生成・修復手法である PALM を提案する。その結果、PALMは他の最先端の手法よりも大幅に優れており、76.6%から180.4%の定理を証明できた。
論文参考訳（メタデータ） (2024-09-22T00:19:27Z)
Building Math Agents with Multi-Turn Iterative Preference Learning [56.71330214021884]
本稿では,モデル性能をさらに向上させるために,補完的な直接選好学習手法について検討する。既存の直接選好学習アルゴリズムは、もともとシングルターンチャットタスク用に設計されている。この文脈に合わせたマルチターン直接選好学習フレームワークを提案する。
論文参考訳（メタデータ） (2024-09-04T02:41:04Z)
Solving Hard Mizar Problems with Instantiation and Strategy Invention [2.048226951354646]
複数のATP法とAI法を用いて,これまでATP未承認であったMizar/MPTP問題の3000以上を証明した。この方法では、これまで未解決だった14163のハード・ミザー問題の3021(21.3%)が解決された。
論文参考訳（メタデータ） (2024-06-25T17:47:13Z)
Autoformalizing Euclidean Geometry [74.72212706513318]
ユークリッド幾何学の自己形式化のためのニューロシンボリックフレームワークを提案する。 1つの課題は、非公式な証明が図に頼り、形式化が難しいテキストのギャップを残すことである。自己形式化定理文の自動意味評価を行う。
論文参考訳（メタデータ） (2024-05-27T14:35:10Z)
Towards Large Language Models as Copilots for Theorem Proving in Lean [81.94024084598598]
大規模な言語モデルでリーン推論を実行するためのフレームワークであるLean Copilotを紹介します。証明手順を提案し、中間的な証明目標を完了し、関連する前提を選択するためのツールを構築します。実験により, 提案手法の有効性を実証し, 提案手法の有効性を検証した。
論文参考訳（メタデータ） (2024-04-18T22:54:08Z)
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)
LEGO-Prover: Neural Theorem Proving with Growing Libraries [86.1191481712352]
LEGO-Prover では,証明された補題を含むスキルライブラリを,定理証明に使用される LLM の能力を高めるためのスキルとして活用する。 LEGO-Proverは、証明をモジュール的に構築することにより、ライブラリから取得した既存のスキルを活用し、証明プロセス中に新しいスキルを作成することができる。我々のアブレーション研究は、これらの新たなスキルが定理の証明に役立つことを示唆し、47.1%から50.4%に改善した。
論文参考訳（メタデータ） (2023-10-01T12:47:59Z)
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)
Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
我々は、定理証明器を訓練するために、定理と証明を自動的に合成するニューラルジェネレータを学習する。実世界の課題に関する実験は、我々の手法による合成データが定理証明器を改善することを示した。
論文参考訳（メタデータ） (2020-02-17T16:06:02Z)

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