Training with Hard Constraints: Learning Neural Certificates and Controllers for SDEs

Resumo Técnico: Treinamento com Restrições Rígidas para SDEs

1. Problema e Motivação

O artigo aborda o desafio de garantir segurança formal em sistemas dinâmicos contínuos governados por Equações Diferenciais Estocásticas (SDEs). Em aplicações críticas, o desempenho empírico de controladores baseados em redes neurais (NN) é insuficiente; é necessário garantir que o sistema satisfaça especificações de "alcançar-evitar" (reach-avoid) com probabilidade alta.

O problema central é a construção de certificados de supermartingala (funções de Lyapunov estocásticas) que satisfaçam um conjunto de desigualdades diferenciais em todo o domínio contínuo do estado.

• Desafio: Métodos existentes frequentemente utilizam penalidades suaves (soft constraints) ou verificação pós-treinamento, o que não oferece garantias de satisfação das restrições em todo o domínio.
• Objetivo: Desenvolver frameworks de treinamento que incorporem restrições rígidas (hard constraints) diretamente no processo de aprendizado, garantindo a validade do certificado e/ou do controlador ao término do treinamento, mantendo a escalabilidade para sistemas de alta dimensão.

2. Metodologia

Os autores propõem duas abordagens complementares para treinar redes neurais com garantias de satisfação de restrições:

A. Abordagem Baseada em Limites (Bound-Training / Hard-SAT)

• Conceito: Inspirada em métodos de robustez de NN, esta abordagem particiona o espaço de estados em células discretas. Utilizando aritmética de intervalos, calcula-se limites superiores e inferiores para a função certificado $V_\theta$ e seu gerador infinitesimal $G[V_\theta]$ dentro de cada célula.
• Função de Perda: Define-se uma função de perda baseada nesses limites. Se a perda for zero, garante-se que todas as desigualdades do certificado (não-negatividade, limites no conjunto inicial/seguro/objetivo e derivada negativa) são satisfeitas em todo o domínio.
• Otimização Conjunta: O método permite o treinamento conjunto de um controlador neural ($\pi_\theta$) e um certificado neural ($V_\theta$), propagando o gradiente através do grafo computacional derivado da dinâmica fechada da SDE.
• Estratégias de Escalabilidade: Para mitigar a explosão combinatória do particionamento em dimensões mais altas, o método emprega:
  • Refinamento Adaptativo: Divide apenas as células que violam as restrições.
  • Mesclagem (Merging): Une células vizinhas que já satisfazem as restrições com uma margem de segurança.
• Garantia: Se a perda atingir zero, o certificado é matematicamente válido para todo o espaço de estados.

B. Abordagem Baseada em Cenários (Scenario-Based Training / PAC)

• Conceito: Projetada para sistemas de alta dimensão onde o particionamento é proibitivo, esta abordagem utiliza otimização estocástica baseada em cenários.
• Mecanismo: Em vez de particionar o espaço, amostra-se um conjunto finito de estados. O problema é formulado como um Programa Linear (LP) otimizando apenas os parâmetros da última camada da rede neural (assumindo que as camadas anteriores são pré-treinadas) e o parâmetro $\beta$.
• Garantia PAC: Utiliza a teoria de otimização convexa para fornecer garantias Provavelmente Aproximadamente Corretas (PAC). Com alta confiança ($1-\delta$), o certificado satisfaz as restrições em todo o domínio, exceto em um conjunto de medida pequena ($\epsilon$) que encolhe conforme o número de amostras ($N$) aumenta.
• Vantagem: A complexidade de amostragem necessária é independente da dimensão do espaço de estados, permitindo escalabilidade para sistemas de 10 dimensões ou mais.

3. Principais Contribuições

1. Framework Hard-SAT: Um método de treinamento com limites que garante satisfação de restrições rígidas para certificados de redes neurais em SDEs, superando métodos de verificação pós-processo.
2. Síntese Conjunta: Extensão do framework para o treinamento simultâneo de controladores e certificados neurais, onde as restrições do certificado guiam diretamente a atualização do controlador, eliminando a necessidade de tentativa e erro.
3. Método Escalável PAC: Uma abordagem baseada em cenários que permite a síntese de certificados para sistemas de alta dimensão (até 10D) com garantias estatísticas ajustáveis.
4. Validação Empírica: Demonstração de que o treinamento prévio (soft) sozinho não gera certificados válidos, enquanto as abordagens propostas conseguem sintetizar soluções verificáveis.

4. Resultados Experimentais

Os autores avaliaram seus métodos em benchmarks de verificação e síntese de controle:

• Verificação (Sistemas de 2D a 10D):
  • O método Hard-SAT superou o estado da arte (Neustroev et al., 2025), exigindo menos partições e tempo computacional, alcançando sucesso em sistemas de até 5 dimensões (GBM - Movimento Browniano Geométrico).
  • O método Baseado em Cenários escalou facilmente para 10 dimensões, alcançando probabilidades de alcançabilidade-alvo ($p_{RA}$) próximas a 1.0 com garantias PAC rigorosas (ex: $\epsilon \approx 10^{-4}$).
• Síntese de Controle (4 Sistemas Complexos):
  • Sucesso na síntese conjunta para: Pêndulo Invertido Estocástico (2D), GBM com objetivo não trivial (2D), Sistema de Lorenz Estocástico (3D) e Dinâmica Longitudinal de uma aeronave XV-15 (3D).
  • Em todos os casos, o algoritmo encontrou controladores e certificados que garantiram $p_{RA} \geq 0.95$.
  • Simulações de Monte Carlo confirmaram uma probabilidade empírica de sucesso de 1.0 para os sistemas em malha fechada.

5. Significado e Impacto

Este trabalho representa um avanço significativo na interseção entre aprendizado de máquina e controle formal estocástico.

• Superação de Limitações: Resolve o dilema entre a expressividade das redes neurais e a necessidade de garantias formais rígidas, algo que métodos anteriores (baseados em SMT ou verificação pós-treinamento) não conseguiam fazer eficientemente para SDEs contínuas.
• Escalabilidade: Ao combinar a garantia absoluta do método baseado em limites (para dimensões moderadas) com a eficiência estatística do método baseado em cenários (para alta dimensão), o trabalho oferece um caminho prático para a aplicação de controle seguro em sistemas complexos do mundo real, como aeronaves e sistemas robóticos sujeitos a ruído.
• Reprodutibilidade: O código foi disponibilizado publicamente, facilitando a adoção e o avanço futuro na área de síntese de controladores certificados.