🤖 machine learning

VNN-LIB 2.0: Rigorous Foundations for Neural Network Verification

Este artigo apresenta o VNN-LIB 2.0, um padrão rigorosamente formalizado para verificação de redes neurais que introduz uma abstração de "teoria de redes" para desacoplar a especificação dos modelos ONNX em evolução, ao mesmo tempo que fornece uma sintaxe precisa, um sistema de tipos e semântica mecanizados em Agda para garantir consistência interna e interoperabilidade.

Autores originais: Ann Roy, Allen Antony, Andrea Gimelli, Matthew L. Daggitt

Publicado 2026-05-11

📖 5 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Ann Roy, Allen Antony, Andrea Gimelli, Matthew L. Daggitt

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ê está tentando fazer uma equipe de robôs diferentes resolver um quebra-cabeça juntos. No mundo da Inteligência Artificial, esses "robôs" são redes neurais (os cérebros por trás da IA), e o "quebra-cabeça" é a verificação (verificar se a IA tomará uma decisão segura ou correta).

Por muito tempo, as pessoas que construíam esses robôs e as pessoas que os verificavam não falavam a mesma língua. Elas usavam um padrão chamado VNN-LIB 1.0, mas era como um dicionário com palavras faltando, sem regras gramaticais e definições que mudavam toda vez que alguém as olhava.

Este artigo apresenta o VNN-LIB 2.0, uma nova "língua" rigorosa que corrige esses problemas. Aqui está como os autores a explicam usando conceitos simples:

1. O Problema: Um Tradutor Quebrado

Pense no VNN-LIB 1.0 como um tradutor que tentava falar duas línguas ao mesmo tempo, mas ficava confuso.

Sem Gramática: Não havia regras estritas sobre como escrever uma pergunta. Assim, um robô podia entender uma frase de um jeito, e outro robô podia entendê-la de forma diferente.
Vocabulário Limitado: Ele só conseguia lidar com quebra-cabeças simples (uma entrada, uma saída). A IA do mundo real frequentemente tem entradas complexas (como uma imagem e algum texto) e múltiplas saídas.
Confusão de Ponto Flutuante: Computadores usam números "aproximados" (como 3,14159...), mas o padrão antigo não especificava se você deveria tratá-los como matemática exata ou aproximações grosseiras. Isso levou a erros perigosos onde um robô pensava que estava seguro, mas não estava.
O Problema da "Caixa Preta": O padrão antigo dependia de um formato de arquivo chamado ONNX (o projeto da IA). Mas o ONNX não tinha uma definição oficial e estrita do que seus símbolos significavam. Era como dar a um robô um projeto desenhado com giz de cera que muda de ideia toda hora sobre o que é uma "parede".

2. A Solução: A "Teoria de Redes" (O Adaptador Universal)

A maior inovação deste artigo é um conceito chamado Teoria de Redes.

Imagine que você está construindo um adaptador de energia universal. Você não quer construir um novo adaptador para cada tomada de parede de cada país (cada versão do ONNX). Em vez disso, você cria uma interface universal que diz: "Contanto que a tomada forneça eletricidade, voltagem e aterramento, eu posso conectar."

A Teoria de Redes ( $\Psi$ ): Esta é essa interface universal. Ela não se importa exatamente como o projeto do ONNX é desenhado. Ela apenas pergunta: "Você tem uma maneira de definir um número? Uma forma? Uma conexão?"
O Resultado: O VNN-LIB 2.0 agora pode conversar com qualquer versão do ONNX, mesmo as futuras, sem precisar ser reescrito. Ele separa a pergunta (a consulta) do projeto (o modelo), permitindo que eles evoluam independentemente.

3. A Nova Língua: VNN-LIB 2.0

Com essa nova base, os autores construíram uma língua muito mais inteligente com três principais melhorias:

Frases Mais Ricas (Sintaxe): Agora você pode perguntar sobre cenários complexos. Em vez de apenas verificar um robô, você pode perguntar: "Se o Robô A e o Robô B trabalharem juntos, eles permanecem seguros?" Você também pode espiar dentro do "cérebro" do robô para verificar seus pensamentos ocultos (camadas ocultas), não apenas a resposta final.
Gramática Estrita (Sistema de Tipos): A língua agora força você a ser preciso. Se você tentar adicionar uma "temperatura" a uma "cor", a língua dirá: "Não, isso não faz sentido." Isso impede que o computador cometa erros matemáticos ao misturar diferentes tipos de números.
Significado Claro (Semântica): Cada palavra na nova língua tem uma definição comprovada matematicamente. Não há palpites. Se você escrever uma consulta, o computador sabe exatamente qual problema matemático você está pedindo para ele resolver.

4. A Opção "Mundo Real" vs. "Matemática Perfeita"

O artigo reconhece uma situação complicada: Alguns robôs são verificados usando "matemática perfeita" (números reais), enquanto o robô real roda em "matemática aproximada" (números de ponto flutuante).

O Jeito Antigo: Isso era um perigo oculto. O verificador diria "Seguro", mas o robô real poderia travar.
O Jeito Novo: O VNN-LIB 2.0 permite que você diga explicitamente: "Eu sei que isso está usando matemática aproximada, mas quero verificá-lo usando matemática perfeita de qualquer maneira." Ele coloca um rótulo de aviso na consulta: "Prossiga com cautela, isso pode ser ligeiramente impreciso." Isso permite que pesquisadores usem ferramentas poderosas sem fingir que a matemática é perfeita quando não é.

5. A Prova "Padrão Ouro"

Para garantir que não cometeram nenhum erro ao escrever essa nova língua, os autores não apenas a escreveram; eles a programaram em um robô de prova matemática chamado Agda.

Pense no Agda como um editor super rigoroso que verifica cada regra da nova língua para garantir que não haja falhas lógicas.
Como a língua é "mecanizada" no Agda, qualquer pessoa pode agora usar essa prova para verificar se suas próprias ferramentas (solucionadores) estão funcionando corretamente. Isso transforma o padrão de uma "sugestão" em um "contrato matematicamente garantido".

Resumo

Em resumo, o VNN-LIB 2.0 é uma nova língua, rigorosa e flexível, para fazer perguntas de segurança à IA. Ela corrige a gramática quebrada do passado, permite perguntas complexas sobre múltiplos modelos de IA e fornece uma base comprovada matematicamente para que, quando uma ferramenta diz "Esta IA é segura", possamos realmente confiar que ela significa exatamente o que diz.

Resumo Técnico: VNN-LIB 2.0: Fundamentos Rigorosos para Verificação de Redes Neurais

Declaração do Problema

A comunidade de verificação de redes neurais tem recorrido cada vez mais ao padrão VNN-LIB (Versão 1.0) para facilitar a interoperabilidade entre solucionadores e ferramentas de nível superior. No entanto, a Versão 1.0 sofre de quatro deficiências críticas que impedem que ela sirva como uma base formal rigorosa:

Ausência de Sintaxe Formal: A Versão 1.0 não define formalmente a sintaxe da linguagem de consultas, levando a implementações mutuamente incompatíveis por diferentes solucionadores.
Expressividade Limitada: O padrão assume uma única rede com uma única entrada e saída. Ele não suporta nativamente múltiplas redes, múltiplas entradas/saídas ou acesso a camadas ocultas, forçando os usuários a fundir modelos artificialmente, o que obscurece a relação entre artefatos verificados e modelos implantados.
Ausência de um Sistema de Tipos: Não há mecanismo para especificar tipos numéricos (por exemplo, ponto flutuante versus valor real), criando ambiguidade e potencial insonez quando solucionadores tratam aritmética de precisão finita como valor real.
Falta de Semântica: O padrão carece de uma semântica formal, tornando impossível provar formalmente a correção de solucionadores, geradores de consultas ou transformações, e dificultando o desenvolvimento de certificados de prova.

Um desafio único para o VNN-LIB, distinguindo-o de padrões como SMT-LIB, é que as consultas não são autocontidas; elas especificam propriedades de modelos de redes neurais externos (tipicamente no formato ONNX). Como o próprio ONNX carece de uma semântica formal e continua a evoluir, definir um padrão VNN-LIB rigoroso exige desacoplar a linguagem de consultas de versões específicas do ONNX, mantendo a compatibilidade.

Metodologia

Os autores abordam esses desafios desenvolvendo os fundamentos teóricos para o VNN-LIB 2.0. A inovação metodológica central é a introdução da Teoria de Redes ( $\Psi$ ).

1. Abstração da Teoria de Redes

Os autores definem uma "teoria de redes" como uma especificação abstrata que captura a sintaxe mínima, julgamentos de tipagem e semântica necessários de um formato de modelo de rede neural para definir o VNN-LIB.

Desacoplamento: $\Psi$ atua como uma interface. Uma implementação concreta de $\Psi$ (por exemplo, para ONNX v1.20.0) fornece definições específicas para tipos de elementos, representações de tensores, estruturas de modelos e referências de saída de nós.
Modularidade: O VNN-LIB 2.0 é definido em relação a um $\Psi$ abstrato. Isso permite que o padrão permaneça estável mesmo à medida que o ONNX evolui; apenas a instanciação de $\Psi$ precisa ser atualizada para novas versões do ONNX, e não o próprio padrão VNN-LIB.
Formalização: Todo o padrão, incluindo sintaxe, tipagem e semântica, é mecanizado no provador de teoremas interativo Agda para garantir consistência interna e eliminar ambiguidades.

2. Sintaxe Formal e Expressividade

Com base na teoria de redes, os autores definem uma gramática formal para o VNN-LIB 2.0 que expande significativamente a expressividade:

Múltiplas Redes: Consultas podem declarar múltiplas redes, suportando cenários como verificação professor-aluno ou arquiteturas codificador-decodificador.
Equivalência de Redes: O padrão introduz declarações equal-to (referenciando o mesmo arquivo de modelo exato) e isomorphic-to (referenciando modelos com a mesma estrutura de grafo, mas potencialmente pesos diferentes). Isso permite que solucionadores compartilhem deduções (por exemplo, limites de variáveis) entre cópias de redes.
Nós Ocultos: A construção declare-hidden permite restrições sobre saídas de camadas intermediárias, essenciais para raciocinar sobre codificações ou mecanismos de atenção.
E/S Multidimensionais: Suporte para números arbitrários de entradas e saídas, acomodando redes multimodais.

3. Sistema de Tipos e Semântica

Tipagem: Um sistema de tipos formal impõe a correção numérica. Garante que operações aritméticas e comparações sejam realizadas em tipos compatíveis (por exemplo, impedindo a mistura de float32 e int32 sem regras de coerção explícitas). O sistema de tipos depende dos julgamentos fornecidos pela teoria de redes subjacente $\Psi$ .
Semântica: A semântica de uma consulta é definida como um problema de satisfatibilidade matemático. Dado um conjunto de modelos $M$ (instanciados a partir de $\Psi$ ) e uma atribuição de entrada $X$ , a semântica determina se existe uma atribuição onde todas as afirmações avaliam-se como verdadeiras.
Consultas de Valor Real: Para acomodar solucionadores existentes que tratam modelos como funções sobre números reais ( $\mathbb{R}$ ), o padrão introduz um mecanismo para "consultas de valor real". Ao usar um tipo real distinto, o autor da consulta autoriza explicitamente o solucionador a interpretar modelos sobre $\mathbb{R}$ , reconhecendo a potencial insonez devido à imprecisão de ponto flutuante. Isso é alcançado construindo uma teoria de redes específica $\Psi_{\mathbb{R}}$ derivada da teoria base.

Contribuições Principais

Teoria de Redes ( $\Psi$ ): A introdução de uma abstração novel que define a interface semântica mínima necessária de um formato de modelo, permitindo que o VNN-LIB seja definido independentemente de versões específicas do ONNX.
Sintaxe e Gramática Formais: Uma gramática livre de contexto precisa para o VNN-LIB 2.0 que suporta múltiplas redes, camadas ocultas e estruturas complexas de entrada/saída.
Sistema de Tipos Formal: Um sistema de tipagem que impõe a correção de tipos numéricos em relação à teoria de redes, abordando a ambiguidade nas representações numéricas.
Semântica Formal: Uma definição matemática rigorosa da semântica de consultas parametrizada pela teoria de redes, permitindo provas formais de correção para ferramentas que consomem ou geram VNN-LIB.
Mecanização: Todo o padrão é formalizado em Agda, fornecendo uma implementação de referência canônica e uma base para provas verificadas por máquina.
Extensão de Valor Real: Uma abordagem modular para suportar análises de valor real por meio de uma teoria de redes derivada, equilibrando a necessidade de correção com a realidade das capacidades atuais dos solucionadores.

Resultados e Validação

Consistência Interna: A formalização em Agda valida a consistência interna da sintaxe, tipagem e semântica, garantindo que o padrão esteja livre das ambiguidades presentes na Versão 1.0.
Demonstração de Expressividade: O artigo demonstra como uma transformação simples da teoria de redes $\Psi$ produz uma instância completa para consultas de valor real, mostrando a flexibilidade da abstração.
Adoção pela Comunidade: O padrão recebeu feedback positivo da comunidade de verificação. Equipes líderes de solucionadores comprometeram-se a apoiar o VNN-LIB 2.0, e o novo padrão está agendado para ser usado na competição VNN-COMP 2026.
Suporte de Ferramentas: Os autores lançaram uma biblioteca de alto desempenho em C++ (com bindings em Python e Julia) implementando um analisador sintático e verificador de tipos compatíveis com o novo padrão, juntamente com a formalização em Agda.

Significado

O artigo afirma que o VNN-LIB 2.0 fornece fundamentos robustos e rigorosos para a verificação confiável de redes neurais. Seu significado reside em duas áreas complementares:

Interoperabilidade Prática: Ao expandir a expressividade (múltiplas redes, nós ocultos) e padronizar a sintaxe, permite que a comunidade especifique e verifique propriedades mais ricas de maneira unificada, facilitando melhores benchmarks e comparações de ferramentas.
Rigor Teórico: Ao fornecer semântica formal e um sistema de tipos, estabelece um "contrato rigoroso" entre ferramentas e solucionadores. Isso permite a verificação formal das próprias ferramentas (solucionadores, otimizadores, verificadores de prova) e resolve questões sutis relacionadas à correção numérica (por exemplo, distinguindo entre semântica de valor real e ponto flutuante).

Os autores enfatizam que, embora o trabalho seja teórico, ele tem consequências concretas: garante interpretação não ambígua de consultas, fornece a linguagem para resolver questões técnicas e prepara o terreno para certificados de prova formalmente verificados no futuro.