Resumen Técnico: Mantener el Estado de la Prueba Activo

Declaración del Problema

Los sistemas de demostración automática de teoremas que utilizan Modelos de Lenguaje Grande (LLM) y el pipeline Draft–Sketch–Prove (DSP) dependen cada vez más de la búsqueda basada en portafolios. Este enfoque implica fijar un conjunto de tácticas candidatas e intentarlas en paralelo en cada "agujero de prueba" (representado por tokens sorry) dentro de una prueba parcialmente especificada.

En el ecosistema actual de Lean 4 con Mathlib, esta búsqueda paralela se ve severamente limitada por la sobrecarga de inicio de rama. Cada rama de búsqueda reconstruye actualmente el estado de la prueba desde cero, incurriendo en dos costos masivos:

1. Carga de Importaciones: Deserializar bibliotecas .olean precompiladas (Mathlib), lo que toma aproximadamente 60 segundos por rama.
2. Elaboración del Cuerpo del Teorema: Volver a verificar los tipos del encabezado del teorema y todos los pasos intermedios hasta el objetivo final. Esto escala con la complejidad de la prueba, oscilando entre 18 y 735 segundos por rama.

Juntos, estos componentes consumen >99% del tiempo de pared por rama. Para un portafolio estándar de 7 tácticas aplicadas a 4 agujeros (28 ramas), la sobrecarga puede superar los 17 minutos en una sola máquina, haciendo inviable la búsqueda basada en portafolios a la escala de los pipelines DSP (que pueden proponer más de 100 candidatos de borrador por teorema). La causa raíz es una discrepancia entre la gestión interna del estado de Lean (que almacena en caché estados elaborados para diagnósticos del IDE) y el acceso externo (que obliga a una reconstrucción completa para cada nueva rama).

Metodología

Los autores introducen la Captura de Instantánea del Estado de la Prueba, un mecanismo que captura el estado de la prueba elaborado una sola vez y lo reutiliza a través de múltiples ramas paralelas, en lugar de reconstruirlo para cada intento.

Arquitectura del Sistema

La solución implica una extensión mínima al Servidor de Lenguaje de Lean 4 (LSP) y una capa de orquestación en Python:

1. Extensiones del Servidor Lean: Se añaden tres nuevos métodos JSON-RPC a Lean.Server.FileWorker:

   • dspSnapshotPing: Un saludo para verificar el soporte de instantáneas.
   • dspSnapshotCapture: Dado un URI de archivo y una posición sorry, esto bloquea hasta que la elaboración alcanza ese punto, registra una referencia de instantánea y devuelve un snapshotId estable.
   • dspSnapshotBranch: Acepta un snapshotId y una matriz de configuraciones de tácticas. Genera tareas paralelas (IO.asTask) para cada táctica, sustituyendo la táctica por sorry y ejecutándola contra el estado de objetivo capturado.

2. Mecanismo de Forking Eficiente:

   • Entorno Compartido: El Environment (que contiene todas las constantes de Mathlib, instancias de clases de tipos y conjuntos simp, aprox. 2–4 GB) es inmutable. Se comparte entre todas las ramas por referencia y nunca se copia.
   • Contexto Copiado: Solo el MetavarContext (obligaciones de prueba abiertas, típicamente unos pocos kilobytes) se copia por rama.
   • Resultado: Forkear una rama cuesta solo el tiempo de copiar unos pocos kilobytes de memoria, reduciendo la sobrecarga de memoria por rama de O(GB) a O(KB) y eliminando la RAM como cuello de botella para el paralelismo.

3. Integración con DSP:

   • El orquestador en Python detecta las posiciones sorry en un boceto generado por un LLM.
   • Captura una instantánea para cada agujero.
   • Despacha todo el portafolio de tácticas (por ejemplo, aesop, norm_num, omega, ring, linarith, decide, simp) en una única llamada RPC por lotes.
   • El servidor distribuye estas ramas en paralelo utilizando el planificador de robo de trabajo de Lean.

Posicionamiento

Este trabajo define la optimización de Nivel 2 en la jerarquía de aceleración de la búsqueda de pruebas:

• Nivel 0 (DSP Estándar): Reconstrucción completa por rama.
• Nivel 1 (p. ej., Kimina): Almacena en caché el Environment post-importación entre teoremas, pero vuelve a elaborar el cuerpo del teorema por rama.
• Nivel 2 (Snapshot-DSP): Almacena en caché el estado post-elaboración (incluido el cuerpo del teorema) y lo bifurca para las ramas dentro del mismo teorema.
• Nota: Esto es ortogonal a los mecanismos de retroceso intra-rama como SavedState utilizados por Aesop.

Contribuciones Clave

1. Implementación del Sistema: Un sistema de captura de instantánea del estado de la prueba que comprende extensiones LSP de Lean 4 y una capa de orquestación en Python que permite el forking ligero de estados de prueba para la ejecución paralela de tácticas.
2. Evaluación: Mediciones exhaustivas de aceleración en 48 problemas miniF2F-v2, demostrando que >99% del tiempo de pared por rama es una sobrecarga eliminada por este enfoque.
3. Lanzamiento de Código Abierto: El binario de Lean parcheado, el pipeline Snapshot-DSP y la suite de evaluación se lanzan como código abierto.

Resultados

Los experimentos se realizaron en 48 problemas miniF2F-v2 (45 benchmarks creados a mano y 3 ejecuciones completas de extremo a extremo) en un MacBook Pro (8 GB de RAM).

• Aceleración del Tiempo de Pared: El enfoque logra una aceleración de 5.6–50× sobre la solución de respaldo estándar (construcción lake por rama).
  • Promedio: 14× de aceleración.
  • Mediana: 9.7× de aceleración (en 45 benchmarks creados a mano).
• Comportamiento de Escalado: La aceleración escala monótonamente con el número de ramas de prueba (agujeros × tácticas).
  • 1 agujero (7 ramas): ~7.9× de aceleración.
  • 5 agujeros (35 ramas): ~29.8× de aceleración.
• Descomposición de Costos:
  • Ejecución de Tácticas: Representa solo unos pocos milisegundos a 500 ms por rama (percentil 95: 289 ms).
  • Sobrecarga: El restante >99% del tiempo de ejecución en la solución de respaldo es sobrecarga de elaboración, que la captura de instantáneas elimina por completo.
  • Costo Nativo: El enfoque nativo de instantáneas añade solo 4–13 segundos de sobrecarga combinada de LSP y ejecución de tácticas sobre el costo de captura único.

Significado y Afirmaciones

El artículo afirma que la captura de instantánea del estado de la prueba es una arquitectura de aceleración pura que no altera la precisión de la prueba ni las estrategias de búsqueda, sino que elimina la barrera de escalabilidad que impide el uso de grandes portafolios de tácticas en máquinas individuales.

• Factibilidad: Transforma escenarios de búsqueda inviables (p. ej., 2.800 ramas que tardan 29 horas) en manejables (3.5 horas) en hardware estándar.
• Cambio Arquitectónico: El trabajo sirve como una "prueba de existencia" de que la frontera entre la gestión interna del estado de Lean y los sistemas de IA externos puede redibujarse. Al exponer la captura y bifurcación de instantáneas como una operación de servidor de primera clase, demuestra que la reutilización de estado a nivel de elaboración es alcanzable con un parche mínimo en las cadenas de herramientas de producción.
• Complementariedad: El mecanismo es ortogonal a la caché a nivel de importación (Nivel 1). Mientras que el Nivel 1 evita reinicios del servidor entre teoremas, el Nivel 2 elimina la re-elaboración del cuerpo del teorema entre ramas. Una futura variante de servidor persistente que combine ambas podría generar mayores ganancias, pero la implementación actual se centra en el cuello de botella del despacho de ramas.

Los autores enfatizan que esto es una intervención dirigida para exponer la cadena de instantáneas de elaboración para su reutilización externa, motivada por la observación de que el servidor de Lean ya calcula y almacena en caché este estado para diagnósticos del IDE, pero falla en exponerlo a los orquestadores externos de búsqueda de pruebas.