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