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

TL;DR

This work addresses the mismatch between LLM-based automated theorem proving and human preferences by introducing CuDIP, a curriculum learning-based Direct Preference Optimization framework. CuDIP automatically constructs high-quality, diverse preference data using fine-grained scoring by LLMs and existing theorem-proving data, reducing reliance on manual annotations. It then applies curriculum-based iterative DPO to progressively refine a prover, yielding notable improvements on benchmarks such as MiniF2F and ProofNet (e.g., pass@1 up to 38.5% on MiniF2F-valid). The approach advances automated theorem proving by aligning optimization with human-like preferences while leveraging curriculum structure to steadily tackle harder problems, with strong empirical gains across multiple model configurations.

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.

Figures (3)

• Figure 1: Overview of Curriculum Learning-based DPO Iterative Theorem Proving (CuDIP). Stage 1: Preparation. The original data is partitioned to create curriculum data, and the base prover is trained using Supervised Fine-Tuning (SFT). Stage 2: Preference Data Generation. A score generator is trained to assign fine-grained scores to candidate strategies for a given proof state, followed by filtering and pairing to generate preference data. Stage 3: Curriculum-based DPO Iteration. The prover model undergoes iterative DPO fine-tuning based on the generated preference dataset, refining both the preference data and the prover model through successive iterations.
• Figure 2: An example of fine-grained preference scoring of all candidate tactics for the initial state of the Lean theorem (a b c: $\mathbb{N}$): a + b + c = c + b + a.
• Figure 3: Comparison curves of different iteration rounds using the CuDIP method. The performance curves depicting the proof success rates of the three model groups after four rounds of DPO iteration based on curriculum learning, evaluated on the MiniF2F-valid, MiniF2F-test, and ProofNet benchmarks.

Theorems & Definitions (2)

• Definition 1
• Definition 2