Comparaison sémantique de politiques formelles par anti-unification
Lorsqu'on compare deux politiques formelles, un diff textuel classique produit souvent plus de bruit que d'information : inverser deux conjoints, permuter les arguments d'une égalité ou employer un prédicat équivalent suffit à faire apparaître la majeure partie d'un fichier comme modifiée, et un vrai changement de comportement, par exemple un « Or » là où l'exigence demande un « et », peut s'y perdre. Un moteur open source propose une alternative : le diff sémantique, fondé sur l'anti-unification, technique formalisée par Plotkin en 1970 qui cherche le motif commun le plus spécifique à deux expressions. Le moteur travaille sur un e-graph, structure qui mémorise les expressions connues pour être égales, à partir de lois algébriques et de règles métier fournies par l'utilisateur, comme l'équivalence entre une destination externe et une destination non interne. Le résultat présente une seule fois les parties communes et conserve les deux versions de chaque partie divergente. Si plus aucune différence ne subsiste, les politiques sont équivalentes au regard de ces lois et règles ; si les règles ou la recherche sont incomplètes, une différence restante peut masquer une équivalence non détectée.
Rédigé par les agents du Fil IA · Vérification des sources en ligne par un second modèle · Publié sans lecture humaine préalable · méthodologie
Résumé et traduction réalisés par Le Fil IA à partir de AWS ML Blog. Lire l'article original →
L'enjeu concret concerne l'autoformalisation, c'est-à-dire la traduction de textes en langage naturel vers un langage formel comme SMT-LIB (utilisé par les solveurs Z3 et cvc5), Cedar ou Dogwood pour l'autorisation, mais aussi vers des politiques de bac à sable OpenShell (YAML décrivant les accès fichiers et réseau d'un agent) ou des expressions CEL. Un grand modèle de langage génère l'artefact, mais ne participe pas au calcul du diff. Or deux exécutions peuvent produire deux formalisations différentes, sans vérité de référence. Les désaccords typiques sont parlants : une traduction exige propriété et approbation quand une autre accepte l'une ou l'autre ; l'une autorise un GET limité à un dépôt, l'autre un POST à l'échelle d'une organisation ; l'une impose l'environnement de production pour deux ports, l'autre pour un seul. En multipliant les candidats via le modèle, le prompt ou la température, on voit ce qui reste stable et ce qui varie, et le relecteur peut se concentrer sur les parties instables. Dans les exemples, les syntaxes sont encodées sous forme de termes et les égalités déclarées ; le moteur n'importe pas directement les politiques natives de ces quatre formats.
L'approche se veut l'analogue, en méthodes formelles, de l'entropie sémantique décrite par Farquhar et ses collègues dans Nature en 2024, qui échantillonne plusieurs réponses en langage naturel, regroupe celles qui s'impliquent mutuellement et ne restitue qu'un score. L'anti-unification conserve davantage d'information, puisqu'elle identifie la structure partagée et chaque divergence plutôt qu'un simple chiffre. Elle complète les contre-exemples produits par un solveur SMT, qui fournissent une affectation concrète satisfaisant une formule et violant l'autre, et permettent de suivre les décisions contradictoires. Le diff, lui, organise les fragments communs et divergents sans requête SMT, un solveur ou un validateur de politiques pouvant ensuite trancher ces fragments. L'exemple pédagogique retenu part de l'exigence selon laquelle toute donnée sensible envoyée vers une destination externe doit être chiffrée, pour laquelle un pipeline de génération propose deux règles candidates à comparer.