Cryptographic certificates of validity for trustworthy AI

Énoncé du problème

Alors que les systèmes d'IA passent de la production de recommandations à l'exécution d'actions autonomes (par exemple, réserver des vols, approuver des factures, déployer du code), les mécanismes d'assurance traditionnels deviennent insuffisants. Les signatures cryptographiques authentifient l'origine d'un message, mais ne peuvent pas prouver qu'une action satisfait des conditions spécifiques de correction, de sécurité ou de conformité à l'avance. De même, la journalisation rétrospective ne peut pas empêcher les violations de politiques avant qu'elles ne se produisent. L'article traite de la nécessité d'un mécanisme capable de fournir une preuve vérifiable de manière indépendante qu'une action d'un agent satisfait une politique formelle convenue avant que l'action ne soit acceptée, sans exiger que le vérificateur fasse confiance à l'implémentation interne de l'agent ou réexécute son calcul.

Méthodologie

L'article propose un cadre pour générer des certificats de validité cryptographiques en jetant un pont entre la logique formelle et les preuves cryptographiques succinctes. La méthodologie suit un pipeline en trois étapes :

1. Spécification formelle : La politique ou la condition de correction pertinente est exprimée sous la forme d'un prédicat logique dans une logique du premier ordre spécifique.
2. Arithmétisation : Ce prédicat est compilé en un problème de vérification de témoin (witness-checking) sur des contraintes polynomiales. La contribution mathématique centrale est une traduction de la validité de la logique du premier ordre en jugements sur des contraintes polynomiales où :
   • La vérité (validité) est représentée par la valeur 0.
   • La fausseté (invalidité) est représentée par une valeur strictement positive.
   • Les connecteurs logiques sont mappés vers des opérations algébriques :
     • L'égalité ($t=t'$) est mappée vers $(t-t')^2$.
     • La conjonction ($\phi \land \psi$) est mappée vers la somme $[\phi] + [\psi]$.
     • La disjonction ($\phi \lor \psi$) est mappée vers le produit $[\phi] \times [\psi]$.
     • La quantification universelle sur une plage est mappée vers une sommation sur cette plage.
   • La récursion et les définitions inductives (par exemple, l'exponentiation) sont encodées en structurant les données du témoin sous forme de matrices, où les colonnes représentent les étapes de dérivation, avec des pointeurs dans une ligne dédiée garantissant que la structure récursive est bien formée.
3. Certification cryptographique : L'agent (ou un prouveur associé) génère une preuve cryptographique succincte (potentiellement à connaissance nulle) démontrant que les contraintes polynomiales dérivées de la politique sont satisfaites par les données d'action spécifiques.

Le processus de vérification implique que le vérificateur contrôle la preuve par rapport à une clé publique et des paramètres. Si la preuve est vérifiée, le système accepte que l'action satisfait le prédicat formel, sans avoir besoin d'inspecter les données privées du témoin de l'agent ou de réexécuter le calcul.

Contributions clés

• Traduction mathématique : L'article fournit une arithmétisation compacte et agnostique de l'application de la validité de la logique du premier ordre en contraintes polynomiales (Définitions 2.3–2.7, Théorème 2.9). Il démontre comment encoder des structures logiques complexes, y compris la récursion et les dérivations inductives, dans des relations algébriques adaptées aux backends cryptographiques.
• Actions d'agents porteuses de preuve : Il conceptualise les actions des agents comme étant « porteuses de preuve » dans un sens cryptographique spécifique. Contrairement au Code Porteur de Preuve (PCC - Proof-Carrying Code), qui nécessite souvent l'inspection du code source, cette approche permet à des agents non approuvés et potentiellement opaques (black-box) de fournir une preuve succincte de conformité.
• Intégration avec les technologies existantes : Le cadre est conçu pour s'interfacer avec les systèmes d'arguments succincts existants (par exemple, les SNARKs, les zkVMs comme Cairo ou RISC0) et les schémas de l'engagement polynomial (par exemple, Halo2, Zinc). Il positionne la logique proposée comme une couche de spécification de haut niveau qui se compile vers ces primitives cryptographiques.
• Distinction par rapport à la vérification au moment de l'exécution (Runtime Verification) : L'approche diffère de la vérification au moment de l'exécution en fournissant un certificat préemptif et succinct plutôt qu'une trace rétrospective, et diffère du PCC standard en ne nécessitant pas que la conception interne de l'agent soit ouverte ou fiable, seulement qu'il puisse produire le certificat.

Résultats et exemples

L'article valide l'approche par des exemples théoriques plutôt que par des benchmarks empiriques :

• Logique de base : Il démontre comment les valeurs de vérité, l'égalité, la conjonction, la disjonction et les vérifications de plage sont encodées sous forme de polynômes qui s'évaluent à zéro si et seulement si la condition est respectée.
• Calcul récursif : Un exemple détaillé encode la définition inductive de l'exponentiation ($a^b$). L'article montre comment une matrice de données de témoin peut encoder un arbre de dérivation, où les lignes 1 à 3 stockent les échantillons d'entrée/sortie et la ligne 4 stocke les pointeurs vers les étapes précédentes. Le prédicat de validité garantit que ces pointeurs forment une structure récursive bien formée.
• Robustesse : L'article note qu'une matrice peut contenir des valeurs d'entrée-sortie correctes mais échouer au prédicat de validité si la structure « porteuse de preuve » (les pointeurs) est manquante ou malformée, illustrant que le certificat valide la dérivation du résultat, et non seulement le résultat lui-même.

Signification et portée

L'article positionne ce travail comme un « juste milieu » entre la vérification formelle du code source et l'authentification cryptographique. Sa principale importance réside dans l'offre d'un analogue cryptographique du code porteur de preuve pour les systèmes d'IA agentiques.

L'auteur note explicitement les limites et la portée de la proposition :

• Portée : L'architecture mathématique est générale et applicable à tout domaine où des parties non approuvées doivent fournir des preuves de correction vérifiables. L'application spécifique aux agents d'IA est choisie car l'action autonome crée un besoin urgent d'assurance préemptive.
• Limites : Un certificat de validité prouve qu'une spécification formelle a été satisfaite. Il ne prouve pas que la spécification formelle elle-même est la « bonne » (c'est-à-dire qu'elle capture correctement les exigences de sécurité, juridiques ou éthiques). L'article souligne que combler l'écart entre les prédicats formels et la sécurité réelle nécessite des processus de gouvernance, d'audit et de gestion des risques (en référence aux cadres du NIST), qui ne peuvent être résolus par les mathématiques ou la cryptographie seuls.
• Travaux futurs : L'article identifie le besoin de détails de mise en œuvre pratique, notamment la conception de compilateurs, l'évaluation des coûts de preuve et l'établissement d'une gouvernance pour l'auteur et l'audit des politiques.

En résumé, l'article propose un fondement théorique et mathématique pour attacher des preuves succinctes et cryptographiquement vérifiables de conformité aux politiques des actions des agents d'IA, déplaçant le modèle de confiance de « faire confiance à l'origine » vers « faire confiance à la preuve ».