Resumen Técnico: Optimización Eficiente en Tiempo de Prueba para la Autoformalización de Pruebas Multi-Agente

1. Planteamiento del Problema

La autoformalización de pruebas completas busca traducir extensas demostraciones matemáticas en lenguaje natural en razonamientos formalmente validados dentro de asistentes de pruebas como Lean. A diferencia de la formalización a nivel de enunciado, que se centra en traducir un único teorema, la autoformalización de pruebas completas es un desafío de largo horizonte. Requina coordinar afirmaciones, contextos y dependencias a través de numerosos pasos de la prueba para construir un todo globalmente verificable.

Los enfoques actuales enfrentan dos limitaciones primarias:

1. Entrenamiento Costoso: Muchos métodos dependen de un ajuste fino supervisado a gran escala, lo cual es difícil debido a la escasez de datos de supervisión emparejados a nivel de prueba.
2. Optimización Ineficiente en Tiempo de Prueba: Los métodos de inferencia existentes a menudo aplican una reparación excesiva y no guiada o un refinamiento iterativo a través de todo el pipeline. En entornos de pruebas completas, la retroalimentación del verificador (por ejemplo, errores de Lean) llega solo después de una larga cadena de generación, rara vez revelando qué decisión ascendente causó el fallo. Esto hace que sea difícil dirigir el cómputo limitado en tiempo de prueba hacia mejoras dirigidas en lugar de reintentos no guiados.

2. Metodología: El Marco de Trabajo TOMAP

Los autores presentan TOMAP (Optimización en Tiempo de Prueba para la Autoformalización de Pruebas Multi-Agente), un marco que estructura la tarea como un pipeline de Decompositor-Formalizador-Probador. La innovación central es una estrategia de optimización en tiempo de prueba eficiente que identifica y apunta al cuello de botella crítico del sistema.

2.1 Pipeline Multi-Agente

El sistema consta de tres agentes especializados:

• Decompositor ($D$): Divide la prueba informal en subproposiciones atómicas y autónomas (unidades de prueba) con dependencias explícitas.
• Formalizador ($F$): Traduce cada subproposición de lenguaje natural en una sentencia formal de Lean.
• Probador ($P$): Genera scripts de tácticas para probar cada objetivo formalizado.
• Verificador ($V$): Un comprobador externo de Lean que valida el archivo de la prueba ensamblado.

2.2 Análisis de Eslabón Débil

Antes de la optimización, los autores realizan un "análisis de eslabón débil" para determinar dónde el cómputo en tiempo de prueba ofrece el mayor retorno. Al intervenir en cada etapa (Decompositor, Formalizador, Probador) de forma individual mientras se mantienen las otras fijas, miden la recuperabilidad del éxito de la verificación de extremo a extremo.

• Hallazgo: El Decompositor es el cuello de botella crítico. Revisar la especificación de las unidades de prueba en lenguaje natural (afirmaciones, supuestos, dependencias) genera ganancias significativamente mayores en el éxito de la verificación final (51.1% de precisión) en comparación con la revisión de sentencias formales (45.1%) o scripts de prueba (33.7%).
• Implicación: Unidades de prueba atómicas y de alta calidad, y autónomas, reducen la formalización y la prueba posteriores a tareas locales dentro de las capacidades del Formalizador y el Probador.

2.3 Estrategía de Optimización en Tiempo de Prueba

TOMAP enfoca todo el cómputo en tiempo de prueba en refinar el Decompositor, tratando al Formalizador y al Probador como ejecutores descendentes fijos. La optimización sigue un bucle de estilo GEPA (Evolución de Prompts Reflexivos):

1. Pool de Candidatos: Mantiene un grupo de candidatos de descomposición para una entrada dada.
2. Calificación por Rúbrica: En lugar de llamar inmediatamente al costoso verificador de Lean, los candidatos son calificados por un "Juez de Rúbrica" basado en un LLM frente a tres dimensiones:
   • Fidelidad Semántica: Alineación con la prueba original en lenguaje natural.
   • Capacidad de Prueba: Si cada unidad es autónoma y lógicamente completa.
   • Amigabilidad con Lean: Claridad, explicidad de los supuestos y evitación de ambigüedades.
3. Evolución Guiada por Pareto: Los candidatos son evaluados en una frontera de Pareto basada en las puntuaciones de la rúbrica. Un LLM proponente reflexivo selecciona candidatos de alto rendimiento, los critica basándose en la retroalimentación de la rúbrica y propone descomposiciones revisadas.
4. Puerta de Verificación: Solo los candidatos que cumplen con un umbral de alta calidad (que pasan la puerta de la rúbrica) se comprometen al pipeline descendente de Formalizador-Probador para la costosa verificación de verdad de terreno de Lean.

Este diseño de dos niveles equilibra la retroalimentación de proxy densa y barata (rúbricas) para guiar la búsqueda con la verificación fiel y costosa reservada solo para candidatos prometedores.

3. Contribuciones Clave

• Identificación del Cuello de Botella: El artículo proporciona evidencia empírica mediante el análisis de eslabón débil de que la calidad de la descomposición de la prueba es el determinante primario del éxito en la autoformalización de pruebas completas, desplazando el enfoque de optimización de todo el pipeline hacia la interfaz del Decompositor.
• Marco de Trabajo TOMAP: Un nuevo método de optimización en tiempo de prueba que desacopla la búsqueda de la verificación. Evoluciona las descomposiciones de las pruebas utilizando retroalimentación de rúbricas multiobjetivo y selección de Pareto, reduciendo significativamente la dependencia de las llamadas costosas a Lean durante la fase de búsqueda.
• Eficiencia y Rendimiento: El enfoque logra resultados de vanguardia sin requerir un entrenamiento a gran escala, apoyándose en su lugar en una optimización eficiente en tiempo de inferencia.

4. Resultados Experimentales

Los experimentos se realizaron en PROOFFLOWBENCH (184 problemas de nivel de pregrado) y miniF2F (244 problemas de nivel de secundaria).

• Rendimiento: TOMAP supera tanto a los baselines basados en entrenamiento (ej. ProofBridge) como a los baselines libres de entrenamiento (ej. PROOFFLOW, Monotonic).
  • En PROOFFLOWBENCH, TOMAP (usando Gemini3-Pro) mejoró la puntuación conjunta de Corrección Sintáctica y Fidelidad Semántica en un 19.0% sobre el mejor método anterior.
  • En miniF2F, logró una mejora del 8.2% en la métrica conjunta.
• Fidelidad Semántica: TOMAP supera significativamente a los generadores monolíticos en la preservación de la estructura semántica de la prueba original, evitando la tendencia de otros métodos a generar código Lean sintácticamente válido pero semánticamente incorrecto.
• Eficiencia de Costo: Aunque TOMAP requiere más cómputo en tiempo de prueba que los baselines ingenuos, logra tasas de éxito más altas con un costo total menor en comparación con los métodos que dependen de reintentos iterativos extensos de todo el pipeline.
• Análisis de Escalamiento: Los estudios de ablación revelan que la mayoría de las ganancias de rendimiento ocurren dentro de las primeras iteraciones de la evolución de la descomposición, proporcionando una guía práctica para seleccionar el presupuesto de tiempo de prueba.

5. Significado y Reivindicaciones

El artículo sostiene que la autoformalización de pruebas completas es fundamentalmente un problema de calidad de descomposición. Al identificar al Decompositor como la etapa con mayor capacidad de recuperación por retroalimentación, los autores demuestran que la optimización eficiente en tiempo de prueba puede lograrse enfocando los recursos en refinar la estructura de la prueba en lenguaje natural en lugar de reintentar repetidamente la formalización o la prueba.

La importancia de TOMAP radica en su capacidad para:

1. Elevar el techo del razonamiento matemático verificable al cerrar la brecha entre las pruebas informales y la verificación formal de manera más fiel.
2. Proporcionar una alternativa escalable y libre de entrenamiento a los complejos enfoques de ajuste fino.
3. Ofrecer un marco práctico para la asignación de cómputo limitado en tiempo de prueba en sistemas multi-agente, priorizando el "eslabón débil" identificado mediante análisis causal.

Los autores señalan limitaciones, incluyendo la restricción a pruebas de escala de benchmark en lugar de matemáticas largas de nivel de investigación, y la suposición de que las pruebas informales de entrada son correctas. Dejan la detección y reparación de pasos de prueba incorrectos como trabajo futuro.