Resumen Técnico: VERITAS: Búsqueda de Pruebas Guiada por Verificadores para la Demostración Formal de Teoremas Zero-Shot

Planteamiento del Problema

Los actuales demostradores de teoremas formales basados en Modelos de Lenguaje de Gran Escala (LLM) suelen colapsar las señales ricas y estructuradas de los verificadores formales (como Lean 4) en un resultado binario de paso/fallo. Los verificadores proporcionan retroalimentación granular que incluye errores de sintaxis, desajustes de tipos, progreso parcial de objetivos y estado de completitud de la prueba. Sin embargo, los procesos estándar descartan estos artefactos intermedios, resumiéndolos en recompensas escalares o descartándolos por completo. Esto obliga al algoritmo de búsqueda a "reaprender" información que el verificador ya ha proporcionado explícitamente, una limitación que se vuelve particularmente costosa en pruebas que requieren cadenas de tácticas dependientes donde la corrección de cada paso depende del efecto del paso anterior sobre el objetivo.

Metodología: El Marco de Trabajo VERITAS

VERITAS es un marco de trabajo zero-shot diseñado para redirigir cada señal del verificador hacia el proceso de generación de la prueba. Emplea una arquitectura de cuatro agentes coordinados por un estado de prueba compartido y un protocolo de búsqueda de dos fases.

1. Cuatro Agentes Especializados

Todos los agentes operan sobre un ProofState (Estado de Prueba) compartido que contiene el teorema, el objetivo actual, las hipótesis, el historial de tácticas y cuatro señales estructuradas de Lean:

• Estratega (Strategist): Mapea el estado de la prueba a una de seis estrategias de alto nivel (directa, inducción, contradicción, casos, reescritura, apply_lemma) y estima la profundidad, restringiendo la búsqueda a un subespacio relevante.
• Recuperador (Retriever): Expone premisas relevantes de Mathlib puntuando la superposición de palabras clave contra los tokens del objetivo, los nombres de los lemas y las firmas.
• Crítico (Critic): Un modelo ligero que califica estados de prueba parciales, sugiriendo tácticas próximas y recomendaciones de poda. Reemplaza los rollouts aleatorios en MCTS con una estimación de valor que integra la retroalimentación de cuatro vías de Lean.
• Táctico (Tactician): Genera $K$ candidatos de táctica condicionados por la estrategia, las premisas recuperadas, la guía del Crítico y, crucialmente, una lista de tácticas fallidas previamente con sus mensajes de error específicos de Lean inyectados como ejemplos negativos.

2. Protocolo de Dos Fases con Garantía de Monotonicidad

El marco utiliza un protocolo conservador de dos fases para asegurar que las ganancias sean atribuibles a la búsqueda impulsada por la retroalimentación:

• Fase 1 (Best-of-N): Un barrido estándar de Best-of-N (por ejemplo, $N=5$) genera tácticas en un solo lote. Si alguna tiene éxito, el teorema se resuelve inmediatamente.
• Fase 2 (MCTS Guiado por el Crítico): Se activa solo si la Fase 1 falla. El conjunto de fallos de la Fase 1 (tácticas y sus errores) se inyecta en el prompt de sistema del Táctico como ejemplos negativos. El Crítico guía un MCTS (Monte Carlo Tree Search) donde:
  • Selección: Utiliza una fórmula UCB extendida que incorpora el valor del Crítico y la alineación de la estrategia.
    এতে
  • Expansión: Los agentes se ejecutan secuencialmente; los candidatos se validan mediante un truco de Validación de Lean en Lote (Batched Lean Validation).
  • Simulación: Reemplaza los rollouts aleatorios con el valor del Crítico aumentado por señales estructuradas ($\sigma_A$ sintaxis, $\sigma_B$ tipo, $\sigma_C$ progreso, $\sigma_D$ completitud).
  • Retropropagación: Transporta las señales estructuradas hacia arriba en lugar de colapsarlas a un win/loss binario, preservando el crédito por el progreso parcial.

Validación de Lean en Lote: En lugar de invocar Lean $K$ veces por cada expansión, los candidatos se compilan en un único archivo .lean como teoremas privados y se validan en una sola llamada. Esto reduce el costo de verificación de $O(K)$ a $O(1)$, produciendo una aceleración de aproximadamente $\sim10\times$.

Monotonicidad: El protocolo garantiza que el conjunto final de teoremas resueltos sea un superconjunto de aquellos resueltos únicamente por la Fase 1 ($S \supseteq S_1$). Esto aisla la contribución de la Fase 2, asegurando que cualquier solución adicional se deba estrictamente al MCTS guiado por el verificador.

Contribuciones Clave

1. Marco de Cuatro Agentes Zero-Shot: Un sistema que redirige la retroalimentación estructurada de Lean (sintaxis, tipo, progreso, completitud) hacia cada decisión de generación sin necesidad de ajuste fino (fine-tuning) de traza.
2. Protocolo de Dos Fases: Un diseño de Best-of-N $\to$ Critic-MCTS con una garantía interna de monotonicidad que permite una atribución limpia de las contribuciones de la búsqueda.
3. Optimización de Eficiencia: Un truco de validación de Lean en lote que reduce el overhead de verificación aproximadamente $10\times$.
4. VERITAS-CombiBench: Un nuevo benchmark de 55 teoremas de combinatoria de autoría verificada en Lean 4, lanzado para exponer las limitaciones del muestreo no guiado.
5. Análisis de Atribución: Evidencia empírica que muestra que 11 teoremas de miniF2F fueron unicamente resolubles mediante la fase de MCTS, algo que el muestreo plano no pudo alcanzar.

Resultados Experimentales

Los experimentos se realizaron en miniF2F (244 teoremas) y VERITAS-CombiBench (55 teoremas).

• Rendimiento en miniF2F: VERITAS logró una tasa de resolución del 40.6% (99/244), superando la línea base independiente de Best-of-5 (36.9%) y un Portfolio diseñado a mano (26.2%).
  • La Fase 2 contribuyó con 11 soluciones únicas que el muestreo plano no pudo lograr, principalmente en problemas que requieren 2–4 tácticas dependientes.
  • En problemas "difíciles" sin sorry, VERITAS alcanzó un 28.9% frente al 25.9% de Best-of-5.
• Rendimiento en VERITAS-CombiBench: Este benchmark resaltó el fallo del muestreo no guiado. El Best-of-5 logró solo un 1.8%, cayendo por debajo del Portfolio (3.6%), debido a que los LLM alucinaron nombres incorrectos de lemas de Mathlib. VERITAS alcanzó un 7.3% mediante la corrección iterativa de estos nombres utilizando la retroalimentación de error de Lean.
• Eficiencia: VERITAS domina la frontera de Pareto para métodos de solo inferencia, logrando una tasa de resolución del 40.6% con aproximadamente 27 llamadas a Lean por teorema a un costo de API de ~$150 por barrido.
• Modos de Fallo: El análisis mostró que el 32% de los fallos fueron de nivel de sintaxis (alucinación de nombres), el 17% eran correctos en tipo pero erróneos, y el 10% fueron "casi aciertos" (progreso parcial del objetivo) donde el Crítico podía proporcionar una guía de alto valor.

Significado y Reivindicaciones

El artículo postula un principio de diseño general: cuando un verificador determinista emite señales intermedias estructuradas, plegarlas de vuelta en la generación amplifica el LLM sustancialmente más que el simple aumento del muestreo.

VERITAS demuestra que:

1. Señales del Verificador como Estado: Las señales deterministas del verificador pueden servir como estado de inferencia, no solo como comprobaciones finales.
2. Sinergia de Componentes: Acoplar estrechamente el verificador con la generación es más efectivo que escalar el LLM o el componente de búsqueda de forma aislada.
3. Corrección Iterativa: Para dominios que requieren recuperación precisa de lemas (como la combinatoria), la corrección iterativa a partir de los errores del verificador es superior al muestreo plano, que tiende a alucinar nombres léxicamente incorrectos.

Los autores concluyen que, si bien VERITAS no es una cura para la creatividad de nivel IMO o la latencia interactiva, su principal contribución es el enrutamiento (routing): recolectar eficientemente las pruebas fáciles en la Fase 1 y gastar el presupuesto computacional en la Fase 2 solo donde los fallos del verificador pueden guiar la siguiente táctica. Se identifica como trabajo futuro la mejora de la recuperación, la creación de críticos más económicos y la destilación de las trazas de la Fase 2 para escalar este principio a la cola difícil restante de los problemas.