DeepSeek-Prover-V2-671B теперь доступен на Novita AI

Компания DeepSeek тихо обновила Prover — свою AI-модель, предназначенную для решения математических доказательств и теорем. Модель DeepSeek-Prover-V2-671B теперь доступна на платформе Model API от Novita AI! В течение ограниченного времени все новые пользователи могут получить $10 бесплатных кредитов, чтобы изучить и создавать решения с помощью этой передовой модели автоматического доказательства теорем.

Вот текущие цены на DeepSeek-Prover-V2-671B на Novita AI:

DeepSeek-Prover-V2-671B: 0,7 $ / млн входных токенов, 2,5 $ / млн выходных токенов

Запускайте свои математические рабочие процессы, исследования и образовательные инструменты с помощью одной из самых продвинутых моделей формального доказательства теорем — теперь всего лишь один API-запрос.

Что такое серия моделей DeepSeek-Prover?

Серия моделей DeepSeek-Prover — это семейство передовых больших языковых моделей (LLM), созданных для решения задачи автоматического доказательства теорем в математике. Разработанные DeepSeek-AI, эти модели специально оптимизированы для генерации, проверки и рассуждения о формальных математических доказательствах — особенно в среде ассистента доказательств Lean 4.

Зачем был создан DeepSeek-Prover?

Хотя современные LLM, такие как GPT-4, впечатляют в математических рассуждениях, они испытывают трудности с задачами формального доказательства из-за нехватки высококачественных и масштабных обучающих данных на формальных языках. DeepSeek-Prover решает эту проблему, автоматически генерируя миллионы синтетических доказательств Lean 4 на основе задач математических олимпиад и дообучаясь на этом уникальном наборе данных.

Как работает DeepSeek-Prover?

Конвейер DeepSeek-Prover включает:

• Автоформализация: Перевод математических задач на естественном языке в формальные утверждения Lean 4 с помощью LLM.
• Фильтрация качества: Отбор утверждений по логической корректности и математической значимости с помощью оценки модели и отклонения гипотез.
• Генерация и проверка доказательств: Попытка доказать отфильтрованные утверждения и сохранение только тех, у которых есть корректные проверяемые доказательства.
• Итеративное обучение: Повторение процесса, каждый раз используя новые высококачественные данные доказательств для дальнейшего улучшения модели.

Благодаря такому подходу серия DeepSeek-Prover создаёт модели, которые непрерывно совершенствуются и подкрепляются одной из крупнейших в мире коллекций формальных математических доказательств.

Основные достижения и вехи более ранних моделей DeepSeek-Prover

• Масштаб: Было сгенерировано более 8 миллионов формальных утверждений Lean 4 с доказательствами.
• Техническая основа: Основаны на больших трансформерных моделях, таких как DeepSeekMath 7B, предобученных на обширных математических данных и дообученных на синтетических доказательствах.
• Передовая производительность: Достигнуты лучшие результаты на эталонных тестах формального доказательства теорем (например, miniF2F, FIMO), превосходя GPT-4 и другие специализированные модели.

Что такое DeepSeek-Prover-V2-671B?

DeepSeek-Prover-V2-671B — флагманская модель в серии DeepSeek-Prover. Вот что её выделяет:

• Огромный масштаб: С примерно 671 миллиардом параметров это одна из крупнейших моделей, предназначенных для формальной математики и доказательства теорем.
• Точность FP8: DeepSeek-Prover-V2-671B изначально обучена и выпущена в точности FP8 (8-битное число с плавающей запятой) — современный формат, обеспечивающий эффективные вычисления и более быструю работу модели с меньшим расходом памяти, сохраняя при этом высокую производительность.
• Передовые возможности: Модель использует современную архитектуру трансформера и поддерживает современные типы тензоров, такие как BF16, FP8_E4M3 и F32, что делает её подходящей для высокопроизводительных исследований и производственных сред.
• Создана для доказательства теорем: Обученная на массивных высококачественных синтетических данных доказательств, эта модель отлично справляется со сложными математическими рассуждениями и генерацией формальных доказательств Lean 4.

Как получить доступ к DeepSeek-Prover-V2-671B на Novita AI

Начать работу с DeepSeek-Prover-V2-671B на Novita AI быстро, просто и без риска. Благодаря реферальной программе вы получите $10 бесплатных кредитов — этого достаточно, чтобы полностью изучить возможности DeepSeek-Prover-V2-671B, создать прототипы и даже запустить первый проект без каких-либо предварительных затрат.

Используйте Playground (без программирования)

• Мгновенный доступ: Зарегистрируйтесь, получите бесплатные кредиты и начните экспериментировать с DeepSeek-Prover-V2-671B и другими топ-моделями за секунды.
• Интерактивный интерфейс: Тестируйте промпты, цепочки рассуждений и визуализируйте результаты в реальном времени.
• Сравнение моделей: Легко переключайтесь между DeepSeek-Prover-V2-671B, Llama 4, DeepSeek и другими, чтобы найти идеальное решение.

Интеграция через API (для разработчиков)

Бесперебойно подключайте DeepSeek-Prover-V2-671B к своим приложениям, рабочим процессам или чат-ботам с помощью единого REST API от Novita AI — без необходимости управлять весами модели или инфраструктурой. Novita AI предлагает SDK на нескольких языках (Python, Node.js, cURL и другие) и расширенные настройки параметров для продвинутых пользователей.

Вариант 1: Прямая интеграция API (пример на Python)

Для начала просто используйте приведённый фрагмент кода:

from openai import OpenAI

client = OpenAI(
    base_url="https://api.novita.ai/v3/openai",
    api_key="<ВАШ КЛЮЧ API Novita AI>",
)

model = "deepseek/deepseek-prover-v2-671b"
stream = True # или False
max_tokens = 2048
system_content = """Будьте полезным помощником"""
temperature = 1
top_p = 1
min_p = 0
top_k = 50
presence_penalty = 0
frequency_penalty = 0
repetition_penalty = 1
response_format = { "type": "text" }

chat_completion_res = client.chat.completions.create(
    model=model,
    messages=[
        {
            "role": "system",
            "content": system_content,
        },
        {
            "role": "user",
            "content": "Привет!",
        }
    ],
    stream=stream,
    max_tokens=max_tokens,
    temperature=temperature,
    top_p=top_p,
    presence_penalty=presence_penalty,
    frequency_penalty=frequency_penalty,
    response_format=response_format,
    extra_body={
      "top_k": top_k,
      "repetition_penalty": repetition_penalty,
      "min_p": min_p
    }
)

if stream:
    for chunk in chat_completion_res:
        print(chunk.choices[0].delta.content or "", end="")
else:
    print(chat_completion_res.choices[0].message.content)

Ключевые возможности:

• Единая конечная точка:/v3/openai поддерживает формат API Chat Completions от OpenAI.
• Гибкие настройки: Регулируйте temperature, top-p, штрафы и другие параметры для получения точных результатов.
• Стриминг и пакетная обработка: Выберите предпочтительный режим ответа.

Вариант 2: Многоагентные рабочие процессы с SDK OpenAI Agents

Создавайте продвинутые многоагентные системы, интегрируя Novita AI с SDK OpenAI Agents:

• Подключайтесь и работайте: Используйте LLM от Novita AI в любом рабочем процессе OpenAI Agents.
• Поддержка передачи, маршрутизации и использования инструментов: Создавайте агентов, которые могут делегировать задачи, сортировать или выполнять функции, используя модели Novita AI.
• Интеграция с Python: Просто укажите SDK на конечную точку Novita (https://api.novita.ai/v3/openai) и используйте свой ключ API.

Подключите API DeepSeek-Prover-V2-671B на сторонних платформах

• Hugging Face: Используйте DeepSeek-Prover-V2-671B в Spaces, конвейерах или с библиотекой Transformers через конечные точки Novita AI.
• Агентские и оркестрационные фреймворки: Легко подключайте Novita AI к таким платформам, как Continue, AnythingLLM, LangChain, Dify и Langflow через официальные коннекторы и пошаговые руководства по интеграции.
• OpenAI-совместимый API: Наслаждайтесь простой миграцией и интеграцией с такими инструментами, как Cline и Cursor, разработанными для стандарта API OpenAI.

Заключение

DeepSeek-Prover-V2-671B предоставляет автоматическое доказательство теорем мирового класса прямо у вас под рукой — будь вы исследователь, разработчик или преподаватель. Готовы попробовать? Зарегистрируйтесь на Novita AI, получите бесплатные кредиты и испытайте будущее формальной математики и доказательств с помощью ИИ уже сегодня!

О Novita AI

Novita AI — это облачная платформа ИИ, которая предоставляет разработчикам простой способ развёртывания AI-моделей с помощью нашего простого API, а также доступное и надёжное GPU-облако для создания и масштабирования решений.