Математика и рассужденияКод
DeepSeek-Prover
Модели DeepSeek для формальных доказательств на языке Lean 4: доказательство проверяет программа, а не человек. Узкий инструмент для математиков и инженеров.
- Разработчик
- DeepSeek, Китай
- Первый выпуск
- авг 2024
- Последний выпуск
- апр 2025
- Размеры
- 7B – 671B
- Лицензия
- Коммерция с условиямиСобственная лицензия DeepSeek (коммерция разрешена с ограничениями)
Какие задачи решает
- Формальная проверка математических выкладок
- Проверка корректности алгоритмов
- Обучение и олимпиадная подготовка
Где применяется
Исследовательские группыРазработка критичного ПООбразование
Требования к железу
НоутбукНоутбук или обычный ПК, до 8 ГБ видеопамяти — младшие версии
подходит1 видеокартаОдна видеокарта на 16–80 ГБ — средние версии
подходитКластерСервер с несколькими видеокартами — флагманские версии
подходитВерсии
- DeepSeek-Prover-V2 7B и 671B
- DeepSeek-Prover-V1.5
- DeepSeek-Prover-V1
Как внедряю у заказчика
- ПодборВыбираю размер модели под задачу и ваше железо, проверяю на ваших примерах.
- УстановкаРазворачиваю на вашем сервере или в закрытом контуре, отдаю API.
- ДообучениеДообучаю на ваших данных (LoRA) или подключаю базу знаний — что дешевле для задачи.
- ВстраиваниеПодключаю к CRM, 1С, боту, сайту или рабочему чату, настраиваю мониторинг.
Похожие модели
Математика и рассужденияKimina-ProverMoonshot AI и Project Numina · Китай, ФранцияМожно в коммерцию
Модели для формальных доказательств в Lean 4 от Moonshot AI (Kimi) и Numina. Есть маленькие версии от 0.6B, которые запускаются на ноутбуке.
ПодробнееМатематика и рассужденияGoedel-ProverПринстонский университет · СШАМожно в коммерциюОткрытые модели для формальных доказательств в Lean 4 из Принстона. Свежая Goedel-Code-Prover доказывает корректность программ.
ПодробнееМатематика и рассужденияDeepSeek-MathDeepSeek · КитайКоммерция с условиямиМатематические модели DeepSeek. Первая версия 7B ввела метод обучения GRPO, V2 на 685B пишет и сама проверяет доказательства уровня олимпиад.
Подробнее