Resumo Técnico: Síntese de Refinamentos de Protocolos de Comunicação Livres de Deadlock Guiada por Especificação com Grandes Modelos de Linguagem

1. Declaração do Problema

Garantir a correção comportamental em sistemas de software distribuídos é um desafio crítico, pois inconsistências sutis em protocolos de comunicação frequentemente levam a deadlocks (impasses). Embora os Grandes Modelos de Linguagem (LLMs) tenham demonstrado proficiência na geração de código sintaticamente correto e no atendimento de propriedades semânticas locais (ex: segurança de tipos), eles carecem de mecanismos para garantir a correção comportamental global, particularmente em cenários de interação complexos.

Inversamente, os Tipos de Sessão Multiparty (MPST) fornecem garantias formais rigorosas, incluindo segurança de comunicação e ausência de deadlock, por meio da subtipagem assíncrona multiparty (AMS). A AMS permite que um protocolo (subtipo) substitua com segurança outro (supertipo) enquanto preserva essas propriedades. No entanto, a síntese automática de tais subtipos não é trivial. O problema é agravado pelo fato de que a AMS é geralmente indecidível, e as ferramentas existentes oferecem suporte limitado para a construção automática de refinamentos de protocolo válidos.

A questão central de pesquisa abordada é: Como refinamentos de protocolo podem ser sistematicamente sintetizados mantendo a correção comportamental (especificamente a ausência de deadlock) sob a subtipagem assíncrona multiparty?

2. Metodologia: O Framework Syntropy

Os autores propõem o Syntropy, um framework que une LLMs e especificações formais para sintetizar refinamentos de protocolo válidos. O framework consiste em dois módulos complementares: Syntropy-Train e Syntropy-Gen.

2.1 Syntropy-Train: Aprendendo a Geração de Subtipos

• Fine-Tuning: Os autores realizam o ajuste fino de LLMs de código aberto (ex: Qwen2.5-Coder-7B) utilizando LoRA (Low-Rank Adaptation).
• Construção de Dados: O conjunto de dados de treinamento compreende pares de (supertipo, subtipo) derivados da literatura de MPST e benchmarks sintéticos. Os subtipos são gerados via procedimentos heurísticos baseados em algoritmos de subtipagem assíncrona e validados por um verificador formal.
• Representação: Os tipos de sessão são convertidos em uma sintaxe estilo BNF amigável ao modelo (ex: p!m; T explícito para envios, p?m; T para recebimentos e REC_X_OPEN/CLOSE para recursão) para reduzir a ambiguidade.
• Prompting: Os prompts incluem contexto teórico descrevendo regras de transformação (Identity, RefA, RefB, RefIn, RefOut, Unfold) para guiar o modelo em direção a transformações estruturalmente válidas.
• Função de Perda: É utilizada uma perda de nível de token ponderada, priorizando a geração de sequências de subtipos válidos sobre rótulos auxiliares.

2.2 Syntropy-Gen: Geração com Restrição via Monitoramento de Dois Níveis

Para garantir a correção semântica além do que o LLM pode garantir por construção, o Syntropy-Gen emprega uma estratégia de monitoramento de dois níveis durante o processo de geração por busca de feixe (beam search):

• Nível 1: Verificação de Derivada ao Nível de Token (Filtragem de Prefixo):
  • A cada etapa de decodificação, o prefixo atual é analisado em uma árvore de sessão parcial.
  • Uma verificação de derivada coindutiva leve verifica se o prefixo ainda pode ser estendido para um subtipo válido do supertipo.
  • Se a verificação falhar (ou seja, se não houver uma conclusão válida possível), o feixe é podado imediatamente. Isso atua como uma sobre-aproximação grosseira para eliminar caminhos infactíveis precocemente.
• Nível 2: Verificador de Ponto Fixo Baseado em Alargamento (Verificação Final):
  • Quando uma sequência candidata atinge o token de Fim de Sequência (EOS), ela é analisada em uma árvore de sessão completa.
  • Um verificador de subtipo completo (baseado em raciocínio de derivada e operadores de alargamento para lidar com recursão) verifica se a árvore completa é um subtipo válido do supertipo.
  • Este passo é conservador; ele aceita subtipos válidos, mas pode rejeitar alguns subtipos válidos devido à indecidibilidade do problema geral.

Este design de dois níveis equilibra a eficiência computacional (Nível 1) com o rigor semântico (Nível 2), garantindo que apenas candidatos que satisfaçam a relação de subtipagem assíncrona sejam retidos.

3. Principais Contribuições

1. Geração de LLM com Garantias Comportamentais: Uma abordagem inovadora que permite aos LLMs sintetizar refinamentos de protocolos MPST com garantia de ausência de deadlock e segurança de comunicação.
2. Refinamento de Protocolo Guiado por Especificação: Uma codificação sistemática de especificações MPST que guia e restringe a geração do LLM, indo além da correção sintática local para propriedades comportamentais globais.
3. Geração Integrada de Restrições: Um fluxo de trabalho de geração de dois níveis que integra a validação de restrições diretamente no processo de síntese via filtragem de prefixo e subsequente verificação.
4. Framework e Avaliação do Syntropy: Implementação e avaliação abrangente demonstrando alta validade e a capacidade de gerar refinamentos diversos e não triviais.

4. Resultados Experimentais

O framework foi avaliado em dois conjuntos de dados (derivados da literatura e sintéticos) utilizando múltiplos LLMs (de 7B a 32B parâmetros).

• Validade: O Syntropy alcança 95,6%–99,5% de validade semântica em todos os modelos ao utilizar o Monitoramento de Dois Níveis, comparado a taxas significativamente menores (ex: 60,4%) para geração direta sem monitoramento. A validade sintática permanece alta (95,4%–98,1%).
• Diversidade: O framework produz refinamentos estruturalmente distintos, incluindo transformações de reordenação (RefA, RefB) e variância (RefIn, RefOut), em vez de variações triviais.
• Escala de Dados: O desempenho satura em torno de 9.500 pares de treinamento; aumentar os dados além disso gera ganhos marginais.
• Estudos de Ablação:
  • A remoção do Monitoramento de Dois Níveis causa uma queda drástica na validade semântica (para ~60%), confirmando sua necessidade para a correção.
  • A remoção do Prompting reduz a diversidade estrutural e diminui ligeiramente a validade semântica, indicando seu papel em guiar a cobertura de transformação.
• Comparação com Modelos de Fronteira: Embora os modelos de fronteira (ex: GPT-5.5, DeepSeek-V4-Pro) possam gerar subtipos válidos com alta validade nos poucos casos que cobrem, sua cobertura é extremamente limitada (4%–18% dos benchmarks). Em contraste, o Syntropy oferece cobertura total em todo o conjunto de benchmarks.

5. Significância e Alegações

O artigo alega que o Syntropy aborda com sucesso a lacuna entre as capacidades generativas dos LLMs e os requisitos rigorosos de correção de sistemas distribuídos. Ao integrar especificações formais (MPST) diretamente no loop de geração, o framework garante que os refinamentos de protocolo sintetizados sejam livres de deadlock e comportamentalmente compatíveis.

Os autores enfatizam que, embora os LLMs de fronteira mostrem potencial, eles atualmente carecem da cobertura sistemática necessária para o refinamento abrangente de protocolos. O Syntropy demonstra que modelos ajustados, quando acoplados a restrições de verificação formal, podem produzir de forma confiável variantes de protocolos diversas e corretas que são difíceis de construir manualmente. Este trabalho posiciona-se como um passo em direção à aplicação de LLMs em tarefas de engenharia de software de missão crítica, onde as garantias comportamentais são inegociáveis.

Limitações Reconhecidas:

• A métrica de validade semântica depende de um verificador que é íntegro, mas incompleto (devido à indecidibilidade da AMS); portanto, candidatos rejeitados não são definitivamente provados incorretos.
• A avaliação está focada atualmente na geração de subtipos dentro de MPST, e a generalização para outros formalismos ou tarefas de geração permanece como um trabalho futuro.