Resumo Técnico: Auditoria Neurosimbólica de Requisitos de Software em Linguagem Natural

Declaração do Problema

Requisitos de software em linguagem natural, particularmente em domínios críticos para a segurança como dispositivos médicos, frequentemente sofrem de ambiguidade, inconsistência e especificação insuficiente. Esses defeitos são perigosos porque se propagam para modelos formais e implementações, potencialmente levando à verificação de especificações incorretas ou à implantação de comportamentos inseguros. Embora os Modelos de Linguagem de Grande Escala (LLMs) tenham avançado o campo da autoformalização (tradução de linguagem natural para especificações verificáveis por máquina), a validade sintática por si só é insuficiente. Uma especificação formal bem formada pode ainda ser globalmente inconsistente, conter condições de acionamento inalcançáveis (vacuidade) ou admitir múltiplas interpretações plausíveis do texto fonte. Na ausência de uma formalização de verdade fundamental, não há um oráculo para detectar essas falhas semânticas, pois os LLMs frequentemente recorrem à leitura estatisticamente mais comum ou omitem restrições implícitas.

Metodologia: O Framework VERIMED

Os autores propõem o VERIMED, um pipeline neurosimbólico projetado para auditar requisitos em linguagem natural traduzindo-os em um modelo unificado SMT (Satisfiability Modulo Theories) e aproveitando consultas ao solucionador para detectar defeitos. O framework opera sobre um esquema fixo de variáveis de estado tipadas (estados de controle booleanos e parâmetros de valor real) e restrições de domínio.

O pipeline consiste em quatro etapas:

1. Resolvedor de Ambiguidade: Antes da formalização, cada requisito é verificado quanto à estabilidade. O sistema amostra $N$ formalizações independentes do LLM com temperatura elevada. Realiza verificação de equivalência SMT bidirecional entre pares de codificações. Se as codificações não forem equivalentes, o requisito é sinalizado como sensível à ambiguidade. O solucionador gera "testemunhas" concretas (estados específicos onde as codificações discordam), que são alimentadas de volta ao LLM para reescrever o requisito até que todas as amostras converjam para uma única codificação.
2. Autoformalizador: Os requisitos desambiguados são traduzidos em uma única especificação SMT-LIB. O sistema emprega um loop de reparo sintático limitado onde mensagens de erro do solucionador orientam o LLM a regenerar código malformado até que um modelo válido seja produzido.
3. Verificador de Propriedades: Este módulo executa quatro consultas de auditoria específicas no modelo montado $M$:
   • Consistência Global: Verifica se $M$ é satisfatível. Se insatisfatível, um núcleo insat identifica requisitos conflitantes.
   • Vacuidade: Para requisitos condicionais, verifica se a condição de acionamento pode ser satisfeita sob restrições de domínio.
   • Violabilidade: Verifica se um requisito pode ser violado dentro do domínio, retornando uma atribuição de violação concreta se possível.
   • Redundância: Verifica se um requisito já é imposto pelo restante da especificação.
4. Verificador de Consultas: Esta etapa verifica perguntas de segurança baseadas em cenários. Verifica se uma resposta proposta é implicada pelo modelo ($M \land s \land \neg a$ é insatisfatível). Se uma violação for encontrada, o solucionador retorna um contraexemplo. Este contraexemplo, juntamente com os requisitos violados, serve como feedback para um loop de reparo corrigir a resposta do LLM.

Contribuições Principais

O artigo apresenta as seguintes contribuições:

• Um Framework Neurosimbólico: O VERIMED operacionaliza a tradução de requisitos em linguagem natural para um único modelo SMT, utilizando saídas do solucionador como o sinal primário para revisão a jusante.
• Auditorias SMT ao Nível de Requisitos: Os autores formulam quatro auditorias (consistência, vacuidade, violabilidade, redundância) que operacionalizam critérios de qualidade estabelecidos.
• Detecção de Ambiguidade via Estocasticidade: O artigo introduz um método para detectar ambiguidade explorando a natureza estocástica dos LLMs. Ao amostrar múltiplas formalizações e verificar inequivalência SMT bidirecional, o sistema sinaliza requisitos que admitem múltiplas leituras plausíveis. Testemunhas geradas pelo solucionador então orientam a clarificação em linguagem natural.
• Reparo Guiado por Contraexemplo (CEGR): O estudo demonstra que a granularidade do feedback simbólico impacta significativamente a eficácia do reparo.

Resultados Experimentais

O framework foi avaliado em um corpus de 64 requisitos de segurança em linguagem natural de uma especificação de máquina de hemodiálise, com avaliação secundária em uma especificação de bomba PCA.

• Autoformalização e Auditoria: O sistema gerou com sucesso um modelo SMT verificável por solucionador para todos os 64 requisitos. O modelo foi globalmente consistente e não continha requisitos vacuos. A auditoria sinalizou 2 requisitos (3,1%) como redundantes. A equivalência semântica de ida e volta (traduzindo SMT de volta para texto e re-formalizando) foi alcançada para 100% dos requisitos, com uma similaridade cossena média de 96,2% entre os textos original e reconstruído.
• Detecção de Mutação: O pipeline detectou 97,3% dos 256 requisitos mutados (representando falhas como supressão de falso alarme e violação de limites) em quatro categorias de falhas.
• Reparo Guiado por Contraexemplo: Em uma tarefa de pergunta e resposta, o uso de contraexemplos SMT concretos como feedback (CEGR) aumentou a precisão verificada de uma linha de base de 55,4% (sem feedback) para 98,5%. Fornecer apenas os requisitos violados (sem o contraexemplo concreto) resultou em 80,0% de precisão, demonstrando que o estado de testemunha concreto é o motor crítico para o reparo.
• Resolução de Ambiguidade: O resolvedor de ambiguidade sinalizou 12 dos 64 requisitos (18,8%) como produzindo múltiplas codificações distintas. Após clarificação guiada por SMT, todos os requisitos sinalizados convergiram para uma única codificação (100% de concordância par a par), reduzindo a média de codificações distintas por requisito de 1,59 para 1,00.

Significado e Alegações

O artigo afirma que o VERIMED operacionaliza com sucesso a auditoria de requisitos de software através de consultas baseadas em SMT, abordando a natureza "invisível" de defeitos semânticos na autoformalização. Os autores enfatizam que:

1. A variação estocástica é um sinal: O desacordo entre formalizações independentes é um indicador confiável de ambiguidade no texto fonte.
2. A granularidade importa: A utilidade do feedback simbólico depende altamente de sua especificidade; contraexemplos concretos são significativamente mais eficazes para reparo do que listas abstratas de requisitos.
3. Consistência é insuficiente: A consistência interna de um modelo formal não garante a ausência de defeitos; preservação comportamental e detecção de ambiguidade são complementos necessários.

Os autores mantêm um escopo modesto, observando que suas descobertas são específicas para dispositivos médicos relacionados à infusão e que a abordagem depende de sinais proxy (consistência, sensibilidade a mutação, etc.) em vez de uma medida direta de fidelidade à intenção. Eles afirmam explicitamente que os resultados não devem ser usados em aplicações críticas para a segurança sem revisão independente de especialistas e que a implementação atual não suporta lógica temporal completa, aproximando requisitos temporais através de condições de estado atuais.