VERINA: новый стандарт оценки генерации проверяемого кода с помощью LLM и формальных доказательств

Проблема верификации при генерации кода с помощью LLM

Большие языковые модели (LLM), используемые в инструментах вроде Cursor и GitHub Copilot, значительно повышают продуктивность программирования. Однако из-за вероятностной природы этих моделей они не могут гарантировать формальную корректность сгенерированного кода, что приводит к ошибкам и снижает эффективность при использовании LLM для критически важных задач.

Ограничения существующих бенчмарков

Существующие бенчмарки, такие как HumanEval и MBPP, сосредоточены на генерации кода и не охватывают формальные спецификации или доказательства. Многие проекты по верификации затрагивают только отдельные задачи и предполагают, что остальные элементы предоставляются человеком. Например, DafnyBench и miniCodeProps ориентированы на генерацию доказательств, а AutoSpec и SpecGen восстанавливают спецификации и доказательства из кода, написанного человеком. Интерактивные системы теорем, например Lean, предлагают перспективы для генерации проверяемого кода с LLM, поддерживая построение доказательств с промежуточными шагами. Тем не менее, существующие бенчмарки на Lean ограничены по охвату задач и качеству.

Представляем VERINA: комплексный бенчмарк

VERINA (Verifiable Code Generation Arena), созданный исследователями из Университета Калифорнии и Meta FAIR, закрывает эти пробелы, объединяя задачи генерации кода, спецификаций и доказательств. В набор входит 189 программных задач, оформленных в Lean, с подробными описаниями проблем, формальными спецификациями, реализациями кода и тестовыми наборами с полным покрытием строк.

Все задачи вручную проверены и уточнены для ясности и точности, взяты из MBPP, LiveCodeBench, LeetCode и других источников, с разным уровнем сложности. Каждая задача включает тесты для проверки положительных и отрицательных сценариев, что обеспечивает глубокую оценку.

Структура набора данных: VERINA-BASIC и VERINA-ADV

VERINA разделен на два поднабора:

VERINA-BASIC: 108 задач, переведенных из кода на Dafny, включая 49 задач из MBPP-DFY50 и 59 из CloverBench, переведенных с помощью модели OpenAI o3-mini и проверенных вручную.
VERINA-ADV: 81 более сложная задача из курсов по теореме доказательства, где студенты формализовали решения в Lean, взятые с LeetCode и LiveCodeBench.

Набор данных поддерживается строгим контролем качества: подробные описания, полное покрытие кода тестами и 100% успешное прохождение тестов с эталонными спецификациями.

Оценка LLM на VERINA: результаты и вызовы

Анализ девяти современных LLM на VERINA выявил четкую иерархию результатов:

Генерация кода достигает наивысших успехов.
Генерация спецификаций имеет средние показатели.
Генерация доказательств остается самой сложной, с pass@1 ниже 3.6% у всех моделей.

VERINA-ADV сложнее во всех трех задачах. Итеративное улучшение доказательств с помощью модели o4-mini повысило успехи на простых задачах с 7.41% до 22.22% после 64 итераций, но улучшения на сложных задачах ограничены. Наличие эталонных спецификаций значительно улучшает генерацию кода, показывая, что формальные спецификации эффективно направляют синтез.

Перспективы и значение

VERINA задает новый стандарт оценки генерации проверяемого кода, объединяя код, спецификации и доказательства в одном бенчмарке. Несмотря на небольшой размер для дообучения, он служит прочной основой для будущих исследований. Масштабирование с помощью автоматической аннотации, улучшение метрик с использованием более мощных проверов, включая LLM и SMT-солверы, а также решение сложных отношений корректности — перспективные направления для повышения качества генерации спецификаций и надежности верификации.

Для дополнительной информации ознакомьтесь с статьей, карточкой набора данных и страницей GitHub. Следите за проектом в Twitter и присоединяйтесь к сообществам ML для обновлений.