✔️ А вот и новый DeepSeek Prover v2, модель, заточенная исключительно на математику.

🚀Масштабная архитектура на базе, которая содержит 671 млрд параметров, что в 96 раз больше, чем у предыдущей версии Prover-V1.5 (7 млрд).

Построен на базе архитектуры «смеси экспертов» (MoE), что снижает затраты на обучение и повышает эффективность решения задач.

Модель заточена на формальное доказательство теорем с помощью языка программирования Lean 4, обеспечивая 100% логическую точность.

Lean 4 — это зависимо типизированный функциональный язык программирования и интерактивное средство доказательства теорем.

Результаты:
• Новая Sota( 88,9%) на MiniF2F-test.
• DeepSeek-Prover-V2 смогла доказать 49 теорем из 658.

Для тренировки использовались 8 млн синтетических примеров, созданных через рекурсивный поиск решений теорем.

🔍 Как это работает:

1) Разложение теорем: DeepSeek-V3 по prompt'у разбивает сложные задачи на подцели.

2) Формализация: Пошаговые рассуждения переводятся в доказательства на Lean 4.

3) Cold-start: Полученные цепочки рассуждений и формальные доказательства используются как начальные данные для обучения модели.

🌟 Два размера:
• 7 B — базовый вариант.
• 671 B — расширенная версия на базе DeepSeek-V3-Base.

https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B