論文の概要: 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:強化学習とモンテカルロ木探索のための補足フィードバックのハーネス化
• 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\%$)のテストセットで、最先端の結果が得られた。

関連論文リスト

• CHORUS: Complementary Experts for High-Coverage Testbench Stimulus Generation [12.10027872270898]
  ハードウェア検証は、大規模言語モデル(LLM)の重要な応用である 従来の教師付き微調整(SFT)-強化学習(RL)パイプラインが達成するものを超えて,パフォーマンスを向上するポストトレーニングフレームワークであるCHORUSを提案する。 ChoRUSはCVDP-ECovで88.0%のPass@1を獲得し、DeepSeek-R1(671B)を13.5ポイント上回っている。
  論文  参考訳（メタデータ） (2026-08-10T18:02:42Z)
• DeepSeek-V4: Towards Highly Efficient Million-Token Context Intelligence [240.40422202055993]
  We present a preview version of DeepSeek-V4 series, including two strong Mixture-of-Experts (MoE) language model。 DeepSeek-V4シリーズには、アーキテクチャと最適化のいくつかの重要なアップグレードが含まれている。 DeepSeek-V4シリーズは、長いコンテキストシナリオにおいて非常に効率的である。
  論文  参考訳（メタデータ） (2026-04-26T14:49:33Z)
• StepFun-Prover Preview: Let's Think and Verify Step by Step [14.896796588073725]
  本稿では,ツール統合推論による形式定理証明のための大規模言語モデルであるStepFun-Prover Previewを提案する。 提案手法は,実時間環境フィードバックに基づく証明を反復的に精錬することにより,人間的な問題解決戦略をエミュレートすることを可能にする。 miniF2F-testベンチマークでは、StepFun-Proverがパス@1成功率70.0%$を達成した。
  論文  参考訳（メタデータ） (2025-07-27T09:38:32Z)
• ReasonFlux-PRM: Trajectory-Aware PRMs for Long Chain-of-Thought Reasoning in LLMs [56.32212611983997]
  本稿では,新しいトラジェクトリ対応PRMであるReasonFlux-PRMを紹介し,トラジェクトリ応答型推論トレースの評価を行う。 ReasonFlux-PRMはステップレベルとトラジェクトリレベルの両方の監視機能を備えており、構造化された連鎖データと整合した微粒な報酬割り当てを可能にする。 得られたReasonFlux-PRM-7Bは、教師付き微調整で平均12.1%、強化学習で4.5%、テスト時間スケーリングで6.3%向上した。
  論文  参考訳（メタデータ） (2025-06-23T17:59:02Z)
• Phi-4-reasoning Technical Report [42.508165017775]
  Phi-4-reasoningは14ビリオンのパラメータ推論モデルであり、複雑な推論タスクにおいて高い性能を実現する。 我々はPhi-4-reasoning-plusを開発した。 どちらのモデルもDeepSeek-R1-Distill-Llama-70Bモデルのような大きなオープンウェイトモデルよりも優れており、完全なDeepSeek-R1モデルのパフォーマンスレベルに近づいている。
  論文  参考訳（メタデータ） (2025-04-30T05:05:09Z)
• Hierarchical Attention Generates Better Proofs [8.676187819105298]
  注意機構を数学的推論構造に整合させる正規化手法であるtextbfHierarchical Attention を導入する。 提案手法は,基礎要素から高レベル概念への5段階階層を確立し,証明生成における構造化情報の流れを確実にする。
  論文  参考訳（メタデータ） (2025-04-27T10:35:05Z)
• Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning [38.4246156415702]
  Kimina-Proverは、形式的定理証明のための新しい推論駆動探索パラダイムを開拓した大きな言語モデルである。 Qwen2.5-72Bから大規模な強化学習パイプラインでトレーニングされたKimina-Proverは、Lean 4の証明生成において、強力なパフォーマンスを示している。 Kimina-Prover は miniF2F ベンチマークに新しい最先端をセットし、pass@8192 で 80.7% に達した。
  論文  参考訳（メタデータ） (2025-04-15T16:23:44Z)
• Open-Reasoner-Zero: An Open Source Approach to Scaling Up Reinforcement Learning on the Base Model [47.108822717757945]
  大規模推論指向RLトレーニングの最初のオープンソース実装であるOpen-Reasoner-Zeroを紹介する。 オープンソースを念頭に置いて、ソースコード、パラメータ設定、トレーニングデータ、さまざまなサイズのモデルウェイトをリリースしています。
  論文  参考訳（メタデータ） (2025-03-31T16:36:05Z)
• Understanding R1-Zero-Like Training: A Critical Perspective [73.25430192337235]
  ベースモデルとRLの2つのコアコンポーネントを分析し,R1-Zeroライクなトレーニングを批判的に検討した。 本稿では,DeepSeek-V3-Baseを含む幅広いベースモデルについて検討し,事前学習特性がRL性能に与える影響について考察する。 AIME 2024では7Bベースモデルで43.3%の精度を達成できる最小限のR1-Zeroレシピを提案する。
  論文  参考訳（メタデータ） (2025-03-26T17:59:14Z)
• Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving [72.8626512877667]
  我々は,2025年4月5日現在,数学問題の自動証明生成における最先端(最先端)性能を実現する,オープンソースの言語モデルであるGoedel-Proverを紹介した。 まず、自然言語の数学問題をNuminaデータセットからLean 4で等価な形式ステートメントに変換するためにLLMをトレーニングします。 次に,一連のプロデューサをトレーニングすることで,形式証明の大規模なデータセットを開発する。 最後に、Goedel-Pset-v1-solvedというデータセットを取得し、Goedel-Pset-v1から800K以上のステートメントの証明を含む。
  論文  参考訳（メタデータ） (2025-02-11T15:27:35Z)
• 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)
• DepthSplat: Connecting Gaussian Splatting and Depth [90.06180236292866]
  ガウススプラッティングと深さ推定を結合するDepthSplatを提案する。 ガウススプラッティングは、強力な深度モデルを学ぶための教師なし事前学習の目的として機能することを示す。 我々のDepthSplatは、ScanNet、RealEstate10K、DL3DVデータセットの最先端のパフォーマンスを実現しています。
  論文  参考訳（メタデータ） (2024-10-17T17:59:58Z)
• 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)

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

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