FVSpec : tests de propriétés du monde réel en tant que défis Lean

Résumé

Nous présentons un benchmark pour évaluer les modèles et agents d'IA sur des tâches réelles de vérification formelle de logiciels. Nous extrayons d'abord 11 039 tests basés sur des propriétés (PBT) issus de dépôts Python réels, puis traduisons automatiquement 2 772 d'entre eux (25 %) en 9 415 spécifications Lean 4 avec des espaces réservés "sorry" (environ 3 formalisations par PBT ; nous conservons plusieurs tentatives lorsqu'aucune ne domine sur les métriques de qualité). Traduire les PBT en spécifications Lean est difficile : cela nécessite de modéliser la sémantique de Python dans Lean, d'inférer la propriété logique encodée dans un PBT impératif, et de gérer les difficultés inhérentes à la programmation typée dépendante dans un langage peu utilisé. Nous décrivons un pipeline LLM à trois agents pour la transpilation des PBT en spécifications Lean, évaluons des métriques de couverture et de qualité, et fournissons des lignes de base pour la génération de preuves utilisant plusieurs approches automatisées et basées sur des modèles. Tout le code (scraper et agents) et les données (PBT et spécifications Lean) sont open source. Notre benchmark vise à stimuler les progrès sur le problème encore peu exploré de la vérification formelle assistée par IA de logiciels réels, un enjeu d'intérêt croissant alors que l'IA produit de plus en plus de code dans le monde.

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.