Resumen Técnico: Optimización del Compromiso Costo-Calidad de los Probadores de Teoremas Agénticos en Lean

Declaración del Problema

Los modelos de lenguaje de gran tamaño (LLM) han logrado avances significativos en la demostración automática de teoremas dentro del asistente de pruebas Lean mediante el empleo de flujos de trabajo agénticos. Estos flujos de trabajo típicamente descomponen problemas complejos en lemas más pequeños, generan numerosos intentos de prueba y utilizan la retroalimentación del compilador para guiar la búsqueda. Si bien este enfoque produce un alto rendimiento en entornos de prueba desafiantes como PutnamBench, sufre de costos computacionales prohibitivos. Los sistemas actuales suelen asignar presupuestos fijos y preespecificados para la descomposición y la generación de pruebas a cada problema, independientemente de su dificultad. Esta política de "pasos fijos" conduce a un desperdicio sustancial, ya que los agentes frecuentemente gastan un cómputo significativo en problemas infactibles o enunciados mal formalizados que tienen pocas probabilidades de tener éxito. El desafío central abordado es la falta de conciencia dinámica del costo en los agentes existentes, lo cual no logra optimizar el compromiso entre el gasto computacional y las tasas de éxito de las pruebas.

Metodología

Los autores proponen una novedosa arquitectura de Agente de Enrutamiento de Acciones diseñada para reemplazar las políticas estáticas con decisiones de enrutamiento dinámicas basadas en datos. El sistema se divide conceptualmente en dos planos:

1. Plano de Datos (Generación de Pruebas)

Inspirado en trabajos previos (e.g., Chen et al., 2025c; Varambally et al., 2025), el plano de datos gestiona la generación real de las pruebas. Opera a través de cuatro módulos:

• Módulo de Descomposición: Un modelo de propósito general (GPT-OSS-20B) descompone el problema original en lemas de lenguaje natural y esquemas de prueba.
• Formalizador: El agente formaliza estos lemas en código Lean utilizando GOEDEL-FORMALIZER-V2-8B, seleccionando el mejor candidato que compile sin errores de sintaxis o de tipo.
• Probador de Descomposición Formal: El sistema intenta demostrar el teorema de nivel superior utilizando los lemas formalizados como axiomas, guiado por el esquema de lenguaje natural.
• Probador de Lemas: Una vez que la descomposición es probada, el agente intenta recursivamente probar los lemas individuales requeridos por la prueba, empujando nuevas dependencias a una pila.

2. Plano de Control (Enrutamiento Costo-Calidad)

El plano de control observa la trayectoria de los intentos de prueba fallidos y decide si continuar intentando el objetivo actual o terminar la trayectoria para reiniciar con una nueva descomposición. Utiliza una política de enrutamiento ligera basada en un compromiso costo-calidad:

• Estado ($s$): Resume el historial de intentos fallidos, incluyendo intentos de prueba, resultados de compilación, mensajes de error y longitudes de salida.
• Espacio de Acción: $\{ \text{INTENTAR}, \text{TERMINAR} \}$. El agente ya sea toma otra muestra de prueba para el objetivo actual o descarta la descomposición actual.
• Función de Utilidad: El enrutador calcula una puntuación de utilidad $\tau(s) = \hat{q}(s) - \lambda\hat{c}(s)$, donde:
  • $\hat{q}(s)$ es la probabilidad predicha de éxito para el siguiente intento (Calidad).
  • $\hat{c}(s)$ es el costo predicho del siguiente intento (medido en tokens de generación de LLM/SFLOPs).
  • $\lambda$ es un hiperparámetro que controla la penalización por el costo computacional.
• Regla de Decisión: Si $\tau(s) > 0$, el agente continúa; de lo contrario, termina la trayectoria actual.

Estimadores:

• Estimador de Costo: Asume que los costos de los intentos son independientes e idénticamente distribuidos, utilizando el costo promedio de los intentos previos en la trayectoria.
• Estimador de Calidad: Un modelo de regresión logística entrenado para predecir la probabilidad de éxito basándose en las características de la trayectoria, específicamente:
  • Similitud de la Prueba: El promedio de la relación de cadenas difusas (fuzzy string ratio) de las pruebas normalizadas (una baja similitud sugiere confusión).
  • Diversidad de Errores: La relación de errores de compilación únicos respecto al total de errores (una baja diversidad sugiere un modo de falla persistente).
  • Conteo de Intentos: El número de intentos previos.

Contribuciones Clave

1. Identificación de la Ineficiencia: El artículo identifica que el escalado de pasos fijos en los agentes de Lean es críticamente ineficiente y que reducir los intentos innecesarios es esencial para un mejor compromiso costo-calidad.
2. Arquitectura Novedosa: El desarrollo de un probador de Lean de estilo lema equipado con un enrutador de costo-calidad en línea y adaptativo que evalúa dinámicamente el valor marginal de la computación adicional.
3. Validación Empírica: Demostración de que el enrutador propuesto disminuye significativamente el cómputo desperdiciado mientras mantiene una precisión competitiva, probando que las trayectorias fallidas contienen señales accionables para la asignación de recursos.

Resultados Experimentales

El sistema fue evaluado en un subconjunto de 85 problemas de PutnamBench, comparando el agente de enrutamiento dinámico contra una línea base de pasos fijos y un agente "oráculo" con acceso a las probabilidades de éxito de verdad fundamental.

• Reducción de Costo: En paridad de precisión, el agente propuesto redujo el presupuesto requerido en un 25.8% en promedio en comparación con la línea base de pasos fijos.
• Mejora de la Precisión: En paridad de costo, el agente logró una mejora del 7.8% en la tasa de resolución.
• Compromisos Específicos:
  • Para lograr una tasa de resolución de ~43.6%, la línea base de pasos fijos requirió 31.6 M de SFLOPs, mientras que el agente de enrutamiento requirió solo 22.6 M de SFLOPs (una reducción de costo del 28.4%).
  • En un régimen de presupuesto medio (~41.6% de tasa de resolución), el agente redujo los costos en un 29.6% (17.5 M vs. 24.9 M SFLOPs).
• Estudios de Ablación:
  • Importancia de las Características: La "diversidad de errores" fue identificada como la característica más crítica para la estimación de la calidad.
  • Impacto del Plano de Datos: La arquitectura de descomposición estilo lema por sí misma mejoró la tasa de resolución en casi un 100% sobre un enfoque de generación de prueba completa usando el mismo modelo de 8B, acercándose al rendimiento de un modelo de 32B.
  • Brecha con el Oráculo: Aunque el agente de enrutamiento superó significativamente a la línea base fija, persiste una brecha respecto al agente oráculo (que logró una reducción de costo del 59.9%), lo que sugiere espacio para mejorar la ingeniería de características y la arquitectura del estimador.

Significancia y Reivindicaciones

El artículo sostiene que las trayectorias fallidas de Lean proporcionan señales accionables para la asignación de recursos consciente del costo en la demostración de teoremas agéntica. Al alejarse de las políticas estáticas de pasos fijos hacia el enrutamiento dinámico, los agentes pueden reducir significamente el desperdicio computacional sin sacrificar el rendimiento. Los autores posicionan este trabajo como un paso fundacional hacia el "control consciente del costo" para la demostración matemática formal, sugiriendo que los futuros agentes deben asignar la computación dinámicamente basándose en el progreso observado y los patrones de falla en lugar de asignar presupuestos de inferencia de forma estática. Los resultados indican que las políticas de pasos fijos dejan un margen sustancial para mejoras de eficiencia, y que las estrategias de enrutamiento pueden mitigar eficazmente los costos innecesarios.