💻 computer science

Composable Verification Pipelines for Multi-Agent Systems

Este artigo introduz um framework de programação funcional e modular implementado em Soda que possibilita pipelines de verificação composíveis para sistemas multiagentes, permitindo que usuários definam descrições de domínio em YAML e executem fluxos de raciocínio transparentes e com terminação garantida para sistemas dinâmicos envolvendo cenários complexos como desinformação e raciocínio emocional.

Autores originais: Julian Alfredo Mendez, Andreas Brännström

Publicado 2026-07-21

📖 4 min de leitura☕ Leitura rápida

CC BY 4.0

Autores originais: Julian Alfredo Mendez, Andreas Brännström

Artigo original sob licença CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo

Imagine um mundo onde programas de computador não são apenas linhas de código, mas personagens em uma história viva. No reino da ciência da computação, existe um campo dedicado a descobrir como esses personagens se movem, mudam e interagem ao longo do tempo. Este é o estudo da "ação e mudança". Pense nisso como um jogo de tabuleiro onde as peças se movem, as regras ditam o que é permitido e o objetivo é prever se o jogo terminará em uma vitória justa ou em uma bagunça caótica. Por anos, cientistas usaram ferramentas pesadas, baseadas em lógica, para escrever essas regras, tentando provar que um sistema se comporta corretamente. Mas essas ferramentas podem ser desajeitadas, como tentar construir um castelo de Lego complexo usando apenas um único tijolo gigante. Elas funcionam, mas não são muito flexíveis ou fáceis de compartilhar com outros tipos de construtores.

Agora, imagine se você pudesse construir esse castelo usando peças modulares, de encaixar, que qualquer pessoa pudesse entender e rearranjar. Esse é o problema que Julian Alfredo Mendez e Andreas Brännström estão enfrentando. Eles querem criar uma maneira de verificar se uma história digital (uma sequência de ações e estados) segue as regras, mas querem fazer isso usando uma abordagem moderna e flexível que pareça mais com construir com LEGO de alta tecnologia do que resolver um quebra-cabeça matemático. Eles estão perguntando: Podemos tornar a verificação de sistemas multiagentes complexos (como uma equipe de robôs ou uma rede social de bots) tão fácil e transparente quanto conectar tubos em uma fábrica?

Os autores introduzem um novo framework chamado "Composable Verification Pipelines" (Pipelines de Verificação Componíveis). Em vez de usar os antigos e pesados tijolos de lógica, eles construíram um sistema baseado em "Tiles" (Ladrilhos) e uma linguagem chamada "Soda". Pense nos "Tiles" como um conjunto de tubos mágicos e transparentes. Cada tubo faz um trabalho simples: recebe um pedaço de dado (como o estado do mundo ou uma ação que um agente tomou), processa-o e o passa para o próximo tubo. Ao encaixar esses tubos, você cria um "pipeline" que pode observar uma história inteira se desenrolar e verificar cada passo contra as regras.

O artigo propõe que você pode descrever um sistema complexo — como um grupo de agentes compartilhando notícias ou tomando decisões — usando um formato simples e legível chamado YAML (que é como uma lista de tarefas estruturada). Uma vez que você escreve suas regras e sua história nesse formato, o framework as transforma automaticamente em uma corrente desses tubos funcionais. À medida que a história se desenrola, os dados fluem pelo pipeline. Um tubo pode verificar se uma ação foi permitida; outro pode ver se uma regra foi quebrada; um terceiro pode combinar tudo para dar um "Sim" ou "Não" final sobre se a história é válida.

Os pesquisadores mostram que essa abordagem não é apenas uma teoria; eles a construíram e a testaram. Eles demonstraram que, ao decompor o processo de verificação nesses componentes pequenos e reutilizáveis, eles conseguem lidar com cenários complexos, como a disseminação de desinformação em uma rede social ou como as emoções afetam as decisões de um agente. Por exemplo, em um caso, uma história sobre um agente compartilhando uma mentira pareceu uma violação de regra no início. Mas quando eles adicionaram "fluentes emocionais" (regras sobre como o agente se sente) ao pipeline, a história de repente fez sentido e tornou-se válida. Isso prova que o sistema deles pode ser facilmente ajustado para incluir novos detalhes mais ricos sem ter que reconstruir toda a máquina.

Crucialmente, o artigo prova que esses pipelines sempre terminarão seu trabalho. Como o sistema é construído a partir de etapas simples e finitas, ele garante que o processo de verificação não ficará preso em um loop infinito. Eles também mediram a velocidade com que ele executa, mostrando que o tempo que leva cresce de uma forma previsível e linear à medida que se adicionam mais regras ou histórias mais longas. Os autores sugerem que este método faz a ponte entre a matemática pesada das linguagens de ação e o mundo flexível e modular da engenharia de software moderna, tornando mais fácil construir e verificar sistemas complexos baseados em regras no futuro.

Resumo Técnico: Pipelines de Verificação Componíveis para Sistemas Multiagentes

Declaração do Problema

A crescente complexidade dos sistemas dinâmicos e multiagentes intensificou a necessidade de mecanismos de verificação executáveis capazes de analisar execuções em evolução sob restrições baseadas em regras. Embora o trabalho seminal sobre linguagens de ação (ex: CMT, GOLOG, STRIPS) forneça semânticas expressivas para o raciocínio sobre ação e mudança, as implementações existentes são predominantemente baseadas em sistemas de programação lógica. Isso cria uma barreira para a integração de soluções de verificação com práticas de engenharia de software convencionais, particularmente dentro das comunidades de programação funcional e orientada a objetos. Os autores identificam uma lacuna no fornecimento de fluxos de trabalho de verificação modulares, composíveis e transparentes que possam ser operacionalizados dentro de ecossistemas de software padrão (como a JVM), mantendo uma semântica rigorosa.

Metodologia

O artigo propõe um framework modular para verificação de transição e trajetória que operacionaliza a semântica de linguagens de ação através de pipelines funcionais executáveis. A metodologia é construída sobre três pilares centrais:

Modelo Formal (Baseado em CMT): O framework utiliza a linguagem de ação CMT, que define uma linguagem de descrição de domínio ( $D_{MT}$ ) consistindo em leis causais estáticas e dinâmicas. Essas leis governam a evolução do estado através de trajetórias definidas como sequências de estados e conjuntos de ações ( $\langle s_0, A_1, s_1, \dots, A_n, s_n \rangle$ ).
- Representação de Fluentes: Diferente das representações tradicionais baseadas em tuplas, o modelo particiona os valores dos fluentes para garantir unicidade global (ex: distinguir 'objetivo-alto' de 'objetivo-baixo' como identificadores distintos).
- Função de Verificação ( $\phi_{verify}$ ): Uma função de verificação formal avalia se uma transição (estado de entrada, conjunto de ações, estado de saída) satisfaz uma regra específica. A função lida com vários tipos de regras, incluindo causa-se-se (causes-if), dispara (triggers), inibe (inhibits), não-concorrência (no-concurrency) e contravém (contravenes).
- Construção de Transição: Um mecanismo de janela deslizante é definido para construir transições incrementalmente a partir de uma sequência de trajetória bruta, garantindo uma base formal para o procedimento de verificação.
Arquitetura Composicional (Tiles & Soda):
- Tiles: Um framework para compor funções tipadas em especificações gráficas e modulares. Os procedimentos de verificação são representados como pipelines onde "tiles" (funções) são conectados para processar estados, ações e regras.
- Soda: Uma linguagem descritiva estaticamente tipada usada para implementar as especificações. As especificações Soda são traduzidas para Scala para execução na Java Virtual Machine (JVM) e podem ser parcialmente traduzidas para Lean para verificação formal.
- Estrutura do Pipeline: O processo de verificação é estruturado como uma sequência de transformações tipadas:
  - Processamento de Trajetória: Uma operação de fold constrói uma sequência de transições a partir da trajetória de entrada.
  - Aplicação de Regras: Uma operação de produto cartesiano combina transições com o conjunto de regras.
  - Verificação: Uma operação de map aplica $\phi_{verify}$ (e $\phi_{inhibit-set}$ para lidar com ações inibidas) a cada par transição-regra.
  - Agregação: Um fold final agrega os resultados para determinar a validade global.
Operacionalização: O framework inclui uma camada de especificação baseada em YAML. Os usuários definem descrições de domínio (fluentes, ações, regras) e trajetórias de entrada em YAML, que são analisados e operacionalizados no modelo de verificação subjacente e no pipeline executável.

Principais Contribuições

O artigo delineia quatro contribuições primárias:

Framework Modular: Introdução de um framework modular para verificação de transição e trajetória baseado nas tecnologias Tiles e Soda.
Semântica Operacionalizada: O framework operacionaliza a semântica de linguagem de ação (especificamente CMT) através de pipelines de verificação executáveis, tratando estados, ações e regras como componentes funcionais composíveis.
Camada de Especificação YAML: Provisão de uma camada de especificação e parser baseados em YAML que permite aos usuários definir descrições de domínio e entradas de trajetória, preenchendo a lacuna entre modelos formais e código executável.
Execução Transparente: Demonstração de que a abordagem fornece um método transparente, executável e escalável para verificar execuções de sistemas baseados em regras, com garantia de terminação do pipeline.

Resultados e Avaliação

Os autores fornecem uma implementação de código aberto e ilustram o framework através de dois exemplos específicos envolvendo propagação de desinformação e raciocínio emocional:

Desinformação e Raciocínio Emocional: O artigo demonstra como o framework suporta o refinamento modular. Em um cenário envolvendo a disseminação de desinformação, uma trajetória inicialmente parece inválida quando apenas estados informacionais são considerados. No entanto, ao estender o modelo com fluentes emocionais (ex: "emocionalmente conflitado" vs. "emocionalmente alinhado"), a mesma trajetória torna-se válida. Isso ilustra a capacidade do framework de incorporar informações contextuais sem alterar a estrutura de verificação subjacente.
Desempenho e Complexidade: A análise teórica (Proposição 4) estabelece a complexidade do pipeline como $O(r \times t \times d)$ , onde $r$ é o número de regras, $t$ é o número de estados/conjuntos de ações, e $d$ é o limite para avaliar a função de verificação. A avaliação empírica em um computador Linux padrão multi-core mostra que os tempos de execução escalam linearmente com o número de regras, consistente com as expectativas teóricas, com pequenas desvios atribuídos ao overhead de gerenciamento de memória.

Significância e Alegações

O artigo alega que sua principal significância reside em unir a pesquisa de planejamento/raciocínio de ação com abordagens de engenharia de software composicional. Ao se afastar de implementações puramente baseadas em programação lógica, o framework:

Permite a integração com ecossistemas de software mainstream baseados em JVM.
Fornece uma visão gráfica das especificações (via Tiles), melhorando a transparência e interpretabilidade.
Garante a terminação do processo de verificação por construção.
Suporta componentes de raciocínio reutilizáveis e refinamento modular de modelos de trajetória.

Os autores mantêm um escopo modesto, observando que o trabalho atual é limitado à verificação sobre trajetórias e descrições de domínio explicitamente especificadas. Não aborda a geração automática de trajetórias ou planejamento, mas sim fornece uma imersão semântica completa da linguagem de ação CMT que é extensível por design.