InvWeaver: нейро-символический фреймворк для синтеза инвариантов в программах с несколькими циклами
Группа исследователей представила InvWeaver — нейро-символический фреймворк для синтеза инвариантов циклов в программах, содержащих несколько взаимодействующих циклов. Работа опубликована на arXiv и посвящена одной из фундаментальных проблем верификации программ — автоматическому построению инвариантов.
В отличие от существующих методов, которые хорошо работают с программами из одного цикла, InvWeaver фокусируется на более сложном случае — нескольких циклах, влияющих друг на друга. Ключевая идея заключается в выявлении межциклических зависимостей и распространении доказательств через комбинацию абстракций на уровне циклов, управляемого обязательствами вывода и уточнения на основе слабейшего предварительного условия.
Для оценки эффективности авторы собрали обширный набор тестов, включая новый датасет на основе классических алгоритмов. Результаты показали, что InvWeaver значительно превосходит существующие методы: фреймворк решил 72 из 82 задач с многопоточными циклами, а также показал высокую производительность на задачах с одним циклом.
InvWeaver сочетает в себе языковые модели (LLM) для генерации гипотез и символьные методы для их проверки и уточнения. Такой подход позволяет автоматизировать процесс, который ранее требовал ручного вмешательства или хорошо зарекомендовал себя только на простых программах.
Разработка может найти применение в верификации программного обеспечения, особенно в критических системах, где корректность кода имеет первостепенное значение. Умение автоматически синтезировать инварианты для сложных алгоритмов сокращает время тестирования и повышает надёжность продукта.
Предложенный датасет также станет бенчмарком для будущих исследований в этой области. Авторы планируют продолжить работу над расширением возможностей InvWeaver и его интеграцией в существующие инструменты верификации.
