Causal Past Logic for Runtime Verification of Distributed LLM Agent Workflows

Resumo Técnico: Lógica do Passado Causal para Verificação em Tempo Real de Fluxos de Trabalho de Agentes LLM Distribuídos

Declaração do Problema
Fluxos de trabalho de agentes de Modelos de Linguagem (LLM) distribuídos, onde múltiplos agentes interagem assincronamente sem memória compartilhada, não podem ser monitorados efetivamente como se produzissem um único log sequencial. Em execuções assíncronas, uma decisão tomada por um agente (uma "linha de vida") depende apenas de eventos que são causalmente visíveis a ele. Um evento que aparece mais cedo em um log sequencial global pode ainda não ser conhecido localmente, enquanto um evento localmente recente pode não refletir o estado mais recente de um agente remoto.

Abordagens existentes de verificação em tempo real frequentemente dependem de traços sequenciais ou análise de logs post-hoc. No entanto, para fluxos de trabalho de agentes, isso é insuficiente porque o monitoramento deve influenciar a execução no ponto da decisão. Se um tomador de decisão (por exemplo, um Committed) não tiver visto causalmente um resultado de teste limpo, o sistema não deve mesclar e relatar uma violação posteriormente; deve bloquear a mesclagem ou solicitar uma nova execução imediatamente. Além disso, mecanismos de guarda padrão em aplicações LLM frequentemente tratam a execução como um log sequencial, ignorando a estrutura causal necessária para a tomada de decisão distribuída correta.

Metodologia
Os autores estendem o framework ZipperGen, um sistema de programação coreográfica para agentes LLM distribuídos, introduzindo a Lógica do Passado Causal (CPL).

1. Modelo Formal (MSCs): As execuções são modeladas como Diagramas de Sequência de Mensagens (MSCs), onde os eventos são distribuídos sobre linhas de vida. A ordem causal é definida pelo fecho reflexivo transitivo da sucessão local e da entrega de mensagens. Cada evento carrega uma valoração de variáveis locais.
2. Lógica do Passado Causal (CPL): A CPL é uma pequena lógica temporal de tempo passado projetada como uma linguagem de guarda em nível de fonte.
   • Sintaxe: Fórmulas incluem modalidades padrão de tempo passado (Anterior $Y$, Desde $S$) interpretadas ao longo de uma única linha de vida, e uma modalidade causal $@A(\phi)$ que avalia $\phi$ no evento mais recente da linha de vida $A$ que é causalmente visível ao evento atual.
   • Acesso a Variáveis: A lógica suporta termos como $@A.x$, que leem o valor da variável $x$ no evento causalmente visível mais recente da linha de vida $A$.
   • Semântica: Uma guarda $\phi@A$ é avaliada localmente pela linha de vida proprietária $A$ em um ponto de decisão (ramo ou loop). O valor verdade determina o fluxo de controle. A lógica não é estrita: se nenhum evento de $A$ for visível, a fórmula avalia-se como falsa.
3. Algoritmo de Monitoramento Online:
   • Os autores propõem um algoritmo de monitoramento distribuído onde cada linha de vida mantém um relógio vetorial e visões de último valor.
   • Estado: Cada agente mantém um relógio vetorial para rastrear o número de eventos vistos de cada outra linha de vida. Ele também mantém um mapa parcial de "visões de último valor" para fórmulas booleanas e valores de variáveis de outras linhas de vida.
   • Propagação: Quando um agente envia uma mensagem, ele anexa seu relógio vetorial atual e visões de último valor. Ao receber uma mensagem, o agente mescla essas visões com seu estado local, atualiza seu relógio vetorial e reavalia todas as guardas de baixo para cima.
   • Correção: O algoritmo garante que o valor do monitor computado localmente coincida com a semântica denotacional da guarda sobre o MSC.

Contribuições Principais

• Lógica do Passado Causal (CPL): Uma lógica nova para fluxos de trabalho de agentes distribuídos que combina operadores padrão de tempo passado com acesso causal ao estado mais recente visível de outros agentes. Permite que guardas expressem condições como "os testes necessários passaram e nenhuma falha foi vista desde então, no passado causal".
• Guardas em Nível de Fonte: Ao contrário de monitores externos que verificam logs post-hoc, as fórmulas CPL são integradas ao código-fonte do fluxo de trabalho. Elas são avaliadas online pelo tomador de decisão para influenciar diretamente o fluxo de controle.
• Monitoramento Distribuído com Relógios Vetoriais: Um algoritmo de monitoramento online eficiente que usa relógios vetoriais e visões de último valor para rastrear a visibilidade causal sem exigir um observador central ou um log sequencial global.
• Verificação Formal: As definições de MSCs, satisfação CPL, o avaliador local e o teorema de correção do monitor são mecanizadas e verificadas em Lean 4. O artigo prova que a avaliação em tempo real local de uma guarda corresponde à sua semântica denotacional no evento atual.
• Implementação Protótipo: Uma implementação protótipo no framework ZipperGen (Python) demonstra a viabilidade da abordagem, mostrando como guardas podem comparar variáveis entre linhas de vida (por exemplo, garantindo que um resultado de teste corresponda ao candidato de mesclagem atual).

Resultados

• Teórico: O artigo prova o Lema 1 (Correção da avaliação local) e o Lema 2 (Invariantes de estado do monitor), culminando no Teorema 1 (Correção do monitor). Essas provas estabelecem que o algoritmo distribuído calcula corretamente o valor verdade de qualquer fórmula CPL com base no passado causal visível à linha de vida proprietária.
• Prático: A implementação protótipo no ZipperGen lida com sucesso com o exemplo de uma revisão de código distribuída, onde um Committed decide mesclar um patch apenas se causalmente ver testes aprovados e varreduras de segurança para o candidato específico, bloqueando a mesclagem se uma falha for visível no passado causal.

Significado
O artigo argumenta que a verificação em tempo real para fluxos de trabalho de agentes LLM distribuídos deve ir além da análise de logs sequenciais. Ao tratar o monitoramento como parte integrante da linguagem de coordenação (via guardas em nível de fonte), o sistema pode tomar decisões corretas com base nas informações causalmente visíveis disponíveis no ponto de decisão, em vez de esperar por um log global ou um observador central. Essa abordagem aborda a dificuldade fundamental da programação distribuída, onde decisões locais dependem de visões causais parciais. O trabalho preenche a lacuna entre programação coreográfica (especificações globais projetadas em agentes locais) e aplicação de execução, garantindo que propriedades de segurança e coordenação sejam aplicadas dinamicamente e corretamente do ponto de vista causal.