DeepSeek обновляет свою математическую модель искусственного интеллекта Prover

Китайская лаборатория искусственного интеллекта ^[1] DeepSeek без лишнего шума обновила Prover ^[2] — свою модель искусственного интеллекта, предназначенную для решения математических доказательств и поиска теорем. По данным South China Morning Post ^[3], DeepSeek загрузил последнюю версию Prover, V2, на платформу разработки AI Hugging Face поздно вечером в среду. Похоже, что она построена поверх модели V3 стартапа, которая имеет 671 миллиард параметров и использует архитектуру смешанного эксперта (MoE).

Параметры примерно соответствуют навыкам решения проблем модели, в то время как MoE разбивает задачи на подзадачи и делегирует их более мелким специализированным «экспертным» компонентам. 

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

В феврале агентство Reuters сообщило ^[4], что DeepSeek, как говорят, впервые рассматривает возможность привлечения внешнего финансирования. Недавно компания выпустила обновленную версию V3, модели общего назначения, и, как ожидается, вскоре обновит свою модель «рассуждения» R1.

Источник ^[5]