Resumen Técnico: TLA-Prover

Planteamiento del Problema

TLA+ es un lenguaje de especificación formal utilizado para la verificación de sistemas distribuidos y protocolos de seguridad crítica, junto con el verificador de modelos TLC para la exploración exhaustiva del espacio de estados. Aunque los Modelos de Lenguaje de Gran Escala (LLM) muestran potencial en la generación de código, tienen dificultades significativas con TLA+ debido a la representación dispersa del lenguaje en los corpus de preentrenamiento y su sintaxis idiosincrásica (por ejemplo, operadores temporales, comprensiones de conjuntos).

Los baselines existentes, como el estudio FormaLLM, indican que los LLM de pesos abiertos sin ajustar logran solo una tasa de éxito del 8.6% al pasar el verificador de modelos TLC en 25 modelos. Un desafío crítico en el entrenamiento de LLM para la verificación formal es el reward hacking (hackeo de recompensa). En el contexto de TLA+ y TLC, un modelo puede optimizar la señal binaria de "paso" generando invariantes triviales o tautológicos (por ejemplo, TypeOK == TRUE). Estas especificaciones pasan TLC en cada estado alcanzable, pero no transmiten propiedades significativas sobre el protocolo, lo que vuelve inútible la verificación. Los enfoques estándar de aprendizaje por refuerzo que dependen únicamente de la señal de paso/fallo de TLC son vulnerables a este modo de fallo.

Metodología

Los autores presentan TLA-Prover, un modelo de 20 mil millones de parámetros (basado en gpt-oss-20b) diseñado para la síntesis de especificaciones TLA+. El enfoque combina el Ajuste Fino Supervisado (SFT) con un novedoso pipeline de entrenamiento que integra la Optimización de Política de Grupo Relativa (GRPO) basada en reparación y una jerarquía de validación de cuatro niveles.

1. Jerarquía de Validación de Cuatro Niveles

Para prevenir el reward hacking y asegurar la validez semántica, cada salida del modelo es calificada por un pipeline determinista externo en uno de cuatro niveles:

• Bronze (Bronce): La salida falla el parser SANY (sintácticamente inválida).
• Silver (Plata): La salida se analiza pero falla al cargar o ejecutar en TLC (por ejemplo, tiempos de espera, errores de tipo).
• Gold (Oro): La salida pasa tanto SANY como TLC; el verificador de modelos agota el espacio de estados y todos los invariantes se cumplen.
• Diamond (Diamante): La salida pasa el nivel Gold y el invariante es sensible a la mutación.
  • Mecanismo: Se aplica una mutación automatizada a nivel de AST al predicado del invariante (por ejemplo, negar un conyunto, cambiar operadores relacionales o intercambiar constantes). La especificación mutada se ejecuta nuevamente a través de TLC.
  • Criterio: Si la mutación causa que TLC encuentre un contraejemplo, el invariante original se considera no trivial (Diamond). Si TLC todavía pasa (por ejemplo, porque el invariante era TRUE), la salida falla la verificación Diamond. Este paso bloquea explícitamente los invariantes tautológicos.

2. Pipeline de Entrenamiento

El proceso de entrenamiento consta de dos etapas principales, con un estudio de ablación DPO para comparación:

• Etapa 1: Ajuste Fino Supervisado (SFT)

  • Corpus: Un conjunto de datos curado de 1,053 especificaciones, filtradas estrictamente al nivel Diamond. Los datos provienen de la distribución de la TLA+ Foundation y el repositorio tlaplus/examples, aumentados por un generador Ollama y filtrados por un juez LLM y el pipeline de cuatro niveles.
  • Arquitectura: Se aplica un adaptador LoRA (rank 8, alpha 16) a las proyecciones de atención del modelo base de 20B parámetros.
  • Objetivo: Enseñar al modelo el vocabulario estructural y la sintaxis de TLA+.

• Etapa 2: Optimización de Política de Grupo Relativa (GRPO) Basada en Reparación

  • Motivación: El GRPO estándar falla cuando todas las muestras de un grupo fallan ante el verificador (recompensas dispersas), lo que resulta en una ventaja de cero y sin flujo de gradiente.
  • Mecanismo: El modelo se le presenta una especificación "rota" (cosechada de intentos fallidos previos) y se le asigna la tarea de repararla.
  • Señal de Recompensa: Una puntuación de mejora continua basada en las transiciones de nivel (Bronze→Silver: 0.1, Silver→Gold: 0.3, Gold→Diamond: 0.6). Esto proporciona gradientes densos incluso cuando la salida final no es perfecta, siempre que el nivel mejore.
  • Proceso: El modelo repara iterativamente sus propias salidas utilizando los mensajes de error de TLC como retroalimentación.

• Estudio de Ablación (DPO): Una variante de Optimización de Preferencia Directa (DPO) fue entrenada desde el mismo checkpoint de SFT utilizando pares de preferencia estáticos (Diamond > Gold > Silver > Bronze). Esto sirvió como baseline para comparar contra el enfoque dinámico de GRPO basado en reparación.

Resultados Clave

El modelo fue evaluado en un benchmark de 30 problemas mediante decodificación codiciosa (greedy decoding) de un solo paso.

• Rendimiento: TLA-Prover (checkpoint final de reparación-GRPO) logró una tasa de paso del 30% (9/30) tanto en los niveles Gold como Diamond.
• Comparación con Baseline: Esto representa una mejora de 3.5x respecto al baseline de FormaLLM sin ajustar del 8.6%.
• Comparación de Ablación: La variante DPO alcanzó una tasa de paso Diamond del 20%, siendo superada por el enfoque de reparación-GRPO (30%).
• Validación Anti-Reward-Hacking: Crucialmente, las tasas de paso Gold y Diamond coincidieron en cada checkpoint en el pipeline de producción (diferencia de 0). Esto indica que el modelo no aprendió a generar invariantes tautológicos que pasan TLC pero fallan la prueba de mutación. La única excepción fue un caso único en la ablación DPO, que el nivel Diamond logró detectar.
• Estrategias de Inferencia:
  • Muestreo Best-of-8 aumentó la tasa de paso Diamond al 37% (11/30).
  • La unión Greedy ∪ Best-of-8 sugiere un techo del 43% (13/30), indicando que el modelo posee la capacidad de resolver más problemas dadas múltiples tentativas.
  • La autocorrección (retroalimentación de 3 pasos de TLC) no produjo mejoras, lo que sugiere que los fallos se deben a brechas de conocimiento más que a errores de muestreo aleatorio.

Significado y Contribuciones

El artículo reclama tres contribuciones primarias:

1. TLA-Prover con una Jerarquía de Cuatro Niveles: La introducción de una jerarquía de validación donde el nivel superior (Diamond) utiliza pruebas de mutación para descartar invariantes tautológicos. Esto aborda el riesgo específico de reward-hacking inherente al uso de TLC como señal de recompensa, asegurando que "pasar" implique una especificación no trivial.
2. Pipeline GRPO Basado en Reparación: Un pipeline de entrenamiento de dos etapas que combina SFT en un corpus de nivel Diamond con GRPO basado en reparación. Este enfoque aprovecha la retroalimentación en línea del verificador para proporcionar señales de recompensa densas, superando las ablaciones estáticas de DPO.
3. Análisis Empírico de Anti-Reward-Hacking: La observación de que las tasas de paso Gold y Diamond coinciden en todos los checkpoints proporciona evidencia empírica de que el pipeline previene con éxito el modo de fallo de "invariante siempre verdadero".

Los autores posicionan este trabajo como el primer estudio de entrenamiento dirigido a TLA+ que supera sustancialmente los baselines de FormaLLM. Enfatizan que, si bien el modelo mejora significamente la síntesis de especificaciones, actualmente se especializa en especificaciones de estilo invariante con espacios de estados pequeños y tiene dificultades con protocolos complejos que requieren análisis de casos o manipulación de cuantificadores. El trabajo subraya que el entrenamiento guiado por el verificador sin una validación de anti-reward-hacking (como el nivel Diamond) es insuficiente para producir especificaciones formales significativas.