論文の概要: miniCTX: Neural Theorem Proving with (Long-)Contexts
- arxiv url: http://arxiv.org/abs/2408.03350v1
- Date: Mon, 5 Aug 2024 20:19:18 GMT
- ステータス: 処理完了
- システム内更新日: 2024-08-08 14:46:00.755783
- Title: miniCTX: Neural Theorem Proving with (Long-)Contexts
- Title(参考訳): miniCTX:(Long-)コンテキストによる神経理論の証明
- Authors: Jiewen Hu, Thomas Zhu, Sean Welleck,
- Abstract要約: miniCTXは、訓練中に観察されていない文脈情報に依存する形式的な数学的定理を証明するモデルの能力をテストする。
miniCTXには、実際のリーンプロジェクトと教科書に由来する定理が含まれており、それぞれに数万のトークンにまたがるコンテキストが関連付けられています。
本稿では,前回のファイル内容に条件付き証明ステップを生成するためにモデルを訓練する簡単なレシピであるファイルチューニングを紹介する。
- 参考スコア(独自算出の注目度): 19.51651334079961
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: We introduce miniCTX, which tests a model's ability to prove formal mathematical theorems that depend on new definitions, lemmas, or other contextual information that was not observed during training. miniCTX contains theorems sourced from real Lean projects and textbooks, each associated with a context that can span tens of thousands of tokens. Models are tasked with proving a theorem given access to code from the theorem's repository, which contains context that is helpful or needed for the proof. As a baseline for miniCTX, we introduce file-tuning, a simple recipe that trains a model to generate a proof step conditioned on the preceding file contents. File-tuning substantially outperforms the traditional neural theorem proving approach that fine-tunes on states alone. Additionally, our file-tuned model improves performance on the standard miniF2F benchmark, achieving a pass rate of 33.61%, which is a new state-of-the-art for 1.3B parameter models. Alongside miniCTX, we offer ntp-toolkit for automatically extracting and annotating theorem proving data, making it easy to add new projects into miniCTX to ensure that contexts are not seen during training. miniCTX offers a challenging and realistic perspective on evaluating neural theorem provers.
- Abstract(参考訳): モデルが新しい定義や補題、あるいは訓練中に観測されなかった文脈情報に依存する形式的な数学的定理を証明する能力をテストするミニCTXを導入する。
miniCTXには、実際のリーンプロジェクトと教科書に由来する定理が含まれており、それぞれに数万のトークンにまたがるコンテキストが関連付けられています。
モデルは定理を証明し、定理のリポジトリからコードにアクセスできるようにする。
ミニCTXのベースラインとして,先行するファイルコンテンツに条件付き証明ステップを生成するためにモデルを訓練するシンプルなレシピであるファイルチューニングを導入する。
ファイルチューニングは、状態のみを微調整する従来のニューラル定理証明アプローチを大幅に上回る。
さらに、我々のファイルチューニングモデルは、標準の miniF2F ベンチマークの性能を改善し、1.3B パラメータモデルのための新しい最先端モデルである 33.61% のパスレートを達成する。
miniCTXとともに、定理証明データを自動抽出し注釈付けするためのntp-toolkitを提供し、miniCTXに新しいプロジェクトを追加して、トレーニング中にコンテキストが見えないようにする。
miniCTXは、ニューラル定理の証明者を評価する上で、挑戦的で現実的な視点を提供する。
関連論文リスト
- Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。
Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
論文 参考訳(メタデータ) (2024-07-14T01:43:07Z) - REFACTOR: Learning to Extract Theorems from Proofs [29.44286369265644]
我々は、REFACTORが、人間が証明を書くのに使用する定理の19.6%を抽出できることを示した。
新たに抽出された定理により,既存のMetaMathデータベースが構築可能であることを示す。
また、新理論データセットでトレーニングされた証明者が、より多くのテスト定理を証明し、最先端のベースラインを上回ることを実証する。
論文 参考訳(メタデータ) (2024-02-26T21:21:30Z) - MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。
5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。
我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
論文 参考訳(メタデータ) (2024-02-14T05:57:58Z) - 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) - LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。
既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。
本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。
本研究では,LLM ベースの証明器 ReProver を開発した。
論文 参考訳(メタデータ) (2023-06-27T17:05:32Z) - 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) - Learnable Boundary Guided Adversarial Training [66.57846365425598]
私たちは、あるクリーンモデルからのモデルロジットを使用して、別のロバストモデルの学習をガイドします。
我々は、CIFAR-100上で、追加の実データや合成データなしで、新しい最先端のロバスト性を実現する。
論文 参考訳(メタデータ) (2020-11-23T01:36:05Z) - Learning Reasoning Strategies in End-to-End Differentiable Proving [50.9791149533921]
条件付き定理プローバーは勾配に基づく最適化により最適規則選択戦略を学習する。
条件付き定理プローサは拡張性があり、CLUTRRデータセット上で最先端の結果が得られることを示す。
論文 参考訳(メタデータ) (2020-07-13T16:22:14Z) - Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
我々は、定理証明器を訓練するために、定理と証明を自動的に合成するニューラルジェネレータを学習する。
実世界の課題に関する実験は、我々の手法による合成データが定理証明器を改善することを示した。
論文 参考訳(メタデータ) (2020-02-17T16:06:02Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。