FVSpec: тесты на основе свойств из реального мира как вызовы для Lean

Аннотация

Мы представляем бенчмарк для оценки моделей и агентов ИИ на задачах формальной верификации реального программного обеспечения. Сначала мы извлекаем 11 039 тестов на основе свойств (PBT) из реальных репозиториев Python, затем автоматически переводим 2 772 из них (25%) в 9 415 спецификаций Lean 4 с заглушками sorry (около 3 формализаций на PBT; мы сохраняем несколько попыток, когда ни одна не доминирует по метрикам качества). Перевод PBT в спецификации Lean является сложной задачей: он требует моделирования семантики Python в Lean, вывода логического свойства, закодированного в императивном PBT, и преодоления неотъемлемых трудностей программирования с зависимыми типами в редко используемом языке. Мы описываем конвейер LLM с тремя агентами для транспиляции PBT в спецификации Lean, оцениваем метрики покрытия и качества, а также предоставляем базовые показатели для генерации доказательств с использованием нескольких автоматических и основанных на моделях подходов. Весь код (скрапер и агенты) и данные (PBT и спецификации Lean) являются открытыми. Наш бенчмарк направлен на стимулирование прогресса в малоизученной проблеме формальной верификации реального программного обеспечения с помощью ИИ, что вызывает растущий интерес по мере того, как ИИ производит всё больше кода в мире.

English

We present a benchmark for evaluating AI models and agents on real-world formal software verification tasks. We first scrape 11,039 property-based tests (PBTs) from real-world Python repositories, then automatically translate 2,772 of them (25%) into 9,415 Lean 4 specifications with sorry placeholders (about 3 formalizations/PBT; we retain multiple attempts when none dominates on quality metrics). Translating PBTs into Lean specifications is challenging: it requires modeling Python semantics in Lean, inferring the logical property encoded in an imperative PBT, and handling the inherent difficulties of dependently-typed programming in a seldom-used language. We describe a three-agent LLM pipeline for transpiling PBTs into Lean specifications, evaluate coverage and quality metrics, and provide baselines for proof generation using several automated and model based approaches. All code (scraper and agents) and data (PBTs and Lean specifications) are open source. Our benchmark aims to drive progress on the underexplored problem of AI-assisted formal verification of real-world software, which is of increasing interest as AI produces more and more of the world's code.