InvBench: Can LLMs Accelerate Program Verification with Invariant Synthesis?

## Контекст Программное тестирование и верификация являются ключевыми задачами в обеспечении надёжности и качества программного обеспечения. Одна из самых сложных задач в этой области — выявление циклических структур («инвариантов»), необходимых для доказательства поведения программы. Исследователи неоднократно сталкивались с проблемой, что автоматические методы выявления инвариантов часто неэффективны или неточны. Для улучшения этих процессов в последние годы набирают популярность глубоко обученные лингвистические модели (LLMs), которые, по мнению авторов, могут ускорить процесс выявления инвариантов. Тем не менее, пока недостаточно широко изучено, насколько эффективны LLMs в этой области и какие модели являются наиболее продвинутыми. ## Метод Для решения проблемы авторов предлагают фреймворк InvBench, который использует технологии глубокого обучения для выявления инвариантов в программах. Фреймворк основывается на свёрточной модели глубокого обучения, которая может работать напрямую с высокоуровневым представлением программ. InvBench включает не только синтез инвариантов, но и проверку их корректности. Для этих целей разработчики использовали стандартную подсистему верификации, чтобы обеспечить формальную гарантию корректности выявленных инвариантов. Таким образом, InvBench не только анализирует, но и оценивает эффективность полученных решений. ## Результаты В ходе экспериментов авторы проверили семь современных LLMs, включая модели Qwen3-Coder-480B и Claude-sonnet-4, в сравнении с традиционным способом UAutomizer. Эксперименты показали, что LLM-based verifiers могут приближаться к эффективности UAutomizer, но пока не могут предложить существенное преимущество. Наиболее заметные различия были замечены в моделях с разным потенциалом, что указывает на важность моделирования. Кроме того, авторы проверили два метода улучшения результатов: supervised fine-tuning и Best-of-N sampling. Например, fine-tuning на 3589 экземплярах повысил процент скоростного ускорения для Qwen3-Coder-480B с 8% до 29.2%, тогда как Best-of-N sampling с N=16 повысило процент успеха Claude-sonnet-4 с 8.8% до 22.1%. ## Значимость Исследование показывает, что InvBench может быть применимо в различных областях, таких как автоматизация программного обеспечения, анализ систем надежности, а также в обучении новых моделей с помощью LLMs. Одним из главных преимуществ является возможность ускорения процесса верификации, что может существенно уменьшить время и стоимость разработки программного обеспечения. Также InvBench открывает пути для дальнейшего исследования методов улучшения текущих моделей и их применения в реальных задачах. ## Выводы InvBench —