DeepSeek выпустила обновлённую модель Prover-V2 для решения математических задач
Китайский стартап DeepSeek без лишнего шума представил новую версию своей специализированной ИИ-модели Prover-V2 - всего через день после релиза третьего поколения Qwen от Alibaba. Модель уже доступна с открытым исходным кодом на платформе Hugging Face.
Prover-V2 - это языковая модель с 671 миллиарда параметров, построенная на архитектуре Mixture-of-Experts (MoE) и основанная на базе DeepSeek V3. Prover-V2 специализируется на формальном доказательстве теорем с помощью языка программирования Lean 4, что позволяет ей автоматически проверять математические доказательства, находить ошибки в рассуждениях и генерировать пошаговые решения - от школьных задач до олимпиадного уровня - с 100% логической точностью.
Как работает?
- Prover-V2 разбивает сложные задачи на простые подзадачи, выстраивая их в логическую цепочку для более точных результатов.
- Для обучения использовался метод «холодного старта» на основе 8 миллиардов синтетических примеров, дополненных новыми данными.
- Применяется обучение с подкреплением, где модель получает обратную связь в формате «верно/неверно» для повышения качества решений.
- Есть облегчённая версия Prover-V2 с 7 млрд параметров и контекстом до 32 тысяч токенов.
Результаты и тесты:
- Prover-V2 успешно решает задачи из престижных математических конкурсов, таких как AIME и PutnamBench.
- На тесте MiniF2F модель демонстрирует точность 88.9% - один из лучших результатов среди ИИ для математики.
Prover-V2 - шаг к созданию ИИ, способного помогать в научных исследованиях, автоматизировать проверку сложных математических доказательств и обучать студентов, связывая формальные доказательства с понятными объяснениями.
Релиз Prover-V2 усиливает позиции китайских ИИ-моделей на мировой арене и подогревает ожидания вокруг будущего мультимодального DeepSeek R2, запуск которого ожидается в ближайшее время.