論文の概要: 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は、ニューラル定理の証明者を評価する上で、挑戦的で現実的な視点を提供する。

関連論文リスト

• Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically [29.908878832382523]
  本稿では,自動検証/評価を可能にする形式言語による証明記述能力の向上に焦点をあてる。 我々は、定理に直接関係する補題がテスト時の定理証明者に与えられないより自然な設定で作業する。 我々は、モデルが定理を補題に分解し、補題を証明し、補題を用いて定理を証明することを奨励するRLベースの訓練アルゴリズムを設計する。
  論文  参考訳（メタデータ） (2024-11-04T05:57:40Z)
• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。 マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。 その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
  論文  参考訳（メタデータ） (2024-10-21T08:04:21Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)
• ATG: Benchmarking Automated Theorem Generation for Generative Language Models [83.93978859348313]
  人間はより広範に複雑な数学的結果を探求するために新しい定理を開発することができる。 現在の生成言語モデル(LM)は、定理の自動証明において著しく改善されている。 本稿では,エージェントが価値ある(あるいは新しい)定理を自動生成できるかどうかを評価する自動定理生成ベンチマークを提案する。
  論文  参考訳（メタデータ） (2024-05-05T02:06:37Z)
• 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)
• 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)
• Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
  我々は、定理証明器を訓練するために、定理と証明を自動的に合成するニューラルジェネレータを学習する。 実世界の課題に関する実験は、我々の手法による合成データが定理証明器を改善することを示した。
  論文  参考訳（メタデータ） (2020-02-17T16:06:02Z)

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

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。