Resumen Técnico: Verificación de Modelos Agénticos

Declaración del Problema

Verificar el código de sistemas generado por Modelos de Lenguaje Grandes (LLM) presenta desafíos únicos que agravan las dificultades existentes en la verificación formal. Aunque los LLM pueden generar cuerpos sustanciales de código para sistemas operativos, compiladores y controladores en lenguajes como C y Rust, los códigos resultantes a menudo carecen de especificaciones formales explícitas. Además, los contratos de seguridad en el código generado por LLM se codifican frecuentemente implícitamente en los sitios de llamada en lugar de hacerse cumplir en los límites de las funciones.

Esta codificación implícita conduce a un modo de fallo específico: las funciones auxiliares (por ejemplo, lectores de indexación por bytes, escritores de aritmética de desplazamiento) a menudo carecen de guardas de límites y desbordamiento, dependiendo de la lógica del llamador circundante para mantener invariantes. En consecuencia, el código funciona correctamente con entradas bien formadas pero falla con entradas adversarias o manipuladas. Las herramientas de verificación tradicionales luchan aquí porque o bien informan en exceso (señalando auxiliares como rotos sin contexto) o informan en defecto (pasando por alto errores porque los llamadores actuales no los activan). Además, los enfoques de verificación basados en LLM existentes a menudo carecen de solidez para la seguridad aritmética y de memoria, mientras que los verificadores deductivos tradicionales luchan con la escala y la naturaleza intensiva en bucles del código de sistemas y carecen de la capacidad de generar contraejemplos concretos.

Metodología: Verificación de Modelos Agénticos

Los autores proponen la Verificación de Modelos Agénticos, un paradigma de verificación que acopla agentes LLM con un backend de verificación de modelos acotados (BMC) bajo el principio: "Los agentes proponen, los solucionadores verifican."

El sistema, instanciado como BMC-Agent, opera a través de un pipeline donde los agentes LLM manejan tareas que requieren juicio semántico, mientras que un backend BMC determinista (CBMC para C, Kani para Rust) descarta todas las decisiones relevantes para la solidez.

Compromisos Arquitectónicos Centrales

1. Inferencia de Especificaciones de Arriba hacia Abajo:

   • Los agentes infieren precondiciones y postcondiciones por función de arriba hacia abajo desde el contexto del llamador.
   • Las especificaciones se generan en un Lenguaje Específico de Dominio (DSL) restringido que se traduce determinísticamente en los primitivos nativos assume/assert del backend.
   • El sistema genera especificaciones de corrección funcional (por ejemplo, expresiones de equivalencia de referencia, identidades algebraicas) además de comprobaciones defensivas de ausencia de pánico, elevando la verificación de la mera evitación de fallos a la fidelidad conductual.

2. Verificación Composicional:

   • La verificación se descompone por función. Cada función se verifica de forma aislada contra su especificación inferida.
   • Las funciones llamadas (callees) se reemplazan por stubs restringidos por sus postcondiciones. Esto implementa una disciplina de asunción-garantía donde la postcondición de un calleo se convierte en la asunción para el llamador.
   • Este enfoque previene la explosión de estado de todo el programa, permitiendo que la verificación escale con el tamaño del espacio de estados de una sola función en lugar de todo el programa.

3. Validación de Contraejemplos Multi-etapa:

   • Los contraejemplos de BMC no se tratan como informes de errores inmediatos. Pasan por un pipeline de validación riguroso para distinguir fallos activos en el árbol de código de fallos latentes o artefactos de modelado:
     • Alcanzabilidad de Entrada: Propagar entradas testigo hacia arriba en el grafo de llamadas para determinar si un llamador puede suministrar los valores.
     • Factibilidad del Calleado: Volver a ejecutar BMC con cuerpos de calleados reales para asegurar que el testigo es alcanzable a través de implementaciones reales.
     • Reproducción Dinámica: Compilar un arnés para ejecutar el testigo en un sistema anfitrión, capturando señales (SIGSEGV, SIGABRT, etc.) para confirmar fallos dinámicos.
     • Auditoría de Realismo: Un agente LLM revisa el contexto completo (especificación, arnés, estado del testigo) para clasificar el hallazgo como realista o poco realista, filtrando artefactos invariantes del marco (por ejemplo, globales no inicializados, estados de hardware imposibles).

4. Bucle de Refinamiento Adaptativo (CEGAR a Nivel de Especificación):

   • Cuando un contraejemplo se clasifica como espurio (por ejemplo, un artefacto de desenrollado de bucles), el sistema no simplemente lo suprime. En su lugar, un LLM propone refinamientos (estrechar precondiciones, fortalecer contratos de calleados o ajustar parámetros del solucionador).
   • Una guardia de solidez asegura que estos refinamientos no enmascaren errores reales.
   • Los refinamientos aceptados se persisten en una base de conocimientos (almacén de especificaciones y biblioteca de patrones) y se propagan a todos los llamadores, extendiendo efectivamente CEGAR desde la abstracción de predicados al nivel de especificación con propagación composicional.

Contribuciones Clave

El documento describe seis contribuciones principales:

1. Paradigma de Verificación de Modelos Agénticos: Un marco donde los agentes LLM gestionan tareas semánticas (inferencia de especificaciones, selección de comprobaciones, clasificación) mientras los backends BMC aseguran la solidez, permitiendo la verificación sin especificaciones de código C y Rust generado por LLM.
2. Capa de Especificación de Arriba hacia Abajo: Un mecanismo para inferir pre/postcondiciones por función y seleccionar comprobaciones aritméticas semánticamente justificadas (por ejemplo, desbordamiento, comprobaciones de puntero) mediante un DSL que se traduce a CBMC/Kani.
3. Arquitectura de Verificación Composicional: Un enfoque escalable que verifica funciones de forma aislada bajo contratos de asunción-garantía, paralelizando a través de capas del grafo de llamadas.
4. Pipeline de Validación: Un proceso de cuatro etapas (alcanzabilidad, factibilidad, reproducción dinámica, auditoría de realismo) que categoriza los hallazgos en niveles de evidencia (por ejemplo, "confirmado dinámico", "confirmado entrada al sistema").
5. Bucle de Refinamiento Multi-nivel: Un sistema que eleva CEGAR al nivel de especificación, utilizando contraejemplos espurios para impulsar refinamientos composicionales que persisten entre ejecuciones.
6. Implementación y Evaluación de BMC-Agent: Una herramienta funcional evaluada en diversos corpus, demostrando la capacidad de confirmar defectos reales, producir verificaciones limpias acotadas en bibliotecas sometidas a fuzzing y probar la equivalencia funcional.

Resultados de la Evaluación

Los autores evaluaron BMC-Agent en cuatro corpus que abarcan C y Rust:

• VibeOS (C): Un kernel ARM64 generado por LLM de 15.000 líneas. BMC-Agent confirmó 34 errores realistas en 12 módulos. De estos, 16 se reprodujeron dinámicamente (SIGSEGV/SIGABRT), 14 se confirmaron como puntos de entrada al sistema y 4 fueron violaciones de modelos formales.
• Bibliotecas OSS Maduras (C): Evaluado en jq, OpenSSL, libcurl, libxml2 y protobuf upb. La herramienta reveló 2 defectos de comportamiento indefinido en jq (presentados como GHSA) y produjo verificaciones limpias acotadas en superficies de analizadores sintácticos sometidas intensamente a fuzzing (por ejemplo, 15/24 funciones hoja en ASN.1 de OpenSSL verificadas limpias).
• Controlador Realtek r8125 (C): Se encontró un bypass de comprobación de límites MMIO protegido por CAP_NET_ADMIN en el ioctl de la herramienta rtl8125, activado al habilitar comprobaciones de desbordamiento específicas mediante el selector de bandera.
• claudes-c-compiler (Rust): Un compilador C generado por LLM de 50.000 líneas. BMC-Agent confirmó 25 errores reales, principalmente defectos de clase pánico en auxiliares de bytes de API pública (fuera de límites de slice, desbordamientos de enteros) y una violación de corrección funcional. También estableció equivalencia funcional acotada para auxiliares de hash ELF y escritura de encabezados.

Observaciones Clave de los Resultados:

• La precisión de la herramienta se atribuye a los detectores de etapa de realismo (filtrando artefactos del marco), la selección de banderas por función (habilitando comprobaciones desactivadas por defecto en configuraciones estándar) y el bucle de retroalimentación (convirtiendo patrones recurrentes en invariantes permanentes).
• En el caso del compilador Rust, los errores siguieron un anti-patrón específico: el LLM escribió funciones auxiliares sin comprobaciones de límites, confiando en que los llamadores mantuvieran invariantes. Esto resultó en código que funcionaba con entradas bien formadas pero fallaba con entradas adversarias, un perfil distinto de los errores de lógica de compilador típicamente escritos por humanos.

Significado y Afirmaciones

El documento afirma que la Verificación de Modelos Agénticos aborda la "brecha de especificación" en el código de sistemas generado por LLM automatizando la inferencia de contratos y acoplando estos con verificación de modelos acotada y sólida.

• Solidez vs. Escalabilidad: Al delegar la solidez a BMC y utilizar agentes para el juicio semántico, el enfoque evita la falta de solidez del razonamiento puro de LLM mientras supera los límites de escalabilidad de la verificación de todo el programa.
• Verificación Accionable: El pipeline de validación multi-etapa asegura que los errores reportados no sean solo contraejemplos teóricos, sino que se clasifiquen por su alcanzabilidad e impacto dinámico, distinguiendo entre fallos activos y tareas de endurecimiento latentes.
• Propagación Composicional: La capacidad del sistema para refinar especificaciones y propagarlas a través del grafo de llamadas le permite aprender de contraejemplos espurios, mejorando la calidad de la verificación con el tiempo sin intervención manual.

Los autores permanecen modestos respecto al trabajo futuro, señalando que la evaluación cuantitativa amplia (precisión/recordación a escala), un análisis más profundo de las suposiciones de corrección de especificaciones y la reducción de costos mediante la optimización de tokens son los siguientes pasos necesarios. Enfatizan que los resultados actuales demuestran la capacidad del pipeline para confirmar defectos y verificar superficies limpias, pero no afirman haber resuelto el problema general de verificar todo el código generado por LLM sin limitaciones.