CuDIP: Enhancing Theorem Proving in LLMs via Curriculum Learning-based Direct Preference Optimization

• URL: http://arxiv.org/abs/2502.18532v1
• Date: Tue, 25 Feb 2025 03:07:02 GMT
• Title: CuDIP: Enhancing Theorem Proving in LLMs via Curriculum Learning-based Direct Preference Optimization
• Authors: Shuming Shi, Ruobing Zuo, Gaolei He, Jianlin Wang, Chenyang Xu, Zhengfeng Yang,
• Abstract summary: This paper introduces a Curriculum Learning-based DPO Iterative Theorem Proving (CuDIP) method.<n>We propose a method for constructing preference data which utilizes LLMs and existing theorem proving data.<n>We then integrate this preference data construction method with curriculum learning to iteratively fine-tune the theorem proving model.
• Score: 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.

Related papers

• A Survey of Direct Preference Optimization [103.59317151002693]
  Large Language Models (LLMs) have demonstrated unprecedented generative capabilities. Their alignment with human values remains critical for ensuring helpful and harmless deployments. Direct Preference Optimization (DPO) has recently gained prominence as a streamlined alternative.
  arXiv  Detail & Related papers  (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]
  We introduce Unsupervised Prefix Fine-Tuning (UPFT) to enhance large language models' reasoning efficiency. UPFT removes the need for labeled data or exhaustive sampling. Experiments show that UPFT matches the performance of supervised methods.
  arXiv  Detail & Related papers  (2025-03-04T18:56:03Z)
• Flow-DPO: Improving LLM Mathematical Reasoning through Online Multi-Agent Learning [14.156753196673598]
  This paper introduces a novel approach to produce high-quality reasoning traces for Large Language Models fine-tuning. Our method employs an incremental output production Flow, where component LLMs collaboratively construct solutions. We train the Flow using online Direct Preference Optimization (DPO) learning with rollouts, generating DPO pairs for each training example and updating models in real-time.
  arXiv  Detail & Related papers  (2024-10-29T17:50:31Z)
• ASFT: Aligned Supervised Fine-Tuning through Absolute Likelihood [14.512464277772194]
  Aligned Supervised Fine-Tuning (ASFT) is an effective approach that better aligns Large Language Models with pair-wise datasets. ASFT mitigates the issue where the DPO loss function decreases the probability of generating human-dispreferred data. Extensive experiments demonstrate that ASFT is an effective alignment approach, consistently outperforming existing methods.
  arXiv  Detail & Related papers  (2024-09-14T11:39:13Z)
• On the Limited Generalization Capability of the Implicit Reward Model Induced by Direct Preference Optimization [25.76847680704863]
  Two main approaches for learning a reward model are 1) training an EXplicit Reward Model (EXRM) as in RLHF, and 2) using an implicit reward learned from preference data through methods such as Direct Preference Optimization (DPO) This work studies the accuracy at distinguishing preferred and rejected answers for both DPORM and EXRM.
  arXiv  Detail & Related papers  (2024-09-05T16:08:19Z)
• Step-level Value Preference Optimization for Mathematical Reasoning [6.318873143509028]
  We introduce a novel algorithm called Step-level Value Preference Optimization (SVPO) Our method achieves state-of-the-art performance on both in-domain and out-of-domain mathematical reasoning benchmarks.
  arXiv  Detail & Related papers  (2024-06-16T09:06:17Z)
• Multi-Reference Preference Optimization for Large Language Models [56.84730239046117]
  We introduce a novel closed-form formulation for direct preference optimization using multiple reference models. The resulting algorithm, Multi-Reference Preference Optimization (MRPO), leverages broader prior knowledge from diverse reference models. Our experiments demonstrate that LLMs finetuned with MRPO generalize better in various preference data, regardless of data scarcity or abundance.
  arXiv  Detail & Related papers  (2024-05-26T00:29:04Z)
• Towards Optimal Learning of Language Models [124.65669486710992]
  We present a theory for the optimal learning of language models (LMs) We derive a theorem, named Learning Law, to reveal the properties of the dynamics in the optimal learning process under our objective. We empirically verify that the optimal learning of LMs essentially stems from the improvement of the coefficients in the scaling law of LMs.
  arXiv  Detail & Related papers  (2024-02-27T18:52:19Z)
• LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
  Large language models (LLMs) have shown promise in proving formal theorems using proof assistants such as Lean. Existing methods are difficult to reproduce or build on, due to private code, data, and compute requirements. This paper introduces LeanDojo: an open-source Lean toolkit consisting of toolkits, data, models. We develop ReProver: an LLM-based prover augmented with retrieval for selecting premises from a vast math library.
  arXiv  Detail & Related papers  (2023-06-27T17:05:32Z)
• Provable Reward-Agnostic Preference-Based Reinforcement Learning [61.39541986848391]
  Preference-based Reinforcement Learning (PbRL) is a paradigm in which an RL agent learns to optimize a task using pair-wise preference-based feedback over trajectories. We propose a theoretical reward-agnostic PbRL framework where exploratory trajectories that enable accurate learning of hidden reward functions are acquired.
  arXiv  Detail & Related papers  (2023-05-29T15:00:09Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.