Resumo Técnico: Agente Event-B

Declaração do Problema

O desenvolvimento de software "correto por construção" depende de métodos formais, onde o comportamento do sistema e os requisitos são expressos matematicamente e verificados por meio de prova de teoremas e verificação de modelos. No entanto, a curva de aprendizado íngreme e a demanda por expertise matemática têm impedido a adoção generalizada desses métodos. Embora os Modelos de Linguagem de Grande Escala (LLMs) tenham mostrado promessa na autoformalização, as abordagens existentes são amplamente limitadas a tarefas isoladas, como prova de teoremas sem formalização ou síntese de modelos verificada apenas por verificação de modelos limitada.

Crucialmente, os métodos atuais baseados em LLMs falham em apoiar a evolução iterativa e conjunta de modelos formais e suas provas associadas. Na prática, o desenvolvimento formal exige que, quando um provador de teoremas falha em descarregar uma obrigação de prova (PO), o sistema permita revisões tanto no modelo formal quanto em seus artefatos de prova. As ferramentas existentes ou assumem um modelo fixo e buscam provas (assistentes de prova LLM) ou constroem modelos sem verificação rigorosa baseada em provas (autoformalização). Há uma falta de frameworks que formulem o desenvolvimento formal como um processo coordenado sobre um espaço de estados conjunto de modelos e provas, permitindo refinamento e reparo iterativos.

Metodologia: Agente Event-B

Para abordar essas lacunas, os autores propõem o Agente Event-B, um novo framework neurosimbólico para síntese e reparo de modelos formais de ponta a ponta. O framework é projetado para receber requisitos em linguagem natural e construir um modelo formal Event-B por meio de um processo iterativo que integra refinamento, síntese e reparo.

A metodologia consiste em três etapas principais:

1. Planejamento de Estratégia de Refinamento

Reconhecendo que o raciocínio automatizado sobre sistemas complexos é desafiador devido ao rápido crescimento do espaço de busca, o Agente Event-B emprega LLMs para planejar uma estratégia de refinamento.

• Decomposição: O agente particiona o conjunto de requisitos em linguagem natural em subconjuntos disjuntos, distribuindo-os por múltiplos passos de refinamento.
• Invariantes de Colagem: Para cada transição entre passos de refinamento, o LLM propõe "invariantes de colagem"—predicados relacionando variáveis abstratas e concretas para garantir consistência.
• Validação: Essas invariantes são validadas por meio de verificação de contraexemplos (usando um verificador de modelos) e tentativas de prova antes de serem aceitas, garantindo que as propriedades provadas em etapas anteriores sejam preservadas.

2. Síntese do Modelo

Para cada passo de refinamento, o agente sintetiza um modelo formal com base nos requisitos atribuídos e nas invariantes de colagem.

• Geração Guiada por Esquema: Para mitigar erros de sintaxe comuns na geração por LLM, o sistema usa um esquema JSON que codifica a gramática Event-B. Isso garante correção estrutural (por exemplo, eventos obrigatórios, declarações de variáveis).
• Loop de Bem-Formação: O modelo gerado é compilado. Quaisquer erros de compilação (por exemplo, incompatibilidades de tipo, variáveis não declaradas) são retornados ao LLM para reparo iterativo até que o modelo seja sintaticamente válido e correto em termos de tipo.

3. Reparo de Modelo e Prova

Esta é a contribuição central do framework, projetada para lidar com a evolução conjunta de modelos e provas.

• Loop de Verificação: Os modelos sintetizados são primeiro verificados por um verificador de modelos (ProB) quanto a violações de invariantes dentro de estados limitados. Se contraexemplos forem encontrados, o modelo é reparado.
• Prova de Teoremas: O modelo é então submetido à prova de teoremas ilimitada. Se as provas falharem, o sistema analisa o estado da prova para diagnosticar o problema.
• Recomendação de Regras de Reparo: O sistema emprega um componente novo que mapeia estados de prova para regras de reparo específicas (por exemplo, "Objetivo Contraditório", "Objetivo Existencial", "Preservação de Invariante Quantificada"). Essas regras são derivadas empiricamente de experiências manuais de descarregamento de provas.
• Execução de Reparo Atômico: Um LLM de "decisão de estratégia de correção" seleciona de uma biblioteca de funções de reparo atômico (por exemplo, StrengthenGuard, AddInvariant, InstantiateHypothesis) e as executa. Isso restringe as modificações do LLM a operações sólidas e verificáveis.
• Corretude: O sistema garante corretude reproduzindo todas as provas após qualquer modificação no modelo. Um reparo é aceito apenas se o efeito combinado descarregar a PO alvo, verificado por solucionadores SMT e provadores de teoremas.

Contribuições Principais

O artigo delineia três contribuições principais:

1. Framework: O Agente Event-B é o primeiro framework de ponta a ponta para síntese e reparo de modelos formais que apoia o desenvolvimento baseado em refinamento com construção coordenada de modelos e derivação de provas, incorporando o princípio da corretude por construção.
2. Ferramenta: Uma ferramenta de prova de conceito integrada ao IDE Rodin (o ambiente padrão para Event-B), aproveitando o ProB para verificação de modelos e provadores padrão do Rodin para prova de teoremas.
3. Avaliação: Uma avaliação abrangente em 27 sistemas formais (variando de simples a complexos) comparando o Agente Event-B com linhas de base, incluindo estudos de ablação e análise de eficiência.

Resultados Experimentais

O framework foi avaliado em 27 sistemas formais com uma média de 182,41 obrigações de prova por sistema. Os resultados demonstram melhorias substanciais em relação às linhas de base (LLM + provadores automáticos, Cursor e PAT-Agent):

• Consistência (Taxa de Descarregamento de Obrigação de Prova - PDR): O Agente Event-B alcançou uma PDR de 97,86%, superando significativamente as linhas de base (89,20% a 95,56%). Manteve uma PDR acima de 97,0% em todos os níveis de complexidade, enquanto as linhas de base mostraram maior variância e degradação de desempenho com a complexidade.
• Corretude (Cobertura de Requisitos - RC e Cumprimento - RF):
  • RC: O Agente Event-B alcançou 97,13%, superando o segundo melhor método em 4,63%.
  • RF: O Agente Event-B alcançou 93,79%, superando o segundo melhor em 18,01%.
  • A razão RF/RC (0,97) indica que, uma vez que um requisito é capturado, o agente descarrega com sucesso as provas associadas, ao contrário das linhas de base onde requisitos capturados frequentemente permaneceram não provados.
• Eficiência: O tempo médio para sintetizar e reparar um sistema foi de 74,45 minutos. O tempo médio para tentar descarregar uma única PO foi de 0,24 minutos, sugerindo que a sobrecarga de reparo escala linearmente com o número de POs em vez de explodir com a complexidade do sistema.
• Estudos de Ablação: Remover a estratégia de refinamento ou o componente de orientação de reparo levou a quedas de desempenho, confirmando que esses dois componentes são mutuamente reforçadores. O refinamento reduz a complexidade da prova, enquanto a orientação de reparo garante a corretude dos passos de refinamento.

Significado e Alegações

Os autores afirmam que o Agente Event-B representa um passo promissor em direção ao desenvolvimento formal prático, sólido e assistido por LLM. Ao tratar o desenvolvimento formal como um espaço de estados conjunto de modelos e provas, o framework supera as limitações da autoformalização isolada ou da prova de teoremas.

O artigo enfatiza que:

• O refinamento é essencial para gerenciar a complexidade, permitindo que o agente decomponha problemas difíceis em etapas gerenciáveis enquanto preserva a corretude.
• O reparo guiado por provas é necessário porque a verificação de modelos sozinha (limitada) é insuficiente para a corretude geral; a prova de teoremas (ilimitada) é necessária, mas exige um mecanismo para reparar tanto o modelo quanto a prova quando o raciocínio automatizado falha.
• A abordagem neurosimbólica combina com sucesso a flexibilidade semântica dos LLMs com a corretude rigorosa das ferramentas de verificação simbólica.

Os autores permanecem modestos quanto ao escopo atual, observando que a biblioteca de regras de reparo é derivada empiricamente e não exaustiva, e que lidar com requisitos em linguagem natural inconsistentes permanece um desafio para trabalhos futuros. No entanto, os resultados sugerem que o framework proposto efetivamente preenche a lacuna entre requisitos em linguagem natural e modelos formais corretos por construção.