tgoop.com/machinelearning_ru/2642
Create:
Last Update:
Last Update:
🚀 Новый DeepSeek-Prover-V2: Модель для доказательства теорем yf Lean 4
Lean 4 — это зависимо типизированный функциональный язык программирования и интерактивное средство доказательства теорем .
Результаты:
• Новая Sota( 88,9%) на MiniF2F-test.
• DeepSeek-Prover-V2 смогла доказать 49 теорем из 658.
🔍 Как это работает:
1) Разложение теорем: DeepSeek-V3 по prompt'у разбивает сложные задачи на подцели.
2) Формализация: Пошаговые рассуждения переводятся в доказательства на Lean 4.
3) Cold-start: Полученные цепочки рассуждений и формальные доказательства используются как начальные данные для обучения модели.
• 7 B — базовый вариант.
• 671 B — расширенная версия на базе DeepSeek-V3-Base.
