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

Resumen Técnico: Formalización en Lean del Límite del Error de Generalización mediante Complejidad de Rademacher y la Integral de Entropía de Dudley

Enunciado del Problema

El desafío central abordado es la verificación formal del rendimiento de generalización en el aprendizaje automático. Específicamente, los autores buscan derivar estimaciones teóricas del error de prueba (riesgo poblacional) a partir del error de entrenamiento (riesgo empírico) utilizando un marco de teoría de la medida. Aunque los enfoques clásicos se basan en la dimensión de Vapnik–Chervonenkis (VC), estos suelen ser independientes de los datos y están adaptados a la clasificación binaria. La teoría del aprendizaje moderna utiliza cada vez más la complejidad de Rademacher, que proporciona límites agudos y dependientes de los datos aplicables a pérdidas de valor real y diversas clases de funciones (por ejemplo, aprendizaje profundo, métodos de kernel). Sin embargo, formalizar estos argumentos en asistentes de prueba es difícil debido a la necesidad de un manejo riguroso de la medibilidad (particularmente para supremos sobre clases de hipótesis no numerables), medidas producto e desigualdades de concentración.

Metodología

Los autores formalizan el límite del error de generalización en Lean 4, aprovechando la extensa infraestructura de probabilidad basada en teoría de la medida de la biblioteca Mathlib. El desarrollo sigue la pipeline estándar de "simetrización + diferencias acotadas" encontrada en libros de texto (por ejemplo, Mohri et al., Wainwright), pero la adapta a las restricciones de la verificación formal:

1. Configuración de Teoría de la Medida: El marco modela la generación de datos mediante un espacio de probabilidad $(\Omega, m_\Omega, \mu)$ y una variable aleatoria $X: \Omega \to \mathcal{X}$. Las muestras se modelan como funciones $\omega: \text{Fin } n \to \Omega$, empujadas hacia adelante para obtener $S = X \circ \omega$.
2. Definiciones Centrales:
   • Complejidad de Rademacher: Definida tanto para casos empíricos (sobre una muestra fija $S$) como esperados (sobre la medida producto $\mu^n$). La versión empírica promedia sobre todos los vectores de signos $\sigma \in \{-1, 1\}^n$.
   • Desviación Uniforme: Definida como el supremo de la diferencia absoluta entre las medias empírica y poblacional sobre una clase de hipótesis $F = \{f_i\}_{i \in \iota}$.
3. Simetrización: Un teorema formal (abs_symmetrization_equation) reemplaza el supremo de las diferencias entre dos muestras independientes con un promedio sobre sumas con signos invertidos, vinculando la desviación uniforme con la complejidad de Rademacher.
4. Concentración: Los autores demuestran una desigualdad de McDiarmid desde cero dentro de Lean. Establecen que el funcional de desviación uniforme satisface la propiedad de diferencias acotadas (cambiar un punto de muestra altera el valor en a lo sumo $2b/n$), permitiendo la derivación de límites de cola de alta probabilidad.
5. Manejo de Conjuntos de Índices No Numerables: Un obstáculo técnico crítico es la medibilidad de los supremos sobre conjuntos de índices no numerables $\iota$. Mathlib proporciona medibilidad para índices numerables, pero no automáticamente para los no numerables. Los autores resuelven esto mediante:
   • Demostrar primero teoremas para conjuntos de índices numerables.
   • Extender los resultados a conjuntos de índices topológicos separables mediante una reducción densa numerable. Esto implica demostrar que, para funciones continuas, el supremo sobre un espacio separable es igual al supremo sobre un subconjunto denso numerable, siempre que se preserve la continuidad bajo integración (garantizada por la dominación uniforme).

Contribuciones Clave

El artículo presenta la primera formalización sistemática del análisis de generalización mediante complejidad de Rademacher. Las contribuciones específicas incluyen:

• Infraestructura Formal Reutilizable: Una pipeline verificada mecánicamente que cubre la complejidad de Rademacher empírica/esperada, simetrización, análisis de diferencias acotadas y la desigualdad de McDiarmid.
• Resolución de Medibilidad: Un mecanismo reutilizable para elevar resultados desde clases de hipótesis numerables a espacios de parámetros topológicos separables. Esto empaqueta explícitamente las condiciones suficientes (separabilidad, primer numerabilidad, dominación uniforme y continuidad bajo integración) requeridas para hacer medibles los supremos no numerables, un paso a menudo implícito en pruebas informales.
• Herramientas de Concentración Formalizadas: Una prueba completa de la desigualdad de McDiarmid y lemas de apoyo para desigualdades máximas, el lema de Massart y números de cobertura.
• Aplicaciones Desarrolladas:
  • Predictores Lineales: Formalización de límites estándar $O(1/\sqrt{n})$ para predictores regularizados con $\ell_2$ y límites $O(\sqrt{\log(d)/n})$ para predictores regularizados con $\ell_1$.
  • Integral de Entropía de Dudley: Una formalización del límite tipo Dudley que relaciona la complejidad de Rademacher con los números de cobertura mediante una construcción de encadenamiento. Esto requirió definir pseudométricas empíricas y manejar la transición desde sumas de encadenamiento discretas a límites integrales.

Resultados

La formalización produce versiones verificadas mecánicamente de límites estándar de la teoría del aprendizaje:

1. Límite Esperado: $E[\text{UD}_n(F)] \leq 2 R_n(F)$, donde $R_n(F)$ es la complejidad de Rademacher.
2. Límite de Alta Probabilidad: Para cualquier $\delta \in (0, 1)$, con probabilidad al menos $1-\delta$:
   $$\text{UD}_n(F) \leq 2 R_n(F) + b \sqrt{\frac{2 \log(1/\delta)}{n}}$$
3. Límites Específicos: El repositorio proporciona pruebas concretas para la complejidad de Rademacher empírica de predictores lineales bajo restricciones $\ell_2$ y $\ell_1$, así como para el límite de la integral de entropía de Dudley.

Significado y Afirmaciones

Los autores posicionan este trabajo como un paso fundamental hacia una teoría de aprendizaje automático confiable y certificada.

• Puente entre Teoría y Verificación: El trabajo demuestra que la teoría del aprendizaje moderna basada en teoría de la medida (que depende de medidas producto, integrabilidad de envolventes y concentración) puede formalizarse en un asistente de prueba sin recurrir a proxies discretos excesivamente simplificados.
• Clarificación de Supuestos Implícitos: Una contribución principal es la identificación explícita de las condiciones requeridas para manejar clases de hipótesis no numerables. La formalización aísla la "reducción densa-numerable" y las hipótesis específicas de continuidad/integrabilidad necesarias, las cuales a menudo se pasan por alto en libros de texto estándar.
• Modularidad: El desarrollo está diseñado para que la pipeline abstracta de Rademacher pueda reutilizarse. Los límites concretos se convierten en "corolarios ejecutables" obtenidos al instanciar la clase de funciones y descargar estimaciones analíticas específicas (por ejemplo, restricciones de norma).
• Comparación con Trabajos Previos: A diferencia de formalizaciones anteriores limitadas a clases de hipótesis finitas (por ejemplo, Bagnall & Stewart) o casos algorítmicos específicos (por ejemplo, estantes de decisión), este trabajo maneja clases de funciones generales, potencialmente no numerables, con pérdidas de valor real.

El artículo concluye que, aunque los límites matemáticos en sí mismos son clásicos, la formalización aclara la estructura lógica precisa y las condiciones secundarias necesarias para su validez en un entorno riguroso, proporcionando una base para futuras extensiones como desigualdades de contracción Lipschitz y conexiones con la complejidad gaussiana.