Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction

## КОНТЕКСТ И ПРОБЛЕМАТИКА Автоматическое доказательство теорем является одним из ключевых направлений в области искусственного интеллекта и вычислительной логики. Эта область направлена на создание алгоритмов и моделей, способных автоматически доказывать математические утверждения, что может значительно ускорить процесс научных открытий и верификацию сложных систем. Однако, существующие методы зачастую сталкиваются с ограничениями в масштабируемости и сложности решаемых задач. Многие из них либо требуют значительных вычислительных ресурсов, либо не способны эффективно справляться с задачами повышенной сложности. Это создает необходимость в разработке новых подходов, которые могли бы обеспечить как высокую производительность, так и доступность для более широкого круга пользователей. Мотивация для создания Goedel-Prover-V2 заключается в преодолении этих ограничений через использование современных языковых моделей и инновационных методологий, таких как синтез данных и самокоррекция, которые позволяют улучшить обучение моделей и их способность решать сложные задачи. ## ПРЕДЛОЖЕННЫЙ МЕТОД Goedel-Prover-V2 представляет собой серию языковых моделей, разработанных для автоматического доказательства теорем. Основой предложенного метода является стандартный процесс итерации экспертов и обучения с подкреплением, в который интегрированы три ключевых инновации. Во-первых, это структурированный синтез данных, который позволяет генерировать синтетические задания с возрастающей сложностью. Это обучает модель постепенно осваивать все более сложные теоремы. Во-вторых, метод самокоррекции, управляемый верификатором, позволяет модели итеративно исправлять свои доказательства, используя обратную связь от компилятора Lean. В-третьих, усреднение моделей, которое объединяет контрольные точки модели, чтобы уменьшить снижение разнообразия выходных данных модели на поздних стадиях обучения. Эти инновации позволяют Goedel-Prover-V2 добиваться высоких результатов в доказательстве теорем, обеспечивая при этом эффективность и устойчивость модели. ## ЭКСПЕРИМЕНТАЛЬНЫЕ РЕЗУЛЬТАТЫ Для оценки эффективности Goedel-Prover-V2 были проведены эксперименты с использованием нескольких тестовых наборов данных. Малая модель Goedel-Prover-V2-8B достигла 84.6% по метрике pass@32 на наборе данных MiniF2F, превосходя DeepSeek-Prover-V2-671B, несмотря на то, что она в 80 раз меньше. Флагманская модель Goedel-Prover-V2-32B достигла 88.1% на MiniF2F при стандартном режиме и 90.4% в режиме самокоррекции, значительно превосходя предыдущее состояние искусства. Более того, она успешно решила 86 задач на PutnamBench при pass@184, заняв первое место среди открытых моделей, обогнав DeepSeek-Prover-V2-671B, который решил 47 задач при pass@1024. Эти результаты демонстрируют, что предложенная методология позволяет достигать высоких показателей производительности при меньших вычислительных затратах и размерах модели. ## ПРАКТИЧЕСКАЯ ЗНАЧИМОСТЬ Goedel-Prover-V2 имеет широкий спектр потенциальных применений в различных областях, включая математику, компьютерные науки и инженерные дисциплины, где требуется автоматизация верификации и доказательства теорем. Одним из ключевых преимуществ является возможность использования более компактных и эффективных моделей, что расширяет доступность технологии для исследовательских групп с ограниченными ресурсами. Кроме того, инновации, заложенные в методологию Goedel-Prover-V2, могут быть адаптированы и для других задач, требующих автоматического синтеза и проверки сложных структур. Переход на модели открытого исходного кода также способствует более широкому распространению и адаптации технологии в научном сообществе, что может ускорить прогресс в области автоматического доказательства теорем. ## ВЫВОДЫ И ПЕРСПЕКТИВЫ Разработка Goedel-Prover-V2 представляет собой значительный шаг вперед в области автоматического доказательства теорем. Основные достижения включают в себя создание компактных и эффективных моделей, превосходящих существующие аналоги, а также внедрение инновационных методологий, таких как структурированный синтез данных и самокоррекция. В будущем исследования могут быть направлены на дальнейшее улучшение способности моделей решать задачи повышенной сложности, а также на расширение возможностей применения данных методов в других областях науки и техники. Важно продолжать развивать открытые платформы и инструменты, которые могут способствовать более быстрому и широкому распространению передовых технологий в научных кругах.