Resumen Técnico: ProofWala

Planteamiento del Problema

La demostración automática de teoremas utilizando métodos neuronales requiere una infraestructura robusta para interactuar con los Probadores de Teoremas Interactivos (ITP, por sus siglas en inglés), extraer datos estructurados de las demostraciones y ejecutar la búsqueda de pruebas a escala. Las herramientas existentes suelen estar fragmentadas, son específicas para cada asistente y están orientadas hacia la ejecución interactiva a nivel de archivo mediante interfaces REPL (Read-Eval-Print Loop). Esta arquitectura presenta limitaciones significativas:

• Escalabilidad: Dificulta el análisis a escala de repositorios y la experimentación paralela.
• Extracción de Datos: Proporciona un acceso limitado a los metadatos a nivel de declaración (por ejemplo, definiciones inductivas, constantes, espacios de nombres) y hace que la construcción de grafos de dependencia de todo el repositorio sea difícil o inviable.
• Brechas entre Asistentes: La falta de herramientas unificadas dificulta la explotación de posibles ganancias translingüísticas y transdominio derivadas del entrenamiento con corpus formales multilingües (por ejemplo, Lean y Rocq).

Metodología

Los autores presentan ProofWala, un marco de ingeniería de pruebas multilingüe diseñado para unificar la interacción, la extracción de datos, el entrenamiento y la búsqueda en diferentes ITP. El marco se construye alrededor de tres componentes principales:

1. El Módulo de Interfaz (itp-interface)

Esta es una biblioteca reutilizable para la interacción programática con los ITP, que proporciona una abstracción unificada para Lean 4 y Rocq (múltiples versiones).

• Backend de Lean 4: En lugar de depender de una arquitectura basada en REPL, los autores implementaron metaprogramas que se ejecutan directamente dentro del elaborador de Lean. Esto permite:
  • Rastreo de tácticas semánticamente fiel a nivel de trazado.
  • Extracción de metadatos a nivel de declaración y construcción de grafos de dependencia de todo el repositorio.
  • Mejor manejo de constructos de tácticas anidadas (por ejemplo, bloques have).
  • Clonación de Entorno: La capacidad de clonar entornos de prueba para la ejecución paralela, lo cual es difícil con los flujos de trabajo estándar de REPL.
  • Robustez de Versión: Una capa de compatibilidad delgada asegura la compatibilidad hacia adelante a través de las versiones de Lean 4 a partir de la 4.15.0.
• Backend de Rocq: Construido sobre coq_serapy, extendiéndolo para soportar la extracción sistemática de estados de prueba y trazas de tácticas, mapeándolos al mismo formato unificado utilizado para Lean.
• Modelo de Estado Unificado: Ambos asistentes se mapean a un sistema de transición de estados estandarizado donde un estado de prueba es un conjunto de obligaciones (metas e hipótesis), y las tácticas transicionan estos estados.

2. Módulo de Datos y Modelo

• Extracción de Datos: El marco extrae pares de estado de prueba–táctica de los principales repositorios (CompCert, MathComp, GeoCoq, Mathlib, CategoryTheory) mediante la ejecución de scripts de tácticas dentro del núcleo del asistente.
• Formato Unificado: Los datos extraídos se almacenan en un formato JSON unificado que abstrae los detalles específicos del asistente mientras preserva la información semántica. El formato de prompt para el entrenamiento es idéntico en Lean y Rocq, omitiendo tokens específicos del asistente para facilitar el entrenamiento transasistente.
• Entrenamiento: Los autores ajustaron un modelo CodeT5-Base (220 millones de parámetros) en tres configuraciones:
  1. ProofWala-Rocq: Entrenado en repositorios de Rocq.
  2. ProofWala-Lean: Entrenado en repositorios de Lean.
  3. ProofWala-Multilingual: Entrenado conjuntamente en ambos asistentes.

3. Módulo de Búsqueda de Pruebas en Paralelo

• Pool de Entornos: Una innovación clave es el pool de entornos, que mantiene múltiples entornos de prueba clonados inicializados en estados de frontera idénticos.
• Ejecución Paralela: Las tácticas candidatas se ejecutan concurrentemente a través de estas instancias clonadas. Este pool se integra con Ray para la ejecución distribuida, permitiendo la búsqueda de pruebas escalable y la anotación a gran escala.
• Algoritmos de Búsqueda: El módulo soporta búsqueda de mejor primera opción (best-first) y de haz (beam search) paralelizada. Mantiene un árbol de prueba anotado que registra únicamente las transiciones de estado válidas y compilables, permitiendo un análisis detallado de la dinámica de búsqueda.

Contribuciones Clave

1. Marco Estandarizado y Biblioteca de Ingeniería: ProofWala proporciona un marco unificado para extraer y organizar datos a nivel de táctica y apoyar el desarrollo de herramientas. Introduce una tubería de instrumentación mediante metaprogramación para Lean que soporta el recorrido de repositorios consciente de las dependencias y la clonación de entornos, capacidades que anteriormente eran difíciles de lograr vía REPL.
2. Soporte para la Completitud de Pruebas en Paralelo: El marco es el primer sistema de código abierto que proporciona búsqueda de pruebas en paralelo al soportar explícitamente entornos de prueba clonados y la evaluación concurrente de tácticas dentro de una interfaz unificada multi-ITP.
3. Datasets y Modelos Multilingües: Los autores lanzan un dataset multilingüe (~450K puntos de datos, 270 millones de tokens) y modelos entrenados (Lean, Rocq y Multilingüe) que facilitan la búsqueda de pruebas de extremo a extremo.

Resultados

Los autores evaluaron los modelos en divisiones de prueba de CompCert, MathComp, GeoCoq, CategoryTheory y Lean/Mathlib, así como en el benchmark MiniF2F.

• Transferencia Translingüística: El modelo ProofWala-Multilingual generalmente iguala o mejora a los baselines monolingües.
  • Mejoras Estadísticamente Significativas: Observadas en el benchmark más grande (Lean/Mathlib) y en el escenario de adaptación de dominio de CategoryTheory (donde el modelo multilingüe fue ajustado con datos de CategoryTheory).
  • Tendencias: Otros conjuntos de datos mostraron tendencias consistentes pero no estadísticamente significativas a favor del entrenamiento multilingüe.
• Adaptación de Dominio: En el dominio de CategoryTheory, el modelo multilingüe logró puntuaciones pass-at-k sustancialmente más altas tras el ajuste fino en comparación con el baseline de solo Rocq, lo que sugiere que el preentrenamiento con datos de lenguajes mixtos ayuda a la adaptación incluso cuando el dominio objetivo está representado en un solo asistente.
• Dinámica de Búsqueda: El análisis de los árboles de prueba reveló que los modelos multilingües a menudo producen árboles más grandes con factores de ramificación más altos, lo que indica que proponen un mayor número de tácticas válidas por estado.
• Escalabilidad: La ejecución paralela mediante pools de entornos mejoró significamente el rendimiento (throughput). Aumentar los trabajadores de CPU de 8 a 20 mejoró el pass@5 en MiniF2F del 22.54% al 26.23%, reduciendo simultáneamente el tiempo promedio de demostración.

Significado y Reivindicaciones

El artículo afirma que ProofWala representa un cambio de las herramientas fragmentadas y específicas de cada asistente hacia una infraestructura unificada y escalable para la demostración de teoremas neuronal.

• Unificación Arquitectónica: Al unificar la ejecución, la recolección de datos, el análisis de dependencias y la búsqueda, el marco permite un análisis sistemático, reproducible y detallado de la búsqueda de pruebas neuronales a través de múltiples ITP.
• Evidencia de Transferencia: El trabajo proporciona evidencia empírica de que el entrenamiento multilingüe genera una transferencia translingüística y transdominio positiva en el razonamiento formal, particularmente en regímenes de altos datos y escenarios de adaptación de dominio.
• Fundamento de Investigación: Los autores posicionan a ProofWala no meramente como un sistema de búsqueda de pruebas, sino como un marco de investigación que transforma la búsqueda de pruebas de una evaluación de "caja negra" en una tubería analizable. Esto permite a los investigadores estudiar la transferencia estructural, los factores de ramificación, el tamaño de los árboles y la latencia de ejecución de formas que antes eran difíciles de obtener.

Los autores señalan que, si bien es probable que se necesiten modelos más grandes y una infraestructura adicional (por ejemplo, recuperación, verificadores) para alcanzar un rendimiento de vanguardia en los benchmarks, su contribución principal es el marco mismo, que aísla los efectos del entrenamiento multilingüe y las estrategias de búsqueda en paralelo. Consideran la extensión a asistentes orientados a documentos (como Isabelle) como un desafío de ingeniería más que una limitación conceptual, dejándolo para trabajos futuros.