Deterministic World Models for Verification of Closed-loop Vision-based Systems

Título: Modelo de Mundo Determinístico para Verificação em Malha Fechada de Controladores Visuais End-to-End

1. Problema e Motivação

Os controladores visuais end-to-end (que mapeiam diretamente imagens de câmera para ações de controle) estão sendo cada vez mais implantados em sistemas críticos de segurança, como veículos autônomos e robótica. No entanto, garantir formalmente a segurança desses sistemas em malha fechada (onde a saída do controlador afeta o estado do sistema, que gera uma nova imagem) permanece um desafio aberto devido a duas barreiras fundamentais:

1. Ausência de Modelo Estado-para-Imagem: Não existe uma equação analítica fechada que descreva como um estado físico (posição, velocidade) se transforma em uma imagem de câmera. Sem isso, não é possível fechar o laço de verificação formal.
2. Explosão da Super-Aproximação: Imagens são de alta dimensão. Propagar conjuntos de imagens através de redes neurais convolucionais (CNNs) gera erros de super-aproximação em cada camada. Ao longo do tempo, esses erros acumulam-se, fazendo com que os conjuntos de estados alcançáveis cresçam excessivamente, resultando em falsos positivos (classificar trajetórias seguras como inseguras).

Trabalhos anteriores utilizaram Modelos Generativos Estocásticos (como cGANs) como substitutos da câmera. No entanto, eles introduzem variáveis latentes estocásticas (ruído aleatório) para gerar diversidade de imagens. Para verificação, essas variáveis latentes devem ser limitadas, mas como não têm significado físico, os limites são definidos de forma conservadora e ampla. Isso cria um conjunto de imagens virtualmente infinito, exacerbando o problema da super-aproximação e tornando a verificação inviável.

2. Metodologia Proposta

Os autores propõem um framework de verificação baseado em três pilares principais:

A. Modelo de Mundo Determinístico (DWM)

Em vez de usar variáveis latentes estocásticas, o DWM é um decodificador neural sem latentes que mapeia diretamente o estado físico ($s$) para uma imagem sintética ($\hat{I}$).

• Arquitetura: Um decodificador que recebe o vetor de estado e gera uma imagem.
• Vantagem: Como a entrada é apenas o estado físico, a variabilidade das imagens reflete apenas a incerteza do estado físico, eliminando o ruído artificial que infla os conjuntos de verificação.

B. Estratégia de Treinamento com Loss Duplo

Para garantir que o modelo não apenas pareça real, mas também se comporte corretamente em relação ao controlador, o DWM é treinado com uma função de perda combinada:

1. Perda de Reconstrução de Pixel ($L_{rec}$): Garante fidelidade visual (MSE ponderada, dando mais peso a regiões relevantes para o controle, como o objeto ou a pista).
2. Perda de Consistência de Controle ($L_{ctrl}$): Penaliza a diferença entre a ação de controle gerada pela imagem real e a ação gerada pela imagem reconstruída. Isso força o modelo a preservar características visuais críticas para a decisão do controlador, mesmo que a reconstrução visual não seja perfeita em pixels irrelevantes.

C. Pipeline de Verificação em Malha Fechada

O framework integra o DWM em um pipeline de verificação baseado em Star Sets (representação eficiente de conjuntos de estados):

1. Propagação: Conjuntos de estados iniciais são propagados através do DWM (para gerar conjuntos de imagens), depois através do controlador CNN (para gerar conjuntos de ações) e finalmente através da dinâmica da planta (para obter o próximo estado).
2. Abordagem de Dois Passos:
   • Passo 1: Calcular os conjuntos de estados alcançáveis no modelo substituto (DWM).
   • Passo 2: Aplicar Previsão Conformal (Conformal Prediction - CP) para inflar esses conjuntos e transferir a garantia para o sistema real.

D. Garantia para o Sistema Real via Previsão Conformal

Como o DWM é um modelo aproximado, existe um erro de modelagem. Para garantir a segurança do sistema real com alta probabilidade:

• Coletam-se pares de trajetórias (Real vs. DWM) a partir de estados iniciais amostrados.
• Calcula-se a desvio máximo (score de não-conformidade) entre as trajetórias reais e as do modelo.
• Usa-se a Previsão Conformal para encontrar um limite estatístico ($\Delta_{1-\alpha}$) que cobre a maioria das trajetórias com probabilidade $1-\alpha$.
• Os conjuntos de estados alcançáveis do modelo são inflados por esse limite. Se o conjunto inflado estiver seguro, o sistema real é garantido como seguro com probabilidade $1-\alpha$.

3. Principais Contribuições

1. Modelagem de Mundo Determinística: Introdução de um substituto de câmera livre de variáveis latentes estocásticas, permitindo conjuntos de imagens fisicamente realizáveis e tratáveis.
2. Loss de Consistência de Controle: Uma nova função de perda que alinha o comportamento do controlador com o modelo, reduzindo erros de modelagem que afetam a segurança.
3. Extensão de Verificação Star-based: Primeira aplicação de análise de alcançabilidade baseada em Star Sets para sistemas de visão em malha fechada.
4. Garantias Realistas via CP: Um método rigoroso para transferir garantias de um modelo substituto para o sistema físico real sem assumir distribuições de erro específicas.

4. Resultados Experimentais

O método foi avaliado em quatro benchmarks: CartPole, MountainCar, Pendulum e um Sistema de Frenagem.

• Comparação com Baseline (cGAN):
  • O DWM superou consistentemente o baseline baseado em cGAN em todas as métricas.
  • F1-Score: O DWM alcançou F1-scores superiores (ex: 0.9817 no MountainCar vs. 0.7990 do cGAN; 0.9842 no Sistema de Frenagem vs. 0.6639).
  • Precisão e Recall: O DWM manteve precisão de 1.0 (nenhuma falsa segurança) e recall significativamente melhor, indicando conjuntos de alcançabilidade muito mais apertados. O cGAN tendia a classificar tudo como inseguro (recall alto, mas precisão zero) devido à super-aproximação causada pelas variáveis latentes.
• Impacto do Loss de Controle: A ablação mostrou que remover as variáveis latentes reduziu drasticamente o limite de Previsão Conformal, e adicionar o loss de consistência de controle reduziu ainda mais esse erro, resultando em limites de erro de trajetória menores.
• Garantia Real: Ao aplicar a inflação via CP, o método manteve alta performance em sistemas com baixa sensibilidade a erros (MountainCar, Frenagem), enquanto em sistemas altamente sensíveis (CartPole), a inflação reduziu o recall, mas forneceu uma garantia matemática rigorosa de segurança.

5. Significância e Conclusão

Este trabalho resolve o dilema entre diversidade generativa e verificabilidade formal. Ao eliminar variáveis latentes estocásticas, os autores demonstram que é possível criar modelos de mundo que são suficientemente precisos para verificação formal, evitando a explosão de conjuntos de estados que inviabiliza a análise de sistemas visuais complexos.

A combinação de um modelo determinístico treinado com consistência de controle e a validação estatística via Previsão Conformal oferece um caminho viável para a certificação formal de controladores baseados em visão em aplicações críticas de segurança, superando as limitações das abordagens anteriores baseadas em GANs.

Limitações Futuras: O modelo atual ainda tem dificuldade com cenários extremamente complexos (múltiplos objetos, iluminação variável) e o tempo de computação para verificação em malha fechada ainda é alto (horas para poucos passos de tempo), sugerindo a necessidade de otimizações focadas em pixels críticos ou monitoramento em tempo real.