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

Resumo Técnico: Aritmética de Intervalo – Inferência de Aprendizado Profundo Verificável em uma Parte Não Confiável

Problema
Sistemas de aprendizado de máquina (ML) descentralizados dependem cada vez mais da delegação de tarefas intensivas em recursos, como a inferência de redes neurais profundas (DNN), para partes externas não confiáveis (provadores) para superar as limitações de blockchain. Um desafio crítico neste paradigma é garantir a integridade dessas computações delegadas sem exigir que o verificador reexecute todo o processo, o que é frequentemente proibitivamente caro.

As técnicas existentes de Computação Verificável (VC) enfrentam obstáculos significativos quando aplicadas ao ML. A maioria dos esquemas de VC opera sobre corpos finitos e é restrita a operações aritméticas (adições e multiplicações). No entanto, as computações padrão de ML envolvem operações não aritméticas, especificamente:

1. Arredondamento de ponto fixo: Necessário após multiplicações de matrizes para gerenciar a precisão e evitar o transbordamento (overflow).
2. Funções de ativação não lineares: Como a ReLU (Unidade Linear Retificada).

Representar essas operações dentro de estruturas convencionais de VC frequentemente exige codificações complexas de circuitos booleanos, polinômios de alto grau ou grandes tabelas de consulta (lookup tables) pré-computadas. Essas abordagens introduzem um overhead substancial no esforço do provador, no custo do verificador e na largura de banda de comunicação, ou falham em suportar operações essenciais como ReLU e arredondamento simultaneamente.

Metodologia: O Framework de Aritmética de Intervalo (Range-Arithmetic)
Os autores propõem o Range-Arithmetic, um novo framework projetado para verificar a inferência de DNN de forma eficiente, mantendo a compatibilidade com sistemas de prova baseados em corpos finitos. A inovação central reside na transformação de operações não aritméticas em etapas aritméticas verificáveis via protocolos sum-check e provas de intervalo concatenadas, evitando codificações booleanas e grandes tabelas de consulta.

O framework opera através dos seguintes mecanismos:

1. Verificação de Multiplicação de Matrizes:
   A verificação da multiplicação de matrizes ($C = AB$) é reformulada como um problema de sum-check. Ao representar os elementos da matriz como Extensões Multilineares (MLEs) sobre um corpo finito, a correção do produto é reduzida à verificação de uma identidade polinomial. Os autores utilizam o lema de Schwartz-Zippel para verificar essa identidade em pontos aleatórios, empregando o protocolo sum-check para reduzir a complexidade de comunicação para $O(\log n)$.

2. Verificação de Arredondamento:
   Para verificar a operação de arredondamento $R(x)$ aplicada após a multiplicação, os autores decompõem o processo em restrições aritméticas. Eles definem a parte descartada do arredondamento ($E$) e o numerador da fração de arredondamento ($D$). A correção é garantida provando duas condições via provas de intervalo agregadas:

   • Os bits descartados residem dentro de um intervalo pequeno específico ($-2^{s-1} \leq e_i < 2^{s-1}$).
   • O valor restante é um múltiplo inteiro de $2^s$ sem transbordamento (wrap-around).
     Esta abordagem permite que o arredondamento seja verificado usando provas de intervalo padrão sem exigir corpos finitos grandes para evitar o transbordamento.

3. Verificação de ReLU:
   A função ReLU, definida como $\text{ReLU}(x) = \max(0, x) = (x + |x|)/2$, é verificada por:

   • Provar que o valor absoluto $Y = |A|$ é não negativo usando uma prova de intervalo.
   • Provar que $a_i^2 = y_i^2$ para todos os elementos usando um protocolo sum-check no polinômio $f(x) = \tilde{I}(s, x)(\tilde{a}^2(x) - \tilde{y}^2(x))$.
   • Verificar a combinação linear final $B = (A + Y)/2$.

4. Composição:
   O framework trata a inferência de redes neurais como uma sequência de camadas. Cada camada (multiplicação de matriz com arredondamento ou ativação ReLU) é verificada de forma independente. O compromisso (commitment) de saída de uma camada serve como entrada para a próxima, permitindo a composição modular de algoritmos de verificação sem a retransmissão de grandes matrizes intermediárias.

Principais Contribuições
O artigo reivindica as seguintes contribuições específicas:

• Framework Unificado: O Range-Arithmetic é o primeiro método a alcançar simultaneamente complexidade de provador de $O(n^3)$, complexidade de verificador de $O(n^2)$ e complexidade de comunicação de $O(\log n)$, enquanto suporta arredondamento de ponto fixo e ReLU.
• Eliminação de Overhead: A abordagem evita a necessidade de codificações de circuitos booleanos, corpos finitos grandes (para evitar transbordamento) e grandes tabelas de consulta pré-computadas, comuns em trabalhos anteriores.
• Sem Pré-processamento: Diferente das abordagens baseadas em R1CS ou circuitos aritméticos, o método não requer overhead de pré-processamento ou codificação.
• Praticidade: Ao não exigir o aumento do corpo finito para evitar o transbordamento, o esquema permanece prático para primos de tamanho criptográfico.

Resultos Experimentais
Os autores avaliaram o algoritmo proposto em uma rede neural linear e um estudo de caso envolvendo uma rede totalmente conectada de quatro camadas treinada no conjunto de dados MNIST (usando 6 bits inteiros e 8 bits fracionários).

• Comparação de Desempenho: Comparado ao método de última geração [20] (que carece de suporte a ReLU e exige aumento de corpo), o Range-Arithmetic demonstrou desempenho superior à medida que o número de camadas da rede aumentava.
• Métricas: O método proposto reduziu o custo computacional tanto para o provador quanto para o verificador, e diminuiu o overhead de comunicação.
• Especificidades: No estudo de caso MNIST, o tempo de execução do provador foi de aproximadamente 230 milissegundos e o tempo de execução do verificador foi de aproximadamente 154 milissegundos.
• Escalabilidade: À medida que o tamanho das matrizes aumentava, o custo de comunicação crescia logaritmicamente, enquanto os tempos de execução do provador e do verificador escalavam polinomialmente.

Significância e Alegações
O artigo posiciona o Range-Arithmetic como provedor do "equilíbrio mais equilibrado" entre esforço do provador, custo do verificador, comunicação e completude de recursos para a inferência de DNN verificável em partes não confiáveis. Os autores enfatizam que, embora os métodos baseados em consulta (lookup-based) possam ser mais rápidos para a verificação pura de ReLU, sua exigência de grandes tabelas auxiliares os torna impraticáveis para verificadores com recursos limitados. O Range-Arithmetic substitui essas tabelas por provas de intervalo leves, oferecendo uma solução mais geral e eficiente para as restrições específicas de sistemas de ML descentralizados. O trabalho visa facilitar aplicações de IA confiáveis e autônomas em ambientes abertos e dinâmicos, permitindo a verificação eficiente de operações de ML complexas e não aritméticas sem reexecução.