⚡ electrical engineering

Parallel Differentiable Reachability for Learning and Planning with Certified Neural Dynamics and Controllers

Este artigo apresenta um framework de alcançabilidade diferenciável e paralelizável em JAX que combina flowpipes de modelos de Taylor com propagação de limites no estilo CROWN para permitir treinamento certificado e planejamento baseado em gradientes para dinâmicas e controladores de redes neurais sob incerteza.

Autores originais: Keyi Shen, Glen Chou

Publicado 2026-05-26

📖 5 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Keyi Shen, Glen Chou

Artigo original sob licença CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo

Imagine que você está ensinando um robô a realizar uma tarefa delicada, como empurrar um objeto em forma de T sobre uma mesa ou pilotar um drone através de uma fenda estreita. Você usa um "cérebro" (uma rede neural) para ajudar o robô a descobrir como se mover. Esse cérebro é incrivelmente bom em adivinhar o que acontecerá a seguir com base na experiência passada.

No entanto, há um grande problema: E se o robô estiver ligeiramente errado? Talvez o chão esteja escorregadio, ou um sensor tenha lido mal a distância por uma pequena fração. No mundo real, esses pequenos erros podem se acumular. Um erro minúsculo no primeiro passo pode levar a uma colisão no décimo passo.

Tradicionalmente, os engenheiros têm duas opções:

Confiar completamente no robô: Isso é rápido e funciona bem na maioria das vezes, mas, se algo der errado, o robô pode colidir porque não levou em conta os "e se".
Verificar a matemática formalmente: Isso garante a segurança calculando todos os resultados possíveis, mas é tão lento e complicado que não pode ser usado enquanto o robô está realmente se movendo ou aprendendo.

Este artigo apresenta uma nova ferramenta chamada DiffReach, que atua como um "calculador de segurança super-rápido" capaz de operar em tempo real. Eis como funciona, usando algumas analogias do cotidiano:

1. A Analogia da "Sombra" (Alcançabilidade)

Imagine que o robô é uma pessoa caminhando em uma floresta nebulosa. Você não sabe exatamente onde ela está, apenas que está em algum lugar dentro de um pequeno círculo ao redor de um ponto conhecido.

Antigo Método: Para estar seguro, você poderia desenhar uma nuvem gigante e difusa ao redor da pessoa, que fica cada vez maior a cada passo, eventualmente cobrindo toda a floresta. Isso é seguro, mas é assustador demais para usar, pois diz "ela pode bater em uma árvore" mesmo que esteja longe.
O Método do Artigo: O DiffReach desenha uma sombra apertada e flexível ao redor do robô. À medida que o robô se move, essa sombra se estica e se contorce para seguir exatamente o caminho do robô, mas nunca fica maior do que o necessário. Ela diz: "Se o robô começar aqui, ele pode acabar em qualquer lugar dentro desta forma específica, mas em nenhum outro lugar".

2. A Analogia da "Linha de Montagem" (Paralelo e Diferenciável)

Geralmente, calcular essas sombras é como uma única pessoa resolvendo um problema matemático em um pedaço de papel. Leva uma eternidade.

A Inovação: Os autores construíram essa ferramenta usando JAX (um poderoso motor de computação). Imagine que, em vez de uma pessoa, você tem uma fábrica com milhares de trabalhadores (GPUs) fazendo a matemática simultaneamente.
Diferenciável: Esta é a parte mágica. Normalmente, os verificações de segurança são como um "placa de pare" — você verifica e, se não for seguro, você para. Você não pode usar a placa de pare para ensinar o robô a dirigir melhor. O DiffReach é como uma rampa suave e deslizante. Como a matemática é "diferenciável", o robô pode olhar para a sombra, ver onde ela está ficando muito larga e ajustar imediatamente seu cérebro (rede neural) para tornar a sombra mais apertada. Isso transforma a segurança de uma "placa de pare" em um "volante".

3. O Motor de Duas Partes

O artigo combina duas técnicas matemáticas diferentes em uma única máquina perfeita:

Modelos de Taylor (A Parte Analítica): Para partes do robô que entendemos com a física (como a aerodinâmica de um drone), eles usam um método que prevê o caminho como uma curva suave.
CROWN (A Parte Neural): Para as partes do "cérebro" (as redes neurais), eles usam uma técnica que verifica os limites dos palpites da IA.
A Unificação: Eles criaram uma linguagem universal (uma "Interface Unificada TM-CROWN") para que esses dois métodos diferentes possam conversar entre si sem perder precisão. É como traduzir uma conversa entre um físico e um especialista em IA sem perder nenhum detalhe na tradução.

4. O Que Eles Realmente Fizeram (Os Resultados)

Os autores não apenas construíram a ferramenta; eles a usaram para fazer duas coisas específicas:

Treinamento Certificado: Eles ensinaram o cérebro do robô a ser "consciente da segurança". Em vez de apenas aprender a atingir um alvo, o cérebro aprendeu a manter sua "sombra" pequena. Se a sombra ficar muito grande (significando que o robô está inseguro), o treinamento o penaliza. O resultado? Robôs que são tão bons em seus trabalhos, mas muito mais seguros quando as coisas dão errado.
Planejamento Seguro (MPC): Eles usaram a ferramenta para planejar trajetórias em tempo real.
- Na Simulação: Eles testaram isso em um braço robótico e em um enxame de drones (com até 72 dimensões de movimento!). A ferramenta foi 100 vezes mais rápida do que os métodos anteriores, mantendo as margens de segurança apertadas.
- No Mundo Real: Eles testaram em um braço robótico real empurrando um objeto em forma de T. O robô planejou com sucesso seus movimentos enquanto evitava obstáculos, mesmo quando o ambiente era ligeiramente imprevisível.

A Conclusão

Este artigo apresenta uma maneira de tornar os robôs inteligentes e seguros ao mesmo tempo. Ao tornar a verificação de segurança rápida o suficiente para rodar em uma placa de vídeo (GPU) e flexível o suficiente para fazer parte do processo de aprendizado, eles permitem que os robôs aprendam com a experiência sem esquecer de vigiar os "e se".

O que eles NÃO afirmaram:

Eles não afirmaram que isso funciona para cirurgia médica ou veículos autônomos em estradas públicas ainda.
Eles não afirmaram que resolve todos os problemas de segurança (eles admitem que ainda luta com horizontes de tempo muito longos ou contatos físicos complexos, como bolas quicando).
Eles focaram estritamente em tarefas de robótica, como empurrar objetos e pilotar drones.

Resumo Técnico: Alcançabilidade Diferenciável Paralela para Aprendizado e Planejamento com Dinâmicas e Controladores Neurais Certificados

Declaração do Problema

Modelos de dinâmicas de redes neurais (NN) e políticas de controle demonstraram forte desempenho empírico em robótica, particularmente em ambientes complexos onde a modelagem analítica é inviável. No entanto, fornecer garantias robustas de segurança para sistemas NN em malha fechada sob incerteza permanece um desafio significativo. A análise de alcançabilidade clássica oferece garantias formais por meio de sobre-approximações de conjuntos alcançáveis, mas frequentemente escala mal, luta com componentes NN e produz limites excessivamente conservadores. Por outro lado, métodos modernos de verificação de redes neurais (NNV), como o CROWN, escalam bem para redes grandes, mas são projetados principalmente para verificação estática, carecem de suporte para dinâmicas de tempo contínuo e são geralmente não diferenciáveis.

Consequentemente, a análise de alcançabilidade é tipicamente restrita à certificação post-hoc, criando ciclos custosos de treinamento não certificado, falha na verificação e retreinamento. Há uma necessidade crítica de um framework que integre a alcançabilidade certificada diretamente nos pipelines de aprendizado robótico e planejamento online, suportando sistemas de tempo contínuo e discreto com componentes analíticos e baseados em NN, mantendo-se diferenciável e eficiente.

Metodologia

Os autores propõem o DiffReach, um framework de alcançabilidade paralelizável e diferenciável implementado em JAX. A inovação central é uma representação unificada que combina a construção de fluxos de modelos de Taylor (TM) para dinâmicas analíticas com a propagação de limites lineares estilo CROWN para componentes neurais.

1. Representação Unificada (Interface Taylor-CROWN)

Para permitir computação em lote em GPU e diferenciação automática, o framework adota uma representação de modelo de Taylor de forma fixa. Em vez de polinômios de tamanho variável, os conjuntos alcançáveis são representados como:
$F(z) = c + Az \oplus I \quad \text{ou} \quad F(z) = c + Az + B \tau z \oplus I$
onde $z$ amplia o estado com o tempo, $c$ é uma constante, $A$ e $B$ são matrizes que capturam dependências afins e quase-quadráticas, e $I$ é um resto intervalar. Esta representação preserva dependências afins sem relaxamento intervalar intermediário.

Componentes Neurais: O framework aproveita o CROWN (via jax_verify) para calcular limites afins para redes neurais. Uma contribuição chave é a imposição de uma restrição de inclinação compartilhada no CROWN, garantindo que os limites inferior e superior compartilhem o mesmo termo linear. Isso permite que as saídas da rede neural sejam representadas como TMs lineares, mantendo a compatibilidade com o pipeline de dinâmicas analíticas.
Sistemas de Tempo Contínuo (CT): Para sistemas CT com controle de feedback NN, o framework alterna entre:
1. Certificação do Controlador: Usando a interface TM-CROWN para certificar a saída do controlador neural dado o envoltório TM do estado atual.
2. Propagação de Dinâmicas: Propagando as dinâmicas do sistema (NN ou ODE analítica) usando fluxos TM sob uma política de retenção de ordem zero para a entrada de controle.
Sistemas de Tempo Discreto (DT): A alcançabilidade reduz-se à propagação passo a passo, onde a interface TM-CROWN certifica o mapa de um passo em cada intervalo de tempo.

2. Aplicações DiffReach-Robótica

Construindo sobre o motor DiffReach, os autores desenvolvem dois métodos focados em robótica:

Treinamento Certificado: Um método de treinamento para dinâmicas e controladores neurais que amplia perdas padrão de previsão ou rastreamento com um termo de regularização consciente de alcançabilidade. Este termo penaliza o crescimento do volume de conjuntos alcançáveis certificados sob incerteza limitada. Para estabilizar o treinamento, emprega-se uma estratégia de aprendizado curricular, aumentando progressivamente o horizonte de simulação e diminuindo o raio de perturbação.
MPC Consciente de Alcançabilidade: Um esquema de Controle Preditivo Baseado em Modelo (MPC) baseado em amostragem que integra conjuntos alcançáveis certificados no planejamento online. O planejador otimiza uma função de custo composta pelo objetivo da tarefa e uma penalidade para trajetórias inseguras ou grandes conjuntos alcançáveis. A paralelização permite a avaliação eficiente de muitas trajetórias candidatas, com refinamento baseado em gradiente aplicado aos principais candidatos para reduzir ainda mais o conservadorismo.

Principais Contribuições

Framework de Alcançabilidade Diferenciável Paralela: Uma representação unificada baseada em JAX que combina fluxos de modelos de Taylor e propagação de limites estilo CROWN para sistemas de tempo contínuo e discreto com dinâmicas/controladores analíticos e baseados em NN.
Método de Treinamento Certificado: Uma abordagem de aprendizado que usa objetivos de conjunto alcançável diferenciável para melhorar a robustez de componentes neurais sob incerteza, incentivando modelos "amigáveis à alcançabilidade".
MPC Consciente de Alcançabilidade: Um esquema de planejamento online que integra conjuntos alcançáveis certificados em MPC baseado em amostragem com refinamento baseado em gradiente, permitindo planejamento verificado por construção.
Validação Experimental: Avaliação abrangente em manipulação não preênse (empurrão em T) e tarefas de quadrotor, incluindo experimentos em hardware e avaliações de alta dimensionalidade (até 72D), demonstrando planejamento online prático com garantias certificadas.

Resultados

O framework foi avaliado em uma GPU RTX 4090 através de várias dimensões:

Eficiência e Estreiteza: Comparado a baselines de última geração para DT (CROWN) e CT (immrax), o DiffReach alcança estreiteza de conjunto alcançável comparável, sendo aproximadamente 100× mais rápido que o CROWN para sistemas DT. Para sistemas CT, produz conjuntos alcançáveis substancialmente mais estreitos que o immrax, que frequentemente sofre de overflow numérico e tubos de volume infinito.
Escalabilidade: O framework escala efetivamente para sistemas de maior dimensionalidade, incluindo um enxame de 6 quadrotors (estado de 72D) e um brao planar de 10 juntas (estado de 40D). Embora a memória escale como $O(n^2)$ , o tempo de execução escala favoravelmente devido a operações matriciais paralelas em GPU.
Treinamento Certificado: Modelos treinados com regularização de alcançabilidade alcançaram desempenho nominal comparável ao treinamento padrão, mas produziram conjuntos alcançáveis substancialmente mais estreitos. Esses conjuntos corresponderam estreitamente aos volumes amostrados de limite inferior, enquanto modelos não certificados produziram previsões frouxas e menos verificáveis.
Planejamento Robusto: Em experimentos de MPC sob perturbações limitadas, o planejador consciente de alcançabilidade manteve altas taxas de sucesso e satisfez restrições, enquanto o MPC padrão com modelos não certificados falhou significativamente sob perturbações maiores (por exemplo, contato não intencional em tarefas de empurrão em T).
Implantação em Hardware: O sistema foi implantado em uma plataforma Kuka iiwa para empurrão em T, operando online a aproximadamente 10 Hz (5 Hz com refinamento), demonstrando a viabilidade de integrar alcançabilidade diferenciável ao controle robótico em tempo real.

Significado e Alegações

O artigo afirma que o DiffReach preenche a lacuna entre verificação formal e aprendizado robótico, fornecendo um primitivo de alcançabilidade diferenciável e acelerado por GPU. Diferentemente de métodos anteriores restritos à verificação offline, este framework permite que objetivos de conjunto alcançável informem diretamente o treinamento de dinâmicas e controladores neurais e a execução de planejamento online.

Os autores enfatizam que sua abordagem permite aprendizado e planejamento "verificados por construção", reduzindo a dependência de ciclos custosos de certificação post-hoc. Ao unificar modelos de Taylor e CROWN dentro de um único grafo de computação, o método preserva dependências afins e suporta sistemas de tempo contínuo e discreto, abordando uma limitação crítica nas atuais ferramentas de análise NN em malha fechada.

O trabalho conclui reconhecendo limitações atuais, como desafios com conservadorismo de longo horizonte e dinâmicas híbridas ou ricas em contato, mas postula que este framework motiva pesquisas futuras sobre alcançabilidade diferenciável escalável e integração mais estreita entre verificação formal, aprendizado robótico e controle.