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

TL;DR

This paper introduces CuDIP, a novel curriculum learning-based approach that applies Direct Preference Optimization to improve automated theorem proving in LLMs, leveraging synthetic preference data to better align models with human reasoning.

Contribution

It presents a new method for constructing preference data using LLMs and theorem data, combined with curriculum learning, to enhance theorem proving performance without extensive human annotations.

Findings

CuDIP outperforms baseline models on MiniF2F and ProofNet datasets.

Synthetic preference data improves model alignment with human reasoning.

Curriculum learning accelerates the fine-tuning process and boosts accuracy.

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.