FVSpec: Pruebas basadas en propiedades del mundo real como desafíos Lean

Resumen

Presentamos un punto de referencia para evaluar modelos y agentes de IA en tareas reales de verificación formal de software. Primero, extraemos 11,039 pruebas basadas en propiedades (PBT, por sus siglas en inglés) de repositorios reales de Python, y luego traducimos automáticamente 2,772 de ellas (el 25 %) en 9,415 especificaciones de Lean 4 con marcadores de posición *sorry* (aproximadamente 3 formalizaciones por PBT; retenemos múltiples intentos cuando ninguno domina en las métricas de calidad). La traducción de PBT a especificaciones de Lean es un desafío: requiere modelar la semántica de Python en Lean, inferir la propiedad lógica codificada en una PBT imperativa y manejar las dificultades inherentes de la programación con tipos dependientes en un lenguaje poco utilizado. Describimos un canal de LLM de tres agentes para la transpilación de PBT a especificaciones de Lean, evaluamos métricas de cobertura y calidad, y proporcionamos puntos de referencia para la generación de demostraciones mediante varios enfoques automatizados y basados en modelos. Todo el código (raspador y agentes) y los datos (PBT y especificaciones de Lean) son de código abierto. Nuestro punto de referencia tiene como objetivo impulsar el progreso en el problema poco explorado de la verificación formal asistida por IA de software real, un tema de creciente interés a medida que la IA produce cada vez más código en el mundo.

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.