Компания DeepSeek AI анонсировала новый проект DeepSeek-Prover-V2 – открытый языковой модель, предназначенная для автоматического доказательства теорем в среде Lean 4. В этой версии разработчики внедрили инновационный рекурсивный алгоритм поиска теорем, который использует возможности DeepSeek-V3 для генерации высококачественных данных инициализации. Новый модель достигает выдающихся результатов в нейронном доказательстве теорем.
Ключевой инновацией является процедура холодного старта, где DeepSeek-V3 разбивает сложные теоремы на более простые подзадачи и формализует их в Lean 4. Для вычислительных поисков использовалась меньшая модель с 7 миллиардами параметров. Полученные формальные доказательства затем связываются с рассуждениями DeepSeek-V3, что позволяет эффективно обучать модель на synthesized dataset с высоким уровнем математической логики и формализации.
DeepSeek также представила ProverBench – новый бенчмарк с 325 задачами, который предлагает более полную оценку математических способностей различных уровней сложности. DeepSeek-Prover-V2 доступен в двух размерах: с 7B и культурным уровнем 671B параметров. Эти достижения демонстрируют шаг вперед в нейронном доказательстве теорем и помогают разработать более мощные AI-системы для формальной математики.
*Компания Meta Platforms Inc. признана экстремистской организацией, ее деятельность на территории России запрещена.