Cada Classificador de Guardrail Testado Falha em Verificação Formal de Segurança

Os pesquisadores Nikita Kezins, Urbas Ekka, Pascal Berrang e Luca Arnaboldi provaram formalmente que cada classificador de guardrail que testaram contém buracos de segurança verificáveis. Os resultados, publicados em 11 de maio no arXiv, expõem uma fraqueza estrutural em como as empresas auditam salvaguardas de LLM em produção.

O trabalho aborda a lacuna entre red-teaming empírico e certificação formal de segurança. Os classificadores de guardrail atuais — filtros que ficam entre as entradas do usuário e as respostas do modelo para bloquear conteúdo prejudicial — mostram números de benchmark fortes, mas não carregam garantias comprovadas. A causa raiz: uma incompatibilidade entre frameworks de verificação emprestados de outros domínios de ML e a natureza da linguagem. As propriedades padrão de epsilon-ball no espaço discreto de tokens não têm significado semântico. "A vizinhança de uma entrada prejudicial" é matematicamente indefinida.

A solução da equipe desloca a verificação para longe do espaço de tokens inteiramente. Em vez disso, eles verificam no espaço pré-ativação do classificador — a camada de embedding interna onde entradas semanticamente similares se agrupam. Uma "região prejudicial" se torna uma forma convexa (ou um hiper-retângulo ou um componente de mistura gaussiana) envolvendo as representações de entradas prejudiciais conhecidas. Como o head sigmoid final é monótono, certificar o ponto de pior caso naquela região convexa certifica cada ponto dentro dela. Isso produz uma prova de solidez em forma fechada sendo executada em tempo O(d), onde d é a dimensão do embedding. Nenhuma aproximação necessária para o caso de hiper-retângulo.

Dois tipos de certificado foram instanciados. Hiper-retângulos alinhados com SVD produzem respostas SAT/UNSAT exatas: o classificador é garantido bloquear a região prejudicial inteira ou não é. Modelos de Mistura Gaussiana (GMMs) produzem certificados probabilísticos sobre clusters semanticamente coerentes, capturando os limites fluidos da linguagem prejudicial do mundo real. Ambos foram aplicados a três classificadores de guardrail treinados pelos autores e comparados em uma tarefa de detecção de toxicidade.

Os resultados são marcantes. Cada configuração de hiper-retângulo retornou SAT — significando que cada classificador tem pelo menos uma região comprovadamente insegura que falha em bloquear, independentemente do desempenho do benchmark. Certificados probabilísticos GMM revelaram divergência arquitetônica. Salvaguardas baseadas em GPT-2 mantiveram 90% de cobertura de região prejudicial em variações de limiar de limite; Llama-3.1-8B manteve 80%. BERT entrou em colapso. No limiar de classificação ótimo, a cobertura de BERT caiu para 55% — um fenômeno que os autores chamam de "colapso de cobertura". BERT alcança cobertura total apenas adotando um limiar extremamente conservador que prejudicaria a precisão em produção.

Para equipes empresariais, as implicações de conformidade são diretas. Avaliações de red-team, testes de penetração e suites de benchmark medem taxas de falha empírica; elas não podem descartar modos de falha fora de sua distribuição de teste. Certificados formais podem. Reguladores no framework da EU AI Act e NIST AI RMF sinalizam movimento em direção a propriedades de segurança auditáveis para implantações de alto risco — documentação que red-teaming sozinho não pode satisfazer. Este framework oferece às equipes de conformidade e governança um artefato concreto: um certificado declarando se um determinado classificador é verificavelmente seguro em uma região de embedding prejudicial definida, não apenas em um conjunto de testes finito.

Questões abertas permanecem. O framework atualmente cobre classificadores com um head sigmoid; estendê-lo para arquiteturas multi-label ou softmax não é abordado. Regiões prejudiciais são delimitadas pelas representações de entradas conhecidas, então novos jailbreaks fora do casco convexo não são certificados contra. Os três classificadores são treinados especificamente para este estudo em vez de ser extraídos de salvaguardas comerciais implantadas como Llama Guard ou a API de moderação do OpenAI, deixando a transferabilidade dos resultados incerta.

O campo agora tem uma alternativa matematicamente fundamentada para red-teaming empírico. Empresas avaliando fornecedores de guardrail devem perguntar se artefatos de verificação formal estão no roadmap do produto.