論文の概要: CuDIP: Enhancing Theorem Proving in LLMs via Curriculum Learning-based Direct Preference Optimization

• arxiv url: http://arxiv.org/abs/2502.18532v1
• Date: Tue, 25 Feb 2025 03:07:02 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-02-27 15:24:46.257684
• Title: CuDIP: Enhancing Theorem Proving in LLMs via Curriculum Learning-based Direct Preference Optimization
• Title（参考訳）: CuDIP: カリキュラム学習による直接選好最適化によるLLMにおける定理証明の強化
• Authors: Shuming Shi, Ruobing Zuo, Gaolei He, Jianlin Wang, Chenyang Xu, Zhengfeng Yang,
• Abstract要約: 本稿では,Curriculum Learning-based DPO Iterative Theorem Proving (CuDIP)法を提案する。 LLMと既存の定理証明データを利用した嗜好データ構築手法を提案する。 次に、この選好データ構築手法とカリキュラム学習を統合し、定理証明モデルを反復的に微調整する。
• 参考スコア（独自算出の注目度）: 22.935127114462475
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Automated theorem proving (ATP) is one of the most challenging mathematical reasoning tasks for Large Language Models (LLMs). Most existing LLM-based ATP methods rely on supervised fine-tuning, which results in a limited alignment between the theorem proving process and human preferences. Direct Preference Optimization (DPO), which aligns LLMs with human preferences, has shown positive effects for certain tasks. However, the lack of high-quality preference data for theorem proving presents a significant challenge. In this paper, we innovatively apply DPO to formal automated theorem proving and introduces a Curriculum Learning-based DPO Iterative Theorem Proving (CuDIP) method. Specifically, we propose a method for constructing preference data which utilizes LLMs and existing theorem proving data to enhance the diversity of the preference data while reducing the reliance on human preference annotations. We then integrate this preference data construction method with curriculum learning to iteratively fine-tune the theorem proving model through DPO. Experimental results on the MiniF2F and ProofNet datasets demonstrate the effectiveness of the proposed method.
• Abstract（参考訳）: 自動定理証明(ATP、Automated theorem Proving)は、大規模言語モデル(LLM)において最も難しい数学的推論タスクの一つである。 既存のLCMベースのATP法の多くは、教師付き微調整に依存しており、その結果、定理証明過程と人間の嗜好の間に限定的な一致が生じる。 直接選好最適化(DPO)は、LLMと人間の選好を一致させ、特定のタスクに対して肯定的な効果を示した。 しかし、定理証明のための高品質な選好データが欠如していることは重要な課題である。 本稿では,DPOを形式的自動定理証明に適用し,カリキュラム学習に基づく反復定理証明法(CuDIP)を提案する。 具体的には、LLMと既存の定理証明データを利用して嗜好データを構築する方法を提案し、人間の嗜好アノテーションへの依存を軽減しつつ、嗜好データの多様性を高める。 次に、この選好データ構築手法とカリキュラム学習を統合し、DPOによる定理証明モデルを反復的に微調整する。 The MiniF2F and ProofNet datas showed the effective of the method。

関連論文リスト

• A Survey of Direct Preference Optimization [103.59317151002693]
  LLM(Large Language Models)は、前例のない生成能力を示す。 人的価値との整合性は、有用で無害なデプロイメントを保証する上で、依然として重要です。 直接優先度最適化(DPO)は、最近、合理化された代替案として注目されている。
  論文  参考訳（メタデータ） (2025-03-12T08:45:15Z)
• The First Few Tokens Are All You Need: An Efficient and Effective Unsupervised Prefix Fine-Tuning Method for Reasoning Models [69.798277882245]
  大規模言語モデルの推論効率を向上させるために,Unsupervised Prefix Fine-Tuning (UPFT)を導入した。 UPFTはラベル付きデータや徹底的なサンプリングの必要性を取り除く。 実験の結果,UPFTは教師付き手法の性能と一致していることがわかった。
  論文  参考訳（メタデータ） (2025-03-04T18:56:03Z)
• Flow-DPO: Improving LLM Mathematical Reasoning through Online Multi-Agent Learning [14.156753196673598]
  本稿では,大規模言語モデルの微調整のための高品質な推論トレースを作成するための新しい手法を提案する。 本手法では,コンポーネントLLMが協調的にソリューションを構築するために,インクリメンタルな出力生成フローを用いる。 オンラインダイレクトパラメータ最適化(DPO)学習を用いてフローをトレーニングし、トレーニング例毎にDPOペアを生成し、モデルをリアルタイムで更新する。
  論文  参考訳（メタデータ） (2024-10-29T17:50:31Z)
• ASFT: Aligned Supervised Fine-Tuning through Absolute Likelihood [14.512464277772194]
  Aligned Supervised Fine-Tuning (ASFT)は、大規模言語モデルとペアワイズデータセットの整合性を改善する効果的なアプローチである。 ASFTは、DPO損失関数が人間の不適切なデータを生成する確率を減少させる問題を緩和する。 大規模な実験により、ASFTは効果的なアライメントアプローチであり、既存の手法より一貫して優れていることが示された。
  論文  参考訳（メタデータ） (2024-09-14T11:39:13Z)
• On the Limited Generalization Capability of the Implicit Reward Model Induced by Direct Preference Optimization [25.76847680704863]
  RLHFのようにEXRM(Explicit Reward Model)を訓練し、DPO(Direct Preference Optimization)などの手法を用いて、嗜好データから学習した暗黙の報酬を用いて報酬モデルを学習する。 本研究は,DPORM と EXRM の双方に対して,推奨回答と拒否回答を区別する精度について検討した。
  論文  参考訳（メタデータ） (2024-09-05T16:08:19Z)
• Step-level Value Preference Optimization for Mathematical Reasoning [6.318873143509028]
  SVPO(Step-level Value Preference Optimization)と呼ばれる新しいアルゴリズムを導入する。 提案手法は,領域内および領域外両方の数学的推論ベンチマーク上での最先端性能を実現する。
  論文  参考訳（メタデータ） (2024-06-16T09:06:17Z)
• Multi-Reference Preference Optimization for Large Language Models [56.84730239046117]
  複数の参照モデルを用いた直接選好最適化のための新しいクローズドフォームの定式化を提案する。 得られたアルゴリズムであるMulti-Reference Preference Optimization (MRPO)は、様々な参照モデルからより広範な事前知識を活用する。 MRPOを微調整したLLMは,データ不足や多量性に関わらず,様々な嗜好データにおいてより一般化されていることを示す。
  論文  参考訳（メタデータ） (2024-05-26T00:29:04Z)
• Towards Optimal Learning of Language Models [124.65669486710992]
  言語モデル(LM)の最適学習の理論を提案する。 我々は、最適学習過程における力学の性質を明らかにするために、学習法則という定理を導出した。 我々は、LMの最適学習が、LMのスケーリング法則における係数の改善に起因することを実証的に検証した。
  論文  参考訳（メタデータ） (2024-02-27T18:52:19Z)
• LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
  大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。 既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。 本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。 本研究では,LLM ベースの証明器 ReProver を開発した。
  論文  参考訳（メタデータ） (2023-06-27T17:05:32Z)
• Provable Reward-Agnostic Preference-Based Reinforcement Learning [61.39541986848391]
  PbRL(Preference-based Reinforcement Learning)は、RLエージェントが、軌道上のペアワイドな嗜好に基づくフィードバックを用いてタスクを最適化することを学ぶパラダイムである。 本稿では,隠れた報酬関数の正確な学習を可能にする探索軌道を求める理論的報酬非依存PbRLフレームワークを提案する。
  論文  参考訳（メタデータ） (2023-05-29T15:00:09Z)

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

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