Formalization of Line Search Methods by Lean

Resumen Técnico: Formalización de Métodos de Búsqueda de Línea mediante Lean

Planteamiento del Problema
El artículo aborda la necesidad de una verificación mecánica rigurosa de la teoría de optimización no lineal, centrándose específicamente en los métodos de búsqueda de línea. Si bien las formalizaciones existentes en el demostrador de teoremas Lean han cubierto algoritmos de primer orden para optimización convexa, métodos de estructura de bloques y condiciones de optimalidad (por ejemplo, las condiciones KKT), el marco teórico específico que rige la búsqueda de línea —crucial para la convergencia global de los métodos iterativos basados en el gradiente— aún no había sido formalizado mecánicamente. Los autores pretenden traducir las definiciones estándar de los libros de texto, las estrategias de selección de tamaño de paso adaptativo y los argumentos de convergencia en código Lean verificable por máquina para eliminar la ambigüedad y asegurar la corrección.

Metodología
Los autores utilizan Lean 4, aprovechando la biblioteca Mathlib, para formalizar los fundamentos matemáticos y la lógica algorítmica de la búsqueda de línea. La metodología consiste en:

1. Modelado Matemático: El espacio vectorial $\mathbb{R}^n$ se modela como funciones de Fin n a $\mathbb{R}$. Los autores definen un producto interno euclídeo y una norma (vnorm) personalizados en lugar de depender de la norma sup de ambiente proporcionada por Mathlib, demostrando propiedades estándar como la desigualdad de Cauchy–Schwarz y la relación entre la norma al cuadrado y el producto interno como teoremas en lugar de axiomas.
2. Formalización de Supuestos: Supuestos clave, tales como la continuidad de Lipschitz del gradiente y la propiedad de aproximación de primer orden (comportamiento de la expansión de Taylor), se definen como predicados explícitos (GradLipschitz, FirstOrderApprox) en lugar de axiomas, asegurando que se transporten como hipótesis en los teoremas.
3. Formalización Algorítmica: El artículo formaliza la lógica de la búsqueda de línea de retroceso (backtracking line search). Reconociendo que la comparación de números reales es indecidible en la lógica de Lean, los autores abstraen la prueba de Armijo en un oráculo booleano (test : N → Bool) para definiciones ejecutables (backtrackRun), mientras prueban la existencia matemática de un tamaño de paso válido utilizando Nat.find para identificar el exponente mínimo que satisface las condiciones.
4. Pruebas de Convergencia: El núcleo de la metodología consiste en demostrar el teorema de Zoutendijk. Esto se logra derivando una cota inferior en la disminución de la función por iteración (combinando las condiciones de Armijo, de curvatura de Wolfe y de Lipschitz) y sumando estas cotas para mostrar que la serie de las derivadas direccionales al cuadrado es finita.

Contribuciones Clave
El artículo proporciona una formalización exhaustiva de los siguientes componentes:

• Definiciones Fundamentales: Definiciones formales para direcciones de descenso, el producto interno euclídeo y la norma euclídea personalizada.
• Criterios de Búsqueda de Línea: Definiciones y pruebas rigurosas para:
  • Condición de Armijo: Demostrar la existencia de un tamaño de paso que satisfaga la disminución suficiente y su implicación de una reducción estricta del valor de la función.
  • Condición de Goldstein: Formalizar los límites duales de los valores de la función.
  • Condiciones de Wolfe: Formalizar tanto la condición de Armijo (disminución suficiente) como la de curvatura, y demostrar que Wolfe implica Armijo.
  • Condiciones No Monótonas: Formalización de la condición de Grippo (máximo deslizante) y la condición de Zhang-Hager (combinación convexa de valores previos), incluyendo pruebas que muestran cómo se reducen a Armijo estándar bajo límites de parámetros específicos.
• Implementación de Retroceso (Backtracking): Una implementación verificada del algoritmo de búsqueda de línea de retroceso que garantiza la terminación y la positividad del tamaño de paso resultante.
• Teorema de Zoutendijk: Una prueba verificada por máquina del teorema de Zoutendijk, que establece que para métodos basados en el gradiente que satisfacen las condiciones de Wolfe, la suma de los cosenos al cuadrado de los ángulos entre el gradiente y la dirección de búsqueda (ponderados por la norma del gradiente) es finita.
• Convergencia Global: Una prueba formal de que, bajo el límite de sumabilidad de Zoutendijk, la norma del gradiente de las iteraciones de descenso más pronunciado converge a cero (específicamente, $\liminf_{k \to \infty} \|\nabla f(x_k)\| = 0$).

Resultados
La formalización verifica con éxito que:

1. Las direcciones de descenso garantizan la existencia de tamaños de paso que disminuyen estrictamente la función objetivo.
2. La búsqueda de línea de retroceso, cuando es guiada por la condición de Armijo, siempre termina con un tamaño de paso válido y positivo.
3. El teorema de Zoutendjúk se cumple bajo el supuesto de gradientes continuos de Lipschitz y condiciones de Wolfe, proporcionando un límite riguroso sobre el comportamiento de la convergencia.
4. La norma del gradiente de la secuencia generada converge a cero, confirmando la convergencia global del método.

Significancia
Los autores posicionan este trabajo como un paso fundacional en la verificación mecánica de la optimización no lineal. Al proporcionar definiciones y pruebas verificables por máquina para la teoría de la búsqueda de línea, el artículo:

• Complementa las formalizaciones existentes de los métodos de optimización de primer orden y las condiciones de optimalidad.
• Cierra la brecha entre las definiciones informales de los libros de texto y el código ejecutable y verificado.
• Establece una base reutilizable para el desarrollo verificado de algoritmos más avanzados en programación no lineal.
• Reduce la ambigüedad en los argumentos estándar de optimización, moviendo el campo hacia el razonamiento formalizado y verificable por máquina.

El código para esta formalización se pone a disposición de la comunidad para apoyar la investigación adicional y las aplicaciones de ingeniería.