Китайский стартап в области ИИ DeepSeek тихо выпустил Prover-V2 — специализированную модель с 671 миллиардом параметров, созданную для решения математических доказательств и теорем. Релиз состоялся всего через день после анонса Alibaba новой линейки моделей Qwen3 и на фоне нарастающего ожидания новой модели DeepSeek R2, ориентированной на рассуждения, пишет IndexBox.
Ключевые особенности Prover-V2
Prover-V2, построенная на базе фреймворка DeepSeek V3, использует архитектуру Mixture-of-Experts (MoE), которая разбивает сложные математические задачи на подзадачи, распределяя их между специализированными модулями-«экспертами». Это позволяет активировать только нужные части модели, обеспечивая высокую вычислительную эффективность. Благодаря квантованию FP8 модель снижает требования к ресурсам, сохраняя при этом математическую точность, что делает её доступной даже для оборудования с ограниченными возможностями.
Модель, выпущенная с открытым исходным кодом на Hugging Face, получила высокую оценку за демократизацию доступа к передовым математическим инструментам. Участники математических олимпиад уже отметили её впечатляющие способности в формальном доказательстве теорем. Одной из ключевых инноваций стала уникальная процедура обучения с «холодного старта», которая позволяет Prover-V2 создавать формальные доказательства с использованием Lean 4 — популярного инструмента для математических исследований. Это связывает интуитивное математическое мышление с формальной строгостью.
Контекст и конкуренция в индустрииРелиз Prover-V2 пришёлся на напряжённый момент в мире ИИ, сразу после анонса линейки Qwen3 от Alibaba, которая также делает акцент на решении математических задач и логических рассуждениях. Хотя крупнейшая публичная модель Qwen3 насчитывает 235 миллиардов параметров, Prover-V2 с её 671 миллиардом параметров демонстрирует выдающуюся производительность при оптимизированных ресурсах благодаря MoE-архитектуре. Это позволяет DeepSeek добиваться высоких результатов с меньшими затратами.
Китайские ИИ-компании всё активнее бросают вызов западным игрокам. Предыдущая модель DeepSeek R1 уже сравнялась по производительности с o1 от OpenAI, но с куда меньшими затратами на обучение. Математический ИИ становится ареной ожесточённой конкуренции: Xiaomi недавно представила свою линейку моделей MiMo-7B, ориентированных на рассуждения. Усиление соперничества подчёркивает важность специализированных ИИ-моделей, способных справляться со сложными математическими задачами и формальными доказательствами. Открытый доступ к таким инструментам делает их достоянием мирового ИИ-сообщества.
Достижения DeepSeek в области ИИСлухи о грядущей модели DeepSeek R2, которая, предположительно, получит около 1,2 триллиона параметров, а также функции компьютерного зрения и ещё более продвинутые способности к рассуждениям, только подогревают интерес. Ожидалось, что R2 появится ещё в марте 2025 года, но точная дата релиза пока не подтверждена. Выпуск Prover-V2 многие рассматривают как стратегический ход, демонстрирующий технические возможности DeepSeek перед запуском флагманской R2.
Подход компании к созданию специализированных ИИ-моделей ярко проявился в DeepSeekMath 7B, которая набрала впечатляющие 51,7% на соревновательном тесте MATH без использования внешних инструментов или методов голосования. Фокус на узкоспециализированном превосходстве, а не на универсальной функциональности, отличает стратегию DeepSeek, позволяя создавать высокоэффективные модели для конкретных задач, параллельно развивая более широкие способности к рассуждениям.
Перспективы и модель R2
Тихий релиз Prover-V2 имеет серьёзные последствия для будущего ИИ в математических исследованиях, потенциально меняя подход к решению сложных доказательств и теорем. Эта модель отражает растущую тенденцию к созданию узкоспециализированных ИИ-инструментов, которые блистают в критически важных областях, вместо погони за универсальным интеллектом. Исследователи теперь могут использовать двойной режим Prover-V2: для быстрого изучения математических задач и для генерации доказательств с высокой степенью уверенности, соединяя интуицию с формальной строгостью.
Тем временем ИИ-сообщество с нетерпением ждёт R2, которая, по слухам, может превзойти ведущие модели OpenAI, Anthropic и других конкурентов, сохраняя при этом экономическую эффективность DeepSeek. Reuters в марте сообщал, что запуск R2 может состояться «уже в этом месяце», но DeepSeek пока не назвал точной даты. Когда R2 появится, она, вероятно, изменит конкурентный ландшафт мирового ИИ благодаря улучшенным возможностям в рассуждениях, программировании и многоязычной обработке.
Следите за NEWS.am Tech на Facebook и Twitter