Resumen Técnico: FVSpec

Declaración del Problema

El artículo aborda la brecha crítica en la verificación formal (FV) asistida por IA para software del mundo real. Las propuestas de seguridad de la IA dependen cada vez más de agentes autónomos para verificar formalmente el código generado por IA, pero los benchmarks actuales no logran respaldar este objetivo. Los benchmarks existentes (por ejemplo, Minif2f, PutnamBench) se centran en problemas de olimpiadas matemáticas o en código de probadores de teoremas escrito por expertos, lo cual difiere significativamente del panorama "normal" de la ingeniería de software. El software del mundo real involucra árboles de dependencias complejos, APIs externas de caja negra y componentes escritos en diferentes lenguajes, lo que lo hace inherentemente más difícil de verificar que los sistemas monolíticos y cerrados. Además, existe una falta de conjuntos de datos de alta calidad y gran escala derivados de código escrito por ingenieros sin intención de verificación formal, lo cual es necesario para entrenar agentes que puedan operar "fuera de la distribución" (out-of-distribution) con respecto a sus datos de entrenamiento.

Metodología

Los autores introducen FVSpec, un pipeline de generación de benchmarks que transforma Pruebas Basadas en Propiedades (PBTs) del mundo real en desafíos de verificación formal en Lean 4. El proceso consta de tres etapas principales:

1. Recolección de Datos (FVSpec:PBT):

   • El equipo extrajo (scraped) 11,039 PBTs únicos de 333 repositorios de código abierto de Python utilizando el framework Hypothesis.
   • Los repositorios fueron filtrados por licencias permisivas y se eliminaron duplicados (incluyendo forks) para asegurar la diversidad.
   • El corpus resultante representa la ingeniería de software "ordinaria", con pruebas que van desde aserciones triviales hasta pruebas de múltiples estrategias complejas.

2. Transpilación Agéntica (FVSpec:FV):

   • Un pipeline de LLM de tres agentes traduce las PBTs de Python y su código asociado a Lean 4.
   • Descubrimiento de Funciones: Utiliza tree-sitter para extraer la Función Bajo Prueba (FUT) y su clausura transitiva de dependencias locales.
   • Traducción: Un agente de formalización genera dos archivos: Impl.lean (un port computable de la función) y Spec.lean (sentencias de teoremas correspondientes a las aserciones de la PBT, con las pruebas dejadas como marcadores sorry).
   • Reparación Iterativa: El pipeline emplea un bucle de Protocolo de Servidor de Lenguaje (LSP). Si el código Lean generado falla al compilar (vía lake build), los diagnósticos del compilador se retroalimentan al agente para su revisión. Este bucle se ejecuta hasta por 16 iteraciones.
   • Manejo de Efectos: Para el código que involucra efectos secundarios (por ejemplo, Redis, E/S de archivos), el agente axiomatiza estos sistemas externos como interfaces no interpretadas. Los teoremas se formulan sobre estos axiomas, asegurando que la obligación de prueba sea significativa respecto a la lógica del código, incluso si los detalles de implementación concreta se abstraen.

3. Post-producción y Filtrado:

   • Las muestras generadas se someten a una validación rigurosa. Los fallos se categorizan (por ejemplo, tiempos de espera, desajustes de tipos, identificadores desconocidos).
   • Se calcula una puntuación de "fidelidad estructural" basada en cinco sub-métricas: cobertura de parámetros, correspondencia de tipos, cobertura de estrategia, cobertura de aserciones y cobertura de dependencias.
   • Las muestras se gradúan por dificultad (Fácil/Difícil) utilizando un juez de LLM calibrado (claude-haiku-4-5).
   • El conjunto de datos final retiene múltiples formalizaciones por cada PBT si ninguna tentativa única domina en métricas de calidad, resultando en 9,415 desafíos derivados de 2,772 PBTs únicos.

Contribuciones Clave

1. FVSpec:PBT: Un corpus de 11,039 PBTs de Python deduplicados extraídos de repositorios de código abierto, que representa el primer conjunto de datos a gran escala y con licencias limpias de PBTs de desarrollo de software ordinario (excluyendo programación competitiva o código de ITP curado).
2. FVSpec:FV: Un conjunto de datos de 9,415 desafíos de verificación formal en Lean 4. Cada desafío incluye el código Python original, la PBT original, una implementación en Lean y una sentencia de teorema en Lean con obligaciones de prueba. El conjunto de datos presenta una fidelidad estructural mediana de 0.65, con el 62% de los desafíos clasificados como "difíciles".
3. Evaluaciones de Línea Base: Métricas de rendimiento para modelos de frontera (Claude Sonnet 4.6, Claude Opus 4.7 y GPT-5.4). Los modelos alcanzaron una tasa de éxito media del 70% en problemas "fáciles" y del 49% en problemas "difíciles", lo que indica que el benchmark aún no está saturado.
4. Lanzamiento de Código Abierto: El pipeline completo (extractor, extractor de dependencias, agente de formalización y scripts) y los conjuntos de datos se liberan bajo una licencia dual MIT/Apache.

Resultados

• Rendimiento del Pipeline: El pipeline de transpilación convirtió exitosamente el 25% de las 11,039 PBTs iniciales en desafíos válidos de Lean (9,415 muestras).
• Métricas de Calidad: La puntuación de fidelidad estructural mediana es de 0.65. La correspondencia de tipos (1.00) y la cobertura de aserciones (0.97) son altas, mientras que la cobertura de parámetros (0.24) y la cobertura de dependencias (0.48) son más bajas, indicando áreas donde la fidelidad de la traducción varía.
• Rendimiento de los Modelos: Los modelos base resolvieron el 70% de las muestras fáciles y el 49% de las difíciles. Las tasas de rechazo fueron bajas (4–8% para fáciles, 3–25% para difíciles), lo que sugiere que los modelos generalmente intentan las tareas.
• Complejidad: La muestra mediana contiene 6 teoremas. El conjunto de datos incluye una amplia gama de complejidad, desde algoritmos de ordenamiento simples hasta complejos programadores de trabajos de flujo de trabajo que involucran tiempos de espera y transiciones de estado.

Significado y Reivindicaciones

El artículo afirma que FVSpec proporciona una base necesaria para avanzar en la verificación formal asistida por IA de software del mundo real. A diferencia de los benchmarks anteriores que dependen de pruebas escritas por expertos o problemas matemáticos, FVSpec deriva especificaciones de ingenieros que no tenían intención de verificación formal. Esto asegura que los problemas estén "fuera de la distribución" con respecto a los datos de entrenamiento estándar de los modelos, ofreciendo una prueba más rigurosa de la capacidad de un agente para generalizar.

Los autores posicionan este trabajo como un paso hacia una "IA Segura Garantizada" y una "Supervisión Formal Escalable", donde los agentes autónomos deben verificar el software tan rápido y efectivamente como lo escriben. Al proporcionar un benchmark a gran escala y realista, FVSpec pretende impulsar el progreso en el entrenamiento de agentes capaces de manejar las complejidades de los ecosistemas de software modernos, incluyendo dependencias externas y efectos secundarios, que a menudo se ignoran en los benchmarks sintéticos. El artículo reconoce modestamente las limitaciones, como la posibilidad de que la axiomatización pase por alto la semántica específica de los efectos secundarios y la falta de líneas base de expertos humanos para la calibración de la dificultad.