Resumo Técnico: LeanSearch v2

Definição do Problema: Recuperação Global de Premissas

O artigo identifica uma lacuna crítica na prova automática de teoremas dentro do ecossistema Lean 4. Embora as ferramentas existentes se destaquem na busca semântica (encontrar declarações individuais que correspondam a uma consulta) ou na seleção de premissas (prever lemas úteis para um único passo de tática), elas falham na recuperação global de premissas.

A recuperação global de premissas é definida como a tarefa de identificar o conjunto completo e logicamente coerente de lemas da biblioteca necessários para provar um teorema inteiro. Isso é distinto de encontrar um único documento relevante porque:

1. Não localidade: Os lemas necessários frequentemente residem em módulos distantes da biblioteca (Mathlib) e não compartilham nenhuma sobreposição lexical com a declaração do problema.
2. Dependência Estratégica: A conexão entre o problema e os lemas não é semântica, mas estrutural, dependendo da "arquitetura lógica" de uma estratégia de prova (por exemplo, remodelar um objetivo para corresponder à interface de um teorema).
3. Completude: A ausência de um único lema essencial de um conjunto de três ou quatro torna a prova incompleta, um modo de falha não capturado pelas métricas padrão de relevância de documentos.

Os autores argumentam que, sem uma recuperação global de premissas eficaz, os provadores de IA desperdiçam computação reprovando lemas locais existentes e lutam para gerar provas eficientes e idiomáticas.

Metodologia: LeanSearch v2

O LeanSearch v2 é um sistema de recuperação em dois modos projetado para enfrentar esse desafio.

1. Modo Padrão (O Substrato de Recuperação)

O modo padrão serve como um mecanismo de busca de alto desempenho para declarações individuais do Mathlib e atua como a base para o modo de raciocínio.

• Construção do Corpus: O sistema utiliza o Jixia, uma ferramenta de análise estática, para extrair todas as declarações do Mathlib. Ele constrói um grafo de dependências e realiza a informalização hierárquica de baixo para cima. Esse processo gera descrições em linguagem natural para cada declaração, incorporando as descrições já informalizadas de suas dependências, garantindo que as descrições estejam fundamentadas em conceitos matemáticos e não em identificadores opacos.
• Pipeline: Emprega um pipeline de duas etapas embedding–reranker usando modelos prontos (Qwen3-Embedding-8B e Qwen3-Reranker-8B) sem ajuste fino específico de domínio.
  • Embedding: Consultas e itens do corpus são codificados usando um modelo de passagem estruturado que inclui o tipo de declaração, assinatura de tipo e descrição informalizada.
  • Reranking: Um reranker consciente de tipo pontua pares consulta-candidato, lidando especificamente com definições e instâncias para superar as dificuldades de recuperação observadas em sistemas anteriores.

2. Modo de Raciocínio (Recuperação Global de Premissas)

O modo de raciocínio baseia-se no Modo Padrão para recuperar conjuntos de premissas através de um loop iterativo esboço-recupera-reflete.

• Geração de Esboço: Dada uma declaração de teorema, um gerador (Claude Sonnet 4.5) propõe um esboço de prova passo a passo, decompondo o teorema em subconsultas. Ele não escreve código, mas define os movimentos matemáticos e as intenções de recuperação.
• Recuperação e Filtragem: Cada subconsulta é enviada ao Modo Padrão. Um modelo de filtro (Kimi K2 Instruct) avalia os principais candidatos, permitindo explicitamente conjuntos vazios se nenhum lema recuperado for genuinamente útil para um passo específico.
• Julgamento de Viabilidade e Reflexão: Um modelo juiz inspeciona os resultados filtrados.
  • Se o conjunto de lemas apoiar a estratégia de prova, o loop termina.
  • Se o conjunto for insuficiente (por exemplo, faltando uma premissa ou sugerindo uma rota inválida), o juiz fornece feedback estruturado a um revisor de esboço, que modifica o esboço da prova e reentra no loop.
• Agregação: As saídas finais são agregadas usando uma regra de desconto de rank entre as subconsultas para formar uma lista unificada de lemas de suporte.

Contribuições Principais

1. Formulação da Tarefa: O artigo define formalmente a recuperação global de premissas como um desafio distinto que exige a recuperação de conjuntos de premissas logicamente coerentes em vez de documentos únicos.
2. Benchmarks: Dois benchmarks curados por especialistas são introduzidos:
   • MathlibQR: 200 declarações e 946 consultas para avaliar a busca de consulta única (Modo Padrão).
   • MathlibMPR: 69 teoremas de pull requests mesclados com grupos de premissas anotados por especialistas (1–8 por teorema) para avaliar a recuperação global de premissas (Modo de Raciocínio).
3. Desempenho do Sistema: O LeanSearch v2 alcança resultados state-of-the-art sem ajuste fino específico de domínio.
   • Modo Padrão: Alcança um nDCG@10 de 0,62 no MathlibQR, superando o próximo melhor sistema (0,53).
   • Modo de Raciocínio: No MathlibMPR, recupera 46,1% dos grupos de premissas verdadeiros entre os 10 principais candidatos, superando significativamente as linhas de base de recuperação de raciocínio (38,0%) e sistemas de seleção de premissas (9,3%).
4. Validação a Montante: Em um experimento controlado com um loop de provador fixo, substituir outros recuperadores pelo modo de raciocínio do LeanSearch v2 aumentou as taxas de sucesso de prova para 20% (vs. 16% para o próximo melhor e 4% sem recuperação), demonstrando que a qualidade da recuperação se propaga diretamente para a geração de provas.

Significado e Alegações

O artigo posiciona este trabalho como o primeiro a aplicar técnicas de recuperação por raciocínio especificamente ao problema de recuperação de premissas no Lean. Os autores afirmam que, embora sistemas de agentes fortes possam às vezes compensar uma recuperação fraca através de reformulação repetida de consultas ou prova local, a lacuna entre uma prova apenas compilável e uma eficiente e idiomática depende fundamentalmente da identificação e reutilização de resultados existentes da biblioteca.

O significado reside em estabelecer a recuperação como um eixo distinto de progresso para a matemática formal. Ao desacoplar o substrato de recuperação do loop de geração de provas, o sistema permite a melhoria independente de estratégias de recuperação. Os autores observam que, embora a metodologia seja agnóstica à linguagem em seu design, a avaliação atual é exclusiva para Lean 4/Mathlib, e o comportamento de tais sistemas dentro de arquiteturas de agentes altamente capazes em tarefas complexas, no nível de repositório, permanece uma área aberta para exploração futura.

O artigo conclui que a combinação de um corpus com informalização hierárquica, um pipeline de recuperação consciente de tipo e um loop iterativo esboço-recupera-reflete fornece uma solução robusta para o desafio de encontrar os lemas dispersos e não locais necessários para provas formais modernas.