Formalization of Line Search Methods by Lean

Technische Samenvatting: Formalisering van Line Search-methoden door Lean

Probleemstelling
Het artikel behandelt de noodzaak van rigoureuze machineverificatie van nietlineaire optimalisatietheorie, met een specifieke focus op line search-methoden. Hoewel bestaande formaliseringen in de Lean theorem prover hebben gefocust op first-order algoritmen voor convexe optimalisatie, blokgestructureerde methoden en optimaliteitsvoorwaarden (bijv. KKT-voorwaarden), bleef het specifieke theoretische kader dat line search beheerst — cruciaal voor de globale convergentie van gradiëntgebaseerde iteratieve methoden — nog te worden formeel geverifieerd. De auteurs beogen standaard tekstboekdefinities, adaptieve stapgrootte-selectiestrategieën en convergentieargumenten te vertalen naar machine-controleerbare Lean-code om ambiguïteit te elimineren en correctheid te waarborgen.

Methodologie
De auteurs maken gebruik van Lean 4, waarbij zij gebruikmaken van de Mathlib-bibliotheek, om de wiskundige fundamenten en algoritmische logica van line search te formaliseren. De methodologie omvat:

1. Wiskundige Modellering: De vectorruimte $\mathbb{R}^n$ wordt gemodelleerd als functies van Fin n naar $\mathbb{R}$. De auteurs definiëren een aangepast Euclidisch inproduct en norm (vnorm) in plaats van te vertrouwen op de ambient sup-norm die door Mathlib wordt aangeboden, waarbij zij standaard eigenschappen zoals de Cauchy–Schwarz-ongelijkheid en de relatie tussen de kwadratische norm en het inproduct bewijzen als stellingen in plaats van axioma's.
2. Formalisering van Aannames: Cruciale aannames, zoals de Lipschitz-continuïteit van de gradiënt en de first-order benaderingseigenschap (Taylor-expansiegedrag), worden gedefinieerd als expliciete predicaten (GradLipschitz, FirstOrderApprox) in plaats van axioma's, waardoor ze als hypothesen in stellingen worden meegedragen.
3. Algoritmische Formalisering: Het artikel formaliseert de logica van backtracking line search. Omdat vergelijken van reële getallen onbeslisbaar is in de logica van Lean, abstraheren de auteurs de Armijo-test naar een Booleaanse oracle (test : N → Bool) voor uitvoerbare definities (backtrackRun), terwijl zij de wiskundige existentie van een geldige stapgrootte bewijzen met behulp van Nat.find om de minimale exponent te identificeren die aan de voorwaarden voldoet.
4. Convergentiebewijzen: De kern van de methodologie bestaat uit het bewijzen van de Zoutendijk-stelling. Dit wordt bereikt door een ondergrens af te leiden voor de functiedaling per iteratie (combinatie van Armijo, Wolfe kromming en Lipschitz-condities) en deze grenzen op te tellen om aan te tonen dat de reeks van gekwadrateerde directionele afgeleiden eindig is.

Belangrijkste Bijdragen
Het artikel biedt een uitgebreide formalisering van de volgende componenten:

• Fundamentele Definities: Formele definities voor dalingsrichtingen, het Euclidische inproduct en de aangepaste Euclidische norm.
• Line Search Criteria: Rigoureuze definities en bewijzen voor:
  • Armijo Conditie: Het bewijzen van de existentie van een stapgrootte die voldoet aan voldoende daling en de implicatie daarvan van een strikte reductie van de functiewaarde.
  • Goldstein Conditie: Het formaliseren van de duale grenzen op functiewaarden.
  • Wolfe Voorwaarden: Het formaliseren van zowel de Armijo (voldoende daling) als de krommingvoorwaarden, en het bewijzen dat Wolfe Armijo impliceert.
  • Niet-monotone Condities: Formalisering van de Grippo-conditie (sliding maximum) en de Zhang-Hager conditie (convex combinatie van vorige waarden), inclusief bewijzen die laten zien dat zij reduceren tot de standaard Armijo onder specifieke parameterlimieten.
• Backtracking Implementatie: Een geverifieerde implementatie van het backtracking line search algoritme dat de terminatie en de positiviteit van de resulterende stapgrootte garandeert.
• Zoutendijk Stelling: Een machine-geverifieerd bewijs van de Zoutendijk-stelling, die vaststelt dat voor gradiëntgebaseerde methoden die voldoen aan de Wolfe-voorwaarden, de som van de gekwadrateerde cosinussen van de hoeken tussen de gradiënt en de zoekrichting (gewogen door de gradiëntnorm) eindig is.
• Globale Convergentie: Een formeel bewijs dat onder de Zoutendijk summabiliteitsgrens, de gradiëntnorm van de steilste daling iteraties convergeert naar nul (specifiek, $\liminf_{k \to \infty} \|\nabla f(x_k)\| = 0$).

Resultaten
De formalisering verifieert succesvol dat:

1. Dalingsrichtingen de existentie garanderen van stapgroottes die de objectieve functie strikt verlagen.
2. Backtracking line search, wanneer gestuurd door de Armijo-conditie, altijd termineert met een geldige, positieve stapgrootte.
3. De Zoutendijk-stelling standhoudt onder de aanname van Lipschitz-continue gradiënten en Wolfe-voorwaarden, wat een rigoureuze grens biedt aan het convergentiegedrag.
4. De gradiëntnorm van de gegenereerde sequentie convergeert naar nul, wat de globale convergentie van de methode bevestigt.

Significantie
De auteurs positioneren dit werk als een fundamentele stap in de machineverificatie van nietlineaire optimalisatie. Door machine-controleerbare definities en bewijzen voor line search-theorie te bieden, dient dit artikel om:

• Bestaande formaliseringen van first-order optimalisatiemethoden en optimaliteitsvoorwaarden aan te vullen.
• De kloof te overbruggen tussen informele tekstboekdefinities en uitvoerbare, geverifieerde code.
• Een herbruikbare basis te leggen voor de geverifieerde ontwikkeling van meer geavanceerde algoritmen in nietlineaire programmering.
• Ambiguïteit in standaard optimalisatieargumenten te verminderen, waarmee het veld beweegt naar geformaliseerde en machine-verifieerbare redenering.

De code voor deze formalisering wordt beschikbaar gesteld aan de gemeenschap om verder onderzoek en engineering-toepassingen in geverifieerde optimalisatie te ondersteunen.