Resumo Técnico: SYSMOBENCH

Declaração do Problema

Modelos formais são críticos para especificar e verificar a correção de sistemas computacionais grandes e complexos, particularmente nos domínios de computação distribuída e concorrente. No entanto, criar esses modelos é notoriamente caro, exigindo um esforço significativo de especialistas para abstrair o código de baixo nível em especificações matemáticas rigorosas. Embora avanços recentes em IA generativa (LLMs e técnicas de agentes) tenham mostrado promessa na geração de especificações de nível de função (ex: pré-condições e pós-condições), permanece incerto se a IA pode modelar efetivamente sistemas reais completos. Os benchmarks existentes visam principalmente pequenos trechos de código ou quebra-cabeças de lógica, falhando em abordar as complexidades de abstrair o design de sistemas, raciocinar sobre segurança (safety) e vivacidade (liveness) sob falhas, e lidar com a escala de artefatos de nível de produção.

Metodologia

Os autores apresentam o SYSMOBENCH, um benchmark projetado para avaliar a capacidade de IA generativa de modelar sistemas reais complexos. O framework foca em sistemas concorrentes e distribuídos, que sustentam infraestruturas críticas como sistemas operacionais e serviços em nuvem.

Componentes Principais

1. Formulação da Tarefa: O benchmark desafia agentes de IA a gerar modelos de sistema formais (especificamente em TLA+, a linguagem de especificação de fato para tais sistemas) a partir de artefatos de sistemas do mundo real. A entrada inclui código-fonte, documentação e traços de execução (runtime traces). A saída deve capturar propriedades comportamentais essenciais e transições de estado, excluindo detalhes de implementação irrelevantes.
2. Artefatos de Sistema: O benchmark inclui atualmente onze artefatos diversos, variando de primitivas de sincronização simples (Spinlock, Mutex, Ringbuffer no Asterinas OS) a protocolos distribuídos complexos (Etcd Raft, Redis Raft, ZooKeeper FLE, Xline CURP) e sistemas gerados por compiladores (PGo).
3. Métricas de Avaliação Automatizadas: Uma contribuição fundamental é o desenvolvimento de métricas quantitativas automatizadas para avaliar a qualidade do modelo sem depender de comparações humanas frágeis ou abordagens de "LLM-como-juiz". As métricas incluem:
   • Correção Sintática: Validada usando o Analisador Sintático SANY. Emprega um esquema de pontuação ponderada (modelo completo vs. por ação) para lidar com a correção parcial.
   • Correção de Execução (Runtime): Medida pela fração de ações do modelo que podem ser executadas sem erros usando o model checker TLC, servindo como um proxy para a auticonsistência lógica.
   • Conformidade: Avaliada via validação de traço, onde execuções de traços provenientes do código do sistema instrumentado são verificadas contra o espaço de estados do modelo gerado. Isso envolve o uso de um LLM para mapear elementos do modelo para elementos do código para lidar com discrepâncias de nomenclatura.
   • Correção de Invariantes: Avalia se o modelo satisfaz propriedades de segurança (safety) e vivacidade (liveness) específicas do sistema. Templates de invariantes são concretizados em fórmulas TLA+ específicas do modelo usando LLMs e, em seguida, verificados via model checking.

Agentes de Avaliação

O estudo avalia três designs distintos de agentes impulsionados por quatro LLMs de última geração (Claude-Sonnet-4, GPT-5, Gemini-2.5-Pro, DeepSeek-R1):

• Agente de Modelagem Básica: Prompta o LLM diretamente com o código-fonte e os requisitos da tarefa.
• Agente de Tradução de Código: Traduz o código do sistema instrução por instrução para TLA+ antes de organizar os fluxos de controle.
• Agente de Aprendizado de Traço: Infere o modelo do sistema unicamente a partir de traços de execução, sem entrada de código.

Resultados Principais

A avaliação revela limitações significativas nas capacidades atuais de IA em relação à modelagem de sistemas complexos:

• Lacuna de Escalabilidade: Agentes de IA performam bem em artefatos pequenos e simples (ex: Asterinas Spinlock), frequentemente alcançando pontuações altas em sintaxe, execução e conformidade. No entanto, o desempenho degrada drasticamente em sistemas maiores e mais complexos como o Etcd Raft. Por exemplo, no Etcd Raft, mesmo o agente de melhor desempenho (Claude-Sonnet-4 com tradução de código) alcançou apenas 15,38% de conformidade e 92,31% de correção de invariante, enquanto outros agentes falharam totalmente em passar nos testes de sintaxe ou execução.
• Desafios de Abstração: Os principais modos de falha para sistemas complexos incluem dificuldade em lidar com a verbosidade do código, compreensão de lógicas de protocolo intrincadas (ex: ordenação do Raft) e a abstração correta de estruturas de dados aninhadas (ex: logs distribuídos).
• Desempenho dos Agentes: O Agente de Tradução de Código geralmente superou o Agente de Modelagem Básica em sistemas complexos, sugerindo que aproveitar as capacidades de tradução de código dos LLMs ajuda a prevenir a alucinação de lógica. O Agente de Aprendizado de Traço teve um desempenho ruim em todos os aspectos, frequentemente falhando em verificações de compilação e execução, indicando que inferir modelos de sistema a partir de traços é atualmente mais difícil para LLMs do que processar código-fonte.
• Análise de Erros: Erros de sintaxe são frequentes, particularmente com símbolos matemáticos e uso incorreto de operadores. Erros de execução frequentemente derivam de configurações inconsistentes ou mal-entendidos das estruturas de dados do TLA+. Notavelmente, os LLMs lutam significamente com propriedades de vivacidade (liveness), com 41,9% das violações de invariante relacionadas à vivacidade comparado a apenas 8,3% para propriedades de segurança (safety), destacando uma fraqueza no raciocínio temporal.
• Utilidade Qualitativa: Apesar das limitações quantitativas, os modelos gerados por IA reproduziram bugs conhecidos em cinco sistemas diferentes, demonstrando utilidade prática para verificação de correção parcial.

Significância e Alegações

Os autores posicionam o SYSMOBENCH como um passo fundamental para avançar a IA da "inteligência de código" para a "inteligência de sistema".

• Benchmarking da Realidade: O artigo alega que, embora a IA mostre promessa em tarefas de codificação, ela atualmente carece da capacidade de compreender, abstrair e especificar sistemas grandes e complexos necessários para verificação formal.
• Avaliação Automatizada: Ao estabelecer métricas automatizadas para sintaxe, execução, conformidade e invariantes, o SYSMOBENCH fornece uma maneira escalável e objetiva de medir o progresso, indo além das limitações dos benchmarks existentes que focam em pequenos programas ou quebra-cabeças de lógica.
• Direção Futura: Os autores veem o SYSMOBENCH como um veículo para estimular abordagens inovadoras de IA. Eles observam que o benchmark é extensível (suportando Alloy e PAT) e está em expansão ativa de sua coleção de artefatos. Eles enfatizam que o objetivo não é meramente gerar código, mas permitir que a IA ajude na verificação formal de sistemas do mundo real críticos para a segurança, de forma semelhante ao papel que o SWE-bench desempenha na engenharia de software.

O artigo conclui que os LLMs atuais são limitados na modelagem de sistemas complexos, mas que o framework fornece as ferramentas necessárias para rastrear melhorias e guiar o desenvolvimento de agentes de IA mais capazes para a modelagem de sistemas formais.