Проблема верификации при генерации кода на основе LLM
Большие языковые модели (LLM) демонстрируют высокие результаты в программировании и широко используются в таких инструментах, как Cursor и GitHub Copilot, для повышения производительности разработчиков. Однако из-за их вероятностной природы LLM не могут предоставить формальные гарантии для генерируемого кода. Сгенерированный код часто содержит ошибки, и при использовании генерации кода на основе LLM эти проблемы могут стать препятствием для производительности.
Разработка подходящих бенчмарков для отслеживания прогресса в генерации проверяемого кода важна, но сложна, поскольку включает в себя три взаимосвязанные задачи: генерацию кода, генерацию спецификаций и генерацию доказательств. Существующие бенчмарки не обеспечивают поддержку всех трёх задач, контроля качества, надёжных метрик и модульной структуры.
Недостаточная всесторонняя поддержка верификации в существующих бенчмарках
Такие бенчмарки, как HumanEval и MBPP, добились хорошего прогресса в генерации кода на основе LLM, но не справляются с формальными спецификациями или доказательствами. Многие усилия, направленные на проверку, нацелены только на одну или две задачи и предполагают, что другие элементы будут предоставлены людьми.
DafnyBench и miniCodeProps предназначены для генерации доказательств, в то время как AutoSpec и SpecGen выводят спецификации и доказательства из кода, написанного человеком. Интерактивные системы доказательства теорем, такие как Lean, представляют собой перспективную цель для генерации проверяемого кода с помощью LLM, поскольку они поддерживают построение доказательств с промежуточными шагами. Однако существующие верификационные бенчмарки в Lean, такие как miniCodeProps и FVAPPS, имеют ограничения в охвате задач и контроле качества.
Введение VERINA: целостный бенчмарк для генерации кода, спецификаций и доказательств
Исследователи из Калифорнийского университета и Meta FAIR предложили VERINA (Verifiable Code Generation Arena) — высококачественный бенчмарк для оценки генерации проверяемого кода. Он состоит из 189 задач по программированию с подробными описаниями задач, кодом, спецификациями, доказательствами и наборами тестов, оформленными в Lean.
VERINA построена с учётом контроля качества, проблемы взяты из таких источников, как MBPP, LiveCodeBench и LeetCode, чтобы предложить разные уровни сложности. Все образцы были вручную проверены и доработаны, чтобы обеспечить чёткие описания на естественном языке, точные формальные спецификации и точные реализации кода. Каждый образец содержит наборы тестов для покрытия положительных и отрицательных сценариев, со 100% покрытием кода и прохождением спецификаций на основе достоверных данных.
Структура и состав набора данных VERINA
VERINA состоит из двух подмножеств с разными уровнями сложности: VERINA-BASIC и VERINA-ADV. VERINA-BASIC содержит 108 задач, переведённых из написанного человеком кода Dafny. Это включает 49 задач из MBPP-DFY50 и 59 дополнительных экземпляров из CloverBench, переведённых с помощью OpenAI o3-mini с несколькими примерами, а затем проверенных. VERINA-ADV содержит 81 более сложную задачу по программированию из студенческих работ в рамках курса по доказательству теорем, где студенты брали задачи с таких платформ, как LeetCode и LiveCodeBench, а затем формализовали решения в Lean.
Понимание производительности: оценка LLM на VERINA
Оценка девяти современных LLM на VERINA показывает чёткую иерархию сложности. Генерация кода достигает наивысшего уровня успеха, за ней следует генерация спецификаций, в то время как генерация доказательств остаётся наиболее сложной задачей, с показателями pass@1 ниже 3,6% для всех моделей. VERINA-ADV сложнее по сравнению с VERINA-BASIC во всех трёх задачах, что подчёркивает, что увеличение сложности задачи значительно влияет на производительность генерации проверяемого кода.
Заключение: VERINA устанавливает новый стандарт в оценке проверяемого кода
В заключение исследователи представили VERINA — прорыв в области бенчмаркинга генерации проверяемого кода. Он предлагает 189 тщательно отобранных примеров с подробными описаниями задач, высококачественным кодом, спецификациями в Lean и обширными наборами тестов с полным покрытием строк. Однако набор данных всё ещё относительно невелик для задач тонкой настройки, что требует масштабирования с помощью автоматизированной аннотации с помощью LLM.
VERINA подчёркивает простые, автономные задачи, подходящие для бенчмаркинга, но не полностью отражающие сложные проекты проверки в реальном мире. Метрику генерации спецификаций можно улучшить в будущем, включив более мощные доказывающие системы, в том числе основанные на LLM или SMT-решателях, для обработки сложных отношений непротиворечивости и полноты.