論文の概要: Proof Artifact Co-training for Theorem Proving with Language Models
- arxiv url: http://arxiv.org/abs/2102.06203v1
- Date: Thu, 11 Feb 2021 18:59:24 GMT
- ステータス: 処理完了
- システム内更新日: 2021-02-13 01:41:58.661276
- Title: Proof Artifact Co-training for Theorem Proving with Language Models
- Title(参考訳): 言語モデルを用いた理論証明のためのArtifact Co-trainingの証明
- Authors: Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W. Ayers, Stanislas
Polu
- Abstract要約: PACT(bf Proof bf Artifact bf Co-bf Training)は、カーネルレベルのコトレーニング用証明項から自己教師付きデータを抽出する一般的な手法である。
我々は、Transformer言語モデルによって駆動されるニューラル定理証明器でリーンを計測し、PACTがテスト定理の保留組における成功率を証明する定理を32%から48%に改善することを示す。
- 参考スコア(独自算出の注目度): 4.934817254755007
- License: http://creativecommons.org/licenses/by-sa/4.0/
- Abstract: Labeled data for imitation learning of theorem proving in large libraries of
formalized mathematics is scarce as such libraries require years of
concentrated effort by human specialists to be built. This is particularly
challenging when applying large Transformer language models to tactic
prediction, because the scaling of performance with respect to model size is
quickly disrupted in the data-scarce, easily-overfitted regime. We propose PACT
({\bf P}roof {\bf A}rtifact {\bf C}o-{\bf T}raining), a general methodology for
extracting abundant self-supervised data from kernel-level proof terms for
co-training alongside the usual tactic prediction objective. We apply this
methodology to Lean, an interactive proof assistant which hosts some of the
most sophisticated formalized mathematics to date. We instrument Lean with a
neural theorem prover driven by a Transformer language model and show that PACT
improves theorem proving success rate on a held-out suite of test theorems from
32\% to 48\%.
- Abstract(参考訳): 形式化された数学の大きなライブラリーで証明される定理の模倣学習のためのラベル付きデータはほとんどなく、そのようなライブラリーは人間の専門家による長年の集中的な努力を必要とする。
これは、大規模なトランスフォーマー言語モデルを戦術予測に適用する場合に特に困難です。なぜなら、モデルサイズに関するパフォーマンスのスケーリングは、データスカースで容易にオーバーフィットした体制で急速に破壊されるからです。
通常の戦術予測目標と並行して、カーネルレベルの証明語から豊富な自己教師ありデータを抽出する一般的な手法であるpact ({\bf p}roof {\bf a}rtifact {\bf c}o-{\bf t}raining)を提案する。
私たちはこの方法論を、これまでで最も洗練された形式化された数学をホストするインタラクティブな証明アシスタントであるLeanに適用します。
トランスフォーマー言語モデルによって駆動される神経定理証明器を用いてリーンを計測し,pact がテスト定理の保留組における定理証明成功率を 32\% から 48\% に向上させることを示した。
関連論文リスト
- 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) - TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative
Language Models [68.65075559137608]
本稿では, ATP ベンチマーク TRIGO を提案する。このベンチマークでは, ステップバイステップの証明で三角法式を縮小するだけでなく, 論理式上で生成する LM の推論能力を評価する。
我々は、Webから三角法式とその縮小フォームを収集し、手作業で単純化プロセスに注釈を付け、それをリーン形式言語システムに翻訳する。
我々はLean-Gymに基づく自動生成装置を開発し、モデルの一般化能力を徹底的に分析するために、様々な困難と分布のデータセット分割を作成する。
論文 参考訳(メタデータ) (2023-10-16T08:42:39Z) - Prototype-based Aleatoric Uncertainty Quantification for Cross-modal
Retrieval [139.21955930418815]
クロスモーダル検索手法は、共通表現空間を共同学習することにより、視覚と言語モダリティの類似性関係を構築する。
しかし、この予測は、低品質なデータ、例えば、腐敗した画像、速いペースの動画、詳細でないテキストによって引き起こされるアレタリック不確実性のために、しばしば信頼性が低い。
本稿では, 原型に基づくAleatoric Uncertainity Quantification (PAU) フレームワークを提案する。
論文 参考訳(メタデータ) (2023-09-29T09:41:19Z) - LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。
既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。
本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。
本研究では,LLM ベースの証明器 ReProver を開発した。
論文 参考訳(メタデータ) (2023-06-27T17:05:32Z) - Efficient Nearest Neighbor Language Models [114.40866461741795]
非パラメトリックニューラルネットワークモデル(NLM)は、外部データストアを用いてテキストの予測分布を学習する。
比較性能を維持しながら、推論速度の最大6倍の高速化を実現する方法を示す。
論文 参考訳(メタデータ) (2021-09-09T12:32:28Z) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。