Resumo Técnico: Blindagem Composicional Baseada em Contratos para Aprendizado por Reforço Multiagente Seguro

Declaração do Problema

No aprendizado por reforço multiagente (MARL) cooperativo, garantir a segurança durante o treinamento e a implantação é um desafio quando restrições de segurança globais não podem ser impostas unilateralmente por nenhum agente individual. Em "problemas de coordenação segura", a admissibilidade da ação de um agente depende das políticas não estacionárias de seus companheiros de equipe. As abordagens padrão dependem de blindagem centralizada, que computa uma relação de ação segura global, ou de mascaramento unilateral (fatorizado), onde cada agente restringe independentemente suas ações com base em suposições de pior caso.

O artigo identifica uma limitação crítica no mascaramento unilateral: ele frequentemente descarta comportamentos seguros ótimos que exigem coordenação. Como ilustrado pelo exemplo motivador do artigo (Figura 1), se a ação segura do Agente A depender de o Agente B escolher uma ação específica, um máscara unilateral pura proibirá a ação do Agente A para permanecer seguro contra todas as possíveis ações do Agente B. Isso leva a uma "decomposição cartesiana conservadora" que exclui ações conjuntas coordenadas seguras e de alta recompensa. O objetivo é alcançar a execução descentralizada (onde os agentes agem com base em informações locais) enquanto se recupera o comportamento seguro ótimo para a equipe sem retornar ao controle centralizado em tempo de execução.

Metodologia

Os autores propõem a Blindagem Composicional Baseada em Contratos, um framework que decompõe uma especificação de segurança global compartilhada em contratos temporais locais. A metodologia consiste em três fases principais:

1. Estrutura Formal e Premissas

• Especificação Global: A segurança é definida por uma única fórmula global $\Phi_{safe}$ no fragmento de segurança da Lógica Temporal Linear ($LTL_{safe}$).
• Contratos Locais: A especificação global é decomposta em uma tupla de obrigações locais $C = \langle \phi_i \rangle_{i=1}^n$, onde cada $\phi_i$ é uma fórmula $LTL_{safe}$ sobre o alfabeto local do agente $i$.
• Assume-Guarantee Circular: Ao contrário de trabalhos anteriores que exigem estruturas de dependência acíclicas, esta abordagem permite suposições circulares. O agente $i$ assume que todos os outros agentes $j \neq i$ satisfazem suas obrigações $\phi_j$. Esta circularidade é resolvida não por uma ordem fixa, mas pela certificação simultânea de toda a tupla.

2. Síntese de Blindagem (Offline)

O processo de síntese constrói uma biblioteca de contratos certificados:

• Construção de Autômatos: Cada obrigação local $\phi_i$ é compilada em um autômato de segurança determinístico $A^C_i$ com um conjunto de "estados ruins" representando violações.
• Produto de Contratos: Um autômato produto global é construído sobre o espaço de estados $S \times Q_1 \times \dots \times Q_n$.
• Certificação de Ponto Fixo: Os autores computam um ponto fixo de maior grau (a "região vencedora retangular" $Win^\square_C$) usando um operador de predecessora assume-guarantee. Esta região representa estados a partir dos quais um produto cartesiano não vazio de máscaras de ação locais (um "retângulo") pode ser mantido de tal forma que:
  1. A ação conjunta permanece dentro da região vencedora.
  2. Nenhum estado ruim é alcançado.
• Critérios de Certificação: Uma tupla de contrato é "certificada" se:
  1. A conjunção das obrigações locais implica semanticamente o objetivo de segurança global ($C \models^\uparrow \Phi_{safe}$).
  2. O estado inicial do sistema está dentro da região vencedora computada.
• Projeção: Uma vez certificada, a região vencedora é projetada para gerar máscaras de ação locais para cada agente. Estas máscaras são "localmente identificáveis por máscara", o que significa que um agente pode determinar suas ações permitidas usando apenas seu histórico de observação local e o identificador de contrato ativo, sem reconstruir as máscas dos outros agentes.

3. Aprendizado e Seleção (Online)

• Construção da Biblioteca: Antes do treinamento, uma busca limitada enumera tuplas de contratos candidatas (limitadas pela profundidade da fórmula e um alfabeto finito). Cada candidata é testada para certificação. O conjunto de tuplas bem-sucedidas forma a Biblioteca Certificada ($\mathcal{L}_{cert}$).
• Seletor Bandit: Durante o treinamento, um algoritmo de multi-armed bandit não estacionário seleciona qual contrato da biblioteca deve ser aplicado para um determinado bloco de treinamento.
  • Cada contrato atua como um "braço".
  • O seletor otimiza o retorno da equipe enquanto garante a segurança.
  • Ele utiliza uma estratégia de Upper Confidence Bound Descontado (D-UCB) para se adaptar à natureza não estacionária do processo de aprendizado (conforme as políticas melhoram, o valor de diferentes contratos muda).
• Garantia de Segurança: O Teorema 3 garante que, desde que o seletor alterne contratos apenas nas fronteiras dos episódios e sempre escolha da biblioteca pré-certificada, o sistema permanecerá seguro de ponta a ponta.

Principais Contribuições

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

1. Decomposição e Compilação: Um método para decompor uma especificação global $LTL_{safe}$ compartilhada em obrigações locais candidatas e compilá-las em autômatos de segurança determinísticos para síntese de blindagem.
2. Correção Formal e Recuperabilidade: Garantias formais para blindagem descentralizada baseadas em raciocínio assume-guarantee circular e pontos fixos de produto de contratos. Os autores provam que, se a política determinística segura ótima for representável por um contrato na biblioteca, o framework pode recuperá-la.
3. Otimização sob Certificação: Um mecanismo usando busca de perfil certificado limitada e seleção D-UCB para reduzir o conservadorismo. Isso permite que o sistema selecione contratos que exponham comportamentos coordenados de alto retorno sem sacrificar a segurança determinística.
4. Avaliação Empírica: Avaliação extensiva em 6 ambientes multiagentes cooperativos (incluindo Flatland, RWARE e Pressure Plate) e 15 variantes algorítmicas, demonstrando a eficácia da abordagem.

Resultados

A avaliação empírica compara o Contract-IPPO e o Contract-IQL propostos contra algoritmos MARL padrão (IPPO, IQL, MAPPO) e vários baselines de blindagem (blindagens unilaterais, blindagens centralizadas).

• Desempenho: Em ambientes onde as máscaras fatorizadas unilaterais são muito conservadoras (ex: RWARE, Pressure Plate, Connector), a blindagem baseada em contratos melhora significativamente o retorno da equipe, convergindo para o desempenho das blindagens centralizadas (como o Shielded-Joint-PPO).
• Segurança: A segurança é estruturalmente imposta; as curvas na Figura 4 medem o retorno retido, implicando que as violações de segurança são prevenidas pelas próprias máscaras.
• Escalabilidade: Nos maiores ambientes, a busca limitada considerou até 12.001 perfis, com até 390 sendo certificados como seguros, demonstrando a viabilidade da abordagem de enumeração offline.
• Descobertas Específicas: No ambiente "Pressure Plate", as blindagens fatorizadas padrão forçavam o corredor a ficar fora das regiões protegidas das portas para ser seguro contra qualquer comportamento do portador. A abordagem baseada em contratos permitiu que o corredor atravessasse ao confiar no compromisso certificado dos portadores de permanecer em suas placas, recuperando o comportamento coordenado ótimo.

Significância e Alegações

O artigo afirma abordar o trade-off fundamental em MARL seguro entre execução descentralizada e coordenação ótima.

• Recuperação de Coordenação: Os autores afirmam que seu método recupera o "comportamento seguro ótimo para a equipe" que é tipicamente perdido por blindagens puramente fatorizadas (unilaterais). Ao permitir que os agentes confiem em suposições circulares que são simultaneamente certificadas, o sistema evita a "decomposição cartesiana conservadora" que descarta ações conjuntas seguras.
• Segurança de Ponta a Ponta: O framework separa a adaptação de recompensa (aprendizado) da imposição de segurança (blindagem). O processo de aprendizado pode explorar e otimizar dentro dos limites de contratos pré-certificados, garantindo que nenhum comportamento inseguro seja admitido durante o treinamento ou implantação.
• Escopo Modesto: O artigo é modesto quanto às suas limitações. Reconhece que a capacidade de recuperar o ótimo global depende da representabilidade da política ótima dentro da biblioteca finita de contratos locais. Se a linguagem de contrato não for expressiva o suficiente (ex: profundidade $D$ muito baixa) para capturar a coordenação necessária, o sistema não pode recuperar o ótimo global. Além disso, a abordagem atual depende de enumeração exaustiva (embora limitada), e sugere-se trabalho futuro para explorar heurísticas para encontrar contratos próximos do ótimo sem a enumeração total.

Em resumo, o artigo apresenta uma abordagem rigorosa e formalmente verificada para MARL seguro que permite que agentes descentralizados coordenem efetivamente sem controle centralizado em tempo de execução, unindo a verificação formal e a otimização de aprendizado por reforço.