Faithful Autoformalization via Roundtrip Verification and Repair

Resumen Técnico: Autoformalización Fiel mediante Verificación de Ida y Vuelta y Reparación

Enunciado del Problema
El artículo aborda una brecha crítica en la autoformalización: la falta de un método fiable para verificar si un Modelo de Lenguaje Grande (LLM) ha capturado fielmente el significado semántico de una declaración en lenguaje natural al traducirla a una representación formal verificable por máquina. Los métodos de evaluación existentes dependen de la validez sintáctica o del éxito en tareas posteriores, lo cual no prueba directamente la fidelidad semántica. Además, cuando se producen errores, las estrategias de reparación actuales se limitan a la regeneración de extremo a extremo, careciendo de la capacidad de diagnosticar dónde en el pipeline de traducción se perdió el significado. Esto es particularmente desafiante en dominios como el derecho estatutario, donde no están disponibles formalizaciones de verdad fundamental.

Metodología
Los autores proponen un Marco de Verificación de Ida y Vuelta y Reparación Acotada que opera sin anotaciones de verdad fundamental. El mecanismo central implica un pipeline de traducción de tres etapas:

1. T1 (Autoformalización): Traduce la entrada en lenguaje natural $x$ a una expresión formal $y_{orig}$ en un formalismo objetivo $\Sigma$.
2. T2 (Retraducción): Traduce $y_{orig}$ de nuevo a lenguaje natural $x'$.
3. T3 (Reformalización): Traduce $x'$ de nuevo a una expresión formal $y_{rt}$.

Verificación: El sistema verifica la equivalencia lógica entre la formalización inicial ($y_{orig}$) y la formalización de ida y vuelta ($y_{rt}$) utilizando una herramienta formal (específicamente un solucionador SMT en los experimentos). Si $y_{orig} \equiv_\Sigma y_{rt}$, el pipeline se considera autoconsistente.

Diagnóstico y Reparación: Cuando la equivalencia falla, el marco emplea un procedimiento de diagnóstico basado en etapas. Un juez LLM examina los artefactos ($x, y_{orig}, x', y_{rt}$) para identificar la primera etapa donde ocurrió la deriva semántica (Etapa 1, 2 o 3). Crucialmente, el diagnóstico es "acotado", lo que significa que la explicación se restringe a los artefactos relevantes solo para esa etapa específica.

• Reparación Acotada: En lugar de regenerar todo el pipeline, un operador de reparación dirigido ($R_i$) corrige únicamente la etapa defectuosa identificada. Las etapas posteriores se regeneran entonces para mantener la coherencia del pipeline.
• Bucle Iterativo: Este proceso se repite hasta un presupuesto fijo ($K=3$) hasta lograr la equivalencia o agotar el presupuesto.

Señal Semántica Auxiliar: Para evaluar la calidad semántica de las formalizaciones independientemente del bucle de reparación, los autores utilizan un modelo bidireccional de Inferencia en Lenguaje Natural (NLI). Esto sirve como un diagnóstico a posteriori para medir la "deriva" (por ejemplo, contradicciones o falta de relación) entre el texto original y el texto reconstruido, distinguiendo entre reglas que son formalmente consistentes pero semánticamente desviadas.

Contribuciones Clave

1. Marco de Verificación de Ida y Vuelta: Un método para señalar la fidelidad de la autoformalización sin formalizaciones de verdad fundamental, aplicable a cualquier formalismo que admita una verificación de equivalencia (por ejemplo, SMT, verificadores de tipos).
2. Reparación Acotada Guiada por Diagnóstico: Un procedimiento que localiza los errores en pasos específicos de traducción, permitiendo correcciones dirigidas en lugar de costosas regeneraciones de todo el pipeline.
3. Análisis Empírico de Cuellos de Botella: Un estudio en dos dominios estatutarios (Código de Transporte de Texas y Código de Parques y Vida Silvestre de Texas) y dos familias de modelos (Claude Opus 4.6 y GPT-5.2) que identifica el paso de diagnóstico como el principal cuello de botella para la reparación acotada, y no el pipeline ni los operadores de reparación en sí mismos.

Resultados
El marco se evaluó en 150 reglas de tráfico y 77 reglas de vida silvestre.

• Efectividad de la Reparación: La reparación acotada guiada por diagnóstico logró las tasas más altas de equivalencia verificada al menor costo cuando la función de diagnóstico era fiable.
• Dependencia del Modelo: Con Claude ejecutando el pipeline y el diagnóstico, la reparación acotada superó a los puntos de referencia (sin reparación, selección aleatoria de etapas, regeneración completa). Sin embargo, con GPT, el paso de diagnóstico fue poco fiable (fuertemente sesgado hacia culpar a la Etapa 1), lo que provocó que la reparación acotada rindiera menos y fuera más costosa que la regeneración completa.
• Intervención Cruzada entre Modelos: Reemplazar únicamente el paso de diagnóstico de GPT con Claude (manteniendo GPT para el pipeline y la reparación) restauró la eficiencia y efectividad de la reparación acotada, demostrando que la función de diagnóstico es la variable crítica.
• Predicción de Fidelidad: La equivalencia formal es un fuerte predictor de la fidelidad semántica. Las reglas que aprobaron la verificación de equivalencia (UNSAT) mostraron una deriva NLI de 1.4× a 2.5× menor que aquellas que fallaron (SAT). Sin embargo, la equivalencia formal es necesaria pero no suficiente; aproximadamente el 16% de las reglas formalmente equivalentes aún exhibieron deriva semántica.

Significado y Afirmaciones
El artículo afirma que la equivalencia formal sirve como una señal práctica y libre de verdad fundamental para la fidelidad semántica en la autoformalización. Demuestra que la reparación acotada, impulsada por un diagnóstico preciso a nivel de etapa, es una estrategia más rentable y eficiente que la regeneración completa. Los autores enfatizan que la fiabilidad de la función de diagnóstico es el factor determinante para el éxito de este enfoque.

El trabajo es modesto en su alcance, señalando que el marco es heurístico y no garantiza la corrección frente a la intención original en lenguaje natural (ya que el pipeline podría estabilizarse en un punto fijo semánticamente diferente). Los autores declaran explícitamente que el sistema no es adecuado para aplicaciones críticas de seguridad sin revisión independiente de expertos y que la evaluación actual se limita a texto estatutario en inglés, requiriendo más estudios para otros géneros como código o texto científico.