Lean Formalization of Generalization Error Bound by Rademacher Complexity and Dudley's Entropy Integral

Resumo Técnico: Formalização Lean do Limite de Erro de Generalização por Complexidade de Rademacher e Integral de Entropia de Dudley

Declaração do Problema

O desafio central abordado é a verificação formal do desempenho de generalização em aprendizado de máquina. Especificamente, os autores visam derivar estimativas teóricas do erro de teste (risco populacional) a partir do erro de treinamento (risco empírico) utilizando um framework de teoria da medida. Embora as abordagens clássicas dependam da dimensão de Vapnik–Chervonenkis (VC), estas são frequentemente independentes dos dados e adaptadas para classificação binária. A teoria moderna de aprendizado utiliza cada vez mais a complexidade de Rademacher, que fornece limites agudos, dependentes dos dados, aplicáveis a perdas de valor real e diversas classes de funções (por exemplo, aprendizado profundo, métodos de kernel). No entanto, a formalização desses argumentos em assistentes de prova é difícil devido à necessidade de tratamento rigoroso da mensurabilidade (particularmente para supremos sobre classes de hipóteses não enumeráveis), medidas produto e desigualdades de concentração.

Metodologia

Os autores formalizam o limite de erro de generalização em Lean 4, aproveitando a extensa infraestrutura de probabilidade de teoria da medida da biblioteca Mathlib. O desenvolvimento segue o pipeline padrão "simetrização + diferenças limitadas" encontrado em livros-texto (por exemplo, Mohri et al., Wainwright), mas adapta-o às restrições da verificação formal:

1. Configuração de Teoria da Medida: O framework modela a geração de dados através de um espaço de probabilidade $(\Omega, m_\Omega, \mu)$ e uma variável aleatória $X: \Omega \to \mathcal{X}$. Amostras são modeladas como funções $\omega: \text{Fin } n \to \Omega$, empurradas para frente para obter $S = X \circ \omega$.
2. Definições Principais:
   • Complexidade de Rademacher: Definida tanto para casos empíricos (sobre uma amostra fixa $S$) quanto esperados (sobre a medida produto $\mu^n$). A versão empírica faz a média sobre todos os vetores de sinais $\sigma \in \{-1, 1\}^n$.
   • Desvio Uniforme: Definido como o supremo da diferença absoluta entre as médias empírica e populacional sobre uma classe de hipóteses $F = \{f_i\}_{i \in \iota}$.
3. Simetrização: Um teorema formal (abs_symmetrization_equation) substitui o supremo das diferenças entre duas amostras independentes por uma média sobre somas com sinais invertidos, ligando o desvio uniforme à complexidade de Rademacher.
4. Concentração: Os autores provam uma desigualdade de McDiarmid a partir do zero dentro do Lean. Eles estabelecem que o funcional de desvio uniforme satisfaz a propriedade de diferenças limitadas (alterar um ponto de amostra altera o valor em no máximo $2b/n$), permitindo a derivação de limites de cauda de alta probabilidade.
5. Tratamento de Conjuntos de Índices Não Enumeráveis: Um obstáculo técnico crítico é a mensurabilidade de supremos sobre conjuntos de índices não enumeráveis $\iota$. A Mathlib fornece mensurabilidade para índices enumeráveis, mas não automaticamente para não enumeráveis. Os autores resolvem isso:
   • Primeiro provando teoremas para conjuntos de índices enumeráveis.
   • Estendendo os resultados para conjuntos de índices topologicamente separáveis via uma redução enumerável densa. Isso envolve provar que, para funções contínuas, o supremo sobre um espaço separável é igual ao supremo sobre um subconjunto denso enumerável, desde que a continuidade seja preservada sob integração (assegurada por dominação uniforme).

Contribuições Principais

O artigo apresenta a primeira formalização sistemática da análise de generalização via complexidade de Rademacher. As contribuições específicas incluem:

• Infraestrutura Formal Reutilizável: Um pipeline verificado mecanicamente cobrindo complexidade de Rademacher empírica/esperada, simetrização, análise de diferenças limitadas e desigualdade de McDiarmid.
• Resolução de Mensurabilidade: Um mecanismo reutilizável para elevar resultados de classes de hipóteses enumeráveis para espaços de parâmetros topologicamente separáveis. Isso empacota explicitamente as condições suficientes (separabilidade, primeira contabilidade, dominação uniforme e continuidade sob integração) necessárias para tornar supremos não enumeráveis mensuráveis, um passo frequentemente implícito em provas informais.
• Ferramentas de Concentração Formalizadas: Uma prova completa da desigualdade de McDiarmid e lemas de apoio para desigualdades máximas, lema de Massart e números de cobertura.
• Aplicações Trabalhadas:
  • Previsores Lineares: Formalização de limites padrão $O(1/\sqrt{n})$ para previsores regularizados $\ell_2$ e limites $O(\sqrt{\log(d)/n})$ para previsores regularizados $\ell_1$.
  • Integral de Entropia de Dudley: Uma formalização do limite do tipo Dudley relacionando complexidade de Rademacher a números de cobertura via uma construção de encadeamento. Isso exigiu definir pseudo-métricas empíricas e lidar com a transição de somas de encadeamento discretas para limites integrais.

Resultados

A formalização produz versões verificadas mecanicamente de limites padrão da teoria de aprendizado:

1. Limite Esperado: $E[\text{UD}_n(F)] \leq 2 R_n(F)$, onde $R_n(F)$ é a complexidade de Rademacher.
2. Limite de Alta Probabilidade: Para qualquer $\delta \in (0, 1)$, com probabilidade de pelo menos $1-\delta$:
   $$\text{UD}_n(F) \leq 2 R_n(F) + b \sqrt{\frac{2 \log(1/\delta)}{n}}$$
3. Limites Específicos: O repositório fornece provas concretas para a complexidade de Rademacher empírica de previsores lineares sob restrições $\ell_2$ e $\ell_1$, bem como o limite da integral de entropia de Dudley.

Significado e Alegações

Os autores posicionam este trabalho como um passo fundamental em direção a uma teoria de aprendizado de máquina confiável e certificada.

• Ponte entre Teoria e Verificação: O trabalho demonstra que a teoria moderna de aprendizado baseada em teoria da medida (que depende de medidas produto, integrabilidade de envoltórios e concentração) pode ser formalizada em um assistente de prova sem recorrer a proxies discretos excessivamente simplificados.
• Esclarecimento de Pressupostos Implícitos: Uma contribuição primária é a identificação explícita das condições necessárias para lidar com classes de hipóteses não enumeráveis. A formalização isola a "redução enumerável-densa" e as hipóteses específicas de continuidade/integrabilidade necessárias, que são frequentemente negligenciadas em livros-texto padrão.
• Modularidade: O desenvolvimento é projetado para que o pipeline abstrato de Rademacher possa ser reutilizado. Limites concretos tornam-se "corolários executáveis" obtidos ao instanciar a classe de funções e descarregar estimativas analíticas específicas (por exemplo, restrições de norma).
• Comparação com Trabalhos Anteriores: Diferentemente de formalizações anteriores limitadas a classes de hipóteses finitas (por exemplo, Bagnall & Stewart) ou casos algorítmicos específicos (por exemplo, estumps de decisão), este trabalho lida com classes de funções gerais, potencialmente não enumeráveis, com perdas de valor real.

O artigo conclui que, embora os próprios limites matemáticos sejam clássicos, a formalização esclarece a estrutura lógica precisa e as condições laterais necessárias para sua validade em um ambiente rigoroso, fornecendo uma base para futuras extensões, como desigualdades de contração Lipschitz e conexões com complexidade gaussiana.