Diff semántico para políticas generadas por LLM: 18 líneas «modificadas» revelan 2 errores

La revisión de código empieza con un diff. Nadie compara a simple vista dos archivos de tres mil líneas cada uno. Con las políticas formales, la cosa se complica: un diff textual resalta cambios sintácticos que no alteran el significado. Basta con intercambiar dos condiciones, invertir los argumentos de una igualdad o sustituir un predicado por una expresión equivalente para que medio archivo parezca modificado. Y un error real, como un Or donde el requisito dice «y», puede perderse fácilmente entre tanto ruido.

AWS Machine Learning Blog describe un motor de código abierto que aborda este problema mediante la antiunificación. Es la idea clásica de Plotkin de 1970: encontrar la plantilla común más específica para dos expresiones.

Para qué sirve si las políticas las escribe un LLM

El principal caso de uso es la autoformalización. Tomas requisitos en lenguaje natural y pides al modelo que los convierta en SMT-LIB para Z3 o cvc5, en políticas de Cedar o Dogwood, en reglas YAML para el entorno aislado de OpenShell o en expresiones CEL. El modelo genera el artefacto, pero no participa en la comparación. Tampoco hay una versión de referencia. Ejecutas el modelo dos veces y obtienes dos formalizaciones diferentes, sin saber cuál es correcta.

El diff semántico muestra dónde coinciden los candidatos y dónde discrepan. Puedes generar más variantes cambiando el modelo, el prompt o la temperatura. Las partes comunes se repiten de una ejecución a otra y pueden revisarse con menos frecuencia. Lo que cambia merece atención primero.

La idea está emparentada con la entropía semántica del trabajo de Farquhar y sus colegas publicado en Nature (2024). Allí se agrupan múltiples respuestas y se obtiene un único número. La antiunificación conserva más información: muestra la estructura compartida y cada discrepancia, en vez de limitarse a una puntuación.

Cómo funciona en un ejemplo

El motor funciona sobre un e-graph, una estructura que almacena expresiones que se sabe que son iguales entre sí. Tú declaras esas igualdades. Para los operadores And y Or, defines asociatividad, conmutatividad e idempotencia. Los hechos propios del dominio, como «external equivale a no internal», se expresan mediante reglas de reescritura. El motor considera todo lo demás una diferencia.

El resultado es un único término. Lo compartido aparece una sola vez y cada discrepancia queda dentro de un nodo Variants con ambas versiones. Si eliges la primera alternativa en todos los nodos, obtienes la política A; si eliges la segunda, la B. La combinación no pierde información.

El ejemplo analizado parte de un requisito de replicación entre regiones en S3: control de versiones, una región de destino aprobada, la misma cuenta y cifrado con una clave del cliente para los objetos confidential, y copia multiparte para los objetos grandes. Las dos formalizaciones difieren en cinco puntos. Tres diferencias son cosméticas: el orden de las condiciones, un Eq invertido y approvedRegion expandido en us-east-1 y eu-west-1. Dos cambian el significado. En una versión, la condición para los objetos confidential exige tanto la cuenta como el cifrado; en la otra, basta con uno de los dos (And se convierte en Or). El umbral de tamaño usa Lte en una versión y Lt en la otra.

Un unified diff convencional marca 18 de las 28 líneas sin indicar qué cambios importan. El diff semántico elimina las reordenaciones y reduce el resultado a los nodos que hay que revisar. Para estos casos existe la métrica cr, la relación de compresión. Cero significa coincidencia total bajo las igualdades declaradas y uno significa que no hay nada en común. En el ejemplo, cr es 0,5862 y el tamaño del resultado es 42.

Limitaciones y próximos pasos

Hay varias salvedades. El motor no importa políticas nativas de Cedar, Dogwood, OpenShell o CEL. Debes codificar manualmente las construcciones necesarias como términos y declarar también las igualdades a mano. Si faltan reglas o la búsqueda es incompleta, una diferencia restante puede ser una equivalencia que el motor no haya encontrado. Un cr bajo tampoco demuestra que el resultado sea correcto: dos candidatos pueden equivocarse de la misma manera. Además, la búsqueda utiliza por defecto un método de Montecarlo, y el campo :completion mostrará budget en lugar de exact si se agota el límite antes de explorar todas las alternativas.

La conclusión práctica para quienes construyen flujos de «requisitos → política formal»: no confíes en una única salida del modelo. Genera varios candidatos, combínalos mediante un diff semántico y entrega a una persona o a un solver SMT solo los nodos Variants. El solver puede encontrar un contraejemplo, es decir, una asignación concreta para la que una fórmula es verdadera y la otra falsa, mientras que el antiunificador indica dónde buscar. Puedes probarlo en cinco minutos: el repositorio yaspar-org/semi-persistent, la compilación con cargo build --release y el ejemplo 12-first-au.egg.