Resumen Técnico: BRIDGE – Construcción de Representaciones en la Síntesis de Programas Verificados Guiada por Dominio

1. Enunciado del Problema

Los Modelos de Lenguaje Grandes (LLM) son cada vez más capaces de generar código, pero en el contexto de la verificación formal, los programas generados a menudo parecen correctos mientras albergan errores sutiles, casos límite omitidos o suposiciones desajustadas. En asistentes de prueba como Lean, la verificación de programas no es una tarea de generación única, sino un problema de predicción de múltiples artefactos. Una verificación exitosa requiere la consistencia mutua de cuatro artefactos acoplados:

1. Código Ejecutable: La implementación.
2. Especificación Formal: Restricciones de comportamiento (precondiciones, postcondiciones, invariantes).
3. Enunciados de Teoremas: Afirmaciones que conectan el código con la especificación.
4. Intentos de Prueba: Scripts verificados por el núcleo para validar las afirmaciones.

Los sistemas actuales de LLM luchan en este escenario porque tratar estos artefactos de forma independiente conduce a una deriva semántica. Un modelo podría generar código que pasa las pruebas pero falla en las comprobaciones de terminación de Lean, una especificación que verifica tipos pero es vacía, o un teorema que es demostrable pero irrelevante para la tarea original. El desafío central es traducir la intención informal en una secuencia de artefactos donde la sintaxis, los tipos, las estructuras de recursión, los contratos y las obligaciones de prueba permanezcan alineados.

2. Metodología: El Marco BRIDGE

Los autores proponen BRIDGE, un marco de prompting estructurado que descompone el proceso de codificación verificable en tres dominios vinculados: Código, Especificación y Teorema/Prueba. En lugar de pedirle a un modelo que salte directamente del lenguaje natural a una prueba final, BRIDGE impone un flujo de razonamiento estructurado donde los artefactos se restringen y verifican mutuamente.

2.1 Descomposición por Dominios

• El Dominio del Código: Produce la implementación final en Lean. BRIDGE compara la generación directa en Lean frente a andamios de razonamiento intermedios.
  • Andamios Funcionales: Inspirados en OCaml y Haskell, estos fomentan datos inmutables, coincidencia de patrones, recursión estructural y definiciones composicionales. Esto se alinea naturalmente con la teoría de tipos dependientes de Lean y la disciplina de terminación.
  • Andamios Imperativos: Inspirados en Python y C++, estos fomentan bucles y mutación.
  • Insight Clave: El programa intermedio es un andamio de razonamiento, no un artefacto fuente certificado. No necesita compilarse en su lenguaje fuente; su propósito es sesgar al modelo hacia una estructura que Lean pueda verificar.
• El Dominio de la Especificación: Describe las garantías previstas. BRIDGE utiliza diversos estilos de razonamiento (Diseño por Contrato, Pruebas Basadas en Propiedades, Desarrollo Guiado por Pruebas, Programación Defensiva) para hacer explícitas las suposiciones, los casos límite y las garantías. Las especificaciones se evalúan no solo por la verificación de tipos, sino por su no vacuidad y su capacidad para distinguir implementaciones correctas de incorrectas plausibles.
• El Dominio del Teorema/Prueba: Hace explícitas las afirmaciones de corrección. Se solicita a los modelos que propongan propiedades (límites, invariantes, monotonía) e intenten pruebas. Este dominio sirve como diagnóstico para la verificación aguas abajo, verificando si los teoremas generados pueden ser elaborados y si las pruebas pueden completarse sin sorry (marcador de posición para objetivos no probados).

2.2 Hipótesis de Razonamiento

La hipótesis central es que el éxito de la verificación depende de la estructura del razonamiento intermedio. La generación directa obliga al modelo a recuperar el algoritmo, expresarlo en Lean, satisfacer las restricciones de tipos/terminación e inferir especificaciones simultáneamente. BRIDGE separa estas presiones. Específicamente, los autores encuentran que un ordenamiento que comienza con la generación de código funcional es particularmente efectivo: el modelo primero genera código compatible con Lean utilizando un andamio funcional, y luego utiliza esa implementación como un ancla semántica para las especificaciones y los enunciados de teoremas.

3. Contribuciones Clave

1. Un Marco de Múltiples Artefactos: BRIDGE introduce un enfoque estructurado para la codificación verificable que descompone la tarea en dominios vinculados de Código, Especificación y Teorema/Prueba, utilizando el razonamiento entre artefactos para reducir la deriva semántica.
2. El Razonamiento Funcional Mejora la Síntesis: En un conjunto de pruebas de 178 problemas en Lean, el razonamiento intermedio alineado funcionalmente mejora la corrección ejecutable en Lean hasta en un 1.5× en comparación con el prompting directo. Logra tasas de éxito comparables con aproximadamente 2× menos evaluaciones en Lean, lo que indica una mayor eficiencia de muestra.
3. Artefactos Aguas Abajo Mejorados: El prompting al estilo BRIDGE produce artefactos formales más útiles. Genera más enunciados de teoremas que se elaboran con éxito en Lean y más intentos de prueba completados alineados con la implementación. El prompting guiado por especificaciones también mejora la generación de código convencional (hasta 17.5 puntos porcentuales en Python).
4. Sesgo Inductivo Aprendible: El Ajuste Fino Supervisado (SFT) en trazas funcionales al estilo BRIDGE supera al ajuste fino de trazas directas emparejado (por ejemplo, una ganancia de 9.1 puntos porcentuales en el conjunto de pruebas VERINA). Esto sugiere que el marco captura un sesgo inductivo aprendible en lugar de ser un efecto de prompt único.

4. Resultados Experimentales

Los autores evaluaron BRIDGE en un conjunto de pruebas personalizado de 178 problemas en Lean y en conjuntos de pruebas públicos, incluidos VERINA, CLEVER y un piloto de DAFNYBENCH respaldado por un solver.

• Corrección Ejecutable: Utilizando andamios funcionales, la tasa de aprobación en el conjunto de pruebas de 178 tareas aumentó de 44/178 (Directo) a 59/178 (Funcional) en la configuración de núcleo mínima. Con rondas de reparación, la brecha se mantuvo positiva (83/178 vs. 77/178).
• Eficiencia de Muestra: Los andamios funcionales alcanzaron un éxito comparable con aproximadamente la mitad del número de evaluaciones en Lean en comparación con el prompting directo, reduciendo el costo de verificar candidatos.
• Transferibilidad: Los beneficios se transfirieron a conjuntos de pruebas públicos. En VERINA, el prompting funcional mejoró las tasas de aprobación hasta en 6.3 puntos porcentuales. En DAFNYBENCH, mejoró la tasa de aprobaciones verificadas @5 en 7.3 puntos porcentuales.
• Diagnósticos de Prueba: En un experimento de prueba completo, el código funcional produjo más pruebas completadas sin sorry (34/178 vs. 20/178 con el probador SFT funcional) y generó implementaciones más cortas y limpias que fueron más fáciles de resolver para los modelos de prueba.
• Ganancias de SFT: El ajuste fino en trazas funcionales mejoró el rendimiento en VERINA del 20.3% al 29.4%, demostrando que la estructura de razonamiento puede ser internalizada por el modelo.

5. Significado y Limitaciones

El artículo afirma que la representación del razonamiento importa. Al estructurar el proceso de generación para alinearlo con el sistema de verificación objetivo (Lean), BRIDGE reduce los fallos de sintaxis, tipos y terminación. El marco proporciona un sesgo inductivo orientado a la verificación que conecta el código, las especificaciones, los enunciados de teoremas y los intentos de prueba, haciendo que el pipeline sea más fácil de inspeccionar y más susceptible a la búsqueda de pruebas aguas abajo.

Afirmaciones Modestas y Limitaciones:

• No es Verificación Completa: BRIDGE estudia el "frontend" de la síntesis verificada. No afirma resolver la verificación semántica completa a escala. Las especificaciones y enunciados de teoremas generados pueden seguir siendo débiles, vacíos o excesivamente moldeados por la implementación.
• Alcance: La evaluación se centra en tareas algorítmicas locales. Los autores aún no han probado BRIDGE en bibliotecas formales grandes, programas con estado ricos o pruebas de largo horizonte.
• Dependencia del Modelo: Los resultados varían según los modelos, los prompts y los presupuestos de búsqueda. BRIDGE se presenta como un sesgo inductivo útil en lugar de una mejora universal independiente del modelo subyacente.
• Trabajo Futuro: Los autores señalan que el siguiente paso es cerrar el ciclo entre los artefactos de BRIDGE y una búsqueda de pruebas más fuerte, integrando potencialmente probadores de teoremas que utilizan herramientas, recuperación de bibliotecas formales y aprendizaje por refuerzo a partir de recompensas verificables.

En resumen, BRIDGE demuestra que descomponer la codificación verificada en pasos de razonamiento estructurados y alineados con el dominio mejora significativamente la calidad y la verificabilidad de los artefactos generados, ofreciendo un camino hacia una síntesis formal más fiable sin requerir la automatización completa del proceso de prueba.