CuDIP：通过基于课程学习的直接偏好优化增强LLM中的定理证明
人工智能
2025-02-27 v1 机器学习
摘要
自动定理证明（ATP）是大型语言模型（LLM）最具挑战性的数学推理任务之一。大多数现有的基于LLM的ATP方法依赖监督微调，这导致定理证明过程与人类偏好之间的对齐有限。直接偏好优化（DPO）是一种将LLM与人类偏好对齐的方法，已在某些任务中显示出积极效果。然而，定理证明领域缺乏高质量的偏好数据是一个重大挑战。在本文中，我们创新性地将DPO应用于形式化自动定理证明，并提出了一种基于课程学习的DPO迭代定理证明方法（CuDIP）。具体而言，我们提出了一种偏好数据构建方法，利用LLM和现有的定理证明数据来增强偏好数据的多样性，同时减少对人类偏好标注的依赖。然后，我们将这种偏好数据构建方法与课程学习相结合，通过DPO迭代微调定理证明模型。在MiniF2F和ProofNet数据集上的实验结果证明了所提出方法的有效性。
引用
@article{arxiv.2502.18532,
title = {CuDIP: Enhancing Theorem Proving in LLMs via Curriculum Learning-based Direct Preference Optimization},
author = {Shuming Shi and Ruobing Zuo and Gaolei He and Jianlin Wang and Chenyang Xu and Zhengfeng Yang},
journal= {arXiv preprint arXiv:2502.18532},
year = {2025}
}