Исследователи представили метод Diffusion-Proof, направленный на преодоление ограничений стандартных авторегрессионных языковых моделей в задачах формальной математики. Традиционные модели, предсказывающие следующий токен, часто сталкиваются с трудностями при построении длинных логических цепочек, необходимых для верификации сложных математических доказательств. Новый подход переносит принципы диффузионных процессов в область формального вывода, позволяя моделям более эффективно исследовать пространство возможных доказательств.
В отличие от классических методов генерации, где модель последовательно выбирает наиболее вероятное продолжение, диффузионный подход позволяет итеративно уточнять структуру доказательства. Это помогает избежать накопления ошибок на ранних этапах рассуждений и повышает точность работы с формальными языками программирования, такими как Lean или Isabelle. Метод обеспечивает более гибкий поиск решений, что критически важно для задач, требующих строгой логической корректности.
Результаты экспериментов показывают, что интеграция диффузионных механизмов позволяет значительно улучшить показатели успешности доказательств по сравнению с моделями, использующими только авторегрессионную архитектуру. Данная разработка открывает новые возможности для автоматизации математических исследований и верификации программного обеспечения, где точность вывода имеет приоритетное значение над скоростью генерации текста.