Talking with Verifiers: Automatic Specification Generation for Neural Network Verification

Este artigo apresenta um novo framework que traduz especificações de verificação de redes neurais de linguagem natural para consultas formais, superando as limitações atuais das ferramentas de verificação ao permitir a validação de requisitos semânticos complexos e de alto nível com baixo custo computacional.

O essencial

Imagine que você tem um cérebro artificial (uma Rede Neural) muito inteligente, usado para coisas importantes como dirigir carros autônomos ou diagnosticar doenças. Agora, imagine que você quer ter certeza absoluta de que esse cérebro não vai cometer um erro grave em uma situação específica.

O problema é que os "inspetores de segurança" atuais (ferramentas de verificação) só entendem uma linguagem muito técnica e chata: números e coordenadas exatas. Eles não entendem o que você, um humano, realmente quer dizer.

Aqui está a explicação do artigo "Talking with Verifiers" (Falando com os Verificadores), usando analogias simples:

1. O Problema: O Tradutor Perdido

Imagine que você é um engenheiro de segurança (o usuário) e quer dizer ao inspetor:

"O carro não deve frear bruscamente se um cachorro aparecer na frente."

Mas o inspetor (a ferramenta de verificação) só entende uma linguagem de computador:

"Se o pixel 1024 na coordenada X for alterado para a cor marrom, a saída Y não pode mudar."

Para usar as ferramentas atuais, você teria que ser um especialista em matemática para traduzir sua ideia simples ("cachorro") em coordenadas de pixels complexas. Isso é difícil, demorado e propenso a erros. Se você não souber exatamente onde o cachorro vai estar, não consegue pedir a verificação.

2. A Solução: O "Intérprete Mágico"

Os autores criaram um sistema de tradução automática que fica no meio do caminho. Eles chamam isso de "Talking with Verifiers".

Pense nesse sistema como um tripé de especialistas trabalhando juntos para traduzir sua fala para a linguagem do computador:

1. O Detetive de Ideias (LLM - Modelo de Linguagem):

   • Você diz: "O pássaro deve ser classificado corretamente mesmo se o bico estiver coberto."
   • O Detetive entende que você está falando sobre um "bico" e uma ação de "cobrir". Ele separa a ideia da frase.

2. O Olho de Águia (Modelo de Visão/Audio):

   • O Detetive diz ao Olho de Águia: "Procure um bico nesta foto específica."
   • O Olho de Águia (que é um modelo de IA moderno) olha a foto e diz: "Encontrei! O bico está nestas coordenadas exatas (X, Y)."
   • Isso é o "Grounding" (ancoragem): transformar uma ideia abstrata em um local físico na imagem.

3. O Tradutor Final (Gerador de Especificação):

   • Agora que sabemos onde está o bico, o Tradutor pega essa informação e escreve a ordem técnica para o inspetor: "Cubra apenas a área do bico (coordenadas X, Y) e veja se o resultado muda."

3. O Resultado: Segurança para o Mundo Real

Com essa nova ferramenta, você pode pedir verificações complexas e semânticas (baseadas no significado) sem precisar saber matemática avançada.

• Exemplo Prático (Imagens): Você pode perguntar: "O que acontece se eu apagar o bico do pássaro?" O sistema encontra o bico na foto e testa se a IA ainda reconhece o pássaro.
• Exemplo Prático (Tabelas): Você pode perguntar: "Se o cliente tiver menos de 50 anos, a decisão de crédito muda?" O sistema sabe que "idade" é a coluna 3 da tabela e testa isso.
• Exemplo Prático (Áudio): Você pode perguntar: "O sistema ouve o alarme de emergência mesmo se houver barulho de furadeira?" O sistema localiza o som da furadeira no arquivo de áudio e testa a robustez.

4. Por que isso é importante?

Antes, as ferramentas de verificação eram como ferramentas de cirurgião: precisavam de um especialista para apontar exatamente onde cortar. Agora, com esse novo sistema, elas são como um GPS para segurança: você diz o destino ("quero garantir que o bico não importa") e o sistema traça a rota técnica automaticamente.

Em resumo:
Os autores não criaram um novo "cérebro" para verificar redes neurais. Eles criaram um ponte que conecta a linguagem humana (nossa forma natural de pensar) com a linguagem rígida das ferramentas de verificação. Isso permite que qualquer pessoa, sem ser um matemático, garanta que a Inteligência Artificial é segura e justa em situações do mundo real.

É como dar um microfone para os humanos e um tradutor para as máquinas, permitindo que conversem sobre segurança sem barreiras.

Resumo técnico

1. O Problema

As ferramentas atuais de verificação formal de Redes Neurais Profundas (DNNs) enfrentam uma barreira significativa de adoção e aplicabilidade prática. Embora existam avanços matemáticos robustos para garantir a correção de modelos, essas ferramentas exigem que as especificações de segurança sejam expressas como restrições numéricas de baixo nível (ex: limites em dimensões fixas de entrada, perturbações em normas $\ell_p$).

Isso cria um "gap" de usabilidade:

• Especificação Semântica vs. Numérica: Requisitos do mundo real são naturalmente expressos em linguagem natural e alto nível (ex: "A decisão de crédito não deve mudar para menores de 50 anos" ou "O pássaro deve ser classificado corretamente mesmo se o bico estiver ocluído").
• Dificuldade de Tradução: Traduzir essas intenções humanas para restrições matemáticas formais é manual, propenso a erros e depende do conhecimento específico da ferramenta de verificação.
• Limitação de Dados Não Estruturados: Em dados como imagens e áudio, regiões semânticas (como um "bico de pássaro" ou um "som de sirene") variam de amostra para amostra e não podem ser capturadas por coordenadas de entrada fixas, tornando muitas especificações semanticamente ricas inacessíveis aos verificadores atuais.

2. Metodologia

Os autores propõem um framework de ponta a ponta que atua como uma camada de integração entre a intenção do usuário (linguagem natural) e os motores de verificação existentes. A abordagem não modifica os algoritmos de verificação subjacentes, mas sim automatiza a geração das consultas de verificação.

O pipeline consiste em três etapas principais (Algoritmo 1):

1. Parsing (Análise Sintática):

   • Utiliza um Modelo de Linguagem Grande (LLM) para interpretar a especificação em linguagem natural.
   • O LLM extrai dois componentes: (i) um conjunto de objetos semânticos a serem localizados no input (ex: "bico", "idade", "sirene") e (ii) a operação desejada (ex: "ocultar", "aumentar volume", "limitar valor").

2. Grounding (Ancoragem/Detecção):

   • Utiliza modelos de percepção de ponta (Visão-Linguagem ou Áudio-Linguagem) para localizar os objetos extraídos no input concreto.
   • Imagens: Usa modelos de detecção de objetos de vocabulário aberto (Open-Vocabulary), como o Grounding DINO, para retornar coordenadas de caixas delimitadoras (bounding boxes) para os objetos mencionados.
   • Áudio: Propõe o uso de modelos de localização de eventos sonoros (embora a implementação completa não tenha sido feita neste trabalho, o conceito é definido).
   • Dados Estruturados (Tabulares): Mapeia nomes de características (features) extraídos pelo LLM diretamente para índices de colunas na tabela.

3. Geração de Especificação:

   • Com base nas coordenadas ou índices obtidos e na operação definida, um gerador constrói uma consulta de verificação formal padrão ($P_x$).
   • Por exemplo, para a imagem do bico, gera-se uma restrição de robustez local que perturba apenas os pixels dentro da caixa delimitadora do bico, verificando se a saída da rede permanece inalterada.

3. Principais Contribuições

1. Identificação da Lacuna de Usabilidade: O trabalho destaca a necessidade crítica de especificar requisitos de alto nível para sistemas DNNs em produção, identificando a tradução manual como o principal obstáculo para a adoção de métodos formais.
2. Mecanismo Automatizado de Geração de Especificações: Propõe um pipeline que mapeia intenções em linguagem natural para especificações formais, utilizando modelos fundacionais (Foundation Models) para entender o contexto e localizar objetos semânticos.
3. Demonstração Empírica de Aplicabilidade: O framework foi testado em cenários representativos (dados tabulares e classificação de imagens), mostrando que é possível verificar especificações semânticas complexas sem alterar os backends de verificação existentes.
4. Reutilização de Componentes Maduros: A abordagem enfatiza a composição de ferramentas existentes (LLMs, detectores de objetos, verificadores de DNN) em vez de criar novos algoritmos de verificação, garantindo compatibilidade imediata com o estado da arte.

4. Resultados

Os experimentos foram conduzidos em dois benchmarks principais:

• Dados Tabulares (Statlog/German Credit Data): Rede totalmente conectada para classificação de risco de crédito.
• Imagens (CUB-200-2011): Classificador ResNet-18 para espécies de pássaros.

Desempenho Quantitativo:

• Parsing (LLM): O uso de modelos como GPT-5 Mini e Gemini 3 Flash resultou em alta precisão na extração de objetos e ações (entre 85% e 100% de acurácia). O GPT-5 Mini atingiu 100% de precisão na ação para dados tabulares.
• Grounding (Detecção): A ancoragem em imagens é mais desafiadora. A detecção individual de configurações atingiu até 55% de precisão. No entanto, ao considerar a união de todas as configurações (ou seja, se qualquer modo de detecção encontrou o objeto correto), a taxa de sucesso subiu para 83%. Isso indica que, embora a detecção fina seja difícil, o sistema frequentemente consegue localizar a região correta com os parâmetros adequados.

Desempenho Qualitativo:

• O pipeline conseguiu traduzir consultas complexas como "A previsão pode mudar se o espinho roxo no fundo for mais ruidoso?" em restrições de perturbação local precisas, ignorando o contexto de verificação e focando na tarefa perceptiva.
• O sistema demonstrou capacidade de lidar com múltiplos objetos disjuntos (ex: "bico e pernas" faltando) e gerar contraexemplos válidos quando a robustez falha.

5. Significado e Impacto

Este trabalho representa um avanço significativo na democratização da verificação formal de redes neurais:

• Acesso a Requisitos de Alto Nível: Permite que engenheiros e usuários finais verifiquem propriedades semânticas complexas sem precisar ser especialistas em matemática de verificação ou em linguagens de especificação de baixo nível.
• Extensão da Aplicabilidade: Torna viável a verificação de cenários críticos em domínios não estruturados (visão, áudio) onde as especificações dependem do conteúdo da entrada, algo impossível com as ferramentas tradicionais.
• Futuro: O framework abre caminho para a verificação de vídeos e restrições temporais em áudio, além de sugerir a evolução para segmentação em nível de pixel (em vez de apenas caixas delimitadoras) para maior precisão.

Em resumo, o artigo propõe uma solução prática e modular que "traduz" a linguagem humana para a linguagem matemática dos verificadores, preenchendo uma lacuna crítica que impediu a aplicação ampla da verificação formal em sistemas de IA do mundo real.