Resumo Técnico: Ponte entre Controle e Verificador de Redes Neurais $\alpha,\beta$-CROWN

Enunciado do Problema

Controladores de redes neurais (RN) baseados em aprendizado demonstraram alta expressividade e forte desempenho empírico em domínios críticos para a segurança, como direção autônoma, robótica e sistemas de energia. No entanto, o desempenho empírico por si só é insuficiente para implantação nesses cenários. Há uma necessidade crítica de verificação formal de propriedades de malha fechada, incluindo estabilidade (por exemplo, estabilidade de Lyapunov), segurança (por exemplo, funções de barreira) e alcançabilidade.

As abordagens de verificação existentes enfrentam limitações significativas:

1. Escalabilidade: Métodos tradicionais, como solucionadores SMT (por exemplo, dReal, Z3), Programação Linear Inteira Mista (MILP) e otimização convexa (SDP, SOS), frequentemente apresentam escalabilidade deficiente, particularmente para sistemas de alta dimensão ou redes profundas, devido à capacidade limitada de explorar aceleração por GPU e paralelismo.
2. Rigidez Estrutural: Muitos métodos estão vinculados a suposições estruturais específicas, como redes lineares por partes rasas com ativações ReLU ou sistemas polinomiais, tornando-os difíceis de transferir entre diferentes configurações de controle ou classes de certificados.
3. Especificidade do Certificado: Métodos de verificação orientados ao controle recentes frequentemente exploram estruturas específicas de certificados (por exemplo, propagação de limites simbólicos), o que limita sua aplicabilidade direta a diferentes classes de certificados.

Metodologia

O artigo introduz um framework unificado que faz a ponte entre a teoria de controle e o verificador de redes neurais mais avançado $\alpha,\beta$-CROWN. A metodologia central baseia-se em tratar problemas de controle como tarefas de verificação ou otimização sobre grafos de computação.

1. O Verificador $\alpha,\beta$-CROWN

O $\alpha,\beta$-CROWN é um motor de limitação de propósito geral para funções não lineares representadas como grafos de computação. Sua operação envolve:

• Grafos de Computação: O framework modela dinâmicas do sistema $f$, controladores $\pi$ e certificados (por exemplo, funções de Lyapunov $V$) como grafos acíclicos direcionados (DAGs) compostos por operações elementares (mapas afins, não linearidades como ReLU, seno, multiplicação, etc.).
• Relaxação Linear Automática (auto LiRPA): O verificador propaga super-approximações lineares sólidas (limites) para trás através do grafo de computação. Para qualquer domínio de entrada $B$, ele calcula um limite inferior afim $F(x) \geq a^\top x + b$. Este processo é totalmente diferenciável e altamente vetorizado, permitindo execução eficiente em GPUs.
• Ramificação e Limite (Branch-and-Bound - BaB): Para lidar com casos em que os limites lineares são inconclusivos, o framework emprega ramificação e limite no domínio de entrada. Ele particiona recursivamente o domínio de entrada em subdomínios. À medida que os domínios encolhem, as relaxações lineares locais se estreitam e o erro de super-approximação diminui.
• Tratamento do Jacobiano: Para sistemas de tempo contínuo que exigem limites de gradiente (por exemplo, $\nabla V \cdot f$), o framework estende o grafo de computação para codificar explicitamente o cálculo do gradiente via regra da cadeia, tratando o cálculo do Jacobiano como outro operador.

2. Reformulação de Problemas de Controle

O tutorial demonstra como reformular problemas clássicos de teoria de controle em problemas de satisfatibilidade ou otimização compatíveis com o $\alpha,\beta$-CROWN sobre domínios de caixa:

• Análise de Alcançabilidade: Cálculo de super-approximações sólidas de conjuntos alcançáveis limitando a saída do mapa de malha fechada $g(x)$ sobre uma caixa de entrada.
• Verificação de Estabilidade (Lyapunov): Conversão do requisito de que uma função de Lyapunov diminui ao longo das trajetórias em um problema de satisfatibilidade. Para sistemas de tempo discreto, isso envolve verificar condições como $(V(g(x)) - (1-\kappa)V(x) \leq 0)$ sobre um conjunto de subnível, reformulado como implicações lógicas sobre uma caixa circundante. Reformulações semelhantes são fornecidas para sistemas de tempo contínuo, incluindo o tratamento da invariância forward nas fronteiras da caixa.
• Verificação de Segurança (Funções de Barreira): Verificação de que um conjunto seguro é forward invariante, verificando condições na derivada de uma função de barreira. Para sistemas afins de controle, o supremo sobre entradas de controle é convertido em um máximo sobre vértices de poliedro.
• Análise de Contração: Reformulação de condições de contração baseadas em matrizes em problemas de satisfatibilidade escalar envolvendo métricas riemannianas.
• Otimização (MPC): Uso do verificador como um otimizador global para Controle Preditivo de Modelo (MPC), minimizando funções de custo sujeitas a dinâmicas não lineares e restrições, guiado por limites inferiores certificados.

3. Treinamento e Síntese

O artigo discute frameworks para co-síntese de controladores e certificados:

• Síntese Indutiva Guiada por Contraexemplo (CEGIS): Uma abordagem iterativa onde contraexemplos encontrados durante a verificação são usados como dados de treinamento.
• Treinamento Certificado: Um paradigma que incorpora os limites inferiores diferenciáveis gerados pelo $\alpha,\beta$-CROWN diretamente na função de perda de treinamento. Isso permite otimização baseada em gradiente para maximizar o limite inferior certificado de uma especificação, produzindo modelos inerentemente "amigáveis à verificação".

Contribuições Principais

1. Framework Unificado: O artigo apresenta uma abordagem unificada para aplicar o $\alpha,\beta$-CROWN a diversas tarefas de controle, incluindo alcançabilidade, estabilidade, segurança e otimização.
2. Escalabilidade via Paralelização em GPU: Ao aproveitar a natureza eficiente e paralelizável da propagação de limites e da ramificação e limite em GPUs, o framework alcança escalabilidade superior em comparação com abordagens tradicionais baseadas em SMT ou MILP, particularmente para sistemas não lineares complexos e de alta dimensão.
3. Aplicabilidade de Propósito Geral: Diferentemente de métodos restritos a arquiteturas de rede específicas ou tipos de certificados, o $\alpha,\beta$-CROWN lida com funções não lineares gerais representadas como grafos de computação, suportando uma ampla gama de operadores (trigonométricos, lineares por partes, etc.).
4. Diferenciabilidade: A propagação de limites lineares é totalmente diferenciável, permitindo a integração de restrições de verificação diretamente no loop de treinamento (treinamento certificado).
5. Implementação Prática: O tutorial fornece uma interface de programação detalhada (API) e exemplos de código demonstrando como definir grafos de computação, formular restrições usando uma Linguagem Específica de Domínio (DSL) e executar tarefas de verificação, cálculo de limites e otimização. Também oferece uma camada de compatibilidade plug-and-play para a API dReal.

Resultados e Alegações

O artigo afirma que o pipeline proposto demonstra escalabilidade superior em problemas de verificação e otimização que são desafiadores para abordagens tradicionais.

• Eficiência: A capacidade de processar dezenas de milhares de subdomínios simultaneamente em uma GPU permite a poda rápida de grandes regiões e certificação com limites grosseiros em domínios minúsculos.
• Versatilidade: O framework lida com sucesso com várias especificações de controle, incluindo estabilidade de Lyapunov, segurança de função de barreira e métricas de contração, reformulando-as como problemas de satisfatibilidade sobre domínios de caixa.
• Benefícios de Treinamento: O artigo observa que, em um ambiente de quadricóptero 2D, modelos treinados com a abordagem de treinamento certificado foram 5 vezes mais rápidos de verificar em comparação com aqueles treinados usando CEGIS, sugerindo que o objetivo de treinamento melhora diretamente a verificabilidade.

Significado

O significado deste trabalho reside na sua tentativa de ponte a lacuna entre a teoria de controle e a verificação escalável de redes neurais. Ao fornecer um framework unificado, eficiente e de propósito geral, os autores visam tornar a certificação formal um componente mais prático e integral do projeto de controle baseado em aprendizado. O tutorial serve para reduzir a barreira de entrada para a aplicação de técnicas de verificação rigorosas a políticas de controle aprendidas complexas, indo além dos testes empíricos para fornecer garantias formais para sistemas críticos de segurança.