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