Learning Robust Control Lyapunov Functions through Lipschitz Neural Networks

Resumo Técnico: Aprendizado de Funções de Lyapunov de Controle Robusto através de Redes Neurais Lipschitz

Definição do Problema
O artigo aborda o desafio de projetar controladores estabilizadores para sistemas dinâmicos não lineares sujeitos a distúrbios aditivos. Embora as funções de Lyapunov sejam uma ferramenta fundamental para a análise de estabilidade, sua construção automática para sistemas não lineares gerais permanece um problema em aberto. Métodos computacionais existentes, como Sum-of-Squares (SOS) ou Desigualdades Matrizes Lineares (LMI), frequentemente enfrentam dificuldades com escalabilidade ou generalidade. Além disso, abordagens recentes de aprendizado profundo que aprendem Funções de Lyapunov de Controle (CLFs) usando redes neurais geralmente focam em dinâmicas exatas sem distúrbios ou dependem de métodos de verificação que são computacionalmente dispendiosos e conservadores (por exemplo, usando apenas informações de ordem zero). O desafio específico abordado aqui é aprender uma Função de Lyapunov de Controle Robusto (RCLF) e um controlador de feedback de estado correspondente que garanta a Limitação Última Uniforme (UUB) na presença de distúrbios aditivos dependentes do estado, garantindo simultaneamente que a verificação dessas condições seja computacionalmente tratável.

Metodologia
O framework proposto integra Redes Neurais Lipschitz (LNNs) com um algoritmo de verificação de alto nível baseado em Branch-and-Bound (BnB).

1. Redes Neurais Lipschitz (LNNs):
   Os autores utilizam LNNs para aprender conjuntamente a RCLF ($V_{\theta_1}$) e o controlador estabilizador ($\pi_{\theta_2}$). Diferente das redes padrão, as LNNs impõem uma constante de Lipschitz predefinida através de parametrizações de camadas específicas (por exemplo, Normalização Espectral, Camadas Ortogonais ou Camadas Sanduíche). Essa restrição é crítica porque permite a derivação de limites explícitos e estreitos para derivadas de ordem superior (Hessiana e derivadas de terceira ordem) da saída da rede em relação à sua entrada. A RCLF é definida como uma saída de rede deslocada para garantir a condição de equilíbrio $V(0)=0$.

2. Algoritmo de Treinamento:
   O processo de treinamento minimiza uma função de perda composta sobre um espaço de estados e fronteira amostrados. Os termos de perda impõem:

   • Definição Positiva: Garantir que $V(x) > 0$ para $x \neq 0$.
   • Condição de Decréscimo: Garantir que a derivada temporal $\dot{V}$ seja negativa fora de uma pequena bola ao redor da origem, contabilizando o pior caso do distúrbio. Isso envolve o limite superior do termo de distúrbio usando a função de limite de distúrbio conhecida $\epsilon(x)$ e as constantes de Lipschitz da rede e da dinâmica do sistema.
   • Fronteira e Cobertura: Incentivar o conjunto de nível subjacente de $V$ a cobrir uma porção máxima do espaço de estados e manter um valor consistente na fronteira.
     O algoritmo inicializa os parâmetros usando soluções de Regulador Quadrático Linear (LQR) e refina iterativamente esses parâmetros, armazenando os parâmetros que resultam na maior região de invariância de forward verificada empiricamente.

3. Verificação de Alta Ordem (Branch-and-Bound):
   Um novo algoritmo de BnB amigável para GPU é introduzido para verificar formalmente a RCLF aprendida. Diferente de solvers tradicionais (ex: dReal) que dependem de limites de ordem zero ou solvers SMT que enfrentam limites de escalabilidade, este método aproveita a suavidade das LNNs.

   • Limites de Ordem Superior: Os autores derivam limites de norma espectral explícitos para a Hessiana e derivadas de terceira ordem das LNNs. Esses limites são usados para construir limites inferiores e superiores estreitos na saída da rede via expansões de Taylor (até segunda ordem).
   • Eficiência do Algoritmo: Ao incorporar informações de primeira e segunda ordem, o algoritmo cria cercamentos significativamente mais estreitos dos valores da função dentro de retângulos de busca. Isso permite uma poda mais agressiva do espaço de busca em comparação com métodos de ordem zero.
   • Complexidade: O artigo estabelece limites de complexidade de tempo no pior caso, mostrando que o número de retângulos avaliados escala polinomialmente com a dimensão do sistema e inversamente com a tolerância, mas é drasticamente reduzido na prática pelos limites mais estreitos.

Principais Contribuições

1. Framework Inovador: Uma abordagem unificada para aprender RCLFs e controladores estabilizadores para sistemas não lineares com distúrbios aditivos dependentes do estado usando LNNs.
2. Limites de Derivada: O estabelecimento de limites de norma espectral explícitos para a Hessiana e derivadas de terceira ordem de LNNs. Esses limites são mais estreitos do que os derivados de informações de ordem zero ou primeira ordem isoladamente, abordando a não convexidade da verificação de Lyapunov.
3. Verificação Amigável para GPU: O desenvolvimento de um algoritmo de BnB que utiliza esses limites de ordem superior e suporta avaliação em lote (batch) em GPUs. Isso acelera significativamente o processo de verificação em comparação com solvers de CPU.
4. Validação Empírica: Simulações extensas em seis sistemas dinâmicos (pêndulo invertido, unicycle, sistema de terceira ordem, cartpole, quadrotor 2D e braço SCARA) demonstrando a capacidade do método de verificar a estabilidade e superar ferramentas existentes (dReal, $\alpha,\beta$-CROWN) em termos de velocidade e escalabilidade.

Resultados
O artigo apresenta resultados de simulação comparando o método proposto contra o dReal (SMT baseado em CPU) e o $\alpha,\beta$-CROwn (propagação de limites baseada em GPU).

• Velocidade de Verificação: O algoritmo de BnB proposto, baseado em GPU, supera consistentemente o dReal, muitas vezes reduzindo o tempo de verificação de horas (ou timeouts) para segundos, mesmo para sistemas com dimensões de estado mais altas (ex: braço SCARA com $n_x=8$).
• Escalabilidade: Enquanto o dReal falha em verificar sistemas com mais de 2-3 camadas em um tempo razoável, o método proposto verifica com sucesso redes de até 4 camadas.
• Regiões de Invariância de Forward: Os controladores aprendidos alcançam regiões de invariância de forward significativamente maiores do que as abordagens LQR padrão e NLC (Neural CLF) não robustas. Para o pêndulo invertido, o método proposto alcançou uma razão de região de invariância de forward de ~75%, comparado a ~23% para o LQR.
• Robustez: A verificação confirma que os controladores aprendidos satisfazem a condição de UUB, mantendo as trajetórias dentro de uma região limitada apesar dos distúrbios.

Significância e Alegações
O artigo alega que sua principal significância reside em unir a expressividade do aprendizado profundo com os requisitos rigorosos da verificação de controle robusto. Ao aproveitar a estrutura específica das redes Lipschitz para derivar limites de derivada de ordem superior, os autores permitem um processo de verificação que é matematicamente rigoroso e computacionalmente eficiente.

Os autores declaram explicitamente que seu framework não certifica a estabilidade para um modelo desconhecido sem um limite de erro conhecido; em vez disso, fornece uma garantia determinística de robustez contra um descompasso de modelo certificado ou distúrbio limitado. O trabalho destaca que, embora as LNNs possam ter expressividade reduzida em comparação com redes não restritas, o compromisso é justificado pela capacidade de realizar uma verificação de alta ordem eficiente, o que é essencial para aplicações de controle de segurança crítica. O artigo conclui que esta abordagem torna a verificação formal de controladores aprendidos e robustos para sistemas não lineares complexos praticamente viável.