DeepSeek-Prover: Продвижение теоремного доказательства в LLMs через синтетические данные большого масштаба

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 на этом синтетическом наборе данных, включающем 8 миллионов формальных утверждений с доказательствами, наша модель достигла точности генерации целого доказательства 46,3% с 64 образцами и 52% кумулятивно на тесте Lean 4 miniF2F, превзойдя базовую модель GPT-4 с 23,0% с 64 образцами и метод обучения с подкреплением поиска по дереву на уровне 41,0%. Кроме того, наша модель успешно доказала 5 из 148 задач в Lean 4 Формализованной Международной Математической Олимпиаде (FIMO), в то время как 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.