🔥 А вот и новый DeepSeek Prover v2

🚀 Новый 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.