DeepSeek-Prover: 대규모 합성 데이터를 통해 LLMs의 정리 증명 기술 발전시키기

프루프 어시스턴트(Proof Assistants)인 린(Lean)은 수학적 증명 검증을 혁신하여 높은 정확성과 신뢰성을 보장하고 있습니다. 대형 언어 모델(Large Language Models, LLMs)이 수학적 추론에서 잠재력을 보이고 있지만, 형식적 정리 증명에서의 발전은 훈련 데이터 부족으로 제약을 받고 있습니다. 이 문제를 해결하기 위해 고등학교 및 대학 입학 전수준의 수학 경시대회 문제에서 유래된 광범위한 린 4 증명 데이터를 생성하는 접근법을 소개합니다.이 접근법은 자연어 문제를 형식적 명제로 번역하고, 저품질 명제를 필터링하며, 증명을 생성하여 합성 데이터를 만드는 과정을 포함합니다. 800만 개의 형식적 명제와 증명으로 구성된 이 합성 데이터셋을 사용하여 DeepSeekMath 7B 모델을 미세 조정(fine-tuning)한 결과, 린 4 miniF2F 테스트에서 64개 샘플로 46.3%의 전체 증명 생성 정확도와 누적으로 52%의 성능을 달성했습니다. 이는 기준 모델인 GPT-4가 64개 샘플로 23.0%의 정확도를 보인 것과 트리 탐색 강화 학습 방법이 41.0%의 성능을 보인 것에 비해 우수한 결과입니다.또한, 우리의 모델은 린 4 국제 수학 올림피아드(FIMO) 벤치마크의 148개 문제 중 5개를 성공적으로 증명했으며, GPT-4는 단 하나도 증명하지 못했습니다. 이러한 결과들은 대규모 합성 데이터를 활용하여 LLMs의 정리 증명 능력을 향상시키는 잠재력을 입증합니다. 합성 데이터셋과 모델은 모두 제공되어 이 유망한 분야에서 더 많은 연구를 촉진할 것입니다.