ReLU Barrier Functions for Nonlinear Systems with Constrained Control: A Union of Invariant Sets Approach

Resumo Técnico: Funções de Barreira ReLU para Sistemas Não Lineares com Controle Constrained

1. Problema e Motivação

A certificação de segurança para sistemas dinâmicos não lineares com restrições de entrada poliédricas (saturação) é um desafio significativo. Métodos tradicionais baseados em Funções de Barreira de Controle (CBF) enfrentam dois obstáculos principais:

1. Restrições de Controle: A saturação pode eliminar controles que preservam a segurança, tornando a síntese de CBFs não convexa e computacionalmente intratável.
2. Conservadorismo vs. Tratabilidade: A escolha da função de classe-K estendida $\alpha(\cdot)$ é crítica. Escolhas lineares permitem programas convexos (LP), mas resultam em conjuntos invariantes certificados muito pequenos (conservadores). Funções não lineares podem gerar conjuntos maiores, mas geralmente exigem otimização não convexa ou treinamento de redes neurais complexo, dificultando a verificação formal.

O objetivo do trabalho é sintetizar CBFs para sistemas não lineares sob restrições de entrada, reduzindo o conservadorismo sem sacrificar a tratabilidade da síntese convexa.

2. Metodologia Proposta

Os autores propõem um pipeline de Aproximação-Verificação que combina síntese convexa em modelos substitutos (surrogates) com verificação rigorosa no sistema original. O processo é dividido em cinco etapas:

1. Aproximação (PWA): Os dinâmicos não lineares fechados são aproximados por um modelo Poli-Afín (PWA) derivado de uma Rede Neural ReLU. Isso permite representar a dinâmica não linear como uma coleção de regiões afins.
2. Síntese Convexa: Utiliza-se Programação Linear (LP) para sintetizar funções de barreira PWA para o modelo substituto.
3. Aumento do Conjunto (UIS): Para reduzir o conservadorismo, introduz-se o método União de Conjuntos Invariantes (UIS). Em vez de selecionar a melhor função $\alpha$ linear, o método combina múltiplos certificados obtidos com diferentes ganhos lineares $\alpha_i$ através de uma composição de máximo ($h(x) = \max_i h_i(x)$).
4. Verificação Facetária: O certificado obtido no modelo PWA é verificado no sistema não linear original. A verificação é realizada de forma eficiente apenas nas "facetas" (superfícies de nível zero) da função de barreira, utilizando o Lema de Farkas para eliminar a variável de controle e verificar a existência de uma entrada admissível que mantenha a trajetória segura.
5. Atualização de Incerteza Local: Se a verificação falhar (encontrando um contraexemplo), o modelo não é re-treinado. Em vez disso, uma incerteza local é atualizada apenas na célula PWA afetada pelo erro, e o programa linear é resolvido novamente. Isso evita a necessidade de limites de incerteza globais excessivamente conservadores.

3. Contribuições Principais

• Surrogado Leaky ReLU para $\alpha(\cdot)$:

  • Os autores propõem o uso de uma função Leaky ReLU (com duas inclinações) para a função $\alpha(\cdot)$.
  • O Teorema 1 prova que qualquer conjunto invariante certificável por uma função $\alpha \in \mathcal{K}_\infty$ genérica também é certificável por uma Leaky ReLU com parâmetros adequados.
  • Isso permite capturar a não linearidade de $\alpha$ (reduzindo conservadorismo) mantendo a estrutura de otimização convexa, evitando a não convexidade bilinear.

• União de Conjuntos Invariantes (UIS):

  • O método UIS combina múltiplos conjuntos invariantes obtidos via LP com diferentes ganhos lineares $\alpha_i$.
  • A função de barreira final é a composição máxima ($h_{max} = \max_i h_i$), que geometricamente corresponde à união dos conjuntos.
  • Vantagem: O conjunto resultante é garantidamente maior ou igual ao melhor conjunto de um único $\alpha$, sem custo adicional de otimização (apenas pós-processamento dos resultados já calculados).

• Pipeline de Aproximação-Verificação com Atualização Local:

  • Diferente de métodos que exigem re-treinamento de redes neurais ou verificação global cara, este método usa verificação facetária exata e atualizações de incerteza apenas nas células onde a falha ocorre. Isso garante a segurança do sistema não linear original com restrições de entrada.

4. Resultados e Simulações

Os autores validaram a abordagem em três cenários de simulação em Python, comparando com métodos existentes (como SEEV e SyntheBC):

1. Pêndulo Invertido:

   • O método UIS produziu um conjunto invariante estritamente maior do que o obtido pelo método de $\alpha$ único (usado em trabalhos anteriores dos autores).
   • Tempo total de certificação: ~46 segundos.

2. Verificação de Certificado de Barreira (Sistema Não Linear Genérico):

   • Comparado a métodos baseados em Redes Neurais profundas (256 neurônios) que levam horas para verificação, o método proposto usou uma rede rasa (20 neurônios) e completou a certificação em ~80 segundos.
   • O conjunto seguro certificado foi maior do que soluções baseadas em SOS (Sum of Squares) e comparável em cobertura ao SyntheBC, mas com garantia formal sob saturação.

3. Carrinho-Pólo (Cart-Pole) com Saturação de Entrada:

   • Sistema 4D com restrições de força.
   • O método escalou com sucesso para dinâmicas não lineares 4D, certificando um conjunto invariante em ~1466 segundos (total), demonstrando a viabilidade para sistemas de ordem superior.

5. Significado e Conclusão

O trabalho oferece uma solução prática para o dilema entre tratabilidade computacional e conservadorismo na síntese de CBFs para sistemas não lineares com restrições.

• Inovação Chave: A capacidade de usar a flexibilidade de funções não lineares (Leaky ReLU) e a união de conjuntos (UIS) dentro de um framework de otimização convexa (LP).
• Impacto: Permite a certificação formal de segurança para sistemas robóticos reais (como carros autônomos e drones) que operam sob limites físicos de atuação, garantindo que as trajetórias permaneçam seguras sem a necessidade de modelos de incerteza globais excessivamente pessimistas ou tempos de computação proibitivos.

Em suma, o método preenche a lacuna entre a síntese teórica de CBFs e a aplicação prática em sistemas com restrições de controle, oferecendo conjuntos de segurança maiores e verificáveis.