Новости Ноябрь 28, 2025
Китайская DeepSeek снова решила пошуметь в мире ИИ. После того как в начале 2025-го компания прославилась одной из первых бесплатных «мыслящих» моделей, теперь она выкатила DeepSeekMath-V2 — версию, которая не охотится за красивым конечным числом, а лезет в святая-святых математики: доказательства теорем.
И да, это уже не про «посчитай мне интеграл», а про строгие, шаг-за-шагом расписанные выводы, которые должны пройти независимую проверку. Тут уже пахнет настоящей математикой, а не дешёвыми лайфхаками.
DeepSeek втиснула в модель цикл «генерация → проверка».
— Сначала обучили верификатор, который умеет проверять доказательства.
— Затем натренировали генератор доказательств, которому этот верификатор служит чем-то вроде строгого научрука.
Генератору приходится самому находить ошибки в своих же доказательствах и чинить их. А когда верификатор сталкивается с особенно сложными случаями, применяется масштабирование проверки — система автоматически размечает новые, тяжёлые примеры, чтобы верификатор рос дальше. Такая матрешка обучения.
DeepSeekMath-V2 не просто «лук, мы сделали модель». Она уже отметилась:
— золото на IMO 2025 и CMO 2024,
— 118/120 на Putnam 2024 (с использованием расширенного вычислительного времени).
Основа — DeepSeek-V3.2-Exp-Base. Модель уже лежит на HuggingFace, а поддержку для инференса можно глянуть в соответствующем репо на GitHub.
Если совсем по-честному — да, никакие задачи тысячелетия она пока не закрыла. Но и никто не ожидал. Важнее то, что такие модели начинают помогать людям лучше понимать математику, а это фундамент для науки, медицины, инженерии — всего, что делает мир чуть более умным.
Компании дальше будут толкать ИИ в сторону глубокого математического понимания. И открытый доступ к таким инструментам отличный ускоритель. Кто знает, может, через пару лет нейросети начнут спорить с профессорами на кафедрах?
Для заинтересованных: у модели есть своя страница на GitHub, PDF с исследованием и готовые файлы на HuggingFace.
