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

Riepilogo Tecnico: Formalizzazione in Lean del Limite di Errore di Generalizzazione tramite Complessità di Rademacher e Integrale di Entropia di Dudley

Enunciato del Problema

La sfida centrale affrontata è la verifica formale delle prestazioni di generalizzazione nell'apprendimento automatico. Nello specifico, gli autori mirano a derivare stime teoriche dell'errore di test (rischio sulla popolazione) dall'errore di training (rischio empirico) utilizzando un quadro basato sulla teoria della misura. Sebbene gli approcci classici si basino sulla dimensione di Vapnik–Chervonenkis (VC), questi sono spesso indipendenti dai dati e adattati alla classificazione binaria. La teoria dell'apprendimento moderna utilizza sempre più la complessità di Rademacher, che fornisce limiti netti, dipendenti dai dati, applicabili a perdite a valori reali e a classi di funzioni diverse (ad esempio, deep learning, metodi a kernel). Tuttavia, formalizzare questi argomenti negli assistenti di prova è difficile a causa della necessità di una gestione rigorosa della misurabilità (in particolare per i supremi su classi di ipotesi non numerabili), delle misure prodotto e delle disuguaglianze di concentrazione.

Metodologia

Gli autori formalizzano il limite dell'errore di generalizzazione in Lean 4, sfruttando l'infrastruttura estesa di probabilità basata sulla teoria della misura della libreria Mathlib. Lo sviluppo segue la pipeline standard "simmetrizzazione + differenze limitate" presente nei manuali (ad esempio, Mohri et al., Wainwright), ma la adatta ai vincoli della verifica formale:

1. Impostazione basata sulla Teoria della Misura: Il quadro modella la generazione dei dati tramite uno spazio di probabilità $(\Omega, m_\Omega, \mu)$ e una variabile casuale $X: \Omega \to \mathcal{X}$. I campioni sono modellati come funzioni $\omega: \text{Fin } n \to \Omega$, spinte in avanti per ottenere $S = X \circ \omega$.
2. Definizioni Fondamentali:
   • Complessità di Rademacher: Definita sia per il caso empirico (su un campione fisso $S$) sia per il caso atteso (sulla misura prodotto $\mu^n$). La versione empirica media su tutti i vettori di segno $\sigma \in \{-1, 1\}^n$.
   • Deviazione Uniforme: Definita come il supremo della differenza assoluta tra le medie empiriche e quelle della popolazione su una classe di ipotesi $F = \{f_i\}_{i \in \iota}$.
3. Simmetrizzazione: Un teorema formale (abs_symmetrization_equation) sostituisce il supremo delle differenze tra due campioni indipendenti con una media sulle somme con segno ribaltato, collegando la deviazione uniforme alla complessità di Rademacher.
4. Concentrazione: Gli autori dimostrano una disuguaglianza di McDiarmid da zero all'interno di Lean. Stabiliscono che il funzionale di deviazione uniforme soddisfa la proprietà delle differenze limitate (cambiare un punto del campione altera il valore al massimo di $2b/n$), permettendo la derivazione di limiti di coda ad alta probabilità.
5. Gestione di Insiemi di Indici Non Numerabili: Un ostacolo tecnico critico è la misurabilità dei supremi su insiemi di indici non numerabili $\iota$. Mathlib fornisce la misurabilità per indici numerabili, ma non automaticamente per quelli non numerabili. Gli autori risolvono questo problema:
   • Dimostrando prima i teoremi per insiemi di indici numerabili.
   • Estendendo i risultati a insiemi di indici topologicamente separabili tramite una riduzione densa numerabile. Ciò comporta dimostrare che, per funzioni continue, il supremo su uno spazio separabile è uguale al supremo su un sottoinsieme numerabile denso, a condizione che la continuità sia preservata sotto integrazione (garantita dalla dominazione uniforme).

Contributi Chiave

Il lavoro presenta la prima formalizzazione sistematica dell'analisi di generalizzazione tramite complessità di Rademacher. I contributi specifici includono:

• Infrastruttura Formale Riutilizzabile: Una pipeline verificata meccanicamente che copre la complessità di Rademacher empirica/attesa, la simmetrizzazione, l'analisi delle differenze limitate e la disuguaglianza di McDiarmid.
• Risoluzione della Misurabilità: Un meccanismo riutilizzabile per sollevare i risultati dalle classi di ipotesi numerabili agli spazi parametrici topologicamente separabili. Questo impacchetta esplicitamente le condizioni sufficienti (separabilità, primo-numerabilità, dominazione uniforme e continuità sotto integrazione) necessarie per rendere misurabili i supremi non numerabili, un passaggio spesso implicito nelle dimostrazioni informali.
• Strumenti di Concentrazione Formalizzati: Una prova completa della disuguaglianza di McDiarmid e lemmi di supporto per le disuguaglianze massimali, il lemma di Massart e i numeri di copertura.
• Applicazioni Eseguite:
  • Predittori Lineari: Formalizzazione dei limiti standard $O(1/\sqrt{n})$ per predittori regolarizzati con $\ell_2$ e dei limiti $O(\sqrt{\log(d)/n})$ per predittori regolarizzati con $\ell_1$.
  • Integrale di Entropia di Dudley: Una formalizzazione del limite di tipo Dudley che lega la complessità di Rademacher ai numeri di copertura tramite una costruzione a catena. Ciò ha richiesto la definizione di pseudo-metriche empiriche e la gestione della transizione dalle somme discrete a catena ai limiti integrali.

Risultati

La formalizzazione produce versioni verificate meccanicamente dei limiti standard della teoria dell'apprendimento:

1. Limite Atteso: $E[\text{UD}_n(F)] \leq 2 R_n(F)$, dove $R_n(F)$ è la complessità di Rademacher.
2. Limite ad Alta Probabilità: Per ogni $\delta \in (0, 1)$, con probabilità almeno $1-\delta$:
   $$\text{UD}_n(F) \leq 2 R_n(F) + b \sqrt{\frac{2 \log(1/\delta)}{n}}$$
3. Limiti Specifici: Il repository fornisce prove concrete per la complessità di Rademacher empirica dei predittori lineari sotto vincoli $\ell_2$ e $\ell_1$, nonché per il limite dell'integrale di entropia di Dudley.

Significato e Affermazioni

Gli autori collocano questo lavoro come un passo fondamentale verso una teoria dell'apprendimento affidabile e certificata.

• Collegamento tra Teoria e Verifica: Il lavoro dimostra che la teoria dell'apprendimento moderna basata sulla teoria della misura (che fa affidamento su misure prodotto, integrabilità degli inviluppi e concentrazione) può essere formalizzata in un assistente di prova senza ricorrere a proxy discreti eccessivamente semplificati.
• Chiarimento delle Assunzioni Implicite: Un contributo primario è l'identificazione esplicita delle condizioni necessarie per gestire classi di ipotesi non numerabili. La formalizzazione isola la "riduzione densa numerabile" e le specifiche ipotesi di continuità/integrabilità necessarie, che sono spesso trascurate nei manuali standard.
• Modularità: Lo sviluppo è progettato in modo che la pipeline astratta di Rademacher possa essere riutilizzata. I limiti concreti diventano "corollari eseguibili" ottenuti istanziando la classe di funzioni e soddisfacendo stime analitiche specifiche (ad esempio, vincoli di norma).
• Confronto con Lavori Precedenti: A differenza di formalizzazioni precedenti limitate a classi di ipotesi finite (ad esempio, Bagnall & Stewart) o a casi algoritmici specifici (ad esempio, stumps decisionali), questo lavoro gestisce classi di funzioni generali, potenzialmente non numerabili, con perdite a valori reali.

Il lavoro conclude che, sebbene i limiti matematici in sé siano classici, la formalizzazione chiarisce la precisa struttura logica e le condizioni collaterali necessarie per la loro validità in un contesto rigoroso, fornendo una base per future estensioni come le disuguaglianze di contrazione di Lipschitz e le connessioni con la complessità gaussiana.