DeepSeek-Prover-V2: новая эра в доказательстве теорем
Компания DeepSeek AI объявила о выходе DeepSeek-Prover-V2, революционной открытой модели, предназначенной для формального доказательства теорем в среде Lean 4. Эта новая версия представляет собой улучшение предыдущих разработок и вводит инновационный рекурсивный процесс поиска доказательств. Используя модель DeepSeek-V3, она генерирует собственные данные для инициализации, что обеспечивает выдающиеся результаты в нейросетевом доказательстве теорем.
Ключевое новшество DeepSeek-Prover-V2 заключается в уникальной процедуре обучения холодного старта, где модель сначала разбивает сложные теоремы на более простые подзадачи. Для поиска доказательств применяется модель с 7 миллиардами параметров, а результатом является полное формальное доказательство, интегрирующее неформальное обоснование.
Модель, достигшая 671 миллиард параметров, показала высокие результаты, включая 88.9% успешных доказательств на тесте MiniF2F. В дополнение, стартует ProverBench — новый бенчмарк, который сосредоточится на более тщательной оценке математической логики и произвола в доказательствах.
Лаборатория DeepSeek предоставляет эти инновации в двух размерах для различных вычислительных ресурсов и готова к сложным математическим задачам.
*компания Meta Platforms Inc. признана экстремистской организацией, ее деятельность на территории России запрещена