DeepSeek-Prover: 대규모 합성 데이터를 통해 LLM의 정리 증명 능력 향상DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale
Synthetic Data
Lean과 같은 증명 보조 도구는 수학적 증명 검증에 혁신을 가져와 높은 정확성과 신뢰성을 보장합니다. 대규모 언어 모델(LLM)은 수학적 추론에서 유망한 가능성을 보여주지만, 형식적 정리 증명 분야에서는 학습 데이터의 부족으로 인해 발전이 제한되고 있습니다. 이 문제를 해결하기 위해, 우리는 고등학교 및 학부 수준의 수학 경시대회 문제에서 유래한 Lean 4 증명 데이터를 대규모로 생성하는 접근법을 소개합니다. 이 접근법은 자연어 문제를 형식적 명제로 변환하고, 저품질 명제를 걸러내며, 증명을 생성하여 합성 데이터를 만드는 과정을 포함합니다. DeepSeekMath 7B 모델을 800만 개의 형식적 명제와 증명으로 구성된 이 합성 데이터셋으로 미세 조정한 후, 우리 모델은 Lean 4 miniF2F 테스트에서 64개 샘플 기준 46.3%, 누적 기준 52%의 전체 증명 생성 정확도를 달성했습니다. 이는 64개 샘플 기준 23.0%의 GPT-4와 41.0%의 트리 탐색 강화 학습 방법을 능가하는 성과입니다. 또한, 우리 모델은 Lean 4 Formalized International Mathematical Olympiad(FIMO) 벤치마크에서 148개 문제 중 5개를 성공적으로 증명했으며, GPT-4는 단 하나도 증명하지 못했습니다. 이러한 결과는 대규모 합성 데이터를 활용하여 LLM의 정리 증명 능력을 향상시킬 수 있는 잠재력을 보여줍니다. 합성 데이터셋과 모델은 이 유망한 분야의 추가 연구를 촉진하기 위해 공개될 예정입니다.