Resumen Técnico: LeanSearch v2

Definición del Problema: Recuperación Global de Premisas

El artículo identifica una brecha crítica en la demostración automática de teoremas dentro del ecosistema Lean 4. Si bien las herramientas existentes destacan en la búsqueda semántica (encontrar declaraciones individuales que coinciden con una consulta) o en la selección de premisas (predecir lemas útiles para un único paso de táctica), fallan en la recuperación global de premisas.

La recuperación global de premisas se define como la tarea de identificar el conjunto completo y lógicamente coherente de lemas de la biblioteca necesarios para demostrar un teorema entero. Esto es distinto de encontrar un único documento relevante porque:

1. No localidad: Los lemas necesarios a menudo residen en módulos distantes de la biblioteca (Mathlib) y no comparten ninguna superposición léxica con la declaración del problema.
2. Dependencia Estratégica: La conexión entre el problema y los lemas no es semántica sino estructural, dependiendo de la "arquitectura lógica" de una estrategia de demostración (por ejemplo, remodelar un objetivo para que coincida con la interfaz de un teorema).
3. Completitud: Omitir un único lema esencial de un conjunto de tres o cuatro hace que la demostración sea incompleta, un modo de fallo que no es capturado por las métricas estándar de relevancia de documentos.

Los autores argumentan que, sin una recuperación global de premisas efectiva, los demostradores de IA desperdician cómputo reprobando lemas locales existentes y luchan por generar demostraciones eficientes e idiomáticas.

Metodología: LeanSearch v2

LeanSearch v2 es un sistema de recuperación de dos modos diseñado para abordar este desafío.

1. Modo Estándar (El Sustrato de Recuperación)

El modo estándar sirve como un motor de búsqueda de alto rendimiento para declaraciones individuales de Mathlib y actúa como la base para el modo de razonamiento.

• Construcción del Corpus: El sistema utiliza Jixia, una herramienta de análisis estático, para extraer todas las declaraciones de Mathlib. Construye un grafo de dependencias y realiza una informalización jerárquica ascendente. Este proceso genera descripciones en lenguaje natural para cada declaración incorporando las descripciones ya informalizadas de sus dependencias, asegurando que las descripciones se basen en conceptos matemáticos en lugar de identificadores opacos.
• Pipeline: Emplea un pipeline de dos etapas de incrustación-reclasificador utilizando modelos listos para usar (Qwen3-Embedding-8B y Qwen3-Reranker-8B) sin ajuste fino específico del dominio.
  • Incrustación: Las consultas y los elementos del corpus se codifican utilizando una plantilla de pasaje estructurada que incluye el tipo de declaración, la firma del tipo y la descripción informalizada.
  • Reclasificación: Un reclasificador consciente del tipo puntúa los pares consulta-candidato, manejando específicamente definiciones e instancias para superar las dificultades de recuperación observadas en sistemas anteriores.

2. Modo de Razonamiento (Recuperación Global de Premisas)

El modo de razonamiento se basa en el Modo Estándar para recuperar conjuntos de premisas a través de un buque iterativo de boceto-recuperación-reflexión.

• Generación de Boceto: Dada una declaración de teorema, un generador (Claude Sonnet 4.5) propone un esquema de demostración paso a paso, descomponiendo el teorema en subconsultas. No escribe código, sino que define los movimientos matemáticos y las intenciones de recuperación.
• Recuperación y Filtrado: Cada subconsulta se envía al Modo Estándar. Un modelo filtro (Kimi K2 Instruct) examina los mejores candidatos, permitiendo explícitamente conjuntos vacíos si ningún lema recuperado es genuinamente útil para un paso específico.
• Juicio de Viabilidad y Reflexión: Un modelo juez inspecciona los resultados filtrados.
  • Si el conjunto de lemas apoya la estrategia de demostración, el bucle termina.
  • Si el conjunto es insuficiente (por ejemplo, falta una premisa o sugiere una ruta inválida), el juez proporciona retroalimentación estructurada a un revisor de bocetos, que modifica el esquema de demostración y vuelve a entrar en el bucle.
• Agregación: Las salidas finales se agregan utilizando una regla de descuento por rango a través de las subconsultas para formar una lista unificada de lemas de apoyo.

Contribuciones Clave

1. Formulación de la Tarea: El artículo define formalmente la recuperación global de premisas como un desafío distinto que requiere la recuperación de conjuntos de premisas lógicamente coherentes en lugar de documentos individuales.
2. Benchmarks: Se introducen dos benchmarks curados por expertos:
   • MathlibQR: 200 declaraciones y 946 consultas para evaluar la búsqueda de consulta única (Modo Estándar).
   • MathlibMPR: 69 teoremas de solicitudes de incorporación (pull requests) fusionadas con grupos de premisas anotados por expertos (1–8 por teorema) para evaluar la recuperación global de premisas (Modo de Razonamiento).
3. Rendimiento del Sistema: LeanSearch v2 logra resultados de vanguardia sin ajuste fino específico del dominio.
   • Modo Estándar: Logra un nDCG@10 de 0.62 en MathlibQR, superando al siguiente mejor sistema (0.53).
   • Modo de Razonamiento: En MathlibMPR, recupera el 46.1% de los grupos de premisas de verdad fundamental dentro de los 10 mejores candidatos, superando significativamente a las líneas base de recuperación de razonamiento (38.0%) y a los sistemas de selección de premisas (9.3%).
4. Validación Aguas Abajo: En un experimento controlado con un bucle de demostrador fijo, reemplazar otros recuperadores con el modo de razonamiento de LeanSearch v2 aumentó las tasas de éxito de demostración al 20% (frente al 16% del siguiente mejor y al 4% sin recuperación), demostrando que la calidad de la recuperación se propaga directamente a la generación de demostraciones.

Significado y Afirmaciones

El artículo posiciona este trabajo como el primero en aplicar técnicas de recuperación por razonamiento específicamente al problema de recuperación de premisas en Lean. Los autores afirman que, si bien sistemas de agentes fuertes a veces pueden compensar una recuperación débil mediante reformulación repetida de consultas o demostración local, la brecha entre una demostración meramente compilable y una eficiente e idiomática depende fundamentalmente de identificar y reutilizar resultados existentes de la biblioteca.

El significado radica en establecer la recuperación como un eje distinto de progreso para las matemáticas formales. Al desacoplar el sustrato de recuperación del bucle de generación de demostraciones, el sistema permite la mejora independiente de las estrategias de recuperación. Los autores señalan que, aunque la metodología es agnóstica al lenguaje en su diseño, la evaluación actual es exclusiva de Lean 4/Mathlib, y el comportamiento de tales sistemas dentro de arquitecturas de agentes altamente capaces en tareas complejas a nivel de repositorio sigue siendo un área abierta para futura exploración.

El artículo concluye que la combinación de un corpus con informalización jerárquica, un pipeline de recuperación consciente del tipo y un bucle iterativo de boceto-recuperación-reflexión proporciona una solución robusta al desafío de encontrar los lemas dispersos y no locales necesarios para las demostraciones formales modernas.