Resumo Técnico: TraceFix: Reparação de Protocolos de Coordenação de Agentes com Contraexemplos TLA+

1. Declaração do Problema

Agentes independentes de Modelos de Linguagem de Grande Escala (LLM) operam cada vez mais em ambientes concorrentes e assíncronos onde mutam um estado externo compartilhado. Em tais configurações, falhas do sistema frequentemente decorrem não de déficits de capacidade de agentes individuais, mas de erros de coordenação decorrentes de intercalações complexas, corridas, deadlocks e apertos de mão perdidos. Esses riscos são latentes; um protocolo pode ter sucesso em execuções observadas, mas falhar sob cronogramas não testados.

Abordagens anteriores tratam a coordenação de LLMs por meio de frameworks de orquestração (grafos explícitos), geração com solucionador no loop para correção de artefatos únicos ou guardas em tempo de execução. No entanto, essas abordagens frequentemente falham em visar especificamente a correção de protocolos concorrentes. Escrever protocolos concorrentes corretos é difícil porque casos extremos emergem apenas sob intercalações específicas e não enumeradas. Uma especificação única, seja gerada por humano ou por LLM, tende a ser plausível, mas subespecificada, carecendo de um mecanismo para descobrir sistematicamente esses casos extremos.

2. Metodologia: O Pipeline TraceFix

O TraceFix introduz um pipeline de verificação primeiro que trata o design de protocolos como um loop iterativo de síntese, verificação de modelo e reparo. O sistema opera em duas fases: síntese em tempo de design e aplicação em tempo de execução.

2.1 Loop em Tempo de Design

O pipeline consiste em quatro estágios impulsionados por um agente de orquestração:

1. Síntese de Topologia: O agente sintetiza uma Representação Intermediária (IR) de Topologia de Protocolo a partir de uma descrição de tarefa em linguagem natural. Esta IR define declarativamente agentes, recursos compartilhados (travas, contadores) e canais de mensagens direcionados e rotulados (filas FIFO). Ela é validada estruturalmente via esquema JSON antes de prosseguir.
2. Geração de Lógica: A topologia é compilada em PlusCal (uma notação algorítmica para TLA+). O agente gera corpos de processo por agente contendo fluxos de controle explícitos (envios, recebimentos, aquisições de travas) e escolhas não determinísticas (either/or).
3. Verificação de Modelo: O código PlusCal é traduzido para TLA+ e verificado usando o verificador de modelo TLC. O TLC explora exaustivamente todos os estados alcançáveis sob suposições limitadas (por exemplo, profundidades de fila limitadas) para verificar propriedades de segurança:
   • Liberdade de Deadlock: Nenhum estado onde nenhum agente possa prosseguir.
   • Exclusão Mútua: Nenhum dois agentes seguram a mesma trava.
   • Travas Órfãs: Nenhuma trava segurada ao término.
   • Drenagem de Canal: Todos os canais estão vazios quando os agentes terminam.
4. Reparo Orientado a Contraexemplos: Se o TLC encontrar uma violação, ele retorna um traço de contraexemplo concreto. Um agente de reparo usa esse traço para editar o código-fonte PlusCal (por exemplo, impondo ordem de travas, adicionando apertos de mão, reestruturando loops) para eliminar o testemunho específico de falha. O loop se repete até que o TLC não encontre violações.

2.2 Aplicação em Tempo de Execução

Uma vez que um protocolo passa na verificação, os corpos de processo verificados são compilados em prompts de sistema para os agentes. Um monitor de topologia executa ao lado dos agentes em tempo de execução. Este monitor aplica a interface de coordenação definida na topologia:

• Ele valida que toda operação de coordenação (envio, recebimento, aquisição, liberação) visa um canal ou recurso declarado com um rótulo válido.
• Ele rejeita qualquer operação que viole a topologia (operações fora da topologia).
• Ele não aplica ordenação de passos ou justiça; apenas garante que os agentes permaneçam dentro do contrato estrutural verificado. Os agentes mantêm autonomia sobre ferramentas de domínio e tomada de decisão dentro dessas restrições.

3. Contribuições Principais

1. Sistema TraceFix: Um agente de design de protocolos que sintetiza uma IR de topologia, gera lógica de coordenação em PlusCal e repara iterativamente protocolos usando contraexemplos do TLC até que a verificação seja bem-sucedida.
2. Benchmark de Coordenação: Um novo benchmark de 48 tarefas em 16 famílias de cenários (abrangendo desenvolvimento de software, pesquisa, manufatura e CI/CD) em três níveis de dificuldade. A verdade fundamental é definida pela correção da coordenação (liberdade de deadlock, exclusão mútua) e não por semântica de domínio.
3. Aplicação de Topologia em Tempo de Execução: Uma camada de monitoramento que preserva a autonomia do agente enquanto rejeita operações de coordenação que se desviam da topologia do protocolo verificado.
4. Estudo de Ablação Emparelhado: Um isolamento experimental da contribuição do reparo orientado a contraexemplos, comparando variantes de protocolos verificados versus não verificados sob condições idênticas de tempo de execução.

4. Resultados Empíricos

A avaliação foi conduzida no benchmark de 48 tarefas usando o Claude Opus 4.6 para design de protocolos e gpt-5-mini/gpt-5-nano para execução em tempo de execução (3.456 execuções no total).

4.1 Convergência de Verificação

• 100% de Taxa de Aprovação Final: Todas as 48 tarefas atingiram a verificação completa do TLC.
• Eficiência: 62,5% das tarefas passaram na primeira tentativa. Nenhuma tarefa exigiu mais de quatro iterações de reparo.
• Escalabilidade: Os espaços de estado abrangiam seis ordens de grandeza (de 30 a 7,7 milhões de estados distintos). Apesar disso, a verificação foi concluída em menos de 60 segundos para cada tarefa (mediana <1s).
• Taxonomia de Falhas: Das 29 tentativas de reparo necessárias, 69% foram deadlocks. Os padrões de falha dominantes foram riscos estruturais de coordenação (por exemplo, recebimentos não determinísticos antes de verificações de canal, agentes hub terminando antes de agentes satélite completarem loops de nova tentativa) e não falhas fundamentais de design. Tarefas apenas com travas passaram 100% na primeira tentativa, indicando que a semântica de canal é a principal fonte de complexidade.

4.2 Desempenho em Tempo de Execução

Uma comparação de quatro arquiteturas de tempo de execução (Monitorada por Topologia, Aplicada por Mediador, Apenas Prompt, Apenas Chat) revelou:

• Maior Conclusão: A execução Monitorada por Topologia alcançou a maior conclusão de tarefas (89,4% em média, 81,5% de conclusão total).
• Segurança: Reduziu significativamente as taxas de Deadlock/Livelock (DL/LL) em comparação com as linhas de base.
• Degradação do Modelo: Quando a capacidade do modelo foi reduzida (de gpt-5-mini para gpt-5-nano), as execuções usando o protocolo verificado degradaram-se a aproximadamente metade da taxa das linhas de base apenas-prompt ou apenas-chat. O protocolo verificado atua como um "buffer de capacidade".
• Tolerância a Falhas: Sob falhas injetadas, o protocolo verificado manteve altas taxas de conclusão, enquanto as linhas de base sofreram quedas severas de desempenho.

4.3 Estudo de Ablação

Sob uma execução Monitorada por Topologia fixa, a comparação entre protocolos verificados e não verificados mostrou que o reparo orientado a contraexemplos reduziu as taxas de DL/LL de 31,1% para 14,1%. A melhoria foi mais pronunciada sob injeção de falhas, confirmando que o processo de reparo remove riscos concretos de coordenação que se amplificam sob condições adversas.

5. Significado e Afirmativas

O artigo afirma que o TraceFix demonstra a viabilidade de um paradigma gerar/verificar/reparar para coordenação de múltiplos agentes de LLM.

• Necessidade de Reparo: O loop é necessário, pois mais de um terço das tentativas iniciais falham, mas é suficiente, pois todos convergem dentro de um pequeno orçamento de iterações.
• Tratabilidade: A verificação de modelo limitada permanece tratável mesmo para grandes espaços de estado, desacoplando o tempo de verificação da magnitude do espaço de estado.
• Benefício em Tempo de Execução: Protocolos verificados fornecem melhorias mensuráveis e tangíveis na conclusão de tarefas e robustez contra degradação do modelo e falhas.
• Limitação de Escopo: O sistema verifica segurança de coordenação (deadlock, exclusão mútua) sob suposições limitadas. Ele não verifica semântica de tarefa, qualidade de saída ou propriedades de vivacidade (por exemplo, término garantido), pois protocolos de LLM frequentemente contêm loops não determinísticos válidos que seriam rejeitados por verificações estritas de vivacidade.

O trabalho posiciona-se como uma instanciação concreta da integração de métodos formais com sistemas de LLM, visando especificamente as "lacunas de especificação e orquestração" identificadas como modos de falha dominantes em sistemas de múltiplos agentes. Ele complementa frameworks de otimização existentes (como DSPy) ao verificar como os agentes coordenam, em vez de o que eles produzem.