Formalização de LLM Detecta 18.8% de Requisitos Ambíguos em Especificações de Segurança

Pesquisadores do Stevens Institute of Technology publicaram VERIMED, um pipeline que emparelha formalização de modelo de linguagem grande com verificação simbólica para capturar defeitos estruturais em requisitos de software em linguagem natural. Em uma especificação de dispositivo hemodiálise publicada, o sistema sinalizou 12 de 64 requisitos como ambíguos e 2 como redundantes—falhas invisíveis à revisão sintática.

VERIMED funciona traduzindo cada requisito em um modelo verificável mecanicamente e aplicando quatro verificações de solucionador: consistência, vacuidade, violabilidade e redundância. Depois testa a estabilidade da codificação do LLM formalizando o mesmo requisito várias vezes independentemente. Se o solucionador produz codificações estruturalmente diferentes, isso sinaliza ambiguidade no texto original.

O artigo, de autoria de Bethel Hall e William Eiers e postado no arXiv em 13 de maio de 2026, relata resultados em um benchmark de hemodiálise. Um LLM recebendo nenhum feedback de solucionador verificou 55.4% das respostas de teste corretamente. Quando dado requisitos violados como contexto, a precisão subiu para 80.0%. Com contraexemplos concretos—as atribuições de variáveis específicas que quebraram cada restrição—a precisão atingiu 98.5%.

Dos 64 requisitos de hemodiálise, 12 (18.8%) produziram formalizações estruturalmente distintas quando amostrados independentemente. Todos os 12 exigiram revisão humana e esclarecimento. Os 2 sinalizadores de redundância similarmente exigiram aprovação manual.

Os resultados são limitados a um benchmark de 64 requisitos. A especificação de hemodiálise é código aberto e reproduzível, mas o pipeline não foi testado contra especificações de requisitos de aeroespacial ou dispositivo médico da escala típica regulatória (centenas a milhares). Os autores assumem a correção da codificação SMT mas não a provam.

O desafio de integração: o pipeline exige que os requisitos sejam formalizáveis em restrições lógicas sem quantificadores. Requisitos envolvendo dinâmica contínua, comportamento probabilístico ou idiomas em linguagem natural que resistem à codificação vão falhar em traduzir ou produzir codificações espúrias. A auditoria de vacuidade captura o último apenas se a codificação sucede. Equipes usando padrões avionics DO-178C ou automotivo ISO 26262 devem tratar 18.8% de ambiguidade como estimativa de piso—requisitos de domínio regulado tendem a incorporar mais suposições implícitas do que especificações de hemodiálise.

Para equipes roteando saída de LLM através de verificação formal, a especificidade do feedback importa. A lacuna entre "aqui está o requisito falhando" e "aqui está o contraexemplo" corresponde a 18.5 pontos percentuais de precisão verificada neste benchmark.