Verification of Unknown Dynamical Systems via Autoencoder Latent Space

Resumo Técnico: Verificação de Sistemas Dinâmicos Desconhecidos via Espaço Latente de Autoencoder

Formulação do Problema
A verificação formal de sistemas dinâmicos de espaço contínuo é essencial para garantir que sistemas autônomos satisfaçam especificações de segurança e vivacidade, frequentemente expressas em Lógica Temporal Linear (LTL). Abordagens padrão envolvem a construção de abstrações de estados finitos para permitir a verificação de modelos. No entanto, essas técnicas enfrentam desafios severos de escalabilidade em configurações de alta dimensão, pois o tamanho da abstração cresce exponencialmente com a dimensão do espaço de estados. Essa questão é exacerbada em sistemas habilitados por IA (por exemplo, aqueles controlados por redes neurais processando dados de LiDAR ou câmeras), onde as dinâmicas são complexas, parcialmente desconhecidas ou caixas pretas. Embora técnicas de redução de dimensionalidade baseadas em dados, como autoencoders, ofereçam uma solução potencial para a escalabilidade, elas geralmente carecem de garantias formais de correção. Especificamente, mapear especificações de alta dimensão para um espaço latente aprendido e garantir que as dinâmicas latentes aprendidas representem fielmente o comportamento do sistema original (incluindo não determinismo) permanece um desafio aberto. Métodos existentes frequentemente trocam correção por flexibilidade ou dependem de suposições fortes sobre as dinâmicas do sistema que não se sustentam para representações aprendidas.

Metodologia
O framework proposto aborda esses desafios combinando redução de dimensionalidade com verificação baseada em abstração para fornecer garantias formais para sistemas de alta dimensão com dinâmicas desconhecidas. A abordagem consiste em quatro etapas principais:

1. Arquitetura de Autoencoder Convexo: Para garantir que o espaço latente seja interpretável e suporte raciocínio sólido, os autores empregam um Autoencoder Convexo. O codificador é restrito a ser uma Rede Neural Convexa de Entrada (ICNN) com restrições estruturais específicas: funções de ativação estritamente monótonas (para atuar como homeomorfismos), camadas iniciais e de salto injetivas e matrizes de peso de posto completo. Essa arquitetura, denominada rede "Entrada Conectada-Saída Conectada" (CICO), garante que a pré-imagem de qualquer conjunto conexo no espaço latente seja um conjunto conexo no espaço de estados original. Essa propriedade é crucial para lidar com a não injetividade do mapeamento quando a dimensão latente é inferior à realização mínima do sistema.

2. Aprendizado de Dinâmicas de Inclusão Latente: Como a redução de dimensionalidade pode resultar em perda de informação, a evolução no espaço latente é modelada como dinâmicas de inclusão (conjunto-valores) em vez de equações de diferenças determinísticas. Os autores introduzem "Processos Gaussianos de Inclusão" (Inclusion GPs), uma formulação novel de Regressão por Processo Gaussiano (GPR) para dinâmicas conjunto-valores. Esse método eleva as dinâmicas a um espaço de dimensão superior onde seguem equações de diferenças envolvendo um parâmetro não observado $c$. Ao aprender um kernel profundo que incorpora essa coordenada não observada, o método prevê a evolução do sistema como um conjunto (especificamente, uma bola no espaço latente) e fornece limites de erro rigorosos baseados na análise do Espaço de Hilbert de Kernel Reprodutor (RKHS).

3. Construção de Abstração Finita Sólida: Usando o GP de Inclusão aprendido, os autores constroem um Sistema de Transição Não Determinístico (NTS) no espaço latente.

   • Mapeamento de Regiões: Regiões de interesse de alta dimensão (conjuntos seguros, inseguros e de objetivo) são mapeadas para o espaço latente. A convexidade do codificador permite uma sub-aproximação baseada em amostragem eficiente e uma super-aproximação probabilística (usando $\epsilon$-RandUp) desses conjuntos.
   • Relação de Transição: Transições entre estados abstratos são computadas propagando regiões através do modelo GP de Inclusão, contabilizando erros de regressão e o parâmetro não observado $c$. Isso garante que a abstração capture conservadoramente todos os comportamentos possíveis do sistema original.
   • Garantias de Correção: O framework prova que, se um estado no NTS latente satisfizer uma especificação de alcance-evitação, então todas as trajetórias correspondentes no sistema original de alta dimensão satisfarão a especificação com um alto nível de confiança ($1-\delta$).

4. Verificação e Decodificação: Ferramentas padrão de verificação de modelos são aplicadas ao NTS latente para identificar estados garantidos de satisfazer a especificação ($Q_{yes}$), estados que não podem satisfazê-la ($Q_{no}$) e estados incertos ($Q_?$). Como o codificador é convexo, estados latentes satisfatórios podem ser eficientemente decodificados de volta para o espaço original de alta dimensão usando otimização convexa para identificar o conjunto de estados iniciais no sistema original que são garantidos de serem seguros.

Contribuições Principais
O artigo faz quatro contribuições primárias:

1. Mapeamento Provavelmente Correto: Um método para mapear especificações de alto nível em um espaço latente usando um codificador CICO, permitindo raciocínio eficiente sobre representações comprimidas enquanto preserva garantias formais.
2. GPs de Inclusão: Uma formulação novel de regressão por Processo Gaussiano para dinâmicas de inclusão-valores (conjunto-valores), permitindo o aprendizado de dinâmicas latentes governadas por inclusões de diferenças sem exigir conhecimento explícito dos parâmetros não observados subjacentes.
3. Framework de Abstração Sólida: Um framework completo para gerar abstrações finitas sólidas no espaço latente baseado em GPs de Inclusão, incluindo procedimentos para mapear garantias de satisfação de volta para o sistema original com provas de correção.
4. Validação Empírica: Demonstração da abordagem em múltiplos sistemas, incluindo um sistema de 26 dimensões controlado por uma rede neural (usando entradas de LiDAR), mostrando melhorias significativas de escalabilidade em relação a métodos de abstração tradicionais.

Resultados
A abordagem foi avaliada em três estudos de caso:

• 3D para 2D: Um sistema de realização mínima onde o método verificou com sucesso todo o espaço latente, enquanto a abstração baseada em dados tradicional no espaço original de 3D falhou em verificar a alcançabilidade devido à incerteza em dimensões de movimento lento.
• 6D para 2D: Um sistema superparametrizado com observações não lineares. O método verificou 100% do espaço latente para o caso sem obstáculos e 59,78% para o caso com obstáculo. Em contraste, tentar a abstração no espaço original de 6D resultou em explosão de estados, falhando em verificar qualquer região além do próprio objetivo dentro do limite de tempo.
• 26D para 2D: Uma tarefa de navegação de robô com entradas de LiDAR e um controlador de rede neural. O método aprendeu com sucesso um espaço latente de 2D que capturou as dinâmicas do sistema com não determinismo mínimo, verificando 50,0001% do espaço latente. Isso demonstrou a capacidade de lidar com espaços de observação de alta dimensão onde métodos tradicionais são inviáveis.

Significado
O artigo afirma preencher uma lacuna crítica entre redução de dimensionalidade e verificação formal. Ao fornecer garantias de solidez tanto para o mapeamento de especificações quanto para as dinâmicas latentes aprendidas, o trabalho elimina falsos positivos nos resultados de verificação, um problema comum no controle baseado em aprendizado. Os autores enfatizam que sua abordagem permite verificação escalável para sistemas de alta dimensão com dinâmicas desconhecidas, uma capacidade anteriormente inatingível com métodos formais existentes. Embora o framework seja sólido, os autores notam modestamente limitações, incluindo a restrição a codificadores convexos (o que limita a expressividade) e questões em aberto sobre incorporação de ruído e síntese de controle, que são identificadas como direções para trabalhos futuros.