Resumo Técnico: Verificação Probabilística de RNN (RNN-ProVe)

Declaração do Problema

Redes Neurais Recorrentes (RNNs) são amplamente empregadas em Aprendizado por Reforço (RL) para lidar com observabilidade parcial e coordenação multiagente, mantendo estados ocultos latentes que codificam o histórico de interações. A verificação dessas políticas é fundamentalmente desafiadora porque o processo de tomada de decisão depende de todo o histórico de observações e ações, e não apenas da entrada atual.

As ferramentas de verificação existentes para RNNs focam principalmente na análise de robustez contra perturbações de entrada limitadas em um horizonte fixo. Esses métodos geralmente dependem de superaproximações geométricas grosseiras (por exemplo, intervalos ou hipercubos) do espaço de estados ocultos. No contexto de RL, essa abordagem admite estados ocultos espúrios—combinações de valores de neurônios que são matematicamente possíveis dentro dos limites da rede, mas são inviáveis dada a política específica e a dinâmica do ambiente. Consequentemente, essas ferramentas frequentemente produzem resultados excessivamente conservadores ou falsos positivos.

Além disso, a verificação exata de políticas baseadas em RNNs requer enumerar todas as configurações de estados ocultos alcançáveis para verificar comportamentos indesejados. Esse problema é equivalente ao cálculo de medidas de pré-imagem de redes neurais, o que é #P-difícil devido à não linearidade e não convexidade das redes neurais. A caracterização exata é computacionalmente inviável para políticas não triviais, e os métodos existentes não escalam para configurações multiagente ou espaços de alta dimensão.

Metodologia: RNN-ProVe

Os autores propõem a Verificação Probabilística de RNN (RNN-ProVe), uma estrutura que migra da verificação exata de pior caso para a verificação probabilística sobre históricos viáveis. Em vez de tentar enumerar todos os estados ocultos possíveis, o RNN-ProVe estima a probabilidade de comportamentos indesejados quantificando o volume do espaço de estados ocultos viáveis que leva a violações.

A estrutura opera através de três fases principais:

1. Aprendizado do Oráculo de Viabilidade:

   • Durante a fase de treinamento de RL, o agente explora o ambiente, gerando um conjunto de dados de pares estado-estado oculto $(s, h)$.
   • O RNN-ProVe treina um classificador de viabilidade $C: S \times H \to \{0, 1\}$ sobre esse conjunto de dados. Esse classificador aprende a distinguir entre estados ocultos que são realmente alcançáveis sob a política treinada (viáveis) e aqueles que não são (inviáveis).
   • Essa etapa aproveita o teorema da aproximação universal para aproximar a variedade complexa e de dimensão inferior de históricos viáveis dentro do espaço de estados ocultos de alta dimensão.

2. Amostragem e Verificação Orientadas pela Política:

   • Para um estado específico de interesse, o método amostra vetores de histórico candidatos do domínio do estado oculto.
   • O classificador treinado $C$ atua como um oráculo, filtrando amostras inviáveis e retendo apenas aqueles estados ocultos $h^*$ que correspondem a históricos de interação válidos que levam ao estado atual.
   • A política é então avaliada sobre esses históricos validados para determinar se resultam em uma violação (por exemplo, selecionar uma ação insegura).

3. Estimação Estatística com Limites de Erro:

   • A estrutura calcula a razão entre históricos validados que violam e o número total de históricos validados para estimar o volume de violação.
   • Crucialmente, o RNN-ProVe deriva limites de confiança estatística usando a desigualdade de Hoeffding. Ele decompõe a tolerância total de erro $\epsilon$ e o parâmetro de confiança $\delta$ em dois componentes:
     • Erro do Classificador: A precisão do oráculo de viabilidade.
     • Variância de Amostragem: O erro estatístico da estimação de Monte Carlo.
   • Isso permite que a estrutura produza certificados de erro limitado e alta confiança em relação à probabilidade de violações comportamentais.

Contribuições Principais

O artigo faz as seguintes contribuições específicas:

• Formulação do Problema: Define formalmente o problema da verificação probabilística para políticas recorrentes de RL sob observabilidade parcial, contabilizando explicitamente o conjunto de estados ocultos viáveis induzido por uma política treinada.
• Estrutura RNN-ProVe: Introduz uma estrutura inovadora que combina aprendizado de viabilidade com estimação de Monte Carlo para avaliar quantitativamente violações comportamentais em políticas baseadas em RNNs.
• Extensão Multiagente: Estende o problema de verificação para RL Multiagente (MARL) totalmente cooperativo. Deriva garantias de erro limitado e alta confiança para identificação de históricos viáveis e estimação de violação em configurações descentralizadas, fornecendo uma aproximação tratável para um problema originalmente #P-difícil.
• Garantias Teóricas: Fornece uma prova teórica (Teorema 2) de que o volume de violação estimado satisfaz limites específicos de erro e confiança, condicionados aos tamanhos de amostra da validação do classificador e da amostragem de verificação.

Resultados Experimentais

Os autores avaliaram o RNN-ProVe em tarefas de navegação de agente único e tarefas cooperativas multiagente "BoxPushing" (BP) usando políticas DRQN.

• Escalabilidade: O RNN-ProVe demonstrou vantagens significativas de escalabilidade. Em tarefas de navegação, métodos baseados em linearização de linha de base exigiram minutos a horas para ambientes pequenos (4x4, 8x8) e esgotaram o tempo em ambientes maiores (16x16). Em contraste, o RNN-ProVe produziu resultados quantitativos em milissegundos em todos os tamanhos de grade testados.
• Precisão vs. Linhas de Base:
  • Comparado ao Monte Carlo ingênuo (amostragem uniforme sem filtragem de viabilidade), o RNN-ProVe forneceu estimativas precisas. A amostragem ingênua produziu taxas de violação significativamente infladas (por exemplo, ~23% vs. ~1,6% em 4x4) porque testou estados ocultos inviáveis que não ocorrem na prática.
  • Comparado a linhas de base de linearização exata (quando viáveis), o RNN-ProVe produziu estimativas de violação comparáveis (por exemplo, ~1,42% vs. ~1,44% em 4x4), mas com garantias probabilísticas e ordens de magnitude menos tempo de computação.
• Desempenho Multiagente: A estrutura verificou com sucesso políticas cooperativas no domínio BP (grades 10x10 e 20x20), identificando taxas médias de violação de aproximadamente 1,18% e 1,7%, respectivamente. Ferramentas existentes não podiam ser aplicadas diretamente a essas configurações cooperativas.
• Insight: Os experimentos revelaram que mesmo políticas com retornos médios altos exibem generalização não uniforme sobre estados ocultos viáveis, com sensibilidades específicas próximas a obstáculos que avaliações empíricas padrão ignoram.

Significado e Alegações

O artigo argumenta que a verificação exata de pior caso para políticas recorrentes de RL não é apenas computacionalmente proibitiva, mas também desalinhada com a estrutura da tomada de decisão dependente de histórico. Os autores afirmam que a verificação probabilística sobre históricos viáveis não é meramente um relaxamento heurístico, mas uma resposta principial a barreiras computacionais fundamentais.

Ao focar no conjunto de estados ocultos que são realmente alcançáveis sob uma política, o RNN-ProVe fornece garantias probabilísticas quantitativas e conscientes da viabilidade. Essa abordagem produz certificados mais informativos do que resultados binários "seguro/inseguro" ou verificações de robustez excessivamente conservadoras, permitindo uma melhor compreensão da confiabilidade e generalização da política em ambientes complexos, parcialmente observáveis e multiagente. O trabalho defende essa perspectiva probabilística como uma abordagem fundamental para raciocinar sobre segurança em sistemas dependentes de histórico.