From Global to Local: Hierarchical Probabilistic Verification for Reachability Learning

1. O Problema

O projeto de controladores com garantias formais de segurança é essencial para sistemas autônomos em ambientes críticos (como coordenação multiagente e navegação de alta velocidade). A abordagem clássica baseada em Alcançabilidade de Hamilton-Jacobi (HJ) fornece garantias de segurança rigorosas, mas sofre da "maldição da dimensionalidade", tornando-se computacionalmente intratável em sistemas de alta dimensão.

Para contornar isso, métodos baseados em aprendizado (como Aprendizado por Reforço) são utilizados para aproximar conjuntos alcançáveis e sintetizar políticas. No entanto, essas aproximações podem introduzir erros que resultam em:

• Conjuntos de segurança excessivamente otimistas: Classificando regiões inseguras como seguras.
• Conjuntos excessivamente conservadores: Descartando estados seguros viáveis.
• Falta de escalabilidade: A verificação global exaustiva é cara e sensível a outliers.

O desafio central é equilibrar a escalabilidade, a precisão e a eficiência computacional, garantindo segurança probabilística sem sacrificar a capacidade de atingir o objetivo.

2. Metodologia

Os autores propõem um framework de verificação probabilística hierárquica que integra certificação global offline e refinamento local online. A arquitetura opera em três níveis principais:

A. Verificação Global Probabilística (Offline)

• Abordagem: Utiliza Otimização de Cenários (Scenario Optimization) para construir um conjunto de segurança global "grosseiro" (coarse).
• Mecanismo: Em vez de usar limites de Lipschitz determinísticos (que são conservadores), o método estima uma bound de desvio de trajetória ($\Delta x^*_t$) amostrando pares de estados (nominal e perturbado) sob a política aprendida ($\pi_{lp}$).
• Resultado: Gera um certificado probabilístico inferior para a função de valor. Se um estado pertence a este conjunto global ($V_{global}$), há uma garantia de que a política aprendida levará o sistema ao objetivo com segurança, com uma probabilidade de falha limitada por $\epsilon$ e confiança $1-\beta$.

B. Refinamento Local Iterativo (Online)

• Motivação: A verificação global pode ser muito conservadora, rejeitando estados que são, na verdade, seguros.
• Abordagem: Um módulo de refinamento local atua na fronteira do conjunto global ($\partial V_{global}$) próximo ao estado atual.
• Mecanismo: Utiliza um algoritmo de crescimento iterativo (Algoritmo 1) que resolve uma sequência de programas convexos. Ele amostra estados vizinhos na fronteira e simula trajetórias para expandir o conjunto verificado, recuperando regiões seguras que foram descartadas pela verificação global.
• Garantia: Mantém as garantias probabilísticas (Teorema 1) para o conjunto refinado localmente ($V_{local}$).

C. Mecanismo de Comutação Híbrida (Controle)

O framework integra a política de alcançabilidade aprendida ($\pi_{lp}$) com um controlador baseado em modelo (MPPI - Model Predictive Path Integral) através de uma lógica de comutação em quatro níveis (Tier):

1. Tier 0 (Manutenção do Alvo): Se o estado está dentro do conjunto alvo, usa um MPPI rápido.
2. Tier 1 (Verificação Global): Se o estado está em $V_{global}$, usa a política aprendida $\pi_{lp}$.
3. Tier 2 (Refinamento Local): Se o estado não está em $V_{global}$, mas foi recuperado em $V_{local}$, usa $\pi_{lp}$.
4. Tier 3 (Recuperação de Segurança): Se o estado não está verificado em nenhum nível, o sistema comuta para um controlador MPPI de recuperação. Este controlador é "warm-started" (inicializado) com a política aprendida para minimizar a distância até a fronteira do conjunto verificado mais próximo, tentando reentrar na zona segura.

3. Principais Contribuições

1. Framework Híbrido de Alcançabilidade Segura: Uma estrutura multi-nível que combina verificação probabilística global com refinamento local adaptativo, integrando políticas aprendidas e controladores baseados em modelo.
2. Expansão Local Baseada em Cenários: Um método eficiente para expandir o conjunto de segurança através de otimização de cenários, recuperando estados seguros que a verificação global conservadora descartaria.
3. Garantias de Segurança Probabilísticas: Provas teóricas que garantem a segurança tanto para o conjunto global quanto para o conjunto localmente refinado, controlando o risco de violação de segurança.
4. Validação Empírica: Demonstração prática em um cenário de corrida de drones, mostrando taxas de sucesso superiores em tarefas de ultrapassagem segura em comparação com métodos de base.

4. Resultados

Os experimentos foram realizados em um cenário de corrida de drones (12 dimensões), onde um drone "ego" deve ultrapassar um oponente e passar por um portão estreito, evitando colisões e turbulências (restrições não convexas).

• Comparação com Baselines: O método proposto (Hybrid) foi comparado a:
  • MPPI com filtro de segurança CBF (Função de Barreira de Controle).
  • MPPI com restrições suaves de segurança.
  • PPO (Proximal Policy Optimization) com filtro CBF.
• Desempenho:
  • O método proposto alcançou uma taxa de sucesso de 90,2%.
  • As melhores baselines (MPPI + CBF e PPO + CBF) alcançaram apenas 62,4% e 14,2%, respectivamente.
  • O método demonstrou maior robustez na evasão de colisões durante a ultrapassagem, enquanto as baselines tendiam a priorizar o objetivo em detrimento da segurança ou falhavam em equilibrar ambos.
• Estudo de Ablação: A remoção da política de alcançabilidade ou do mecanismo de comutação reduziu drasticamente a taxa de sucesso, confirmando que a combinação de aprendizado (para direção) e verificação (para segurança) é essencial.

5. Significado e Impacto

Este trabalho oferece uma solução prática para o dilema entre escalabilidade e segurança em sistemas de controle autônomo de alta dimensão.

• Redução de Conservadorismo: Ao recuperar regiões seguras via refinamento local, o sistema torna-se menos conservador do que métodos puramente globais, permitindo manobras mais agressivas e eficientes (como ultrapassagens em corridas).
• Eficiência Computacional: Foca o custo computacional pesado apenas nas regiões críticas (fronteiras), mantendo a operação online viável.
• Segurança Garantida: Fornece um mecanismo de "fallback" (Tier 3) que garante que, mesmo quando a política aprendida falha ou não é verificada, o sistema tenta ativamente recuperar a segurança, evitando comportamentos catastróficos.

Em resumo, a proposta unifica a eficiência do aprendizado de máquina com a robustez da verificação formal, criando um paradigma viável para a implantação de sistemas autônomos complexos em ambientes do mundo real.