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

Resumen Técnico: Aritmética de Rango – Inferencia de Aprendizaje Profundo Verificable en una Parte No Confiable

Planteamiento del Problema
Los sistemas de aprendizaje automático (ML) descentralizados dependen cada vez más de la delegación de tareas intensivas en recursos, como la inferencia de redes neuronales profundas (DNN), a partes externas no confiables (probadores) para superar las limitaciones de la cadena de bloques. Un desafío crítico en este paradigma es garantizar la integridad de estas computaciones delegadas sin requerir que el verificador reejecute todo el proceso, lo cual suele ser prohibitivamente costoso.

Las técnicas de Computación Verificable (VC) existentes enfrentan obstáculos significativos cuando se aplican al ML. La mayoría de los esquemas de VC operan sobre campos finitos y están restringidos a operaciones aritméticas (sumas y multiplicaciones). Sin embargo, las computaciones estándar de ML involucran operaciones no aritméticas, específicamente:

1. Redondeo de punto fijo: Requerido después de las multiplicaciones de matrices para gestionar la precisión y prevenir el desbordamiento (overflow).
2. Funciones de activación no lineales: Como ReLU (Unidad Lineal Rectificada).

Representar estas operaciones dentro de los marcos de VC convencionales a menudo requiere codificaciones de circuitos booleanos complejas, polinomios de alto grado o tablas de búsqueda precomputadas de gran tamaño. Estos enfoques introducen un sobrecosto sustancial en el esfuerzo del probador, el costo del verificador y el ancho de banda de comunicación, o bien fallan al intentar soportar operaciones esenciales como ReLU y el redondeo simultáneamente.

Metodología: El Marco de Trabajo de Aritmética de Rango
Los autores proponen Range-Arithmetic (Aritmética de Rango), un nuevo marco diseñado para verificar la inferencia de DNN de manera eficiente manteniendo la compatibilidad con los sistemas de prueba basados en campos finitos. La innovación central radica en transformar las operaciones no aritméticas en pasos aritméticos verificables mediante protocolos de sum-check y pruebas de rango concatenadas, evitando así las codificaciones booleanas y las tablas de búsqueda de gran tamaño.

El marco opera a través de los siguientes mecanismos:

1. Verificación de la Multiplicación de Matrices:
   La verificación de la multiplicación de matrices ($C = AB$) se reformula como un problema de sum-check. Al representar los elementos de la matriz como Extensiones Multilineales (MLE) sobre un campo finito, la corrección del producto se reduce a la verificación de una identidad polinómica. Los autores utilizan el lema de Schwartz-Zippel para verificar esta identidad en puntos aleatorios, empleando el protocolo sum-check para reducir la complejidad de comunicación a $O(\log n)$.

2. Verificación del Redondeo:
   Para verificar la operación de redondeo $R(x)$ aplicada después de la multiplicación, los autores descomponen el proceso en restricciones aritméticas. Definen la parte descartada del redondeo ($E$) y el numerador de la fracción de redondeo ($D$). La corrección se asegura probando dos condiciones mediante pruebas de rango agregadas:

   • Los bits descartados se encuentran dentro de un intervalo pequeño específico ($-2^{s-1} \leq e_i < 2^{s-1}$).
   • El valor restante es un múltiplo entero de $2^s$ sin desbordamiento (wrap-around).
     Este enfoque permite que el redondeo sea verificado utilizando pruebas de rango estándar sin requerir campos finitos grandes para prevenir el desbordamiento.

3. Verificación de ReLU:
   La función ReLU, definida como $\text{ReLU}(x) = \max(0, x) = (x + |x|)/2$, se verifica:

   • Probando que el valor absoluto $Y = |A|$ es no negativo usando una prueba de rango.
   • Probando que $a_i^2 = y_i^2$ para todos los elementos usando un protocolo sum-check sobre el polinomio $f(x) = \tilde{I}(s, x)(\tilde{a}^2(x) - \tilde{y}^2(x))$.
   • Verificando la combinación lineal final $B = (A + Y)/2$.

4. Composición:
   El marco trata la inferencia de redes neuronales como una secuencia de capas. Cada capa (multiplicación de matrices con redondeo o activación ReLU) se verifica de forma independiente. El compromiso de salida (output commitment) de una capa sirve como entrada para la siguiente, permitiendo la composición modular de algoritmos de verificación sin retransmitir matrices intermedias de gran tamaño.

Contribuciones Clave
El artículo reclama las siguientes contribuciones específicas:

• Marco Unificado: Range-Arithmetic es el primer método que logra simultáneamente una complejidad de probador de $O(n^3)$, una complejidad de verificador de $O(n^2)$ y una complejidad de comunicación de $O(\log n)$ mientras soporta tanto el redondeo de punto fijo como ReLU.
• Eliminación de Sobrecosto: El enfoque evita la necesidad de codificaciones de circuitos booleanos, campos finitos grandes (para prevenir el desbordamiento) y tablas de búsqueda precomputadas de gran tamaño, que son comunes en trabajos previos.
• Sin Preprocesamiento: A diferencia de los enfoques basados en R1CS o circuitos aritméticos, el método no requiere preprocesamiento ni sobrecarga de codificación.
• Practicidad: Al no requerir el agrandamiento del campo finito para evitar el desbordamiento, el esquema sigue siendo práctico para primos de tamaño criptográfico.

Resultados Experimentales
Los autores evaluaron su algoritmo propuesto en una red neuronal lineal y un caso de estudio que involucra una red totalmente conectada de cuatro capas entrenada con el conjunto de datos MNIST (usando 6 bits enteros y 8 bits fraccionarios).

• Comparación de Desempeño: En comparación con el método de vanguardia [20] (que carece de soporte para ReLU y requiere el agrandamiento del campo), Range-Arithmetic demostró un desempeño superior a medida que aumentaba el número de capas de la red.
• Métricas: El método propuesto redujo el costo computacional tanto para el probador como para el verificador, y disminuyó la sobrecarga de comunicación.
• Especificaciones: En el caso de estudio de MNIST, el tiempo de ejecución del probador fue de aproximadamente 230 milisegundos y el tiempo de ejecución del verificador fue de aproximadamente 154 milisegundos.
• Escalabilidad: A medida que aumentaban los tamaños de las matrices, el costo de comunicación crecía logarítmicamente, mientras que los tiempos de ejecución del probador y del verificador escalaban polinómicamente.

Significancia y Reivindicaciones
El artículo posiciona a Range-Arithmetic como un proveedor del "equilibrio más balanceado" entre el esfuerzo del probador, el costo del verificador, la comunicación y la completitud de funciones para la inferencia de DNN verificable en partes no confiables. Los autores enfatizan que, si bien los métodos basados en búsquedas (lookup-based) pueden ser más rápidos para la verificación pura de ReLU, su requerimiento de tablas auxiliares de gran tamaño los hace poco prácticos para verificadores con recursos limitados. Range-Arithmetic reemplaza estas tablas con pruebas de rango ligeras, ofreciendo una solución más general y eficiente para las restricciones específicas de los sistemas de ML descentralizados. El trabajo tiene como objetivo facilitar aplicaciones de IA confiables y autónomas en entornos abiertos y dinámicos al permitir la verificación eficiente de operaciones de ML complejas y no aritméticas sin necesidad de reejecución.