Diff semântico para políticas geradas por LLM: 18 linhas “alteradas” revelam 2 bugs

A revisão de código começa com um diff. Ninguém compara visualmente dois arquivos de três mil linhas cada. Com políticas formais, a situação é mais complicada: um diff textual destaca mudanças de sintaxe que não alteram o significado. Troque a ordem de duas condições, inverta os argumentos de uma igualdade, substitua um predicado por uma expressão equivalente, e metade do arquivo parece ter mudado. Um bug real, como Or onde o requisito diz “e”, pode facilmente se perder nesse ruído.

O AWS Machine Learning Blog descreve um motor de código aberto que resolve esse problema por meio da antiunificação. É a ideia clássica de Plotkin, de 1970: encontrar o padrão comum mais específico para duas expressões.

Para que isso serve quando um LLM escreve as políticas

O principal caso de uso é a autoformalização. Você pega requisitos em linguagem natural e pede ao modelo que os transforme em SMT-LIB para Z3 ou cvc5, em políticas Cedar ou Dogwood, em regras YAML para o sandbox OpenShell ou em expressões CEL. O modelo produz o artefato, mas não participa da comparação. Também não existe uma versão de referência. Execute o modelo duas vezes e você terá duas formalizações diferentes, sem saber qual está correta.

O diff semântico mostra onde os candidatos concordam e onde divergem. É possível gerar mais versões mudando o modelo, o prompt ou a temperatura. As partes comuns se repetem entre as execuções e podem ser verificadas com menos frequência. O que muda deve ser revisado primeiro.

A ideia é próxima da entropia semântica apresentada no trabalho de Farquhar e colegas na Nature (2024). Nesse caso, várias respostas são agrupadas para produzir um único número. A antiunificação preserva mais informação: mostra a estrutura compartilhada e cada divergência, em vez de apenas uma pontuação.

Como funciona na prática

O motor opera sobre um e-graph, uma estrutura que armazena expressões reconhecidamente iguais entre si. Você declara essas igualdades. Para os operadores And e Or, define associatividade, comutatividade e idempotência. Fatos específicos do domínio, como “external equivale a não internal”, são expressos como regras de reescrita. O motor considera todo o restante uma diferença.

O resultado é um único termo. O conteúdo compartilhado aparece uma vez, e cada divergência fica em um nó Variants com as duas versões. Ao escolher a primeira alternativa em todos os nós, você obtém a política A; ao escolher a segunda, obtém a B. A combinação não perde informação.

O exemplo analisado envolve um requisito de replicação entre regiões no S3: versionamento, uma região de destino aprovada, a mesma conta e criptografia com uma chave do cliente para objetos confidential, além de cópia multipartes para objetos grandes. As duas formalizações diferem em cinco pontos. Três diferenças são cosméticas: a ordem das condições, um Eq invertido e approvedRegion expandido em us-east-1 e eu-west-1. Duas alteram o significado. Em uma versão, a condição para objetos confidential exige tanto a conta quanto a criptografia; na outra, basta um dos dois (And vira Or). O limite de tamanho usa Lte em uma versão e Lt na outra.

Um unified diff convencional marca 18 das 28 linhas sem indicar quais mudanças importam. O diff semântico elimina as reordenações e reduz o resultado aos nós que precisam ser revisados. Para casos assim, existe a métrica cr, a razão de compressão. Zero significa concordância total sob as igualdades declaradas, e um significa que não há nada em comum. No exemplo, cr é 0,5862 e o tamanho do resultado é 42.

Limitações e próximos passos

Há algumas ressalvas. O motor não importa políticas nativas de Cedar, Dogwood, OpenShell ou CEL. Você precisa codificar manualmente as construções necessárias como termos e também declarar as igualdades à mão. Se faltarem regras ou a busca estiver incompleta, uma diferença restante pode ser uma equivalência que o motor não encontrou. Um cr baixo também não comprova a correção: dois candidatos podem cometer o mesmo erro. Além disso, a busca usa por padrão um método de Monte Carlo, e o campo :completion mostrará budget em vez de exact se o limite for atingido antes que todas as alternativas sejam exploradas.

A conclusão prática para quem monta pipelines de “requisitos → política formal”: não confie em uma única saída do modelo. Gere vários candidatos, combine-os por meio de um diff semântico e encaminhe apenas os nós Variants a uma pessoa ou a um solver SMT. O solver pode encontrar um contraexemplo, ou seja, uma atribuição concreta para a qual uma fórmula é verdadeira e a outra é falsa, enquanto o antiunificador mostra onde procurar. Dá para experimentar em cinco minutos: o repositório yaspar-org/semi-persistent, a compilação com cargo build --release e o exemplo 12-first-au.egg.