Исследователи представили новый подход к автоматической верификации программного обеспечения, использующий LLM-агентов для генерации доказательств в интерактивных системах типа Coq. В отличие от традиционных методов с жестко заданными стратегиями, новая архитектура позволяет моделям динамически адаптировать процесс доказательства, что значительно снижает потребность в ручном труде экспертов и повышает масштабируемость формальной проверки кода.
Формальная верификация традиционно считается «золотым стандартом» надежности ПО, однако её внедрение ограничено высокой стоимостью подготовки доказательств. Существующие автоматизированные системы часто навязывают модели фиксированный алгоритм действий, что приводит к ошибкам при работе со сложными логическими структурами. Предложенный метод переносит фокус на агентную архитектуру, где модель самостоятельно планирует шаги доказательства, опираясь на обратную связь от среды исполнения.
Система демонстрирует способность эффективно взаимодействовать с инструментами доказательства, минимизируя количество итераций, необходимых для успешной верификации. Это открывает путь к интеграции формальных методов в стандартные процессы разработки, делая процесс проверки кода более доступным для широкого круга инженерных задач, требующих повышенной безопасности и корректности алгоритмов.
Ключевые факты
- Метод направлен на автоматизацию работы с интерактивными системами доказательств, такими как Coq.
- Агентная архитектура заменяет жесткие человеческие стратегии динамическим планированием доказательств.
- Подход значительно снижает объем экспертных усилий, необходимых для формальной верификации программ.
- Исследование сфокусировано на решении проблемы масштабируемости формальных методов в современной разработке.