Resumo Técnico: Verificação de Redes Neurais de Ponto Flutuante ao Nível de Software
Declaração do Problema
Embora a verificação de redes neurais tenha avançado significativamente ao fornecer garantias formais para modelos idealizados de valores reais, essas abordagens frequentemente falham em considerar os detalhes específicos de implementação de sistemas implantados. Em aplicações críticas de segurança (ex: CPS, IoT), as redes neurais são implementadas usando aritmética de ponto flutuante de precisão finita (tipicamente IEEE 754 de 32 bits) e dependem de bibliotecas matemáticas padrão (ex: math.h). Esses detalhes de baixo nível introduzem erros de arredondamento e comportamentos não associativos que podem invalidar provas de segurança derivadas de modelos de precisão infinita. Por exemplo, o artigo demonstra que a função de ativação SoftSign, que é não-decrescente em aritmética real, deixa de sê-lo quando implementada em ponto flutuante de 32 bits.
Tentativas existentes de verificar código de redes neurais ao nível de software produziram resultados mistos. Verificadores de software frequentemente lutam para escalar para grandes instâncias de redes neurais, forçando os praticantes a retornar a modelos de precisão infinita não confiáveis ou a abandonar a verificação em favor de testes. Além disso, observou-se que ferramentas existentes produzem resultados incorretos em certas configurações, lançando dúvidas sobre sua confiabilidade como oráculos de segurança para implementações de ponto flutuante. Há uma falta de avaliação rigorosa e padronizada de verificadores de software automatizados especificamente em código de redes neurais.
Metodologia
Para abordar essas lacunas, os autores conduziram uma avaliação rigorosa de oito verificadores de software automatizados de última geração em código de redes neurais. A metodologia envolveu três componentes primários:
Construção de Benchmark (NeuroCodeBench 2.0): Os autores construíram um benchmark abrangente composto por 912 exemplos de verificação. Este benchmark cobre:
- Funções Matemáticas: 58 instâncias testando propriedades (ex: monotonicidade, periodicidade, limites lineares) de funções padrão da
math.h.
- Funções de Ativação: 57 instâncias testando propriedades de ativações comuns (ex: ReLU, TanH, SoftSign, GELU).
- Camadas Neurais: 86 instâncias cobrindo transformações afins, normalização, pooling e camadas SoftMax.
- Redes Neurais Completas: 711 instâncias incluindo redes de Hopfield, redes ReLU codificadas por SAT, redes de aproximação polinomial, redes com limite de Lipschitz e redes derivadas de VNN-COMP (tarefas de Densidade de Probabilidade e Aprendizado por Reforço).
- Verdade Fundamental (Ground Truth): Cada instância é pré-rotulada como "segura" ou "insegura" usando técnicas como teste de força bruta, construção exaustiva ou geração de contraexemplos, garantindo um veredito correto conhecido para avaliação.
Padronização e Compatibilidade: Para garantir uma comparação justa e reprodutibilidade, os autores converteram todas as instâncias do benchmark para o formato usado pela Competição Internacional de Verificação de Software (SV-COMP). Isso envolveu a criação de arquivos C autossuficientes que incluem a implementação do modelo, propriedades de segurança e dependências necessárias. O fluxo de trabalho utilizou o framework BenchExec para gerenciar limites de recursos e execução, garantindo que as ferramentas fossem executadas com as mesmas configurações usadas na edição de 2024 do SV-COMP.
Avaliação Experimental: O estudo avaliou oito ferramentas (2LS, CBMC, CPAChecker, DIVINE, ESBMC, PeSCo, Pinaka, UAutomizer) sob duas condições:
- Baseline: Execução de verificadores nas instâncias puras do benchmark.
- Modelos Operacionais: Fornecimento de implementações explícitas da biblioteca
math.h (usando MUSL e CORE-MATH) para observar se o fornecimento das definições de função melhora os resultados de verificação.
- Análise Histórica: Os autores também analisaram o desempenho histórico de uma ferramenta (ESBMC) de 2018 a 2026 para observar tendências no campo.
Principais Contribuições
- NeuroCodeBench 2.0: A criação de um benchmark de grande escala e verdade fundamental especificamente projetado para a verificação de nível de software de redes neurais de ponto flutuante. Inclui 912 instâncias que variam de funções simples a redes completas com até 170 mil parâmetros.
- Integração com SV-COMP: O benchmark foi formatado para ser compatível com a infraestrutura do SV-COMP, tornando-o parte do conjunto oficial de benchmarks para a edição de 2026. Isso permite a avaliação automatizada e reprodutível usando configurações de ferramentas padrão.
- Avaliação Rigorosa: O primeiro estudo sistemático comparando oito verificadores de software de última geração em código de redes neurais, revelando uma variação significativa de desempenho e correção.
- Análise de Modelos Operacionais: Uma investigação sobre se o fornecimento de implementações explícitas de bibliotecas matemáticas (MUSL, CORE-MATH) melhora o desempenho do verificador, descobrindo que o impacto é dependente da ferramenta e frequentemente negligenciável ou negativo.
Resultados
A avaliação rendeu várias descobertas críticas sobre o estado atual da verificação de software para redes neurais:
- Baixa Correção e Escalabilidade: Os resultados foram descritos como "bastante decepcionantes". As ferramentas exibiram uma grande variação através do benchmark, com a ferramenta de melhor desempenho (CBMC) resolvendo 371 de 912 instâncias corretamente, enquanto outras resolveram significativamente menos. A taxa média de solução entre categorias variou, com algumas categorias complexas (ex: Aprendizado por Reforço) apresentando taxas de solução de apenas 3%. A maioria das ferramentas falhou em verificar mais de uma única camada por vez.
- Vereditos Incorretos: Diversas ferramentas produziram uma alta taxa de resultados incorretos. Por exemplo, o CBMC produziu quase 25% de vereditos definitivos incorretos (principalmente falsos positivos), e o Pinaka e o UAutomizer também mostraram taxas de erro significativas. Apenas o ESBMC não produziu vereditos incorretos entre as ferramentas que resolveram um número substancial de instâncias.
- Impacto de Modelos Operacionais: O fornecimento de implementações explícitas de
math.h (MUSL ou CORE-MATH) não levou a melhorias visíveis no geral. Para algumas ferramentas (CBMC, ESBMC, Pinaka), o desempenho na verdade diminuiu devido à complexidade adicional de verificar o código da biblioteca. Para outras (CPAChecker, PeSCo), o número de instâncias resolvidas aumentou, mas isso frequentemente veio acompanhado de um surto de vereditos incorretos.
- Limites de Escalabilidade: As ferramentas tiveram dificuldades significativas com redes neurais completas. A taxa de solução caiu para dígitos únicos em categorias complexas como Aprendizado por Reforço e Densidade de Probabilidade. Mesmo para redes sintéticas, ferramentas como o ESBMC só conseguiam resolver instâncias com larguras muito pequenas (ex: largura 4) antes de sofrerem timeout.
- Progresso Histórico: A análise do ESBMC de 2018 a 2026 mostrou melhorias não monótonas, mas geralmente constantes. Um pico notável de vereditos incorretos em 2022-2023 foi rastreado até um erro de implementação em um algoritmo de k-indução, que foi corrigido após o lançamento do NeuroCodeBench 1.0 anterior. A introdução do NeuroCodeBench 1.0 em 2024 levou a uma redução drástica de vereditos incorretos em toda a comunidade, embora o impacto do NeuroCodeBench 2.0 (final de 2025) tenha sido mais moderado.
Significância e Alegações
O artigo alega que, embora a verificação de redes neurais ao nível de software seja conceitualmente viável, os atuais verificadores de software de última geração ainda não estão prontos para lidar com essa tarefa de forma eficaz. O estudo destaca que as ferramentas atuais não conseguem verificar confiavelmente mais de uma única camada, frequentemente retornam resultados incorretos e carecem de suporte total para bibliotecas matemáticas padrão.
Os autores argumentam que seu trabalho serve como um necessário "choque de realidade" para a comunidade de verificação. Ao fornecer um benchmark rigoroso com verdade fundamental conhecida, eles demonstram que o gap entre a verificação idealizada e a implementação de software é atualmente amplo demais para que as ferramentas existentes o atravessem sem melhorias significativas. O artigo postula que o lançamento do NeuroCodeBench já estimulou o progresso, evidenciado pela redução de vereditos incorretos após seu lançamento inicial. No entanto, os autores concluem que certificar a implementação completa de redes neurais contra desvios numéricos de pior caso continua sendo um desafio de longo prazo que requer suporte nativo para bibliotecas matemáticas e procedimentos de decisão customizados adaptados para aritmética de ponto flutuante.