論文の概要: TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts

• arxiv url: http://arxiv.org/abs/2407.03203v2
• Date: Fri, 04 Oct 2024 03:06:26 GMT
• ステータス: 翻訳完了
• システム内更新日: 2024-10-07 15:06:39.610804
• Title: TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts
• Title（参考訳）: TheoremLlama: 汎用LLMをLean4エキスパートに変える
• Authors: Ruida Wang, Jipeng Zhang, Yizhen Jia, Rui Pan, Shizhe Diao, Renjie Pi, Tong Zhang,
• Abstract要約: TheoremLlamaは、汎用的なLean4エキスパートをトレーニングするエンドツーエンドフレームワークである。 我々のフレームワークは,MiniF2F-ValidデータセットとTestデータセットでそれぞれ36.48%,33.61%の累積精度を達成した。
• 参考スコア（独自算出の注目度）: 26.98890165420689
• License:
• Abstract: Proving mathematical theorems using computer-verifiable formal languages like Lean significantly impacts mathematical reasoning. One approach to formal theorem proving involves generating complete proofs using Large Language Models (LLMs) based on Natural Language (NL) proofs. However, due to the scarcity of aligned NL and Formal Language (FL) theorem-proving data most modern LLMs exhibit suboptimal performance.This scarcity results in a paucity of methodologies for training LLMs and techniques to fully utilize their capabilities in composing formal proofs. To address these challenges, this paper proposes TheoremLlama, an end-to-end framework that trains a general-purpose LLM to be a Lean4 expert. TheoremLlama includes NL-FL dataset generation and bootstrapping method to obtain aligned dataset, curriculum learning and block training techniques to train the model, and iterative proof writing method to write Lean4 proofs that work together synergistically. Using the dataset generation method in TheoremLlama, we provide Open Bootstrapped Theorems (OBT), an NL-FL aligned and bootstrapped dataset. Our novel NL-FL bootstrapping method, where NL proofs are integrated into Lean4 code for training datasets, leverages the NL reasoning ability of LLMs for formal reasoning. The TheoremLlama framework achieves cumulative accuracies of 36.48% and 33.61% on MiniF2F-Valid and Test datasets respectively, surpassing the GPT-4 baseline of 22.95% and 25.41%. Our code, model checkpoints, and the generated dataset is published in GitHub
• Abstract（参考訳）: Leanのようなコンピュータで検証可能な形式言語を用いた数学的定理の証明は、数学的推論に大きな影響を及ぼす。 形式的定理証明の1つのアプローチは、自然言語(NL)の証明に基づいたLarge Language Models (LLM)を用いた完全証明を生成することである。 しかし, 整合性NLと形式言語(FL)定理の欠如により, 現代のLLMでは, 準最適性能を示すデータが多く, この不足は, 形式的証明を構成する上で, それらの能力を十分に活用するためのLLMと技法の訓練方法の欠如を招きかねない。 これらの課題に対処するため,本稿では,汎用LLMをLean4エキスパートにトレーニングするエンドツーエンドフレームワークであるTheoremLlamaを提案する。 TheoremLlamaには、NL-FLデータセットの生成とブートストラップ手法が含まれており、整列したデータセット、モデルのトレーニングのためのカリキュラム学習とブロックトレーニング技術、および相乗的に機能するLean4証明を書くための反復的証明記述方法が含まれている。 TheoremLlamaのデータセット生成手法を用いて、NL-FLアライメントとブートストラップデータセットであるOpen Bootstrapped Theorems(OBT)を提供する。 NL証明をLean4コードに統合してデータセットをトレーニングする新しいNL-FLブートストラップ法では,LLMのNL推論能力を活用できる。 TheoremLlamaフレームワークは、MiniF2F-ValidおよびTestデータセットでそれぞれ36.48%と33.61%の累積精度を達成し、GPT-4ベースラインの22.95%と25.41%を上回っている。 私たちのコード、モデルチェックポイント、および生成されたデータセットはGitHubで公開されています

関連論文リスト

• Proof Automation with Large Language Models [6.587933406842906]
  大規模言語モデル(LLM)は、自然言語で非公式な証明を自動的に生成する可能性を示している。 本稿では,まず LLM に初期証明を生成することを促し,次に目標とする記号法を利用して低レベルの問題を反復的に修復する,新しい生成・修復手法である PALM を提案する。 その結果、PALMは他の最先端の手法よりも大幅に優れており、76.6%から180.4%の定理を証明できた。
  論文  参考訳（メタデータ） (2024-09-22T00:19:27Z)
• Reliable Reasoning Beyond Natural Language [0.047888359248129786]
  大きな言語モデル(LLM)は、しばしば、確実に柔軟に推論する能力の限界を示す。 本稿では,問題文から全ての関連情報を論理コード文として抽出し,エンコードする手法を提案する。 次に、論理型プログラミング言語(Prolog)を用いて、明示的な推論の反復的な計算を行う。
  論文  参考訳（メタデータ） (2024-07-16T04:34:18Z)
• DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data [65.5290035371111]
  本稿では,高校・学部レベルの数学競争問題から得られたリーン4証明データを生成する手法を提案する。 この合成データセットでDeepSeekMath 7Bモデルを微調整します。 我々のモデルは、Lean 4 Formalized International Mathematical Olympiad (FIMO)ベンチマークで148の問題を5つ証明しましたが、GPT-4は証明できませんでした。
  論文  参考訳（メタデータ） (2024-05-23T09:03:42Z)
• Towards Large Language Models as Copilots for Theorem Proving in Lean [81.94024084598598]
  大規模な言語モデルでリーン推論を実行するためのフレームワークであるLean Copilotを紹介します。 証明手順を提案し、中間的な証明目標を完了し、関連する前提を選択するためのツールを構築します。 実験により, 提案手法の有効性を実証し, 提案手法の有効性を検証した。
  論文  参考訳（メタデータ） (2024-04-18T22:54:08Z)
• $\forall$uto$\exists$val: Autonomous Assessment of LLMs in Formal Synthesis and Interpretation Tasks [21.12437562185667]
  本稿では,形式構文を自然言語に翻訳する際のLLM評価のスケールアップ手法を提案する。 我々は、文脈自由文法(CFG)を用いて、その場で配布外のデータセットを生成する。 我々はまた、このパラダイムの実現可能性と拡張性を示すために、複数のSOTAクローズドおよびオープンソースLCMの評価を行う。
  論文  参考訳（メタデータ） (2024-03-27T08:08:00Z)
• Assessing the Reliability of Large Language Model Knowledge [78.38870272050106]
  大規模言語モデル(LLM)は、知識探索タスクにおける高い性能のため、知識ベースとして扱われてきた。 LLMが実際に正しい答えを連続的に生成する能力をどのように評価するか。 LLMの信頼性を直接測定するための新しい指標であるMOdel kNowledge relIabiliTy score (MONITOR)を提案する。
  論文  参考訳（メタデータ） (2023-10-15T12:40:30Z)
• Struc-Bench: Are Large Language Models Really Good at Generating Complex Structured Data? [49.688233418425995]
  Struc-Benchは、大きな言語モデル(LLM)を特徴とする包括的なベンチマークである。 Pスコア(Prompting Score)とHスコア(Heuristical Score)の2つの革新的な指標を提案する。 実験の結果,LLaMA-7Bに構造認識の微調整を適用すると,性能が大幅に向上することがわかった。
  論文  参考訳（メタデータ） (2023-09-16T11:31:58Z)
• LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
  大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。 既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。 本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。 本研究では,LLM ベースの証明器 ReProver を開発した。
  論文  参考訳（メタデータ） (2023-06-27T17:05:32Z)
• CodeGen2: Lessons for Training LLMs on Programming and Natural Languages [116.74407069443895]
  我々はエンコーダとデコーダベースのモデルを単一のプレフィックスLMに統一する。 学習方法は,「フリーランチ」仮説の主張を考察する。 データ配信においては,混合分布と多言語学習がモデル性能に及ぼす影響について検討した。
  論文  参考訳（メタデータ） (2023-05-03T17:55:25Z)

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

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