Resumen Técnico: Agente Event-B

Enunciado del Problema

El desarrollo de software "correcto por construcción" depende de métodos formales, donde el comportamiento del sistema y los requisitos se expresan matemáticamente y se verifican mediante demostración de teoremas y verificación de modelos. Sin embargo, la pronunciada curva de aprendizaje y la demanda de experiencia matemática han obstaculizado la adopción generalizada de estos métodos. Aunque los Modelos de Lenguaje Grande (LLM) han mostrado promesa en la autoformalización, los enfoques existentes se limitan en gran medida a tareas aisladas, como la demostración de teoremas sin formalización o la síntesis de modelos verificada únicamente mediante verificación de modelos acotada.

Crucialmente, los métodos actuales basados en LLM no logran apoyar la evolución iterativa y conjunta de modelos formales y sus pruebas asociadas. En la práctica, el desarrollo formal requiere que, cuando un demostrador de teoremas no pueda descargar una obligación de prueba (PO), el sistema permita revisiones tanto del modelo formal como de sus artefactos de prueba. Las herramientas existentes asumen un modelo fijo y buscan pruebas (asistentes de prueba LLM) o construyen modelos sin una verificación rigurosa basada en pruebas (autoformalización). Existe una falta de marcos que formulen el desarrollo formal como un proceso coordinado sobre un espacio de estados conjunto de modelos y pruebas, permitiendo el refinamiento y la reparación iterativos.

Metodología: Agente Event-B

Para abordar estas lagunas, los autores proponen Agente Event-B, un nuevo marco neurosimbólico para la síntesis y reparación de modelos formales de extremo a extremo. El marco está diseñado para tomar requisitos en lenguaje natural y construir un modelo formal Event-B mediante un proceso iterativo que integra refinamiento, síntesis y reparación.

La metodología consta de tres etapas principales:

1. Planificación de la Estrategia de Refinamiento

Reconociendo que el razonamiento automatizado sobre sistemas complejos es un desafío debido al rápido crecimiento del espacio de búsqueda, el Agente Event-B emplea LLM para planificar una estrategia de refinamiento.

• Descomposición: El agente divide el conjunto de requisitos en lenguaje natural en subconjuntos disjuntos, distribuyéndolos a través de múltiples pasos de refinamiento.
• Invariantes de Unión: Para cada transición entre pasos de refinamiento, el LLM propone "invariantes de unión" (gluing invariants)—predicados que relacionan variables abstractas y concretas para garantizar la consistencia.
• Validación: Estas invariantes se validan mediante verificación de contraejemplos (usando un verificador de modelos) y intentos de prueba antes de ser aceptadas, asegurando que las propiedades probadas en etapas anteriores se preserven.

2. Síntesis del Modelo

Para cada paso de refinamiento, el agente sintetiza un modelo formal basado en los requisitos asignados y las invariantes de unión.

• Generación Guiada por Esquema: Para mitigar los errores de sintaxis comunes en la generación por LLM, el sistema utiliza un esquema JSON que codifica la gramática de Event-B. Esto garantiza la corrección estructural (por ejemplo, eventos obligatorios, declaraciones de variables).
• Bucle de Bienformación: El modelo generado se compila. Cualquier error de compilación (por ejemplo, incompatibilidades de tipo, variables no declaradas) se retroalimenta al LLM para reparación iterativa hasta que el modelo sea sintácticamente válido y correcto en cuanto a tipos.

3. Reparación de Modelo y Prueba

Esta es la contribución central del marco, diseñada para manejar la evolución conjunta de modelos y pruebas.

• Bucle de Verificación: Los modelos sintetizados se verifican primero mediante un verificador de modelos (ProB) para detectar violaciones de invariantes dentro de estados acotados. Si se encuentran contraejemplos, el modelo se repara.
• Demostración de Teoremas: Luego, el modelo se somete a demostración de teoremas no acotada. Si las pruebas fallan, el sistema analiza el estado de la prueba para diagnosticar el problema.
• Recomendación de Reglas de Reparación: El sistema emplea un componente novedoso que mapea los estados de prueba a reglas de reparación específicas (por ejemplo, "Objetivo Contradictorio", "Objetivo Existencial", "Preservación de Invariante Cuantificada"). Estas reglas se derivan empíricamente de experiencias manuales de descarga de pruebas.
• Ejecución de Reparación Atómica: Un LLM de "decisión de estrategia de reparación" selecciona de una biblioteca de funciones de reparación atómicas (por ejemplo, StrengthenGuard, AddInvariant, InstantiateHypothesis) y las ejecuta. Esto restringe las modificaciones del LLM a operaciones sólidas y verificables.
• Solidez: El sistema garantiza la solidez reproduciendo todas las pruebas después de cualquier modificación del modelo. Una reparación solo se acepta si el efecto combinado descarga la PO objetivo, verificado por solucionadores SMT y demostradores de teoremas.

Contribuciones Clave

El artículo describe tres contribuciones principales:

1. Marco: El Agente Event-B es el primer marco de extremo a extremo para la síntesis y reparación de modelos formales que admite el desarrollo basado en refinamiento con construcción coordinada de modelos y derivación de pruebas, encarnando el principio de corrección por construcción.
2. Herramienta: Una herramienta de prueba de concepto integrada en el IDE Rodin (el entorno estándar para Event-B), aprovechando ProB para la verificación de modelos y demostradores estándar de Rodin para la demostración de teoremas.
3. Evaluación: Una evaluación exhaustiva en 27 sistemas formales (desde simples hasta complejos) comparando al Agente Event-B con líneas base, incluidos estudios de ablación y análisis de eficiencia.

Resultados Experimentales

El marco se evaluó en 27 sistemas formales con un promedio de 182.41 obligaciones de prueba por sistema. Los resultados demuestran mejoras sustanciales sobre las líneas base (LLM + demostradores automáticos, Cursor y PAT-Agent):

• Consistencia (Tasa de Descarga de Obligaciones de Prueba - PDR): El Agente Event-B logró un PDR del 97.86%, superando significativamente a las líneas base (89.20% a 95.56%). Mantuvo un PDR superior al 97.0% en todos los niveles de complejidad, mientras que las líneas base mostraron mayor variabilidad y degradación del rendimiento con la complejidad.
• Corrección (Cobertura de Requisitos - RC y Cumplimiento - RF):
  • RC: El Agente Event-B logró 97.13%, superando al segundo mejor método en 4.63%.
  • RF: El Agente Event-B logró 93.79%, superando al segundo mejor en 18.01%.
  • La relación RF/RC (0.97) indica que una vez capturado un requisito, el agente descarga con éxito las pruebas asociadas, a diferencia de las líneas base donde los requisitos capturados a menudo permanecían sin probar.
• Eficiencia: El tiempo promedio para sintetizar y reparar un sistema fue de 74.45 minutos. El tiempo promedio para intentar descargar una sola PO fue de 0.24 minutos, lo que sugiere que la sobrecarga de reparación escala linealmente con el número de POs en lugar de explotar con la complejidad del sistema.
• Estudios de Ablación: Eliminar ya sea la estrategia de refinamiento o el componente de guía de reparación provocó caídas en el rendimiento, confirmando que estos dos componentes se refuerzan mutuamente. El refinamiento reduce la complejidad de las pruebas, mientras que la guía de reparación garantiza la corrección de los pasos de refinamiento.

Significado y Afirmaciones

Los autores afirman que el Agente Event-B representa un paso prometedor hacia el desarrollo formal asistido por LLM, práctico y sólido. Al tratar el desarrollo formal como un espacio de estados conjunto de modelos y pruebas, el marco supera las limitaciones de la autoformalización o la demostración de teoremas aisladas.

El artículo enfatiza que:

• El refinamiento es esencial para gestionar la complejidad, permitiendo al agente descomponer problemas difíciles en pasos manejables mientras preserva la corrección.
• La reparación guiada por pruebas es necesaria porque la verificación de modelos por sí sola (acotada) es insuficiente para la corrección general; se requiere la demostración de teoremas (no acotada), pero esto exige un mecanismo para reparar tanto el modelo como la prueba cuando falla el razonamiento automatizado.
• El enfoque neurosimbólico combina con éxito la flexibilidad semántica de los LLM con la solidez rigurosa de las herramientas de verificación simbólica.

Los autores mantienen una postura modesta respecto al alcance actual, señalando que la biblioteca de reglas de reparación se deriva empíricamente y no es exhaustiva, y que manejar requisitos en lenguaje natural inconsistentes sigue siendo un desafío para trabajos futuros. Sin embargo, los resultados sugieren que el marco propuesto cierra efectivamente la brecha entre los requisitos en lenguaje natural y los modelos formales correctos por construcción.