CuDIP: Enhancing Theorem Proving in LLMs via Curriculum Learning-based Direct Preference Optimization
작성자
- Haebom
카테고리
비어 있음
저자
Shuming Shi, Ruobing Zuo, Gaolei He, Jianlin Wang, Chenyang Xu, Zhengfeng Yang
개요
본 논문은 대규모 언어 모델(LLM)을 이용한 자동 정리 증명(ATP)에서, 기존의 지도 학습 기반 방법들의 한계를 극복하기 위해 직접적 선호도 최적화(DPO) 기법을 도입한 새로운 방법인 CuDIP(Curriculum Learning-based DPO Iterative Theorem Proving)을 제시합니다. CuDIP은 LLM과 기존 정리 증명 데이터를 활용하여 다양하고 고품질의 선호도 데이터를 생성하는 방법을 제안하며, 이를 커리큘럼 학습과 통합하여 반복적으로 정리 증명 모델을 미세 조정합니다. MiniF2F 및 ProofNet 데이터셋을 이용한 실험 결과를 통해 제안된 방법의 효과를 입증합니다.
시사점, 한계점
•
시사점:
◦
LLM 기반 ATP에서 DPO 적용의 효과성을 보여줌으로써, 인간의 선호도에 더욱 부합하는 ATP 시스템 개발 가능성을 제시합니다.
◦
LLM과 기존 데이터를 활용한 선호도 데이터 생성 방법은 고품질 데이터 확보의 어려움을 완화하는 데 기여합니다.
◦
커리큘럼 학습과의 통합을 통해 모델의 학습 효율성을 높였습니다.
•
한계점:
◦
제안된 선호도 데이터 생성 방법의 성능은 사용된 LLM과 기존 데이터의 질에 의존적일 수 있습니다.
◦
실험은 MiniF2F 및 ProofNet 데이터셋에 국한되어 있으며, 다른 데이터셋으로의 일반화 가능성은 추가 연구가 필요합니다.
◦
인간의 선호도를 완벽히 반영하는 것은 여전히 어려움이 있으며, 향후 더욱 정교한 선호도 모델링이 필요할 수 있습니다.
