Scalable Verification of Neural Control Barrier Functions Using Linear Bound Propagation

Resumo Técnico: Verificação Escalável de Funções de Barreira de Controle Neurais

1. Problema e Contexto

As Funções de Barreira de Controle (CBFs) são ferramentas fundamentais para a certificação de segurança em sistemas de controle dinâmico não lineares, garantindo que o estado do sistema permaneça dentro de um conjunto seguro (invariância de controle). Recentemente, CBFs representadas por Redes Neurais (Neural CBFs) ganharam destaque devido à sua expressividade e capacidade de lidar com dinâmicas complexas e restrições não convexas.

No entanto, um gargalo computacional crítico limita a adoção prática dessas redes: a verificação pós-treinamento. Para garantir que uma rede neural treinada seja uma CBF válida, é necessário provar que ela satisfaz condições matemáticas rigorosas (derivadas de Lie) em todo o espaço de estados.

• Limitações atuais: Métodos existentes baseados em Satisfiability Modulo Theories (SMT) ou Programação Inteira Mista (MIP) sofrem de baixa escalabilidade. Eles tornam-se computacionalmente proibitivos à medida que o tamanho da rede neural ou a dimensionalidade do sistema aumentam.
• Restrições de Ativação: Muitas abordagens de verificação eficientes são restritas a redes com funções de ativação ReLU, limitando a capacidade de modelar não-linearidades suaves necessárias para problemas complexos.

2. Metodologia Proposta

Os autores propõem um novo framework de verificação que substitui a verificação exata não linear por condições lineares suficientes, eliminando a necessidade de solvers SMT caros. A abordagem baseia-se em três pilares principais:

1. Propagação de Limites Lineares (LBP) Estendida para Gradientes:

   • O método estende a técnica de Linear Bound Propagation (LBP) para calcular limites lineares superiores e inferiores não apenas para os valores de saída da rede, mas também para os seus gradientes (Jacobianos).
   • Isso é crucial porque a condição de CBF envolve derivadas espaciais da função de barreira.
   • Para lidar com a não-linearidade das derivadas e produtos bilineares (entre pesos e derivadas de ativação), o método utiliza Relaxações de McCormick.
   • Diferente de trabalhos anteriores que exigiam passagens adiantadas (forward passes) adicionais, esta abordagem formula os limites em relação às saídas pré-ativação, permitindo um cálculo eficiente e recursivo.

2. Modelagem de Dinâmica e Restrições Lineares:

   • As dinâmicas do sistema ($f(x)$ e $g(x)$) são aproximadas por expansões de Taylor de primeira ordem com limites de erro certificados (usando limites de Lagrange).
   • Combinando os limites da rede neural (valores e gradientes) com os limites da dinâmica, o método deriva um surrogato linear conservador ($\phi_{linear}$) para a condição de invariância de CBF.
   • Se este surrogato linear for satisfeito, a condição original não linear é garantida como satisfeita.

3. Estratégia de Refinamento Adaptativo (Malha Simplicial):

   • Como os limites lineares podem ser muito conservadores em domínios grandes, o método emprega uma estratégia de refinamento adaptativo.
   • Em vez de usar hiperretângulos (comuns em outras abordagens), o espaço de estados é particionado em simplices (malha simplicial).
   • O algoritmo identifica regiões onde a verificação é inconclusiva e divide os simplices ao longo de suas arestas mais longas.
   • O processo é paralelizável, permitindo o uso eficiente de GPUs para verificar múltiplas regiões simultaneamente.

3. Contribuições Principais

1. Novo Método de Verificação: Introdução de uma técnica que combina LBP e Relaxação de McCormick para verificar CBFs neurais, suportando funções de ativação não lineares arbitrárias (como tanh, sigmoid, ReLU), superando as limitações de métodos baseados em SMT.
2. Estratégia de Refinamento Escalável: Desenvolvimento de uma estratégia de refinamento baseada em malha simplicial que reduz o conservadorismo dos limites de forma adaptativa e paralelizável.
3. Escalabilidade Comprovada: Demonstração experimental de que a abordagem consegue verificar redes neurais significativamente maiores do que as técnicas state-of-the-art baseadas em SMT, mantendo a garantia de segurança.

4. Resultados Experimentais

Os autores avaliaram o método em diversos benchmarks, incluindo sistemas de controle 2D, um pêndulo invertido (Cart-Pole) e sistemas não lineares clássicos (Darboux, Barrier 2-4).

• Comparação: O método foi comparado com o solver SMT dreal (usado em trabalhos anteriores como Abate et al., 2021a).
• Desempenho:
  • O método proposto foi ordens de magnitude mais rápido. Por exemplo, para a rede "Barrier 4" (64x64), o método propôs levou 25.37s, enquanto o dreal atingiu o tempo limite (timeout).
  • Para redes maiores (ex: Darboux com [128, 256, 128]), o método proposto certificou 100% do espaço de estado em 144.68s, enquanto o dreal falhou.
  • O método conseguiu lidar com a presença de variáveis de controle ($u$) na condição de invariância, algo que é computacionalmente difícil para solvers SMT.
• Eficiência: O uso de GPUs permitiu o processamento em lote de múltiplos simplices, demonstrando alta eficiência computacional.

5. Significado e Impacto

Este trabalho representa um avanço significativo na área de controle seguro baseado em aprendizado de máquina.

• Viabilidade Prática: Ao remover o gargalo da verificação, o método permite o uso de redes neurais maiores e mais expressivas para síntese de CBFs, o que é essencial para sistemas robóticos complexos e dinâmicos não lineares.
• Flexibilidade: A capacidade de aceitar qualquer função de ativação semideferenciável abre caminho para otimizações de treinamento mais suaves e estáveis, que são frequentemente bloqueadas pela necessidade de usar apenas ReLU para facilitar a verificação.
• Aplicabilidade: A abordagem é agnóstica ao processo de treinamento e pode ser integrada em frameworks de "aprendizado-verificação" (learner-verifier) para síntese automática de controladores seguros.

Em suma, o artigo oferece uma solução escalável e matematicamente rigorosa para o problema de certificação de segurança em sistemas de controle neural, superando as barreiras computacionais que anteriormente limitavam a aplicação prática dessas tecnologias em ambientes do mundo real.