論文の概要: LeanDojo: Theorem Proving with Retrieval-Augmented Language Models

• arxiv url: http://arxiv.org/abs/2306.15626v1
• Date: Tue, 27 Jun 2023 17:05:32 GMT
• ステータス: 処理完了
• システム内更新日: 2023-06-28 12:32:37.221524
• Title: LeanDojo: Theorem Proving with Retrieval-Augmented Language Models
• Title（参考訳）: leandojo: 検索型言語モデルによる定理証明
• Authors: Kaiyu Yang, Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, Anima Anandkumar
• Abstract要約: 大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。 既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。 本稿では、ツールキット、データ、モデル、ベンチマークで構成されるオープンソースのリーングラウンドであるLeanDojoを紹介します。 ReProver: 巨大な数学ライブラリから敷地を選択するための検索機能を備えた最初のLLM証明器を開発した。
• 参考スコア（独自算出の注目度）: 52.72938065009112
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Large language models (LLMs) have shown promise in proving formal theorems using proof assistants such as Lean. However, existing methods are difficult to reproduce or build on, due to private code, data, and large compute requirements. This has created substantial barriers to research on machine learning methods for theorem proving. This paper removes these barriers by introducing LeanDojo: an open-source Lean playground consisting of toolkits, data, models, and benchmarks. LeanDojo extracts data from Lean and enables interaction with the proof environment programmatically. It contains fine-grained annotations of premises in proofs, providing valuable data for premise selection: a key bottleneck in theorem proving. Using this data, we develop ReProver (Retrieval-Augmented Prover): the first LLM-based prover that is augmented with retrieval for selecting premises from a vast math library. It is inexpensive and needs only one GPU week of training. Our retriever leverages LeanDojo's program analysis capability to identify accessible premises and hard negative examples, which makes retrieval much more effective. Furthermore, we construct a new benchmark consisting of 96,962 theorems and proofs extracted from Lean's math library. It features challenging data split requiring the prover to generalize to theorems relying on novel premises that are never used in training. We use this benchmark for training and evaluation, and experimental results demonstrate the effectiveness of ReProver over non-retrieval baselines and GPT-4. We thus provide the first set of open-source LLM-based theorem provers without any proprietary datasets and release it under a permissive MIT license to facilitate further research.
• Abstract（参考訳）: 大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。 しかし、既存のメソッドは、プライベートコード、データ、大規模な計算要求のため、複製や構築が困難である。 これは、定理証明のための機械学習手法の研究に重大な障壁を生み出した。 本稿では、ツールキット、データ、モデル、ベンチマークで構成されるオープンソースのリーングラウンドであるLeanDojoを導入することで、これらの障壁を取り除く。 LeanDojoはLeanからデータを抽出し、プログラムで証明環境とのインタラクションを可能にする。 これは証明における前提の詳細なアノテーションを含み、前提選択のための貴重なデータを提供する:定理証明における重要なボトルネックである。 このデータを用いて,大規模な数学ライブラリから敷地を選択するための検索機能を備えた最初のLCMベースの証明器であるReProver(Retrieval-Augmented Prover)を開発した。 価格は安く、gpuの1週間のトレーニングしか必要ない。 検索はLeanDojoのプログラム分析機能を利用して、アクセス可能な前提と厳しいネガティブな例を特定します。 さらに,Leanの数学ライブラリから抽出した96,962の定理と証明からなる新しいベンチマークを構築した。 これは、トレーニングで使われない新しい前提に依存する定理を一般化することを要求するデータ分割に挑戦する特徴である。 このベンチマークをトレーニングと評価に使用し,非検索ベースラインとGPT-4に対するReProverの有効性を実験的に検証した。 したがって、プロプライエタリなデータセットを使わずに、オープンソースのLCMベースの定理プローバーの最初のセットを提供し、さらなる研究を促進するために寛容なMITライセンスの下でリリースする。

関連論文リスト

• InternLM2.5-StepProver: Advancing Automated Theorem Proving via Expert Iteration on Large-Scale LEAN Problems [47.93470713879515]
  InternLM2.5-SteperはMiniF2F、Lean-Workbook-Plus、ProofNet、Patnamベンチマークのオープンソースステート・オブ・ザ・アートを実現している。 MiniF2Fテストでは65.9%をパスし、Lean-Workbook-Plusの17.0%の問題を証明(あるいは否定)している。
  論文  参考訳（メタデータ） (2024-10-21T07:18:23Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)
• TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts [26.98890165420689]
  TheoremLlamaは、汎用的なLean4エキスパートをトレーニングするエンドツーエンドフレームワークである。 我々のフレームワークは,MiniF2F-ValidデータセットとTestデータセットでそれぞれ36.48%,33.61%の累積精度を達成した。
  論文  参考訳（メタデータ） (2024-07-03T15:36:18Z)
• Towards Large Language Models as Copilots for Theorem Proving in Lean [81.94024084598598]
  大規模な言語モデルでリーン推論を実行するためのフレームワークであるLean Copilotを紹介します。 証明手順を提案し、中間的な証明目標を完了し、関連する前提を選択するためのツールを構築します。 実験により, 提案手法の有効性を実証し, 提案手法の有効性を検証した。
  論文  参考訳（メタデータ） (2024-04-18T22:54:08Z)
• Can LLMs Separate Instructions From Data? And What Do We Even Mean By That? [60.50127555651554]
  大規模言語モデル(LLM)は、多くの実用的なアプリケーションにおいて印象的な結果を示すが、基本的な安全性機能は欠如している。 これにより、間接的なプロンプトインジェクションのような操作に脆弱になり、一般に安全クリティカルなタスクには適さない。 モデル出力から計算可能な命令データ分離の形式的尺度と経験的変量を導入する。
  論文  参考訳（メタデータ） (2024-03-11T15:48:56Z)
• Training Language Models to Generate Text with Citations via Fine-grained Rewards [19.176465185343417]
  大型言語モデル(LLM)は幻覚を起こす傾向があり、信頼できる情報源への参照が欠如しているため、その応答は信頼性に欠けることが多い。 本研究では,LLMに高い支援力と関連性のある引用を生成するための,微粒な報酬を用いた効果的な学習フレームワークを提案する。 LLaMA-2-7Bでは、細粒度の報酬がGPT-3.5-turboを上回り、ベースラインの中で最高の性能を達成している。
  論文  参考訳（メタデータ） (2024-02-06T19:00:40Z)
• 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)
• An In-Context Learning Agent for Formal Theorem-Proving [10.657173216834668]
  我々は、LeanやCoqのような環境で、形式的定理コンテキストのためのコンテキスト内学習エージェントを提示します。 COPRAは大規模言語モデルに対して、ステートフルなバックトラック検索から戦術的応用を提案することを何度も求めている。 我々はCompCertプロジェクトのMiniF2FベンチマークとCoqタスクセットに対するCOPRAの実装を評価した。
  論文  参考訳（メタデータ） (2023-10-06T16:21:22Z)
• LEGO-Prover: Neural Theorem Proving with Growing Libraries [86.1191481712352]
  LEGO-Prover では,証明された補題を含むスキルライブラリを,定理証明に使用される LLM の能力を高めるためのスキルとして活用する。 LEGO-Proverは、証明をモジュール的に構築することにより、ライブラリから取得した既存のスキルを活用し、証明プロセス中に新しいスキルを作成することができる。 我々のアブレーション研究は、これらの新たなスキルが定理の証明に役立つことを示唆し、47.1%から50.4%に改善した。
  論文  参考訳（メタデータ） (2023-10-01T12:47:59Z)

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

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