Resumo Técnico: Otimização de Lipschitz para Verificação Formal de Homografias

1. Declaração do Problema

A implantação de redes neurais profundas (DNNs) em domínios críticos para a segurança, como direção autônoma, aeroespacial e saúde, exige garantias formais de robustez. Os métodos atuais de verificação formal concentram-se principalmente em perturbações limitadas pela norma $\ell_p$ (por exemplo, ruído, alterações de contraste) que atuam diretamente no espaço de pixels. No entanto, essas abordagens falham em modelar adequadamente perturbações originadas no mundo físico 3D, como movimento da câmera, mudanças de ponto de vista ou deslocamentos da geometria da cena.

Embora as bolas $\ell_p$ possam teoricamente englobar as imagens resultantes de perturbações físicas, elas superestimam a variedade real de imagens perturbadas, levando a limites frouxos e pouco informativos que frequentemente falham em provar a robustez da rede. Os métodos existentes para robustez 3D limitam-se a abordagens estatísticas (garantias mais fracas), transformações afins 2D (incapazes de modelar efeitos de perspectiva) ou simulações complexas que exigem modelos explícitos de cena 3D. Existe uma lacuna crítica na verificação formal de transformações de geometria projetiva, especificamente homografias, que descrevem o mapeamento plano-a-plano entre diferentes visões de uma superfície plana sob movimento de câmera 3D.

2. Metodologia

Os autores propõem um framework de verificação formal que visa a robustez contra perturbações de movimento 3D da câmera de captura, especificamente para cenas com estruturas predominantemente planas (por exemplo, marcações rodoviárias, sinais de trânsito, planos de solo).

2.1. Derivação de Homografia de Forma Fechada

O método começa estabelecendo um mapeamento de forma fechada de perturbações de pose da câmera para valores de pixels.

• Modelagem Geométrica: Assumindo um modelo de câmera de estenopeico e um recurso de cena plana (por exemplo, $z=0$ no referencial do mundo), os autores derivam a matriz de homografia $H(\kappa)$ induzida por perturbações de pose de 6-DOF (rolagem, arfagem, guinada e translação).
• Parametrização: A homografia é parametrizada por um vetor $\kappa$ representando o delta na pose em relação a uma câmera de referência. Para cenários específicos (por exemplo, rotação pura de guinada), os autores derivam expressões analíticas explícitas para $H(\kappa)$ e sua inversa $H^{-1}(\kappa)$.
• Função de Valor de Pixel: O valor de um pixel transformado $G(\kappa)$ é computado mapeando as coordenadas transformadas de volta à imagem original via $T^{-1}(\kappa)$ e aplicando interpolação bilinear. Isso resulta em uma função não linear $G(\kappa) = I \circ T^{-1}(\kappa)$.

2.2. Aproximação por Trechos Lineares (PWL) e Otimização de Lipschitz

Para verificar a rede, a função não linear $G(\kappa)$ deve ser superestimada por limites lineares que possam ser propagados através do verificador.

• Limites por Trechos Lineares: O espaço de parâmetros $B$ é partitionado em subdomínios. Dentro de cada subdomínio, a função $G(\kappa)$ é aproximada por limites lineares ($LB$e$UB$) derivados de pontos amostrados, seguindo a abordagem de Batten et al. [7].
• Continuidade de Lipschitz: Para garantir que os limites sejam sólidos (ou seja, contenham estritamente os valores verdadeiros da função), os autores analisam a continuidade de Lipschitz de $G(\kappa)$. Eles derivam limites superiores analíticos para a constante de Lipschitz $L$ calculando o gradiente da transformação inversa $T^{-1}(\kappa)$.
• Tratamento de Descontinuidades: Os autores abordam a não continuidade da inversa da homografia em ângulos críticos (onde o denominador se aproxima de zero). Eles definem o domínio de diferenciabilidade $Diff(B)$ e identificam locais candidatos para gradientes máximos (fronteiras e valores específicos de arco-tangente) para calcular constantes de Lipschitz válidas.
• Otimização: Utilizando otimização de Lipschitz, o algoritmo refina iterativamente os limites. Ele avalia a função em pontos amostrados e usa a constante de Lipschitz para limitar o máximo global da violação do limite. Se a violação do limite exceder um limiar $\epsilon$, o subdomínio é dividido e o processo se repete até a convergência.

2.3. Implementação

O método é implementado como um front-end que gera limites lineares para qualquer verificador downstream. Os autores adaptaram o verificador VENUS para lidar com esses limites por trechos lineares, aprimorando seu framework de propagação de limites para derivar limites de pré-ativação a partir de restrições de entrada lineares, em vez de intervalos fixos.

3. Principais Contribuições

1. Verificação Formal de Transformações Projetivas: O artigo deriva homografias de forma fechada induzidas por perturbações de pose de 6-DOF e demonstra sua compatibilidade com restrições por trechos lineares e otimização de Lipschitz. Isso permite limites comprovadamente apertados sobre valores de pixels sob transformações não afins (projetivas).
2. Implementação Eficiente: Os autores fornecem uma implementação eficiente que supera o algoritmo PWL existente [7]. As melhorias incluem correções de meio-pixel para gradientes exatos, inclusão de valores de parâmetros omitidos no conjunto candidato de Lipschitz, dicotomia no espaço de parâmetros e paralelização ao nível de pixel.
3. Benchmarking e Estudo de Caso: O método é avaliado em benchmarks VNN-COMP (MNIST, CIFAR-10, GTSRB) e em um classificador de visibilidade de pista de pouso do mundo real.

4. Resultados

• Melhorias de Desempenho: Comparado a uma reimplementação do algoritmo PWL [7], o método proposto alcança até 89% de aceleração no tempo de execução e 7% de limites mais apertados em curvas de pixels complexas. Em transformações pequenas, as iterações Branch-and-Bound (BaB) foram reduzidas em mais de 71%.
• Descoberta de Vulnerabilidades: A avaliação nos benchmarks VNN-COMP revela que redes treinadas com aumento de dados padrão (incluindo ataques de norma $\ell_p$) exibem fraquezas sistemáticas a perturbações geométricas 3D. Por exemplo, modelos GTSRB (direção autônoma) mostraram 0% de robustez certificada a perturbações 3D (rolagem, arfagem, guinada e translação). Mesmo modelos MNIST e CIFAR mostraram robustez significativamente menor a arfagem, guinada e translação em comparação com perturbações de norma $\ell_p$.
• Estudo de Caso do Mundo Real: Aplicado a um classificador de visibilidade de pista de pouso treinado no conjunto de dados LARD, o método certificou robustez para apenas 16% das imagens de teste sob translações de 10 cm e 1% sob rotações de 1°, destacando vulnerabilidades práticas em sistemas de percepção críticos para a segurança.
• Análise de Sensibilidade: O estudo confirma que a robustez certificada diminui à medida que a amplitude da transformação aumenta (por exemplo, ângulo de guinada), um desafio conhecido na verificação formal que requer divisão de domínio.

5. Significado e Alegações

O artigo alega apresentar o primeiro framework de verificação formal para transformações de geometria projetiva que não depende de simulações complexas, redes substitutas ou modelos explícitos de formação de imagem. Ao aproveitar a tratabilidade analítica das homografias para cenas planas, os autores fecham a lacuna entre a verificação afim 2D e a modelagem completa de cena 3D.

O significado reside em:

• Conformidade Regulatória: Fornecer as garantias matemáticas necessárias para certificar IA em indústrias críticas para a segurança (aviação, veículos autônomos), onde o movimento da câmera é uma fonte primária de incerteza.
• Avanço Metodológico: Estender a otimização de Lipschitz e técnicas PWL para lidar com transformações não afins, distorcidas por perspectiva, que anteriormente eram consideradas intratáveis analiticamente para verificação formal.
• Insight Prático: Demonstrar que as redes atuais de última geração são frágeis a perturbações 3D realistas, sugerindo que o treinamento ou a verificação de robustez devem evoluir além das restrições de norma $\ell_p$ para abordar variações do mundo físico.

Os autores mantêm um tom modesto, reconhecendo que transformações grandes exacerbam não linearidades e que o método é atualmente mais adequado para cenas predominantemente planas com parallaxe e oclusão limitados. Eles posicionam seu trabalho como um meio-termo principista para verificar uma vasta gama de casos de uso em robótica e visão computacional.