DeepSeek-Prover: 대규모 합성 데이터를 통해 LLM의 정리 증명 능력 향상

DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data

May 23, 2024

저자: Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, Xiaodan Liang

cs.AI

초록

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의 정리 증명 능력을 향상시킬 수 있는 잠재력을 보여줍니다. 합성 데이터셋과 모델은 이 유망한 분야의 추가 연구를 촉진하기 위해 공개될 예정입니다.

English

Proof assistants like Lean have revolutionized mathematical proof verification, ensuring high accuracy and reliability. Although large language models (LLMs) show promise in mathematical reasoning, their advancement in formal theorem proving is hindered by a lack of training data. To address this issue, we introduce an approach to generate extensive Lean 4 proof data derived from high-school and undergraduate-level mathematical competition problems. This approach involves translating natural language problems into formal statements, filtering out low-quality statements, and generating proofs to create synthetic data. After fine-tuning the DeepSeekMath 7B model on this synthetic dataset, which comprises 8 million formal statements with proofs, our model achieved whole-proof generation accuracies of 46.3% with 64 samples and 52% cumulatively on the Lean 4 miniF2F test, surpassing the baseline GPT-4 at 23.0% with 64 samples and a tree search reinforcement learning method at 41.0%. Additionally, our model successfully proved 5 out of 148 problems in the Lean 4 Formalized International Mathematical Olympiad (FIMO) benchmark, while GPT-4 failed to prove any. These results demonstrate the potential of leveraging large-scale synthetic data to enhance theorem-proving capabilities in LLMs. Both the synthetic dataset and the model will be made available to facilitate further research in this promising field.