論文の概要: 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\%$)のテストセットで、最先端の結果が得られた。

関連論文リスト

• 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)
• Revisiting and Maximizing Temporal Knowledge in Semi-supervised Semantic Segmentation [7.005068872406135]
  平均教師と共同学習に基づくアプローチは、確認バイアスと結合問題を緩和するために用いられる。 これらのアプローチは、複雑なトレーニングパイプラインとかなりの計算負担を伴うことが多い。 本稿では,トレーニングプロセス中に得られた時間的知識を最大限活用することにより,制約を効果的に緩和するPrevMatchフレームワークを提案する。
  論文  参考訳（メタデータ） (2024-05-31T03:54:59Z)
• Proving Theorems Recursively [80.42431358105482]
  本稿では、定理をレベル・バイ・レベルで証明するPOETRYを提案する。 従来のステップバイステップメソッドとは異なり、POETRYは各レベルで証明のスケッチを検索する。 また,POETRYが検出した最大証明長は10～26。
  論文  参考訳（メタデータ） (2024-05-23T10:35:08Z)
• 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)
• Advancing LLM Reasoning Generalists with Preference Trees [119.57169648859707]
  推論に最適化された大規模言語モデル(LLM)のスイートであるEulusを紹介する。 Eurusモデルは、様々なベンチマークでオープンソースのモデルの間で最先端の結果を得る。
  論文  参考訳（メタデータ） (2024-04-02T16:25:30Z)
• EVP: Enhanced Visual Perception using Inverse Multi-Attentive Feature Refinement and Regularized Image-Text Alignment [40.328294121805456]
  この研究は、コンピュータビジョンタスクにStable Diffusionネットワークを使用する方法を舗装した以前のVPDに基づいている。 Inverse Multi-Attentive Feature Refinement (IMAFR) モジュールを開発した。 第2に、安定拡散バックボーンの特徴抽出を改善するための新しい画像テキストアライメントモジュールを提案する。
  論文  参考訳（メタデータ） (2023-12-13T22:20:45Z)
• Revisiting Deformable Convolution for Depth Completion [40.45231083385708]
  深度完備化は、スパース深度マップから高品質の高密度深度マップを作成することを目的としている。 従来の作業では、通常、RGBイメージをガイダンスとして使用し、推定された粗い深度マップを洗練するための反復的な空間伝播を導入している。 変形可能なカーネルの畳み込みを単一パスリファインメントモジュールとして活用する,効率的なアーキテクチャを提案する。
  論文  参考訳（メタデータ） (2023-08-03T17:59:06Z)
• Regularization and Variance-Weighted Regression Achieves Minimax Optimality in Linear MDPs: Theory and Practice [79.48432795639403]
  ミラー降下値反復(MDVI)は、KL(Kulback-Leibler)とRL(Entropy-regularized reinforcement learning)の抽象化である。 MDVIを線形関数近似を用いて研究し,$varepsilon$-optimal policyを同定するために必要なサンプル複雑性について検討した。 我々は,無限水平線形MDPに対して,最小限のサンプル複雑性を実現する最初の理論的アルゴリズムである分散重み付き最小二乗法MDVIを提案する。
  論文  参考訳（メタデータ） (2023-05-22T16:13:05Z)
• The Wisdom of Hindsight Makes Language Models Better Instruction Followers [84.9120606803906]
  強化学習は、人間のフィードバックによる指示に合うように、大きな言語モデルを微調整することに成功している。 そこで本稿では,本論文で提案するアプローチとして,原文を緩和することでフィードバックを指導に変換する手法と,教師付き手法によるアライメント向上のためのモデルをトレーニングする手法を提案する。 言語モデルと命令を整合させる新しいアルゴリズムであるHIR(Hindsight Instruction Relabeling)を提案する。
  論文  参考訳（メタデータ） (2023-02-10T12:16:38Z)

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

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