Formalization of Line Search Methods by Lean

Resumo Técnico: Formalização de Métodos de Busca de Linha por Lean

Problema
O artigo aborda a necessidade de verificação rigorosa de máquina da teoria de otimização não linear, focando especificamente em métodos de busca de linha. Embora as formalizações existentes no provador de teoremas Lean tenham abrangido algoritmos de primeira ordem para otimização convexa, métodos estruturados em blocos e condições de otimalidade (ex: condições KKT), o arcabouço teórico específico que rege a busca de linha — crucial para a convergência global de métodos iterativos baseados em gradiente — carecia de formalização verificada. Os autores visam traduzir definições padrão de livros didáticos, estratégias de seleção de tamanho de passo adaptativo e argumentos de convergência em código Lean verificável por máquina para eliminar ambiguidades e garantir a correção.

Metodologia
Os autores utilizam o Lean 4, aproveitando a biblioteca Mathlib, para formalizar os fundamentos matemáticos e a lógica algorítmica da busca de linha. A metodologia envolve:

1. Modelagem Matemática: O espaço vetorial $\mathbb{R}^n$ é modelado como funções de Fin n para $\mathbb{R}$. Os autores definem um produto interno euclidiano e uma norma customizada (vnorm) em vez de depender da norma sup-ambiente fornecida pela Mathlib, provando propriedades padrão como a desigualdade de Cauchy–Schwarz e a relação entre a norma ao quadrado e o produto interno como teoremas, em vez de axiomas.
2. Formalização de Pressupostos: Pressupostos fundamentais, como a continuidade de Lipschitz do gradiente e a propriedade de aproximação de primeira ordem (comportamento de expansão de Taylor), são definidos como predicados explícitos (GradLipschitz, FirstOrderApprox) em vez de axiomas, garantindo que sejam carregados como hipóteses nos teoremas.
3. Formalização Algorítmica: O artigo formaliza a lógica da busca de linha por retrocesso (backtracking line search). Reconhecendo que a comparação de números reais é indecidível na lógica do Lean, os autores abstraem o teste de Armijo em um oráculo Booleano (test : N → Bool) para definições executáveis (backtrackRun), enquanto provam a existência matemática de um tamanho de passo válido usando Nat.find para identificar o expoente mínimo que satisfaz as condições.
4. Provas de Convergência: O núcleo da metodologia envolve a prova do teorema de Zoutendik. Isso é alcançado derivando um limite inferior na diminuição da função por iteração (combinando as condições de Armijo, curvatura de Wolfe e Lipschitz) e somando esses limites para mostrar que a série das derivadas direcionais ao quadrado é finita.

Principais Contribuições
O artigo fornece uma formalização abrangente dos seguintes componentes:

• Definições Fundamentais: Definições formais para direções de descida, o produto interno euclidiano e a norma euclidiana customizada.
• Critérios de Busca de Linha: Definições rigorosas e provas para:
  • Condição de Armijo: Provar a existência de um tamanho de passo que satisfaz a diminuição suficiente e sua implicação de redução estrita do valor da função.
  • Condição de Goldstein: Formalizar os limites duplos nos valores da função.
  • Condições de Wolfe: Formalizar tanto a condição de Armijo (diminuição suficiente) quanto a de curvatura, e provar que Wolfe implica Armijo.
  • Condições Não Monótonas: Formalização da condição de Grippo (máximo deslizante) e da condição de Zhang-Hager (combinação convexa de valores anteriores), incluindo provas que mostram que elas se reduzem à Armijo padrão sob limites de parâmetros específicos.
• Implementação de Backtracking: Uma implementação verificada do algoritmo de busca de linha por retrocesso que garante a terminação e a positividade do tamanho de passo resultante.
• Teorema de Zoutendik: Uma prova verificada por máquina do teorema de Zoutendik, que estabelece que, para métodos baseados em gradiente que satisfazem as condições de Wolfe, a soma dos cossenos quadrados dos ângulos entre o gradiente e a direção de busca (ponderada pela norma do gradiente) é finita.
• Convergência Global: Uma prova formal de que, sob o limite de somabilidade de Zoutendik, a norma do gradiente das iteratas de descida mais íngreme converge para zero (especificamente, $\liminf_{k \to \infty} \|\nabla f(x_k)\| = 0$).

Resultos
A formalização verifica com sucesso que:

1. Direções de descida garantem a existência de tamanhos de passo que diminuem estritamente a função objetivo.
2. A busca de linha por retrocesso, quando guiada pela condição de Armijo, sempre termina com um tamanho de passo válido e positivo.
3. O teorema de Zoutendik é válido sob a suposição de gradientes contínuos de Lipschitz e condições de Wolfe, fornecendo um limite rigoroso sobre o comportamento de convergência.
4. A norma do gradiente da sequência gerada converge para zero, confirmando a convergência global do método.

Significância
Os autores posicionam este trabalho como um passo fundamental na verificação de máquina da otimização não linear. Ao fornecer definições e provas verificáveis por máquina para a teoria de busca de linha, o artigo:

• Complementa as formalizações existentes de métodos de otimização de primeira ordem e condições de otimalidade.
• Preenche a lacuna entre definições informais de livros didáticos e código executável e verificado.
• Estabelece uma base reutilizável para o desenvolvimento verificado de algoritmos mais avançados em programação não linear.
• Reduz a ambiguidade nos argumentos padrão de otimização, movendo o campo em direção ao raciocínio formalizado e verificável por máquina.

O código para esta formalização é disponibilizado à comunidade para apoiar pesquisas futuras e aplicações de engenharia em otimização verificada.