Ну что, готовы к новому релизу от DeepSeek? На 🤗 только что появились веса DeepSeek Prover V2 671B — новой модели для доказательства теорем и математики. Оригинальный DeepSeek Prover был версией DeepSeek Math 7B, затюненной на доказательство теорем при помощи Lean. В версии 1.5 добавили RL и MCTS. Новая модель идёт в двух размерах — 671B и 7B, причём даже 7B модель бьёт лучшую известную модель — ризонер на основе Qwen 2.5 72B, а ведь Kimina Prover вышла всего пару недель назад. Такие модели нужны потому что, несмотря на гигантские прорывы в ризонинге, современные модели вроде Gemini 2.5 Pro и o3-mini (по o4-mini и o3 результатов пока что нет) всё ещё плохо справляются с формальной математикой. Основная проблема — формализация, general-purpose могут решить задачу, но не могут её формализовать, в отличие от специализированных моделей. Это сильно уменьшает их полезность — проверка правильное ли решение выдала LLM в куче реальных задач сопоставима по сложности с доказательством вручную. Так что специализированные LLM для математики всё ещё имеют смысл. Веса @ai_newz