論文の概要: DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data

• arxiv url: http://arxiv.org/abs/2405.14333v1
• Date: Thu, 23 May 2024 09:03:42 GMT
• ステータス: 処理完了
• システム内更新日: 2024-05-24 18:04:42.697171
• Title: DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data
• Title（参考訳）: DeepSeek-Prover: 大規模合成データによるLLMの定理証明の促進
• Authors: Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, Xiaodan Liang,
• Abstract要約: 本稿では,高校・学部レベルの数学競争問題から得られたリーン4証明データを生成する手法を提案する。 この合成データセットでDeepSeekMath 7Bモデルを微調整します。 我々のモデルは、Lean 4 Formalized International Mathematical Olympiad (FIMO)ベンチマークで148の問題を5つ証明しましたが、GPT-4は証明できませんでした。
• 参考スコア（独自算出の注目度）: 65.5290035371111
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Proof assistants like Lean have revolutionized mathematical proof verification, ensuring high accuracy and reliability. Although large language models (LLMs) show promise in mathematical reasoning, their advancement in formal theorem proving is hindered by a lack of training data. To address this issue, we introduce an approach to generate extensive Lean 4 proof data derived from high-school and undergraduate-level mathematical competition problems. This approach involves translating natural language problems into formal statements, filtering out low-quality statements, and generating proofs to create synthetic data. After fine-tuning the DeepSeekMath 7B model on this synthetic dataset, which comprises 8 million formal statements with proofs, our model achieved whole-proof generation accuracies of 46.3% with 64 samples and 52% cumulatively on the Lean 4 miniF2F test, surpassing the baseline GPT-4 at 23.0% with 64 samples and a tree search reinforcement learning method at 41.0%. Additionally, our model successfully proved 5 out of 148 problems in the Lean 4 Formalized International Mathematical Olympiad (FIMO) benchmark, while GPT-4 failed to prove any. These results demonstrate the potential of leveraging large-scale synthetic data to enhance theorem-proving capabilities in LLMs. Both the synthetic dataset and the model will be made available to facilitate further research in this promising field.
• Abstract（参考訳）: Leanのような証明アシスタントは、数学的証明の検証に革命をもたらし、高い精度と信頼性を確保している。 大きな言語モデル(LLM)は数学的推論において有望であるが、形式的定理証明の進歩は訓練データの欠如によって妨げられている。 この問題に対処するため,高校・学部レベルの数学競争問題から得られたリーン4証明データを広範囲に生成する手法を提案する。 このアプローチでは、自然言語問題を形式的なステートメントに翻訳し、低品質なステートメントをフィルタリングし、合成データを生成するための証明を生成する。 この合成データセットを用いてDeepSeekMath 7Bモデルを微調整した結果,64サンプルを46.3%,Lean 4 miniF2F試験を52%累積して,ベースライン GPT-4 を23.0%,64サンプルを21.0%,木探索強化学習法を41.0%とした。 さらに、我々のモデルはLean 4 Formalized International Mathematical Olympiad (FIMO)ベンチマークで148の問題を5つ証明しました。 これらの結果は,LLMの定理証明能力を高めるために,大規模合成データを活用する可能性を示している。 この将来性のある分野のさらなる研究を促進するために、合成データセットとモデルの両方が利用可能になる。

関連論文リスト

• 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)
• Proof Automation with Large Language Models [6.587933406842906]
  大規模言語モデル(LLM)は、自然言語で非公式な証明を自動的に生成する可能性を示している。 本稿では,まず LLM に初期証明を生成することを促し,次に目標とする記号法を利用して低レベルの問題を反復的に修復する,新しい生成・修復手法である PALM を提案する。 その結果、PALMは他の最先端の手法よりも大幅に優れており、76.6%から180.4%の定理を証明できた。
  論文  参考訳（メタデータ） (2024-09-22T00:19:27Z)
• LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN prover [56.34998574538897]
  我々は、GitHub上のLean 4リポジトリから抽出された大規模なフォーマルデータからなるデータセットであるLEAN-GitHubを提案する。 我々のモデルは1回のパスで48.8%、64回のパスで54.5%、Lean 4 miniF2Fテストで54.5%に達し、最先端のメソッドを52%上回った。
  論文  参考訳（メタデータ） (2024-07-24T12:28:03Z)
• TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts [26.98890165420689]
  TheoremLlamaは、汎用的なLean4エキスパートをトレーニングするエンドツーエンドフレームワークである。 我々のフレームワークは,MiniF2F-ValidデータセットとTestデータセットでそれぞれ36.48%,33.61%の累積精度を達成した。
  論文  参考訳（メタデータ） (2024-07-03T15:36:18Z)
• Key-Point-Driven Data Synthesis with its Enhancement on Mathematical Reasoning [110.80663974060624]
  キーポイント駆動型データ合成(KPDDS)は質問応答対を合成する新しいデータ合成フレームワークである。 KPDDSは厳格な品質管理と相当なスケーラビリティを備えた新しい質問の生成を保証する。 KPMathは,800万以上の質問応答対から構成される,数学的推論に適した広範囲な合成データセットである。
  論文  参考訳（メタデータ） (2024-03-04T18:58:30Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)
• TarGEN: Targeted Data Generation with Large Language Models [51.87504111286201]
  TarGENは、高品質な合成データセットを生成するための、多段階のプロンプト戦略である。 我々は,LLMが不正確なラベル付きインスタンスを修正できるようにする自己補正法により,TarGENを増強する。 合成データセットを元のデータセットと比較した包括的な分析により、データセットの複雑さと多様性の類似または高いレベルが明らかになる。
  論文  参考訳（メタデータ） (2023-10-27T03:32:17Z)

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

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