Diff sémantique pour les politiques générées par LLM : sur 18 lignes « modifiées », 2 bugs seulement

Une revue de code commence par un diff. Personne ne compare à l'œil deux fichiers de trois mille lignes. Avec les politiques formelles, c'est pire : le diff textuel met en évidence une syntaxe qui ne change pas le sens. On a permuté deux conditions, retourné les arguments d'une égalité, remplacé un prédicat par un équivalent, et la moitié du fichier semble modifiée. Quant au vrai bug, par exemple un Or là où l'exigence dit « et », il se perd facilement dans ce bruit.

Le blog AWS Machine Learning décrit un moteur open source qui résout ce problème grâce à l'anti-unification. C'est une idée classique de Plotkin, datant de 1970 : pour deux expressions, on cherche le gabarit commun le plus spécifique.

À quoi bon, si ce sont des LLM qui écrivent les politiques

Le scénario principal est l'autoformalisation. Vous prenez des exigences en langage naturel et demandez à un modèle de les transformer en SMT-LIB pour Z3 ou cvc5, en politiques Cedar ou Dogwood, en règles YAML de sandbox OpenShell ou en expressions CEL. Le modèle écrit l'artefact, mais ne participe pas à la comparaison. Il n'existe pas de référence. Lancez le modèle deux fois et vous obtenez deux formalisations différentes, sans savoir laquelle est la bonne.

Le diff sémantique montre où les candidats concordent et où ils divergent. On peut générer davantage de variantes en changeant de modèle, de prompt ou de température. Les parties communes se répètent d'une exécution à l'autre et peuvent être vérifiées moins souvent. Ce qu'il faut vérifier en priorité, c'est ce qui change.

C'est un cousin de l'entropie sémantique du travail de Farquhar et de ses collègues dans Nature (2024). Là, de nombreuses réponses sont regroupées en clusters pour obtenir un seul nombre. L'anti-unification conserve davantage d'information : elle montre la structure commune et chaque divergence, et pas seulement un score.

Comment cela fonctionne, sur un exemple

Le moteur s'appuie sur un e-graph, une structure qui stocke des expressions connues pour être égales entre elles. Les égalités, c'est vous qui les déclarez. Pour les opérateurs And et Or, vous définissez l'associativité, la commutativité et l'idempotence. Les faits propres au domaine, par exemple « external est égal à non internal », s'écrivent comme une règle de réécriture (rewrite). Tout le reste est considéré par le moteur comme une différence.

Le résultat se présente comme un seul terme. Ce qui est commun n'apparaît qu'une fois, et chaque divergence se trouve dans un nœud Variants contenant les deux versions. Si l'on choisit la première variante dans tous les nœuds, on obtient la politique A ; si l'on choisit la seconde, la politique B. La fusion se fait sans perte.

L'exemple étudié porte sur une exigence de réplication interrégionale dans S3 : versionnement, région de destination approuvée, pour les objets confidential le même compte et un chiffrement avec clé client, et pour les gros objets une copie multipart. Les deux formalisations diffèrent en cinq endroits. Trois différences sont cosmétiques : l'ordre des conditions, un Eq retourné et approvedRegion développé en us-east-1 et eu-west-1. Deux changent le sens. Dans une version, la condition pour les objets confidential exige à la fois le compte et le chiffrement, dans l'autre, l'un des deux suffit (And est devenu Or). Le seuil de taille est Lte dans une version et Lt dans l'autre.

Un unified diff classique marque 18 lignes sur 28 sans dire quels changements comptent. Le diff sémantique supprime les permutations et ramène le résultat aux nœuds qu'il faut vraiment lire. Pour ces cas, il existe la métrique cr, le taux de compression. Zéro signifie un accord complet compte tenu des égalités déclarées, et un signifie qu'il n'y a rien de commun. Dans l'exemple, cr vaut 0,5862 pour une taille de résultat de 42.

Limites et marche à suivre

Quelques réserves s'imposent. Le moteur n'importe pas les politiques natives de Cedar, Dogwood, OpenShell ou CEL. Vous encodez à la main les constructions nécessaires sous forme de termes et déclarez à la main les égalités. Si les règles manquent ou si la recherche est incomplète, la différence restante peut être une équivalence que le moteur n'a pas trouvée. Un faible cr ne prouve pas non plus la justesse : deux candidats peuvent se tromper de la même façon. De plus, la recherche par défaut utilise la méthode de Monte-Carlo, et le champ :completion affichera budget au lieu de exact si la limite est atteinte avant d'avoir parcouru toutes les variantes.

En pratique, pour ceux qui construisent des pipelines « exigences → politique formelle » : ne faites pas confiance à une seule sortie du modèle. Générez plusieurs candidats, fusionnez-les via le diff sémantique et ne soumettez à un humain ou à un solveur SMT que les nœuds Variants. Le solveur peut trouver un contre-exemple, c'est-à-dire une affectation concrète pour laquelle une formule est vraie et l'autre non, et l'anti-unificateur indiquera où chercher. On peut essayer en cinq minutes : dépôt yaspar-org/semi-persistent, compilation via cargo build --release et exemple 12-first-au.egg.