Resumen Técnico: Síntesis de Diseño de Conceptos Dirigida por LLM Verificada

Planteamiento del Problema

Los sistemas de software modernos se ensamblan cada vez más mediante la composición de unidades de comportamiento reutilizables (por ejemplo, autenticación, etiquetado, control de acceso). Si bien definir el comportamiento de las unidades individuales suele ser sencillo, especificar la lógica de coordinación que garantiza que estas unidades interactúen de forma segura es difícil. La metodología de Diseño de Conceptos [Jac21] aborda esto organizando las aplicaciones alrededor de "conceptos" (unidades de funcionalidad autónomas y orientadas al usuario) conectados por "reacciones" (reglas de sincronización).

Sin embargo, el Diseño de Conceptos carece actualmente de una semántica formal para las reacciones. Esta ausencia dificulta:

1. Definir con precisión qué significa un diseño.
2. Verificar automáticamente que un diseño preserva los invariantes de seguridad (por ejemplo, "los datos sensibles no deben permanecer en una cola de mensajes fallidos").
3. Sintetizar automáticamente la lógica de coordinación segura.

Además, incluso si un diseño satisface un invariante de seguridad, puede no coincidir con la intención del usuario. Muchos diseños de reacción distintos pueden satisfacer el mismo invariante, incluyendo algunos implausibles (por ejemplo, desclasificar datos sensibles para satisfacer un invariante en lugar de mover los datos). El artículo identifica la necesidad de un mecanismo para orientar la síntesis hacia el diseño pretendido por el usuario sin requerir que este formalice completamente su intención mediante complejas restricciones lógicas.

Metodología

El artículo presenta foundry, una herramienta prototipo que implementa un bucle de Síntesis Inductiva Guiada por Contraejemplos (CEGIS) impulsado por Modelos de Lenguaje de Gran Escala (LLMs). La metodología consta de tres componentes principales:

1. Semántica Formal

Los autores definen una semántica basada en autómatas para conceptos y reacciones:

• Conceptos: Se modelan como semiautómatas parciales inicializados (máquinas de estado deterministas con entradas pero sin salidas).
• Reacciones: Se modelan como un semiautómata monitor parcial que observa el autómata del concepto compuesto. Las reacciones se activan basadas en disparadores (when), condiciones de estado (where) y efectos (then).
• Composición: La aplicación es una composición sincrónica de los autómatas de los conceptos y el monitor de la reacción.
• Objetivo de Verificación: La seguridad se verifica comprobando que la aplicación está "asentada" (sin obligaciones pendientes) exactamente cuando se cumple el invariante de seguridad. Esto se codifica en Alloy 6 y se comprueba mediante verificación de modelos acotada.

2. Bucle de Síntesis Dirigido por LLM

El proceso de síntesis opera de la siguiente manera:

1. Propuesta: Un LLM propone reacciones candidatas (o revisa las existentes) para satisfacer un invariante dado.
2. Traducción: Un segundo agente traduce las descripciones de los conceptos, las reacciones y los invariantes (actualmente escritos en lenguaje natural) a Alloy 6.
3. Verificación: El verificador de modelos de Alloy comprueba el diseño candidato contra el invariante y cualquier escenario proporcionado.
4. Retroalimentación: Si la verificación falla, el contraejemplo (un rastro que viola el invariante o el escenario) se entrega de vuelta al LLM para refinar el diseño.

3. Mecanismos de Orientación

Para abordar la naturaleza "subespecificada" de la síntesis basada solo en invariantes, el artículo propone dos mecanismos de orientación:

• Prompts de Lenguaje Natural: Proporcionar descripciones textuales del comportamiento pretendido junto con el invariante.
• Síntesis Guiada por Escenarios: Proporcionar escenarios positivos (permitidos) y negativos (prohibidos). A diferencia de los prompts, los escenarios tienen una semántica formal y pueden verificarse automáticamente contra los diseños candidatos.
• Elicitación de Escenarios: Un procedimiento dirigido por LLM donde el modelo propone prefijos de acción cortos que violan el invariante y el usuario los clasifica como deseables o indeseables. El modelo luego propone reparaciones (sufijos) para los prefijos deseables. Esto desplaza la tarea del usuario de la autoría de escenarios a la clasificación de los mismos.

Contribuciones Clave

1. Semántica Formal: Una semántica basada en autómatas para los conceptos y reacciones del Diseño de Conceptos, permitiendo la verificación acotada de invariantes y escenarios.
2. Bucle de Síntesis Verificado: Un procedimiento de síntesis dirigido por LLM, de tipo CEGIS, para generar diseños de reacción, integrado con un mecanismo guiado por escenarios para orientar la síntesis hacia los diseños pretendidos.
3. Elicitación de Escenarios: Una técnica dirigida por LLM para apoyar la exploración temprana del diseño, permitiendo que los usuarios clasifiquen los escenarios propuestos que violan el invariante en lugar de autorizarlos desde cero.
4. Evaluación Empírica: Una evaluación exhaustiva en tres aplicaciones (Cola de Mensajes Fallidos con datos sensibles, Sistema de Gestión de Cursos, Enlaces de Evidencia de un Solo Uso) y doce variantes de diseño utilizando el LLM GPT-5.5.

Resultados

La evaluación, realizada sobre un banco de pruebas de 12 variantes de diseño, arrojó los siguientes hallazgos:

• Síntesis de Solo Invariante:

  • Los LLMs suelen alcanzar un diseño verificado rápidamente (a menudo al primer intento).
  • Sin embargo, los diseños rara vez son estables entre ejecuciones.
  • La síntesis de solo invariante produce frecuentemente diseños implausibles (por ejemplo, prohibir acciones válidas o desclasificar datos) porque los invariantes por sí solos subespecifican el espacio de diseño.

• Guía de Escenario vs. Prompt:

  • La síntesis guiada por escenarios recuperó los diseños pretendidos de forma más consistente que el prompting de lenguaje natural (10/12 variantes frente a 8/12 variantes con entradas iniciales).
  • Los escenarios son más fáciles de revisar mecánicamente (puramente aditivos) en comparación con los prompts, que pueden ser frágiles y ambiguos.
  • Sobreajuste (Overfitting): Los conjuntos mínimos de escenarios pueden conducir al sobreajuste, donde el modelo falla en generalizar (por ejemplo, manejando solo cardinalidades específicas de mensajes). Añadir escenarios con cardinalidades variadas mitigó este problema.

• Elicitación de Escenarios:

  • La elicitación de 20 escenarios recuperó el diseño pretendido en 9/12 variantes, comparado con 5/12 con 10 escenarios.
  • No determinismo: La propuesta de escenarios por parte del LLM es no determinista; diferentes ejecuciones elicitan diferentes conjuntos de escenarios, lo que conduce a resultados no monotónicos (más escenarios no siempre garantizan una mejor cobertura).
  • Comportamientos Omitidos: Si el proceso de elicitación omite un escenario crítico (por ejemplo, una ruta de inscripción específica), la síntesis puede converger a un diseño que prohíbe ese comportamiento, el cual no era la intención.

• Modos de Fallo:

  • Los principales modos de fallo fueron la omisión de escenarios críticos (falta de cobertura) y el sobreajuste (fallo de generalización).
  • Los problemas de calidad incluyeron reacciones y condiciones redundantes, aunque esto no afectó la corrección respecto al invariante.

Significación y Reivindicaciones

El artículo sostiene que la verificación formal es esencial cuando se utilizan LLMs para la síntesis de diseño de alto nivel. Aunque los LLMs pueden generar diseños que satisfacen invariantes simples, no se puede confiar en ellos para producir el diseño pretendido sin la orientación adicional.

La importancia del trabajo radica en demostrar que los escenarios sirven como artefactos de orientación efectivos y verificables. Estos cierran la brecha entre los requisitos de seguridad formales (invariantes) y la intención informal del usuario. El artículo argumenta que mientras los invariantes aseguran la seguridad, los escenarios aseguran la plausibilidad y la alineación con la intención.

Los autores mantienen la modestia sobre el estado actual del prototipo:

• La traducción de lenguaje natural a Alloy depende de un LLM, lo que introduce una fuente potencial de error (aunque la inspección manual no encontró problemas en los diseños verificados finales).
• La verificación es acotada; la ausencia de contraejemplos no garantiza la corrección ilimitada.
• La evaluación se limita a una configuración de LLM (GPT-5.5) y un conjunto específico de benchmarks, aunque una verificación cruzada con Claude Fable 5 mostró un éxito similar, lo que sugiere que el enfoque no es específico de un modelo.
• Se requiere trabajo futuro para reemplazar la traducción basada en LLM con un lenguaje fuente formal, escalar la verificación a aplicaciones más grandes y mejorar la elicitación de escenarios para manejar el no determinismo y las brechas de cobertura de forma más robusta.