Formalization of Line Search Methods by Lean

Sintesi Tecnica: Formalizzazione dei Metodi di Line Search tramite Lean

Definizione del Problema
Il documento affronta la necessità di una verifica rigorosa tramite macchina della teoria dell'ottimizzazione non lineare, concentrandosi specificamente sui metodi di ricerca della linea (line search). Sebbene le formalizzazioni esistenti nel teorema prover Lean abbiano coperto gli algoritmi del primo ordine per l'ottimizzazione convessa, i metodi a struttura a blocchi e le condizioni di ottimalità (ad esempio, le condizioni KKT), il quadro teorico specifico che governa la ricerca della linea — cruciale per la convergenza globale dei metodi iterativi basati sul gradiente — restava da formalizzare. Gli autori mirano a tradurre le definizioni standard dei libri di testo, le strategie di selezione adattiva della dimensione del passo e gli argomenti di convergenza in codice Lean verificabile dalla macchina, al fine di eliminare l'ambiguità e garantire la correttezza.

Metodologia
Gli autori utilizzano Lean 4, sfruttando la libreria Mathlib, per formalizzare le fondamenta matematiche e la logica algoritmica della ricerca della linea. La metodologia prevede:

1. Modellazione Matematica: Lo spazio vettoriale $\mathbb{R}^n$ è modellato come funzioni da Fin n a $\mathbb{R}$. Gli autori definiscono un prodotto interno euclideo e una norma (vnorm) personalizzati invece di fare affidamento sulla norma sup-norm fornita da Mathlib, dimostrando le proprietà standard come la disuguaglianza di Cauchy–Schwarz e la relazione tra la norma al quadrato e il prodotto interno come teoremi piuttosto che come assiomi.
2. Formalizzazione delle Assunzioni: Assunzioni chiave, come la continuità di Lipschitz del gradiente e la proprietà di approssimazione del primo ordine (comportamento dell'espansione di Taylor), sono definite come predicati espliciti (GradLipschitz, FirstOrderApprox) anziché come assiomi, assicurando che siano portate come ipotesi nei teoremi.
3. Formalizzazione Algoritmica: Il documento formalizza la logica della ricerca della linea con backtracking. Riconoscendo che il confronto tra numeri reali è indecidibile nella logica di Lean, gli autori astraggono il test di Armijo in un oracolo booleano (test : N → Bool) per le definizioni eseguibili (backtrackRun), mentre dimostrano l'esistenza matematica di una dimensione del passo valida utilizzando Nat.find per identificare l'esponente minimo che soddisfa le condizioni.
4. Dimostrazioni di Convergenza: Il nucleo della metodologia consiste nel dimostrare il teorema di Zoutendijk. Ciò viene ottenuto derivando un limite inferiore sulla diminuzione della funzione per iterazione (combinando le condizioni di Armijo, di Wolfe e di Lipschitz) e sommando questi limiti per dimostrare che la serie delle derivate direzionali al quadrato è finita.

Contributi Chiave
Il documento fornisce una formalizzazione completa dei seguenti componenti:

• Definizioni Fondamentali: Definizioni formali per le direzioni di discesa, il prodotto interno euclideo e la norma euclidea personalizzata.
• Criteri di Ricerca della Linea: Definizioni e prove rigorose per:
  • Condizione di Armijo: Dimostrare l'esistenza di una dimensione del passo che soddisfi la diminuzione sufficiente e la sua implicazione di riduzione stretta del valore della funzione.
  • Condizione di Goldstein: Formalizzare i limiti duali sui valori della funzione.
  • Condizioni di Wolfe: Formalizzare sia la condizione di Armijo (diminuzione sufficiente) che quella di curvatura, e dimostrare che Wolfe implica Armijo.
  • Condizioni Non-Monotone: Formalizzazione della condizione di Grippo (massimo scorrevole) e della condizione di Zhang-Hager (combinazione convessa dei valori precedenti), inclusi i teoremi che mostrano come queste si riducano ad Armijo standard sotto specifici limiti di parametri.
• Implementazione del Backtracking: Un'implementazione verificata dell'algoritmo di ricerca della linea con backtracking che garantisce la terminazione e la positività della dimensione del passo risultante.
• Teorema di Zoutendijk: Una dimostrazione verificata dalla macchina del teorema di Zoutendijk, che stabilisce che per i metodi basati sul gradiente che soddisfano le condizioni di Wolfe, la somma dei quadrati dei coseni degli angoli tra il gradiente e la direzione di ricerca (pesata dalla norma del gradiente) è finita.
• Convergenza Globale: Una dimostrazione formale che, sotto il limite di sommabilità di Zoutendijk, la norma del gradiente delle iterazioni di discesa più rapida converge a zero (specificamente, $\liminf_{k \to \infty} \|\nabla f(x_k)\| = 0$).

Risultati
La formalizzazione verifica con successo che:

1. Le direzioni di discesa garantiscono l'esistenza di dimensioni del passo che diminuiscono strettamente la funzione obiettivo.
2. La ricerca della linea con backtracking, quando guidata dalla condizione di Armijo, termina sempre con una dimensione del passo valida e positiva.
3. Il teorema di Zoutendijk è valido sotto l'assunzione di gradienti Lipschitz continui e condizioni di Wolfe, fornendo un limite rigoroso sul comportamento della convergenza.
4. La norma del gradiente della sequenza generata converge a zero, confermando la convergenza globale del metodo.

Significatività
Gli autori pongono questo lavoro come un passo fondamentale nella verifica delle macchine dell'ottimizzazione non lineare. Fornendo definizioni e prove verificabili dalla macchina per la teoria della ricerca della linea, il documento:

• Integra le esistenti formalizzazioni dei metodi di ottimizzazione del primo ordine e delle condizioni di ottimalità.
• Colma il divario tra le definizioni informali dei libri di testo e il codice eseguibile e verificato.
• Stabilisce una base riutilizzabile per lo sviluppo verificato di algoritmi più avanzati nella programmazione non lineare.
• Riduce l'ambiguità negli argomenti standard dell'ottimizzazione, muovendo il campo verso un ragionamento formalizzato e verificabile dalla macchina.

Il codice per questa formalizzazione è reso disponibile alla comunità per supportare ulteriori ricerche e applicazioni ingegneristiche nell'ottimizzazione verificata.