Resumo Técnico: Síntese Neuro-Simbólica de Modelos de Uso de Cadeias de Markov Formalmente Verificados

1. Declaração do Problema

O principal gargalo que impede a adoção generalizada do Teste Estatístico Baseado em Modelo (MBST - Model-Based Statistical Testing) além dos nichos de missão crítica é a construção manual de modelos de uso de cadeias de Markov. Esses modelos são essenciais para deslocar os objetivos de teste da cobertura de código absoluta para a inferência estatística em relação à qualidade esperada em campo. No entanto, traduzir requisitos de linguagem natural ambíguos e não estruturados em topologias de transição de estados e matrizes de probabilidade matematicamente consistentes exige expertise significativa em métodos formais.

Embora os Grandes Modelos de Linguagem (LLMs) tenham demonstrado capacidades de extração sintática, as abordagens puramente neurais sofrem de quatro limitações críticas quando aplicadas ao MBST:

1. Volatilidade Estocástica e Alucinação: Os LLMs podem omitir casos de borda críticos, construir transições impossíveis ou violar invariantes do sistema, levando a casos de teste inválidos.
2. Falha de Calibração: Os LLMs têm dificuldade com o raciocínio numérico preciso, frequentemente falhando em satisfazer as restrições estocásticas de linha rigorosas ($\sum_j p_{ij} = 1$) e as complexas restrições multivariáveis necessárias para cadeias de Markov válidas.
3. Explosão do Espaço de Estados: Os LLMs operando dentro de janelas de contexto finitas não conseguem rastrear ou gerar efetivamente modelos de transição altamente concorrentes e de múltiplos fluxos sem perder a coerência estrutural.
4. Divergência de Viabilidade Semântica: Os LLMs são excelentes no progresso semântico, mas frequentemente violam restrições de viabilidade física e lógica (por exemplo, executar uma transição de checkout com um carrinho vazio), gerando caminhos que são semanticamente lógicos, mas fisicamente inexequíveis.

A literatura existente carece de uma avaliação de ponta a ponta sobre se a construção automatizada de modelos pode preservar as propriedades estruturais e probabilísticas necessárias para as garantias de detecção de falhas do MBST.

2. Metodologia: O Framework NeSy-MBST

O artigo introduz o Teste Estatístico Baseado em Modelo Neuro-Simbólico (NeSy-MBST), um framework híbrido que desacopla a análise semântica da resolução de restrições matemáticas. A arquitetura integra cinco estágios estreitamente acoplados:

A. Arquitetura de Memória Dupla de Progresso-Viabilidade

O sistema particiona a construção do modelo em dois sistemas de memória complementares:

• Memória de Progresso Neural: Um LLM ajustado (fine-tuned) analisa os requisitos de linguagem natural para rascunhar um grafo de fluxo semântico (o "quê"), capturando as topologias comportamentais pretendidas.
• Memória de Viabilidade Simbólica: Um motor baseado em regras impõe invariantes lógicos estritos, precondições e guardas de transição (o "como"), validando cada transição candidata antes da admissão.

B. Aprendizado de Autômatos Ativo via $L^*$ com Oráculos de LLM

O framework emprega uma variante especializada do algoritmo de aprendizado de autômatos ativo $L^*$ para descobrir o espaço de estados.

• Consultas de Pertencimento (Membership Queries): O algoritmo consulta um oráculo de LLM restrito por gramática (limitado aos outputs: Sim, Não, Não tenho certeza) para determinar se uma sequência de entrada candidata é aceita.
• Consultas de Equivalência (Equivalence Queries): O autômato de hipótese atual é testado contra o Sistema Sob Teste (SUT) real. As divergências geram contraexemplos usados para refinar a hipótese.
• Escalação: Se o LLM retornar "Não tenho certeza", a consulta é escalonada para especialistas humanos ou execução em tempo de execução do SUT, garantindo que o loop de aprendizado nunca incorpore informações não verificadas.

C. Modelagem Hierárquica Dependente de Caminho

Para lidar com a dependência de caminho sem explosão combinatória, o NeSy-MBST utiliza uma hierarquia de dois níveis:

1. Estrutura de Árvore Superior: Sequências frequentes e dependentes de caminho são modeladas como uma cadeia de Markov de ordem superior incorporada em uma árvore.
2. Modelo de Markov Inferior: Caminhos de exceção ou infrequentes são modelados usando cadeias de Markov de primeira ordem padrão.

D. Otimização de Restrições Matemáticas

Em vez de pedir ao LLM para gerar probabilidades numéricas diretamente, o framework delega essa tarefa a um solver simbólico:

1. Extração de Restrições: O LLM extrai relações comparativas (ex: $P(\text{checkout}|\text{carrinho}) > P(\text{navegar}|\text{carrinho})$) dos requisitos.
2. Otimização Convexa: Um motor de programação convexa (SLSQP) resolve a matriz de probabilidade de transição $P$ que satisfaz todas as restrições extraídas, a estocasticidade de linha e os limites específicos do domínio, enquanto maximiza a entropia para evitar vieses injustificados.

E. Adaptação de Modelo em Ciclo Fechado

O framework trata o modelo de uso como um artefato vivo. A telemetria de tempo de execução (logs de execução, métricas de cobertura, dados de falha) é alimentada de volta ao motor de modelagem. O LLM analisa as divergências entre o comportamento previsto e o observado, e o solver simbólico recalibra as probabilidades, garantindo que o modelo converja para os padrões de uso do mundo real.

3. Principais Contribuições

• Framework NeSy-MBST: Uma arquitetura inovadora que combina aprendizado ativo $L^*$, oráculos de LLM restritos por gramática, solvers simbólicos e feedback de ciclo fechado para automatizar a síntese de modelos de uso.
• Verificação Formal de Output de LLM: A introdução de um loop de verificação simbólica que detecta violações estruturais (estados inalcançáveis, ausência de auto-loops) e dispara o re-prompt direcionado, convertendo um problema de geração limitado por recall em um problema de completude guiado por verificação.
• Decomposição Ortogonal de Erros: O artigo estabelece que a completude estrutural (topologia) e a calibração probabilística (pesos) são propriedades ortogonais, abordadas separadamente pelo loop simbólico e pelo otimizador convexo, respectivamente.
• Validação Empírica: Uma avaliação abrangente em um benchmark de Sistemas Ciber-Físicos (CPS) de Veículos Autônomos (AV) e duas especificações de e-commerce, comparando o NeSy-MBST com baselines puramente neurais e abordagens manuais tradicionais.

4. Resultados Experimentais

Avaliado em um benchmark de CPS de AV (9 estados, 13 transições) e modelos de e-commerce (até 42 estados, 218 transições), o NeSy-MBST alcançou o seguinte:

• Precisão de Extração (RQ1): Alcançou um F1 score de nível de sistema de 0,9125, excedendo o limiar de segurança crítica de 0,90. Isso representa uma melhora de 39,1% sobre o melhor baseline GPT-4o (Hybrid SMF) e uma melção de 14,8% sobre o baseline de modelo único mais forte (Claude 3.5 Sonnet).
• Cobertura de Detecção de Falhas (RQ2): Alcançou 85,7% de cobertura de transição, um ganho de 35,7 pontos percentuais sobre o baseline puramente neural (50%). Isso sugere um aumento significativo na diversidade de caminhos que revelam falhas.
• Calibração Probabilística (RQ3): Alcançou uma Divergência de Jensen–Shannon (JSD) de 0,012 (vs. 0,157 para o baseline puramente neural), confirmando que o otimizador convexo preserva a fidelidade da alocação de testes operacionais. A distância de Frobenius normalizada foi de 0,0654, indicando alta similaridade estrutural com a distribuição de referência.
• Eficiência: Gerou suítes de teste de cobertura total de modelo em menos de seis minutos para modelos com até 42 estados.
• Estudo de Ablação (RQ4):
  • O Loop Simbólico foi identificado como o principal motor para a completude estrutural (aumentando o F1 de transição de 0,78 para 0,96).
  • O Otimizador Convexo mostrou-se responsável por governar a calibração probabilística sem alterar as métricas estruturais.
  • O Feedback de ciclo fechado forneceu melhorias marginais na fidelidade distributiva, sendo valioso principalmente para campanhas de teste de longo prazo.

5. Significância e Alegações

O artigo afirma que o NeSy-MBST elimina o gargalo da modelagem manual sem comprometer o rigor estatístico exigido por Sistemas Ciber-Físicos (CPS) de missão crítica.

• Preenchendo a Lacuna: Os resultados demonstram que a integração neuro-simbólica pode alcançar a fidelidade estrutural (F1 $\ge$ 0,90) e a calibração probabilística exigidas pelo MBST, as quais as abordagens puramente neurais não conseguem garantir.
• Proxy de Detecção de Falhas: Embora o estudo não tenha medido as taxas diretas de detecção de defeitos contra um corpus de falhas inseridas, o artigo argumenta que o aumento de 35,7% na cobertura de transição é um forte proxy para a detecção de falhas, consistente com as melhorias de 25–40% relatadas na literatura de implementação de MBT industrial.
• Padrão de Engenharia: Os autores propõem que o aumento de LLM para a geração de modelos de teste formais deve transitar de uma curiosidade de pesquisa para uma prática de engenharia padrão, desde que duas condições sejam atendidas: (1) os LLMs operem sob restrições estruturais (output restrito por gramática, verificação simbólica) para prevenir alucinações e (2) os parâmetros numéricos sejam atribuídos por solvers certificados, não pelo LLM diretamente.

O artigo conclui que esta abordagem torna o teste estatístico rigoroso acessível a práticas mais amplas de desenvolvimento de software, movendo-o além das equipes especializadas em segurança crítica, ao mesmo tempo em que reconhece que trabalhos futuros são necessários para validar esses achados em sistemas industriais de maior escala e com diversos estilos de requisitos.