DeepSeek, китайская лаборатория искусственного интеллекта, тихо обновила Prover — свою ИИ-систему, предназначенную для решения математических доказательств и теорем. Согласно South China Morning Post, DeepSeek загрузила последнюю версию Prover, V2, на платформу для разработки ИИ Hugging Face поздно вечером в среду. Похоже, она построена на основе модели V3 компании, которая имеет 671 миллиард параметров и использует архитектуру смеси экспертов (MoE). Параметры примерно соответствуют способности модели решать задачи, а MoE разбивает задачу на подзадачи и распределяет их между меньшими, специализированными «экспертными» компонентами.
DeepSeek в последний раз обновляла Prover в августе, описывая его тогда как пользовательскую модель для формального доказательства теорем и математических рассуждений. В феврале Reuters сообщал, что DeepSeek, которая недавно выпустила обновленную версию V3 — общей направленности — и, как ожидается, скоро обновит свою модель R1 для «рассуждений», рассматривает возможность привлечения внешнего финансирования впервые.