Resumen Técnico: TLA+-Bench

Planteamiento del Problema

El campo de la generación de especificaciones formales a partir de lenguaje natural enfrenta una brecha de medición crítica. Aunque los modelos de lenguaje de gran escala (LLMs) son cada vez más tasked para generar especificaciones de TLA+ a partir de descripciones en lenguaje natural, el progreso es difícil de cuantificar con precisión. Los recursos existentes suelen calificar los resultados basándose en la semejanza textual con una referencia o en el éxito simple del análisis sintáctico (parsing). Estos métodos no loginan verificar la corrección, sobreestimando a menudo la capacidad del modelo. A diferencia de la generación de código general donde las pruebas son aproximadas, TLA+ cuenta con un oráculo decidible (el verificador de modelos TLC) que puede determinar la satisfacción de propiedades sobre todo el espacio de estados alcanzables. Sin embargo, los conjuntos de datos previos no han aprovechado este oráculo exacto a escala, ni han proporcionado los metadatos necesarios para controlar las variaciones de entrada o los niveles de dificultad.

Metodología

Construcción del Conjunto de Datos (TLA+-Bench)

Los autores construyeron un conjunto de datos y un benchmark que comprende 1,300 especificaciones extraídas de 13 repositorios públicos. El conjunto de datos está estratificado en dos niveles:

• Nivel Gold (403 especificaciones): Contiene módulos TLA+ emparejados con configuraciones de verificación de modelos ejecutables. Estos son verificados por el verificador de modelos TLC para asegurar que satisfacen las propiedades declaradas sobre el espacio de estados completo y alcanzable.
• Nivel Silver (897 especificaciones): Contiene módulos que se analizan sintácticamente con éxito pero carecen de configuraciones ejecutables, lo que permite estudios de tasa de parseo a gran escala.

Metadatos y Aumentación:
Cada especificación está aumentada con:

• Cuatro Descripciones en Lenguaje Natural: Generadas por dos proveedores (GPT-5 y Claude Opus 4.5) en dos estilos distintos:
  • Declarativo: Revela los nombres reales del módulo (probando la recuperación de la interfaz).
  • Intención (Intent): Oculta los nombres, indicando únicamente los requisitos del sistema (probando el diseño desde cero).
• Etiquetas: Etiquetas de dificultad (Básico, Intermedio, Avanzado) y etiquetas de categoría (Sistema vs. Utilidad).
• Identificación de Fixtures Triviales: Las especificaciones válidas que solo tienen un estado alcanzable (que pasan trivialmente) son identificadas y excluidas del conjunto de evaluación principal para evitar puntuaciones infladas.

Protocolo de Evaluación

El benchmark evalúa los modelos utilizando un enfoque basado en la ejecución en lugar de la superposición textual:

1. Puerta de Validez: La especificación generada debe analizarse sintácticamente bajo el parser SANY.
2. Puerta Semántica: La especificación se ejecuta contra la configuración de referencia usando el verificador de modelos TLC. TLC explora todo el espacio de estados alcanzables para decidir si las propiedades nombradas son violadas.
3. Definición de Corrección: Una especificación es "correcta" solo si pasa ambas puertas.

El Sobre de Corrección (Correctness Envelope):
El artículo introduce el concepto de un "sobre de corrección" para demostrar que un único número de corrección es insuficiente. Los autores miden la corrección bajo cuatro regímenes distintos sobre el mismo conjunto de salidas:

• Consciente de la Configuración (Configuration-Aware): El modelo recibe los nombres de la interfaz (constantes/propiedades) en el prompt.
• Por Defecto (Default): El modelo debe recuperar los nombres de la interfaz por sí solo.
• Sustantivo (Substantive): Los aciertos deben ejercer un comportamiento real (multi-estado) y verificar propiedades no tautológicas.
• Supervivencia a Mutaciones (Mutation-Surviving): La propiedad verificada debe ser "de carga" (verificado mediante pruebas de mutación donde la propiedad se reemplaza con TRUE).

Resultados Clave

1. El Sobre de Corrección

La elección del régimen de calificación altera drásticamente el rendimiento reportado. Sobre el mismo conjunto de salidas de modelos de frontera:

• Tasa Consciente de la Configuración: 18.7% (Modelo con nombres de interfaz proporcionados).
• Tasa por Defecto: 10.0% (Modelo recupera nombres de interfaz).
• Tasa Sustantiva: 4.0% (Los aciertos deben ejercer comportamiento).
• Tasa de Supervivencia a Mutaciones: 1.7% (Las propiedades deben verificar aspectos no triviales).

Esto representa una diferencia de once veces (18.7% a 1.7%) basada únicamente en las elecciones de calificación, resaltando que los benchmarks previos que reportan un solo número seleccionan silenciosamente uno de estos regímenes.

2. Validez vs. Corrección

Existe una brecha significativa entre la validez sintáctica y la corrección semántica.

• Modelos de Frontera: Las tasas de parseo oscilan entre el 63% y el 89%, pero las tasas de corrección (bajo el régimen por defecto) oscilan entre el 4% y el 16%.
• Modelos Abiertos: Las tasas de parseo son significativamente menores (7% a 29%), con tasas de corrección del 0% al 1%.
• Conclusión: Los modelos escriben TLA+ válido con mucha más frecuencia de la que escriben TLA+ correcto. Un benchmark que se detuviera en el parseo clasificaría falsamente a estos modelos como capaces.

3. Dificultad y Modos de Fallo

• Abismo de Dificultad: La corrección cae abruptamente a medida que aumenta la dificultad del problema. Para los modelos de frontera, la tasa de corrección cae del 25% en especificaciones básicas al 2% en especificaciones intermedias y avanzadas.
• Taxonomía de Fallos: El modo de fallo dominante es la Vinculación de Configuración (nombres discordantes entre el módulo generado y la configuración de referencia), que representa hasta el 74% de los fallos para algunos modelos. Otros fallos incluyen errores de parseo, violaciones de seguridad y violaciones de liveness.
• Consistencia de Fallos: Los modelos suelen fallar en las mismas categorías en las mismas especificaciones, lo que sugiere que la dificultad reside tanto en la estructura de la tarea como en la capacidad del modelo.

Significación y Reivindicaciones

El artículo afirma que TLA+-Bench proporciona el primer benchmark basado en la ejecución para la generación de TLA+ a partir de lenguaje natural que utiliza un oráculo exacto. Su contribución principal no es solo el conjunto de datos, sino la visión metodológica de que un oráculo exacto no produce un único número de corrección.

En su lugar, la corrección es un rango (el "sobre de corrección") dependiente de:

1. Si se le indica al modelo los nombres de la interfaz.
2. Si el acierto ejercita un comportamiento real.
3. Si la propiedad verificada es de carga.

Los autores sostienen que los benchmarks previos han inflado la capacidad aparente al utilizar oráculos débiles (por ejemplo, el parseo o conjuntos de pruebas finitos) o al realizar elecciones de calificación implícitas. Al hacer estas elecciones explícitas y medir sus límites, TLA+-Bench permite a los investigadores:

• Medir la brecha real entre la generación válida y la correcta.
• Estudiar modos de fallo específicos (por ejemplo, recuperación de interfaz vs. lógica de modelado).
• Estratificar los resultados por dificultad para entender dónde fallan los modelos.

El artículo concluye que, si bien los modelos muestran promesa en la generación de TLA+ sintácticamente válido, actualmente luchan significativamente con la generación de especificaciones semánticamente correctas, particularmente a medida que la complejidad del problema aumenta o cuando se requiere la recuperación de la interfaz. El lanzamiento incluye las especificaciones, las descripciones, las salidas de los modelos y las herramientas de calificación para permitir una investigación reproducible y extendida.