Diffusion-Proof: формальное доказательство теорем с помощью диффузионных языковых моделей
Diffusion-Proof — первое применение диффузионных языковых моделей к формальной математике: dLLM-Prover-7B (полная генерация доказательств) в связке с dLLM-Corrector-7B (двунаправленная коррекция доказательств через infilling). Система достигает +1,61% на ProofNet-Test и +6,14% на MiniF2F-Test относительно базовых моделей и решает задачу IMO, которую DeepSeek-Prover-V2-7B не смог решить.
Почему это важно
Демонстрирует, что диффузионные LLM способны превосходить авторегрессионные модели в формальном доказательстве теорем, где накопление ошибок на уровне токенов особенно критично.
Важность: 2/5
Сильная исследовательская статья, открывающая новое направление для диффузионных моделей в формальной математике.