論文の概要: miniCTX: Neural Theorem Proving with (Long-)Contexts

• arxiv url: http://arxiv.org/abs/2408.03350v2
• Date: Thu, 3 Oct 2024 14:20:40 GMT
• ステータス: 処理完了
• システム内更新日: 2024-11-08 12:44:50.307260
• 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: Real-world formal theorem proving often depends on a wealth of context, including definitions, lemmas, comments, file structure, and other information. We introduce miniCTX, which tests a model's ability to prove formal mathematical theorems that depend on new context that is not seen 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 needed for the proof. As a baseline for miniCTX, we tested fine-tuning and prompting methods that condition theorem proving on preceding context. Both approaches substantially outperform traditional methods that rely solely on state information. We found that this ability to use context is not captured by previous benchmarks such as miniF2F. 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 evaluation of neural theorem provers.
• Abstract（参考訳）: 実世界の形式定理の証明は、定義、補題、コメント、ファイル構造、その他の情報を含む多くの文脈に依存することが多い。 トレーニング中に見えない新しい文脈に依存した形式的な数学的定理を立証するモデルの能力をテストするミニCTXを導入する。 miniCTXには、実際のリーンプロジェクトと教科書に由来する定理が含まれており、それぞれに数万のトークンにまたがるコンテキストが関連付けられています。 モデルは、定理が証明に必要な文脈を含む定理のリポジトリからコードにアクセスできることを証明することを任務とする。 ミニCTXのベースラインとして,先行する文脈で証明された条件定理を微調整し,提案手法を推し進めた。 どちらのアプローチも、状態情報のみに依存する従来の手法よりも大幅に優れている。 このコンテキストを使用する機能は、 miniF2Fのような以前のベンチマークではキャプチャされないことがわかった。 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)

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

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