用课程学习优化大模型证明定理，提升推理能力
CuDIP: Enhancing Theorem Proving in LLMs via Curriculum Learning-based Direct Preference Optimization
- 构建自动偏好数据，减少人工标注依赖
- 在MiniF2F和ProofNet上准确率显著提升
- 适合需要高精度数学推理的研究者
自动化定理证明（ATP）是大型语言模型（LLMs）面临的最具挑战性的数学推理任务之一。现有基于LLM的ATP方法多依赖监督微调，导致证明过程与人类偏好对齐不足。直接偏好优化（DPO）虽能对齐人类偏好，但定理证明缺乏高质量偏好数据。本文创新性地将DPO应用于形式化自动定理证明，提出基于课程学习的迭代定理证明方法CuDIP。通过结合LLM与已有定理证明数据，构建多样化偏好数据，降低对人工标注的依赖。再融合课程学习，通过DPO逐步迭代优化定理证明模型。在MiniF2F和ProofNet数据集上的实验表明该方法有效。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。