DeepSeek представила DeepSeek-Prover-V2: рекурсивный поиск доказательств и новый бенчмарк

DeepSeek AI выпустила DeepSeek-Prover-V2 — открытую большую языковую модель для формального доказательства теорем в среде Lean 4. Ключевое новшество — рекурсивный пайплайн доказательств, в котором DeepSeek-V3 разбивает сложные теоремы на подцели и формализует их, а модель на 7 миллиардов параметров ищет доказательства для каждой подцели. Полученные корректные доказательства объединяются с цепочкой рассуждений DeepSeek-V3, создавая синтетический набор данных для обучения. Затем модель дообучается на этих данных с подкреплением, где наградой служит бинарная обратная связь «правильно/неправильно». Флагманская версия DeepSeek-Prover-V2-671B с 671 миллиардом параметров достигла 88,9% правильных доказательств на тесте MiniF2F и решила 49 из 658 задач PutnamBench. Также представлен бенчмарк ProverBench, включающий 325 задач — 15 из последних соревнований AIME и 310 из учебников и туториалов. Модель выпущена в двух размерах: 7B и 671B параметров на базе DeepSeek-V3-Base и DeepSeek-Prover-V1.5-Base соответственно; у 7B-версии длина контекста увеличена до 32 тысяч токенов.