Logic-Based Verification of Task Allocation for LLM-Enabled Multi-Agent Manufacturing Systems

Resumo Técnico: Verificação Lógica de Alocação de Tarefas para Sistemas de Manufatura Multi-Agente Habilitados por LLM

1. Problema e Motivação

A indústria de manufatura enfrenta uma crescente demanda por produtos personalizados, o que exige sistemas de controle altamente flexíveis e adaptáveis. Arquiteturas de Sistemas Multi-Agente (MAS) foram propostas para distribuir a tomada de decisão, mas elas tradicionalmente dependem de modelos de tarefas pré-definidos, limitando sua capacidade de se adaptar a novos requisitos de produto sem comprometer a segurança.

Recentemente, Modelos de Linguagem Grandes (LLMs) foram introduzidos para aumentar a flexibilidade no planejamento de tarefas. No entanto, os LLMs carecem de garantias formais de segurança; suas saídas podem violar restrições críticas, como evitar colisões, respeitar relações de precedência ou gerenciar conflitos de recursos compartilhados. O problema central abordado é: como gerar planos de tarefas adaptativos para novos requisitos de produto usando LLMs, garantindo ao mesmo tempo que todas as restrições de segurança do chão de fábrica sejam satisfeitas antes da execução?

2. Metodologia e Arquitetura Proposta

O artigo propõe uma arquitetura de controle híbrida que combina a flexibilidade dos LLMs com a rigorosidade da verificação formal baseada em lógica. O sistema opera sob o paradigma de Síntese Indutiva Guiada por Contraexemplo (CEGIS), onde planos candidatos são iterativamente verificados e refinados.

A arquitetura envolve os seguintes componentes e fluxos:

• Agentes de Produto (PA) Habilitados por LLM:

  • Interpretam requisitos de produto e regras de segurança em Linguagem Natural (NL).
  • Geram um plano de tarefas representado como um Grafo Acíclico Direcionado (DAG), capturando dependências e concorrência.
  • Compilam o DAG em um Autômato de Estados Finitos (FSA) que modela o comportamento conjunto dos recursos.

• Agente Controlador Central (CCA) e Especificação de Segurança:

  • Recebe os requisitos de segurança em NL e os transforma em Especificações de Lógica Temporal Linear em Traços Finitos (LTLf).
  • Traduz as fórmulas LTLf em Autômatos de Segurança (FSA), onde estados de violação são explicitamente definidos.
  • Exemplos de restrições: ordem de execução (precedência) e exclusão mútua (dois robôs não podem ocupar o mesmo espaço simultaneamente).

• Processo de Validação (Verificação):

  • O CCA realiza uma análise de alcançabilidade (usando Busca em Profundidade - DFS) sobre o produto do autômato do plano de execução ($A_{plan}$) e o conjunto de autômatos de segurança ($A_{safety}$).
  • O algoritmo verifica se algum estado de violação ($Q_{v,s}$) é alcançável durante a execução do plano.
  • Se uma violação for detectada, o sistema gera um rastro de testemunha (witness trace) que mostra exatamente como a falha ocorre.

• Replanejamento com Feedback:

  • O CCA envia o plano inseguro, a condição de violação e o rastro de testemunha de volta ao PA (LLM) como um prompt estruturado.
  • O LLM utiliza esse feedback contextual para corrigir o plano, ajustando a ordem das tarefas ou a alocação de recursos, e o ciclo de verificação se repete até que um plano seguro seja encontrado ou o limite de tentativas seja atingido.

3. Contribuições Principais

O trabalho apresenta três contribuições fundamentais:

1. Arquitetura de Controle Híbrida: Um framework que integra LLMs para geração dinâmica de planos com verificação formal baseada em autômatos para garantir segurança.
2. Processo de Verificação Formal: Um método que avalia planos de tarefas usando LTLf traduzido em autômatos, permitindo a detecção de conflitos de recursos e violações de precedência em nível de execução.
3. Mecanismo de Feedback Iterativo: Um loop de replanejamento que utiliza resultados de verificação estruturados para guiar o LLM na correção de planos inseguros, sem a necessidade de redesenhar modelos pré-definidos.

4. Resultados do Estudo de Caso

O framework foi validado em um cenário de montagem multi-robô com três cenários de complexidade crescente (S1, S2, S3), variando o número de robôs, peças e regras de segurança.

• Comparação: O framework proposto foi comparado com uma abordagem de "LLM Puro" (sem verificação formal).
• Taxa de Satisfação de Regras:
  • O LLM puro apresentou taxas de satisfação de segurança variando entre 50% e 75,93%.
  • O framework proposto elevou essas taxas para 86,25% a 92,50% em todos os cenários.
• Desempenho Computacional:
  • O tempo de verificação aumentou com a escala do problema (de 0,1s em S1 para 25,46s em S3), refletindo o crescimento do espaço de estados explorado (de 170 para 14.618 estados).
  • O número médio de tentativas de reparo também aumentou com a complexidade, mas o sistema conseguiu corrigir a maioria dos planos inseguros dentro do limite de 5 tentativas.

5. Significado e Conclusão

Este trabalho demonstra que é possível combinar a adaptabilidade dos LLMs com a segurança rigorosa necessária em ambientes industriais. A principal inovação reside na capacidade de verificar e corrigir planos gerados por IA antes da execução, mitigando riscos de falhas catastróficas em sistemas de manufatura reconfiguráveis.

Limitações e Trabalhos Futuros:

• A validação atual depende de especialistas para validar a tradução de requisitos de segurança em LTLf (hipótese A.1), o que pode limitar a escalabilidade.
• O tempo de verificação cresce exponencialmente com o número de agentes, sugerindo a necessidade futura de arquiteturas de verificação hierárquica ou composicional para fábricas de grande escala.
• O objetivo final é estender o framework para verificação de segurança online, permitindo adaptação em tempo real a eventos imprevistos.

Em suma, o artigo oferece um caminho promissor para a implementação segura de agentes de IA autônomos em ambientes de manufatura complexos e dinâmicos.