Resumo Técnico: Treinamento Baseado em Conjuntos de Certificados de Barreira Neurais para Verificação de Segurança de Sistemas Dinâmicos

1. Declaração do Problema

A verificação de segurança de sistemas dinâmicos de tempo contínuo é crítica para agentes autônomos em ambientes de segurança crítica (por exemplo, veículos autônomos, UAVs, manipuladores robóticos). Um sistema é considerado seguro se nenhuma trajetória que começa em um conjunto inicial $X_I$ entrar em um conjunto inseguro $X_U$.

Os métodos de verificação existentes enfrentam limitações significativas:

• Métodos baseados em simulação sofrem com crescimento exponencial do tempo de execução em relação à dimensão do sistema.
• Análise de alcançabilidade utiliza computações baseadas em conjuntos para evitar o tempo de execução exponencial, mas pode ser computacionalmente intensiva.
• Certificados de Barreira oferecem uma prova formal de segurança definindo uma função escalar $B$ que separa $X_I$ de $X_U$ através de seu conjunto de nível zero. No entanto, abordagens recentes para sintetizar certificados de barreira baseados em redes neurais dependem de um ciclo iterativo de treinamento-verificação. Neste ciclo, uma rede neural é treinada em amostras do espaço de estados e, em seguida, formalmente verificada usando um solver externo (por exemplo, SMT). Se a verificação falhar (contraexemplos encontrados), a rede é retreinada. Este processo é custoso, potencialmente exigindo muitos ciclos, e não garante convergência para um certificado válido dentro de um único procedimento.

2. Metodologia: Treinamento Baseado em Conjuntos

Os autores propõem uma nova abordagem de treinamento baseada em conjuntos que integra a verificação formal diretamente no processo de treinamento da rede neural, eliminando a necessidade de uma etapa de verificação separada.

Conceito Central

Em vez de treinar em amostras discretas e verificar posteriormente, o método treina a rede neural $B_\theta$ usando uma função de perda baseada em conjuntos, sólida. Esta função de perda é computada sobre conjuntos inteiros (envoltórios) do espaço de estados, em vez de pontos individuais. Quando a perda atinge zero, a validade do certificado de barreira é formalmente provada por construção.

Componentes Técnicos Principais

A. Função de Perda Baseada em Conjuntos Sólida
A função de perda codifica as três propriedades exigidas para um certificado de barreira (Teorema 1):

1. Propriedade P I (Estados Inseguros): Todos os estados em $X_U$ devem mapear para valores positivos. A perda $L_I$ penaliza o limite inferior da imagem baseada em conjuntos de $X_U$.
2. Propriedade P II (Estados Iniciais): Todos os estados em $X_I$ devem mapear para valores não positivos. A perda $L_{II}$ penaliza o limite superior da imagem baseada em conjuntos de $X_I$.
3. Propriedade P III (Dinâmica do Conjunto de Nível Zero): A derivada de Lie $L_f B_\theta$ deve ser negativa no conjunto de nível zero $X_Z = \{x \mid B_\theta(x) = 0\}$.
   • Como $X_Z$ é desconhecido e não convexo, o método computa um envoltório apertado de $X_Z$ usando uma união de zonótopos via uma estratégia recursiva de branch-and-bound (dividindo o espaço de entrada e descartando regiões sem pontos zero).
   • Para cada zonótopo no envoltório, a derivada de Lie é envolta usando propagação direta baseada em conjuntos de gradientes e as dinâmicas do sistema.
   • A perda $L_{III}$ penaliza os limites superiores desses envoltórios de derivada de Lie.

A perda total é $L = L_I + L_{II} + L_{III}$. Se $L=0$, o sistema é formalmente verificado como seguro.

B. Propagação Direta Baseada em Conjuntos
Para computar essas perdas, o método propaga zonótopos (um tipo específico de poliedro convexo) através das camadas da rede neural:

• Camadas Lineares: Computadas exatamente via mapas afins.
• Camadas Não Lineares: Envoltas usando superaproximações conservadoras (por exemplo, delimitação de intervalo).
• Gradientes e Derivadas de Lie: O conjunto de gradientes é propagado para trás, e a derivada de Lie é computada como o produto interno do conjunto de gradientes e o conjunto de fluxo.

C. Algoritmo
O loop de treinamento (Algoritmo 1) inicializa a rede, computa perdas baseadas em conjuntos para $P_I$, $P_{II}$ e $P_{III}$, atualiza os parâmetros via descida de gradiente e termina assim que a perda total é zero.

3. Contribuições Principais

1. Síntese de Procedimento Único: Uma abordagem nova para sintetizar certificados de barreira neurais em um único procedimento de treinamento baseado em conjuntos, removendo o ciclo iterativo de treinamento-verificação.
2. Função de Perda Sólida: Uma perda baseada em conjuntos que codifica solidamente todas as propriedades do certificado de barreira. Um valor de perda zero constitui uma prova formal de segurança.
3. Refinamento Iterativo: Um procedimento iterativo para envolver dinamicamente o conjunto de nível zero e a derivada de Lie exigidos para a Propriedade P III.
4. Avaliação Extensiva: Avaliação em 13 benchmarks cobrindo dinâmicas lineares, polinomiais e não polinomiais, incluindo sistemas de alta dimensão (até 9D) e configurações de conjuntos complexas.

4. Resultados Experimentais

A abordagem foi implementada usando a toolbox CORA e comparada com ferramentas de última geração: SynNBC e FOSSIL (treinamento-verificação iterativo) e PRoTECT (otimização de soma de quadrados).

• Taxa de Sucesso: O método proposto alcançou uma taxa de sucesso de 100% em todos os 13 benchmarks.
  • Em contraste, SynNBC e PRoTECT falharam em dinâmicas não polinomiais e em benchmarks com múltiplos conjuntos iniciais/inseguros.
  • FOSSIL alcançou altas taxas de sucesso, mas degradou em sistemas de dimensão mais alta (por exemplo, 70% em Peruffo 6D, 80% em Peruffo 8D).
• Tempo de Execução: A abordagem de treinamento baseada em conjuntos foi significativamente mais rápida que o FOSSIL. Por exemplo, no benchmark Peruffo (8D), o método proposto levou 1,0s em média, comparado a 47,7s para o FOSSIL.
• Eficiência de Treinamento: O método geralmente convergiu em poucas épocas de treinamento. Em contraste, o FOSSIL frequentemente exigiu múltiplos ciclos de treinamento-verificação, onde cada ciclo poderia envolver até 1.000 épocas.
• Estudos de Ablação:
  • Arquitetura da Rede: Redes rasas (camada linear única) foram suficientes para sistemas lineares, mas falharam em sistemas não polinomiais. Redes mais profundas foram necessárias para dinâmicas complexas.
  • Envoltório do Conjunto de Nível Zero: Dinâmicas mais complexas exigiram envoltórios de conjunto de nível zero mais elaborados (mais divisões/iterações) para satisfazer a Propriedade P III.

5. Significado e Alegações

O artigo alega que esta abordagem representa uma mudança de paradigma na verificação de segurança ao colapsar as fases de treinamento e verificação.

• Garantias Formais: Diferentemente do treinamento padrão de redes neurais, que não oferece garantias formais de segurança, este método garante que uma perda zero implica um certificado de barreira válido.
• Escalabilidade: As operações reduzem-se a multiplicações de matrizes eficientes, resultando em complexidade polinomial que escala bem com a dimensão do sistema.
• Versatilidade: A abordagem é largamente agnóstica às dinâmicas do sistema, lidando naturalmente com dinâmicas não lineares complexas (não polinomiais) e representações de conjuntos complexas (por exemplo, uniões de conjuntos, regiões não convexas) com as quais métodos baseados em intervalos lutam.
• Eficiência: Ao eliminar o ciclo iterativo custoso, o método fornece um caminho mais eficiente para a verificação formal de sistemas de alta dimensão e não lineares.

Os autores concluem que sua síntese baseada em conjuntos pode gerar eficientemente certificados de barreira sem exigir verificação subsequente, superando trabalhos anteriores particularmente em sistemas de alta dimensão e não polinomiais.