Исследователи представили AxDafny — фреймворк для агентной генерации кода на языке Dafny, который автоматически создает не только исполняемые программы, но и доказательства их корректности. Система использует итеративный процесс исправления ошибок, опираясь на обратную связь от верификатора для уточнения инвариантов, утверждений и аргументов завершимости, что позволяет создавать программное обеспечение с гарантированным отсутствием критических уязвимостей.
Традиционные LLM часто допускают логические ошибки при написании кода, которые сложно обнаружить без глубокого тестирования. AxDafny меняет парадигму, превращая процесс написания кода в цикл взаимодействия между языковой моделью и формальным верификатором. Агент последовательно генерирует код и необходимые для него доказательства, анализирует сообщения об ошибках от компилятора Dafny и автоматически вносит правки до тех пор, пока программа не пройдет полную верификацию.
Для оценки эффективности системы авторы разработали бенчмарк LCB-Pro-Dafny, включающий 250 задач по программированию повышенной сложности. Этот набор данных позволяет измерять способность моделей справляться с задачами, требующими не только синтаксической точности, но и глубокого понимания формальной логики и алгоритмических доказательств, что является важным шагом в сторону создания надежных ИИ-ассистентов для критически важных систем.
Ключевые факты
- AxDafny — фреймворк для итеративной генерации кода и доказательств корректности на языке Dafny.
- Система автоматически исправляет код на основе отчетов верификатора, уточняя инварианты и утверждения.
- Представлен новый бенчмарк LCB-Pro-Dafny, состоящий из 250 задач уровня соревновательного программирования.
- Подход направлен на решение проблемы галлюцинаций в коде через интеграцию формальных методов верификации в агентный цикл.