\texttt{Range-Arithmetic}: Verifiable Deep Learning Inference on an Untrusted Party

Résumé Technique : Range-Arithmetic – Inférence de Deep Learning Vérifiable par une Partie Non Fiable

Énoncé du Problème
Les systèmes d'apprentissage automatique (ML) décentralisés reposent de plus en plus sur l'externalisation de tâches gourmandes en ressources, telles que l'inférence de réseaux de neurones profonds (DNN), vers des parties externes non fiables (les prouveurs) pour surmonter les limitations des blockchains. Un défi critique dans ce paradigme est d'assurer l'intégrité de ces calculs externalisés sans exiger que le vérificateur réexécute l'intégralité du processus, ce qui est souvent prohibitif en termes de coût.

Les techniques existantes de Calcul Vérifiable (VC) font face à des obstacles importants lorsqu'elles sont appliquées au ML. La plupart des schémas VC opèrent sur des corps finis et sont restreints aux opérations arithmétiques (additions et multiplications). Cependant, les calculs standards du ML impliquent des opérations non arithmétiques, spécifiquement :

1. L'arrondi en virgule fixe : Nécessaire après les multiplications matricielles pour gérer la précision et prévenir le dépassement de capacité (overflow).
2. Les fonctions d'activation non linéaires : Telles que ReLU (Rectified Linear Unit).

Représenter ces opérations dans les cadres de VC conventionnels nécessite souvent des encodages de circuits booléens complexes, des polynômes de haut degré ou de grandes tables de recherche précalculées. Ces approches introduisent un surcoût substantiel de l'effort du prouveur, du coût du vérificateur et de la bande passante de communication, ou échouent à supporter simultanément des opérations essentielles comme ReLU et l'arrondi.

Méthodologie : Le Cadre Range-Arithmetic
Les auteurs proposent Range-Arithmetic, un nouveau cadre conçu pour vérifier efficacement l'inférence de DNN tout en maintenant la compatibilité avec les systèmes de preuve basés sur des corps finis. L'innovation centrale réside dans la transformation des opérations non arithmétiques en étapes arithmétiques vérifiables via des protocoles sum-check et des preuves de plage (range proofs) concaténées, évitant ainsi les encodages booléens et les grandes tables de recherche.

Le cadre fonctionne via les mécanismes suivants :

1. Vérification de la Multiplication Matricielle :
   La vérification de la multiplication matricielle ($C = AB$) est reformulée comme un problème de sum-check. En représentant les éléments de la matrice comme des extensions multilinéaires (MLE) sur un corps fini, la correction du produit est réduite à la vérification d'une identité polynomiale. Les auteurs utilisent le lemme de Schwartz-Zippel pour vérifier cette identité en des points aléatoires, employant le protocole sum-check pour réduire la complexité de communication à $O(\log n)$.

2. Vérification de l'Arrondi :
   Pour vérifier l'opération d'arrondi $R(x)$ appliquée après la multiplication, les auteurs décomposent le processus en contraintes arithmétiques. Ils définissent la partie rejetée de l'arrondi ($E$) et le numérateur de la fraction d'arrondi ($D$). La correction est assurée en prouvant deux conditions via des preuves de plage agrégées :

   • Les bits rejetés se situent dans un intervalle spécifique et restreint ($-2^{s-1} \leq e_i < 2^{s-1}$).
   • La valeur restante est un multiple entier de $2^s$ sans dépassement de capacité (wrap-around).
     Cette approche permet de vérifier l'arrondi en utilisant des preuves de plage standards sans nécessiter de corps finis de grande taille pour prévenir le dépassement de capacité.

3. Vérification de ReLU :
   La fonction ReLU, définie par $\text{ReLU}(x) = \max(0, x) = (x + |x|)/2$, est vérifiée par :

   • La preuve que la valeur absolue $Y = |A|$ est non négative en utilisant une preuve de plage.
   • La preuve que $a_i^2 = y_i^2$ pour tous les éléments en utilisant un protocole sum-check sur le polynôme $f(x) = \tilde{I}(s, x)(\tilde{a}^2(x) - \tilde{y}^2(x))$.
   • La vérification de la combinaison linéaire finale $B = (A + Y)/2$.

4. Composition :
   Le cadre traite l'inférence de réseau de neurones comme une séquence de couches. Chaque couche (multiplication matricielle avec arrondi ou activation ReLU) est vérifiée indépendamment. L'engagement de sortie d'une couche sert d'entrée pour la suivante, permettant la composition modulaire des algorithmes de vérification sans re-transmettre de grandes matrices intermédiaires.

Contributions Clés
Le document revendique les contributions spécifiques suivantes :

• Cadre Unifié : Range-Arithmetic est la première méthode à atteindre simultanément une complexité de prouveur de $O(n^3)$, une complexité de vérificateur de $O(n^2)$ et une complexité de communication de $O(\log n)$ tout en supportant l'arrondi en virgule fixe et ReLU.
• Élimination du Surcoût : L'approche évite le recours aux encodages de circuits booléens, aux corps finis de grande taille (pour prévenir le dépassement de capacité) et aux grandes tables de recherche précalculées, qui sont communes dans les travaux antérieurs.
• Absence de Pré-traitement : Contrairement aux approches basées sur R1CS ou les circuits arithmétiques, la méthode ne nécessite aucun surcoût de pré-traitement ou d'encodage.
• Praticité : En ne nécessitant pas l'agrandissement du corps fini pour éviter le dépassement de capacité, le schéma reste pratique pour des nombres premiers de taille cryptographique.

Résultats Expérimentaux
Les auteurs ont évalué l'algorithme proposé sur un réseau de neurones linéaire et une étude de cas impliquant un réseau entièrement connecté à quatre couches entraîné sur le jeu de données MNIST (utilisant 6 bits entiers et 8 bits fractionnaires).

• Comparaison de Performance : Comparée à la méthode de pointe [20] (qui manque de support pour ReLU et nécessite l'agrandissement du corps), Range-Arithmetic a démontré une performance supérieure à mesure que le nombre de couches du réseau augmentait.
• Métriques : La méthode proposée a réduit le coût computationnel pour le prouveur et le vérificateur, ainsi que la surcharge de communication.
• Spécificités : Dans l'étude de cas MNIST, le temps d'exécution du prouveur était d'environ 230 millisecondes, et le temps d'exécution du vérificateur d'environ 154 millisecondes.
• Scalabilité : À mesure que les tailles de matrices augmentaient, le coût de communication croissait de manière logarithmique, tandis que les temps d'exécution du prouveur et du vérificateur suivaient une croissance polynomiale.

Signification et Revendications
Le papier positionne Range-Arithmetic comme offrant le "compromis le plus équilibré" entre l'effort du prouveur, le coût du vérificateur, la communication et l'exhaustivité des fonctionnalités pour l'inférence de DNN vérifiable par des parties non fiables. Les auteurs soulignent que, bien que les méthodes basées sur la recherche (lookup-based) puissent être plus rapides pour la vérification pure de ReLU, leur exigence de grandes tables auxiliaires les rend peu pratiques pour les vérificateurs aux ressources limitées. Range-Arithmetic remplace ces tables par des preuves de plage légères, offrant une solution plus générale et efficace pour les contraintes spécifiques des systèmes de ML décentralisés. Ce travail vise à faciliter les applications d'IA de confiance et autonomes dans des environnements ouverts et dynamiques en permettant la vérification efficace d'opérations de ML complexes et non arithmétiques sans réexécution.