論文の概要: DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search

• arxiv url: http://arxiv.org/abs/2408.08152v1
• Date: Thu, 15 Aug 2024 13:40:03 GMT
• ステータス: 処理完了
• システム内更新日: 2024-08-16 13:46:24.755512
• Title: DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search
• Title（参考訳）: DeepSeek-Prover-V1.5:強化学習とモンテカルロ木探索のための補足フィードバックのハーネス化
• Authors: Huajian Xin, Z. Z. Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, Wenjun Gao, Qihao Zhu, Dejian Yang, Zhibin Gou, Z. F. Wu, Fuli Luo, Chong Ruan,
• Abstract要約: 私たちはDeepSeek-Prover-V1.5を紹介します。 このモデルはDeepSeek-Prover-V1から派生した拡張形式定理証明データセットを用いて教師付き微調整を行う。 本稿では,モンテカルロ木探索の変種であるRMaxTSを提案する。
• 参考スコア（独自算出の注目度）: 16.477438279316576
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We introduce DeepSeek-Prover-V1.5, an open-source language model designed for theorem proving in Lean 4, which enhances DeepSeek-Prover-V1 by optimizing both training and inference processes. Pre-trained on DeepSeekMath-Base with specialization in formal mathematical languages, the model undergoes supervised fine-tuning using an enhanced formal theorem proving dataset derived from DeepSeek-Prover-V1. Further refinement is achieved through reinforcement learning from proof assistant feedback (RLPAF). Beyond the single-pass whole-proof generation approach of DeepSeek-Prover-V1, we propose RMaxTS, a variant of Monte-Carlo tree search that employs an intrinsic-reward-driven exploration strategy to generate diverse proof paths. DeepSeek-Prover-V1.5 demonstrates significant improvements over DeepSeek-Prover-V1, achieving new state-of-the-art results on the test set of the high school level miniF2F benchmark ($63.5\%$) and the undergraduate level ProofNet benchmark ($25.3\%$).
• Abstract（参考訳）: DeepSeek-Prover-V1.5はLean 4の定理証明用に設計されたオープンソースの言語モデルで、トレーニングと推論プロセスの両方を最適化することでDeepSeek-Prover-V1を強化します。 DeepSeekMath-Baseで事前訓練され、DeepSeek-Prover-V1から派生した拡張形式定理証明データセットを使用して、フォーマルな数学的言語で専門化されている。 さらなる改良は、証明アシスタントフィードバック(RLPAF)からの強化学習によって達成される。 本稿では,DeepSeek-Prover-V1のシングルパス全耐久生成手法の他に,モンテカルロ木探索の変種であるRMaxTSを提案する。 DeepSeek-Prover-V1.5は、DeepSeek-Prover-V1よりも大幅に改善され、高校レベルのminiF2Fベンチマーク(63.5\%$)と学部レベルのProofNetベンチマーク(25.3\%$)のテストセットで、最先端の結果が得られた。

関連論文リスト

• Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving [72.8626512877667]
  本稿では,オープンソースの大規模言語モデル(LLM)であるGoedel-Proverを紹介する。
  論文  参考訳（メタデータ） (2025-02-11T15:27:35Z)
• From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs [25.69931278771869]
  本稿では,形式的推論の即時適用シナリオである形式的検証に焦点を当てる。 我々は5つの形式仕様言語で18kの高品質な命令応答ペアを構築した。 フォーマルなデータによる微調整は、数学、推論、コーディング能力も強化する。
  論文  参考訳（メタデータ） (2025-01-27T17:00:56Z)
• DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learning [147.16121855209246]
  第一世代の推論モデルであるDeepSeek-R1-ZeroとDeepSeek-R1を紹介します。 DeepSeek-R1-Zeroは大規模な強化学習を通じて訓練されている。 DeepSeek-R1は、RLの前にマルチステージトレーニングとコールドスタートデータを組み込んでいる。
  論文  参考訳（メタデータ） (2025-01-22T15:19:35Z)
• DeepSeek-V3 Technical Report [147.16121855209246]
  We present DeepSeek-V3, a strong Mixture-of-Experts (MoE) language model with 671B total parameters with 37B activated for each token。 我々は14.8兆の多様性と高品質のトークンでDeepSeek-V3を事前訓練し、その後にSupervised Fine-Tuning and Reinforcement Learningのステージを受講した。 包括的な評価によると、DeepSeek-V3は他のオープンソースモデルよりも優れており、主要なクローズドソースモデルに匹敵するパフォーマンスを実現している。
  論文  参考訳（メタデータ） (2024-12-27T04:03:16Z)
• RankRAG: Unifying Context Ranking with Retrieval-Augmented Generation in LLMs [60.38044044203333]
  大規模言語モデル(LLM)は、通常、検索拡張生成(RAG)において、レトリバーからトップkコンテキストを利用する。 本稿では,RAGにおける文脈ランク付けと回答生成の両目的のために,単一のLLMをチューニング可能な新しい命令微調整フレームワークであるRanRAGを提案する。 例えば、GPT-4-0613, GPT-4-turbo-2024-0409, ChatQA-1.5, RAGベンチマークの最先端性能を備えたオープンソースモデルなどである。
  論文  参考訳（メタデータ） (2024-07-02T17:59:17Z)
• DeepSeek-Coder-V2: Breaking the Barrier of Closed-Source Models in Code Intelligence [43.589403386634615]
  DeepSeek-Coder-V2は、コード固有のタスクでGPT4-Turboに匹敵するパフォーマンスを実現する、オープンソースのコード言語モデルである。 DeepSeek-Coder-V2はさらに6兆トークンを追加して、DeepSeek-V2の中間チェックポイントから事前トレーニングされている。 標準的なベンチマーク評価では、GPT4-Turbo、Claude 3 Opus、Gemini 1.5 Proといったクローズドソースモデルと比較して、DeepSeek-Coder-V2は優れたパフォーマンスを実現している。
  論文  参考訳（メタデータ） (2024-06-17T13:51:35Z)
• DeepSeek-V2: A Strong, Economical, and Efficient Mixture-of-Experts Language Model [118.06260386652778]
  We present DeepSeek-V2, a strong Mixture-of-Experts (MoE) language model characterized by economical training and efficient inference。 DeepSeek-V2は、MLA(Multi-head Latent Attention)やDeepSeekMoEといった革新的なアーキテクチャを採用している。 DeepSeek-V2はDeepSeek 67Bと比較して大幅に性能が向上し、トレーニングコストは42.5%削減された。
  論文  参考訳（メタデータ） (2024-05-07T15:56:43Z)
• The Wisdom of Hindsight Makes Language Models Better Instruction Followers [84.9120606803906]
  強化学習は、人間のフィードバックによる指示に合うように、大きな言語モデルを微調整することに成功している。 そこで本稿では,本論文で提案するアプローチとして,原文を緩和することでフィードバックを指導に変換する手法と,教師付き手法によるアライメント向上のためのモデルをトレーニングする手法を提案する。 言語モデルと命令を整合させる新しいアルゴリズムであるHIR(Hindsight Instruction Relabeling)を提案する。
  論文  参考訳（メタデータ） (2023-02-10T12:16:38Z)

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

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