Graph Construction and Matching for Imperative Programs using Neural and Structural Methods

1. Declaração do Problema

O desafio central abordado é a reutilização de artefatos de verificação (especificações, contratos e provas) na engenharia de software. Apesar da existência de grandes repositórios desses artefatos, sua reutilização permanece majoritariamente manual e ineficiente. Desenvolvedores têm dificuldade em encontrar artefatos relevantes porque as soluções existentes frequentemente diferem em:

• Sintaxe: Diferentes linguagens de programação (C, Java, C#) e estilos de especificação (ACSL, JML, Dafny).
• Níveis de Abstração: Graus variados de detalhe na implementação.
• Vocabulário de Domínio: Terminologia específica que obscurece a similaridade semântica.

As abordagens atuais frequentemente dependem de adaptação manual ou correspondência sintática simples, falhando em capturar correspondências semânticas sob equivalência parcial (onde apenas fragmentos de comportamento ou intenção se alinham). Os autores propõem que representar esses artefatos como grafos tipados e atribuídos, enriquecidos com embeddings semânticos neurais, pode preencher essa lacuna, permitindo a descoberta automatizada de similaridades estruturais e semânticas.

2. Metodologia

O artigo apresenta um pipeline unificado e de ponta a ponta que transforma programas imperativos e suas anotações em representações de grafos, enriquece-os com dados semânticos e realiza correspondência de similaridade.

A. Geração e Transformação de Dados

Os pesquisadores iniciaram com um conjunto de dados base de 56 programas em C (categorizados por complexidade estrutural: corretos, diferenças óbvias, diferenças sutis). Eles geraram sistematicamente variantes multilíngues usando scripts Python baseados em regras:

1. C + ACSL: Programas em C anotados com a Linguagem de Especificação ANSI/ISO C (ACSL).
2. Java + JML: Programas em C traduzidos para Java e anotados com a Linguagem de Modelagem Java (JML).
3. C# + Dafny: Programas em C traduzidos para C# e posteriormente transformados em Dafny (uma linguagem orientada à verificação com especificações integradas).

B. Construção de Grafos

O pipeline converte código-fonte e especificações em grafos direcionados, tipados e atribuídos usando networkx.

• Estrutura: Nós representam elementos sintáticos (variáveis, predicados, fluxo de controle, obrigações de prova), e arestas representam relações (fluxo de controle, fluxo de dados, dependências lógicas).
• Análise Sintática (Parsing):
  • C: Utiliza clang.cindex (libclang) para extrair Árvores de Sintaxe Abstrata (ASTs).
  • Java: Utiliza javalang para extração de ASTs.
  • Dafny: Utiliza correspondência de padrões baseada em regex para extrair assinaturas de métodos e especificações (devido à falta de um analisador padrão no pipeline).
• Injeção de Especificação: Crucialmente, especificações formais (por exemplo, requires, ensures, invariant) não são apenas texto; elas são explicitamente injetadas como nós dedicados e vinculados aos seus elementos de programa correspondentes dentro do grafo.

C. Enriquecimento Semântico (Embeddings Neurais)

Para capturar significado além da sintaxe, o pipeline integra Modelos de Linguagem de Grande Escala (LLMs):

• Linearização Textual: Nós do grafo são agregados em sequências textuais.
• Geração de Embeddings:
  • SentenceTransformer (all-MiniLM-L6-v2) é utilizado para os pipelines C, Java e C#.
  • CodeBERT é utilizado para o pipeline Dafny.
• Armazenamento Vetorial: Esses modelos geram embeddings vetoriais densos que capturam tanto padrões sintáticos quanto significado semântico latente (incluindo a intenção das especificações).

D. Correspondência de Grafos

A correspondência é realizada via cálculo de similaridade par a par:

• Métrica: A similaridade cosseno é calculada entre os vetores de embedding de diferentes grafos de programas.
• Saída: Um escore de similaridade (de 0,0 a 1,0) é gerado para cada par de programas, permitindo a classificação e recuperação dos artefatos mais similares semanticamente e estruturalmente.

3. Contribuições Principais

1. Pipeline Unificado: Um único framework de ponta a ponta para construção e correspondência de grafos através de linguagens heterogêneas (C, Java, C#) e frameworks de especificação (ACSL, JML, Dafny).
2. Transformação Automatizada: Implementação de scripts baseados em regras para gerar conjuntos de dados aumentados com especificações, garantindo consistência estrutural entre linguagens.
3. Representação Híbrida: Uma técnica novel que codifica tanto a estrutura do programa (via grafos baseados em AST) quanto especificações formais (via nós injetados) em uma única estrutura de grafo.
4. Integração Neural: Integração bem-sucedida de modelos baseados em transformadores (SentenceTransformer, CodeBERT) para enriquecer nós de grafos com embeddings semânticos, permitindo correspondência de similaridade que vai além da comparação nível de token.
5. Viabilidade Multilíngue: Demonstração de que representações de grafos consistentes podem ser construídas para corresponder artefatos através de diferentes ecossistemas de linguagens.

4. Resultados

Os experimentos foram conduzidos no conjunto de dados gerado (168 instâncias totais entre categorias).

• Distribuição de Similaridade: O sistema distinguiu com sucesso algoritmos não relacionados (escores de similaridade baixos, por exemplo, 0,35–0,60) e variantes do mesmo algoritmo (escores de similaridade altos, por exemplo, 0,80–0,95+).
• Sensibilidade Semântica: Escores altos foram observados para programas com padrões algorítmicos compartilhados (por exemplo, ordenação, busca) mesmo quando implementados em linguagens diferentes ou com estilos de especificação distintos.
• Impacto da Especificação: A inclusão de especificações formais na estrutura do grafo melhorou a expressividade da correspondência. Por exemplo, no conjunto de dados Dafny, variantes de "quicksort" mostraram similaridade muito alta (0,95–1,00), enquanto algoritmos estruturalmente distintos (por exemplo, ordenação por inserção vs. quicksort) mostraram similaridade próxima de zero.
• Robustez: O sistema lidou efetivamente com variantes "espelho" e "únicas", identificando equivalência lógica apesar de mudanças sintéticas superficiais.

5. Significância e Trabalho Futuro

Significância:

• Reutilização Escalável: Este trabalho fornece uma base prática para automatizar a recuperação e adaptação de artefatos de verificação, afastando-se da busca manual.
• Correspondência Semântica: Ao combinar grafos estruturais com embeddings neurais, a abordagem aborda a "lacuna semântica" que a correspondência puramente sintática perde.
• Agnosticismo de Linguagem: O pipeline prova que artefatos de verificação podem ser normalizados em um formato de grafo comum, facilitando a verificação cruzada entre linguagens.

Limitações e Direções Futuras:

• Dependência de Análise Sintática: A abordagem atual depende fortemente de regex e extração baseada em regras (especialmente para Dafny), o que pode ser frágil para código complexo ou não padrão. Trabalhos futuros visam uma análise sintática semântica completa.
• Especificidade do Modelo: Os modelos de embedding são de propósito geral e não foram treinados especificamente em artefatos de verificação formal, potencialmente perdendo nuances semânticas de granularidade fina.
• Próximos Passos: Os autores planejam integrar algoritmos de correspondência aproximada de grafos e técnicas de reescrita de grafos para não apenas encontrar artefatos similares, mas também adaptá-los e refiná-los automaticamente para novos contextos.

Em conclusão, este artigo estabelece um primeiro passo crítico em direção ao Raciocínio Formal Infundido por Aprendizado (LIFR), demonstrando que uma abordagem híbrida de construção de grafos estruturais e enriquecimento semântico neural é um caminho viável para verificação de software automatizada e escalável.