🤖 machine learning

The Complexity of Verifying Feedforward Neural Networks in Quantised Settings

Este artigo estabelece o panorama da complexidade computacional para a verificação de redes neurais feedforward em contextos quantizados, demonstrando que a verificação permanece NP-completa para redes com precisão aritmética fixa sob especificações lineares e de vetores de bits, ao mesmo tempo que fornece novos limites superiores para redes quantizadas dinamicamente sob especificações de vetores de bits.

Autores originais: Eric Alsmann, Martin Lange, Marco Sälzer

Publicado 2026-05-29

📖 5 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Eric Alsmann, Martin Lange, Marco Sälzer

Artigo original sob licença CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo

Imagine que você tem um robô muito inteligente (uma Rede Neural Feedforward) que toma decisões, como reconhecer um gato em uma foto ou dirigir um carro autônomo. Antes de soltar esse robô no mundo real, precisamos ter 100% de certeza de que ele não cometerá um erro perigoso. Esse processo é chamado de verificação.

Por muito tempo, cientistas tentaram verificar esses robôs fingindo que eram feitos de matemática perfeita, de precisão infinita (como usar uma régua que pode medir até o tamanho de um átomo, para sempre). Mas, no mundo real, os computadores não são perfeitos. Eles usam aritmética quantizada, que é como usar uma régua que tem marcas apenas a cada milímetro. Você precisa arredondar as coisas e, às vezes, fica sem espaço (estouro).

Este artigo faz uma grande pergunta: A troca de "matemática perfeita" para "matemática real, arredondada" torna muito mais difícil provar que o robô é seguro?

Aqui está a análise de suas descobertas, usando algumas analogias do cotidiano:

1. Os Três Tipos de Robôs

Os autores examinaram três maneiras diferentes de esses robôs serem construídos:

O Robô Ideal (RNN Racional): Construído com matemática perfeita, de precisão infinita.
O Robô Pré-Quantizado (RNN Quantizada): Construído desde o início usando a "régua de milímetro" (matemática de largura finita).
O Robô Convertido (Quantizado Dinamicamente): Um robô perfeito que nós forçamos a usar a "régua de milímetro" depois que ele já foi treinado.

2. Os Dois Tipos de Regras de Segurança

Para verificar se o robô é seguro, damos a ele regras. O artigo examina dois tipos de livros de regras:

Regras Lineares (LP): São regras simples, de linha reta. Pense nelas como um sinal de trânsito dizendo: "Se a velocidade for inferior a 50, você está seguro". Essas regras são fáceis de visualizar como uma forma suave e convexa.
Regras de Vetor de Bits (BV): São regras complexas, em nível de bit. Pense nelas como um sistema de segurança que verifica interruptores específicos dentro do cérebro do computador. "Se o bit 3 estiver ligado E o bit 7 estiver desligado, mas o bit 2 estiver ligado, então é um problema". Elas podem descrever formas muito irregulares, complexas e não lineares.

3. As Principais Descobertas: É Mais Difícil?

Cenário A: Regras Simples (Restrições Lineares)

O Resultado: Não, não é mais difícil.
Seja o robô perfeito ou use a "régua de milímetro", e sejam as regras simples ou complexas, verificar a segurança permanece NP-completo.

A Analogia: Imagine tentar encontrar uma chave específica em uma gaveta gigante e bagunçada. Se as chaves forem feitas de ouro (matemática perfeita) ou plástico (matemática arredondada), e se a gaveta estiver organizada ou caótica, a dificuldade de encontrar a chave não muda. Ainda é um problema "difícil", mas é do mesmo nível de dificuldade de antes.
Por que isso importa: Significa que não precisamos inventar computadores inteiramente novos e superpoderosos para verificar robôs do mundo real. As ferramentas que já temos para matemática perfeita podem ser adaptadas para matemática do mundo real sem ficar exponencialmente mais lentas.

Cenário B: Regras Complexas (Restrições de Vetor de Bits)

O Resultado: Depende do "tamanho do cérebro" do robô.

Se o robô já foi construído com a "régua de milímetro": Verificar a segurança ainda é NP-completo (mesma dificuldade de antes).
Se pegarmos um robô perfeito e o forçarmos a usar a "régua de milímetro" (Quantização Dinâmica): Isso fica muito mais difícil. Salta para PSPACE-completo.
- A Analogia: Imagine que você tem uma receita perfeita (o robô perfeito). Agora, você precisa cozinhar em uma cozinha minúscula com um conjunto específico e limitado de panelas e frigideiras (a aritmética de largura finita). Se você usar as panelas limitadas desde o início, está tudo bem. Mas se tentar traduzir a receita perfeita para a cozinha limitada enquanto cozinha, o número de maneiras possíveis de as coisas darem errado explode. Você precisa acompanhar tantos cenários "e se" (como alinhar números de tamanhos diferentes) que a memória necessária para verificar todos eles cresce massivamente.

4. O Mistério dos Números de Ponto Flutuante

O artigo também examinou números de ponto flutuante (a maneira padrão como os computadores lidam com decimais, como 3,14).

Expoente Fixo: Se o intervalo de números for fixo (como uma régua com um comprimento máximo fixo), a dificuldade permanece gerenciável (PSPACE).
Ponto Flutuante Geral: Se o intervalo puder mudar drasticamente, a dificuldade pode saltar ainda mais alto (NEXPTIME).
A Analogia: Na matemática de ponto flutuante, os números podem ser muito pequenos ou muito grandes. Para somá-los, o computador precisa primeiro "alinhar" eles (como alinhar vírgulas decimais). Se os números forem de tamanhos muito diferentes, o computador precisa armazenar uma enorme quantidade de dados para fazer esse alinhamento. Os autores descobriram que essa etapa de "alinhamento" é o que torna o problema potencialmente muito, muito mais difícil de resolver.

Resumo

O artigo essencialmente diz:

Boas Notícias: Para o tipo mais comum de verificação de segurança (regras lineares), a troca para matemática do mundo real, arredondada, não torna o trabalho impossível. Ainda é do mesmo nível de dificuldade da matemática perfeita teórica.
Más Notícias: Se você estiver usando regras muito complexas, em nível de bit, em um robô perfeito que você está forçando a usar matemática arredondada, o trabalho torna-se significativamente mais difícil (PSPACE).
O Desconhecido: Se você usar matemática de ponto flutuante padrão com intervalos selvagens, o trabalho pode ser ainda mais difícil, mas os autores não têm 100% de certeza ainda; eles apenas sabem que é pelo menos tão difícil quanto o nível "PSPACE".

Em resumo: A quantização (arredondamento) não quebra a verificação para regras simples, mas torna cenários complexos e dinâmicos muito mais custosos computacionalmente.

Resumo Técnico: A Complexidade da Verificação de Redes Neurais Feedforward em Cenários Quantizados

Declaração do Problema

O artigo investiga a complexidade computacional da verificação formal de Redes Neurais Feedforward (FNNs) em cenários quantizados. Embora o problema de alcançabilidade para FNNs operando sobre aritmética de valores reais (pesos racionais) seja estabelecido como NP-completo, implementações práticas dependem de aritmética de largura finita (por exemplo, números de ponto flutuante de 64 bits ou números de ponto fixo). Essa transição introduz efeitos de quantização, como arredondamento, overflow e underflow.

Os autores abordam uma lacuna potencial de compreensão: a mudança da aritmética de valores reais idealizada para a aritmética discreta de largura finita aumenta a complexidade computacional da verificação? Além disso, eles examinam como a complexidade muda com base em:

Formalismos de Especificação: Restrições de Programação Linear (LP) versus lógicas de Vetor de Bits (BV) (que permitem raciocínio não linear e em nível de bit).
Definição da Rede: Se a FNN é definida com pesos racionais exatos (FNN Racional) ou pesos pré-quantizados (FNN Quantizada).
Codificação de Parâmetros: Se a largura de bits da aritmética é fornecida como parte da entrada em unário (realista para tamanhos de registradores de hardware) ou binária (realista para especificações decimais).

Metodologia

Os autores formalizam cinco problemas distintos de decisão de alcançabilidade, denotados como REACH, variando conforme o tipo de aritmética e a linguagem de especificação:

REACHQ(LP): FNNs Racionais com especificações LP (cenário padrão).
REACHF(LP): FNNs Quantizadas (pesos já em aritmética de largura finita) com especificações LP.
REACHF(BV): FNNs Quantizadas com especificações de Vetor de Bits.
REACH(F, LP): FNNs Racionais onde a aritmética de largura finita alvo $F$ faz parte da entrada (quantização dinâmica) com especificações LP.
REACH(F, BV): FNNs Racionais com quantização dinâmica e especificações de Vetor de Bits.

Abordagem Analítica:

Limites Inferiores de Complexidade: Os autores utilizam reduções de problemas conhecidos como difíceis (por exemplo, 3SAT) para estabelecer NP-dificuldade e PSPACE-dificuldade. Eles demonstram que os "dispositivos" (gadgets) padrão usados para codificar lógica booleana em FNNs (usando ativações ReLU) permanecem válidos mesmo sob aritmética de largura finita, desde que a aritmética possa representar inteiros pequenos e frações como $1/2$ .
Limites Superiores de Complexidade:
- Para especificações LP, os autores baseiam-se no limite polinomial dos tamanhos de solução na programação linear (Teorema 1) para mostrar que uma testemunha (vetor de entrada) pode ser adivinhada e verificada em tempo polinomial.
- Para especificações BV com quantização dinâmica, os autores empregam Autômatos Finitos Não Determinísticos Succintos (NFA). Eles constroem autômatos que representam a relação entrada-saída da FNN quantizada e as fórmulas de especificação. O espaço de estados desses autômatos é exponencialmente grande, mas descrito de forma compacta (sucidamente).
- Eles distinguem entre aritmética de ponto fixo e ponto flutuante. Para ponto flutuante, eles observam que a aritmética geral requer deslocamentos de alinhamento que dependem da diferença de expoentes. Se a largura do expoente for ilimitada (fornecida em binário), o tamanho do buffer de alinhamento torna-se exponencial, potencialmente quebrando os limites PSPACE. Eles restringem suas provas de limite superior PSPACE a casos onde a largura do expoente é constante.

Contribuições e Resultados Chave

O artigo estabelece uma paisagem de complexidade abrangente, resumida na Tabela 1 do texto:

1. Especificações de Programação Linear (LP)

REACHQ(LP): Reafirmado como NP-completo (citando Sälzer e Lange, 2021).
REACHF(LP): Provado NP-completo. Os autores mostram que, mesmo com pesos pré-quantizados, o problema permanece em NP porque o tamanho da entrada da testemunha é polinomial em relação ao tamanho da rede.
REACH(F, LP): Provado NP-completo. Mesmo quando os parâmetros de largura de bits fazem parte da entrada (quantização dinâmica), o problema permanece NP-completo. Os autores argumentam que o tamanho da testemunha permanece limitado polinomialmente em relação ao tamanho da entrada, independentemente de as larguras de bits serem codificadas em unário ou binário.

2. Especificações de Vetor de Bits (BV)

REACHF(BV): Provado NP-completo. Para redes já quantizadas, o uso da lógica de vetor de bits não aumenta a complexidade além de NP.
REACH(F, BV) (Ponto fixo e Ponto flutuante com largura de expoente constante): Provado PSPACE-completo.
- Limite Inferior: Corresponde ao resultado de PSPACE-dificuldade estabelecido anteriormente por Henzinger et al. (2021).
- Limite Superior: Os autores fornecem o primeiro limite superior PSPACE correspondente. Eles alcançam isso reduzindo o problema ao problema de não vazio de NFAs representados de forma sucinta.
REACH(F, BV) (Ponto flutuante Geral): O problema é PSPACE-difícil e reside dentro de NEXPTIME.
- Os autores observam que, para aritmética de ponto flutuante geral (onde a largura do expoente é variável e fornecida em binário), a etapa de alinhamento na adição/multiplicação requer um tamanho de buffer que depende da diferença de expoentes. Isso impede a construção de um NFA sucinto com tamanho de descrição polinomial, deixando o limite superior exato aberto (atualmente NEXPTIME).

Significado e Alegações

O artigo afirma resolver um "mal-entendido generalizado" regarding a complexidade da verificação de FNNs quantizadas, abordando especificamente os resultados de Henzinger et al. (2021).

Esclarecimento dos Motores de Complexidade: Os autores argumentam que o salto de NP para PSPACE observado em trabalhos anteriores não é causado pela própria quantização, mas pela combinação de quantização dinâmica (onde a aritmética faz parte da entrada) e o uso de especificações de Vetor de Bits. Para especificações lineares padrão, a quantização não aumenta a classe de complexidade; ela permanece NP-completa.
Viabilidade de Ferramentas: Os resultados sugerem que o desenvolvimento de ferramentas de verificação sólidas para FNNs quantizadas usando especificações lineares é viável sem sobrecarga assintótica em comparação com solvers de valores reais existentes, pois ambos permanecem NP-completos.
Limites Superiores para BV: O artigo complementa a conhecida PSPACE-dificuldade da verificação quantizada dinâmica com especificações BV estabelecendo PSPACE-completude para aritmética de ponto fixo e ponto flutuante com expoente limitado.
Problemas Abertos: Os autores modestamente identificam que, para aritmética de ponto flutuante geral com expoentes ilimitados, o requisito de alinhamento pode empurrar o problema além de PSPACE (para NEXPTIME), e permanece uma questão em aberto se um limite inferior correspondente pode ser provado.

Em conclusão, o artigo fornece uma classificação rigorosa mostrando que, embora especificações de vetor de bits em redes dinamicamente quantizadas introduzam complexidade PSPACE, o caso padrão de restrições lineares em redes quantizadas mantém a NP-completude do caso racional.