Resumen Técnico: CAM-Bench

Enunciado del Problema

Las benchmarks existentes para demostración de teoremas formales dirigidas a Modelos de Lenguaje Grande (LLM) se centran predominantemente en problemas de estilo olímpico y dominios algebraicos (por ejemplo, MiniF2F, PutnamBench, ProofNet). Aunque estas benchmarks han impulsado el progreso en el razonamiento formal, dejan las matemáticas computacionales y aplicadas significativamente subrepresentadas.

Los problemas en matemáticas aplicadas (por ejemplo, optimización, álgebra lineal numérica, análisis numérico) difieren fundamentalmente de las declaraciones de teoremas aisladas. A menudo dependen del contexto, basándose en:

• Definiciones, notación y algoritmos introducidos localmente.
• Convenciones y resultados elementales específicos de cada capítulo.
• Suposiciones heredadas que no se declaran explícitamente en el ejercicio, pero que son necesarias para una formalización fiel.

Las benchmarks actuales luchan por evaluar si los modelos pueden rastrear estas suposiciones locales, descomponer pruebas basadas en contextos de libros de texto y aplicar resultados elementales que aún no están disponibles como lemas estándar en bibliotecas formales como Mathlib4. Existe una necesidad de una benchmark que apunte a problemas de matemáticas aplicadas donde el "contexto local" es tan crítico como la declaración del teorema en sí misma.

Metodología

Los autores introducen CAM-Bench, una benchmark para demostración de teoremas en Lean 4 que comprende 1.000 objetivos de prueba derivados de 778 ejercicios de libros de texto en optimización, álgebra lineal numérica y análisis numérico. La construcción de esta benchmark se basa en una tubería novedosa de recuperación de dependencias y formalización diseñada para transformar ejercicios dependientes del contexto en objetivos autocontenidos y verificables por máquina.

1. Tubería de Recuperación y Enriquecimiento de Dependencias

Para abordar la naturaleza no autocontenida de los ejercicios de libros de texto, los autores desarrollaron un procedimiento recursivo de expansión de dependencias (Algoritmo 1):

• Expansión Recursiva: Partiendo de un ejercicio crudo, el sistema extrae referencias (teoremas, ecuaciones, algoritmos) y recupera recursivamente sus definiciones y dependencias hasta una profundidad acotada.
• Naturalización de Abajo hacia Arriba: El árbol de dependencias se procesa de abajo hacia arriba. Un naturalizador LLM fusiona representaciones enriquecidas, resolviendo referencias locales, estandarizando la notación y suavizando transiciones para asegurar que las definiciones de nivel inferior se incorporen antes de que las dependencias de nivel superior las utilicen.
• Recuperación de Condiciones Implícitas: El sistema hace explícitas las suposiciones requeridas (por ejemplo, restricciones de dominio, positividad, convexidad) solo cuando están respaldadas por el problema original o el contexto recuperado. Este enriquecimiento está basado en la fuente; no conjetura dependencias faltantes, sino que las deja de lado si no pueden recuperarse.
• Revisión Multirredonda: Las declaraciones enriquecidas pasan por un bucle de validación para verificar la ausencia de suposiciones, la desviación de la tarea y la idoneidad para Lean. Las reparaciones se limitan a corregir defectos locales sin alterar el objetivo matemático ni inventar dependencias no respaldadas.

2. Formalización en Lean Impulsada por Modularización

Una vez establecido un objetivo informal, el sistema lo convierte en código Lean 4 utilizando una estrategia de construcción por bloques con contexto congelado:

• Descomposición Semántica en Bloques: Los ejercicios heterogéneos se descomponen en bloques semánticos tipados (definiciones, problemas de optimización, algoritmos, objetivos de teorema). Esto separa el contexto de soporte del objetivo final del teorema.
• Traducción Incremental: El sistema traduce los bloques secuencialmente. Las declaraciones previamente aceptadas se mantienen como un contexto congelado y de solo lectura. Esto previene errores en cascada y localiza los fallos en el bloque actual.
• Reparación Guiada por el Compilador y Semántica:
  • Reparación de Compilación: Si un bloque falla al compilarse, un corrector utiliza los diagnósticos del compilador para generar parches locales (sintaxis, anotaciones de tipo, resolución de espacios de nombres).
  • Revisión Semántica: Un revisor compara el candidato compilable contra el bloque informal para asegurar la fidelidad semántica (preservando variables, suposiciones y conclusiones). Las discrepancias desencadenan una reescritura semántica.
• Control Consciente del Historial: El sistema mantiene un historial de intentos fallidos y razones de rechazo para evitar la oscilación y guiar las reparaciones subsiguientes lejos de las direcciones fallidas previamente.

3. Construcción y Validación de la Benchmark

El conjunto de datos final incluye el ejercicio crudo, el contexto recuperado, el teorema informal normalizado y el objetivo Lean final. La validación ocurre en dos niveles:

• Nivel de Fuente: Asegura que el objetivo informal sea fiel al ejercicio del libro de texto y esté autocontenido.
• Nivel de Lean: Asegura que la declaración formal preserve el objetivo informal revisado. Solo el 92,5 % de las declaraciones candidatas se consideraron utilizables después de la validación semántica, lo que resalta la dificultad de la autoformalización fiel.

Contribuciones Clave

1. Conjunto de Datos CAM-Bench: Una benchmark curada de 1.000 objetivos de prueba en Lean que abarca optimización, álgebra lineal numérica y análisis numérico. Proporciona artefactos rastreables desde ejercicios crudos hasta objetivos Lean verificados por máquina, llenando la brecha en la evaluación de matemáticas aplicadas.
2. Tubería de Recuperación de Dependencias: Un método novedoso para construir objetivos Lean fieles a partir de ejercicios dependientes del contexto. Combina expansión recursiva de dependencias, enriquecimiento basado en la fuente y reparación restringida para manejar definiciones y suposiciones locales que no son lemas estándar de Mathlib4.
3. Evaluación Exhaustiva y Análisis de Errores: El artículo evalúa LLMs de vanguardia y agentes de formalización en CAM-Bench. Identifica modos de fallo específicos:
   • Fundamentación en Bibliotecas/API: Los modelos fallan al fundamentar pruebas en la infraestructura disponible de Mathlib, alucinando APIs o omitiendo resultados puente.
   • Representación Formal: Errores en la disciplina de tipos, desajustes de dimensiones/índices y fallos de coerción.
   • Descomposición de Pruebas: Incapacidad para descomponer pruebas de largo horizonte en lemas auxiliares o mantener el control sobre argumentos complejos de optimización/numéricos.

Resultados

Rendimiento de Línea Base

• Modelos No Agentes: Incluso las líneas base no agentes más fuertes (por ejemplo, Deepseek-v4-pro, Claude-sonnet-4-6) lograron una precisión verificada en Lean baja, siendo la mejor del 19,67 % (Pass@32).
• Brecha entre Informal y Formal: Existe una discrepancia significativa entre la corrección informal (Precisión informal Pass@1 ~70–84 %) y la corrección verificada en Lean (<20 %). Los modelos capturan argumentos de alto nivel pero fallan en satisfacer la sintaxis estricta de Lean, la disciplina de tipos y las restricciones de bibliotecas.
• Mejora por Agentes: Los sistemas de búsqueda de pruebas con agentes (por ejemplo, GPT-5.4 con reparación iterativa y uso de herramientas) mejoraron significativamente el rendimiento, alcanzando una precisión verificada del 44,00 %. Sin embargo, esto conllevó un alto costo de tokens (~1,96 millones de tokens frente a ~0,26–0,70 millones para las líneas base).

Evaluación de Agentes Externos

Dos sistemas agentes externos, M2F y Aristotle, fueron evaluados en 200 instancias muestreadas con un presupuesto de tiempo de 8 horas:

• M2F: Resolvió 143/200 instancias (71,5 %).
• Aristotle: Resolvió 125/200 instancias (62,5 %).
• A pesar de estas mejoras, la benchmark sigue sin estar saturada. Muchos fallos se atribuyeron a infraestructura matemática faltante, cadenas largas de lemas auxiliares y razonamiento específico de optimización.

Significado y Afirmaciones

El artículo afirma que CAM-Bench sirve como un complemento crítico a las benchmarks formales existentes al apuntar a problemas de matemáticas aplicadas que dependen de conceptos de libros de texto y teoremas elementales. Su importancia radica en:

1. Evaluación del Razonamiento Dependiente del Contexto: Prueba la capacidad de un modelo para rastrear suposiciones locales y reconstruir el contexto, una capacidad esencial para la formalización del mundo real pero a menudo eludida por las benchmarks de teoremas aislados.
2. Diagnóstico de Cuellos de Botella Sistémicos: Los resultados destacan que los demostradores actuales basados en LLM luchan no solo con la sintaxis, sino con la fundamentación en Mathlib, la disciplina de tipos y la descomposición de pruebas de largo horizonte.
3. Impulso al Desarrollo de Infraestructura: La benchmark sugiere que el progreso en matemáticas aplicadas formales requiere una infraestructura Mathlib más sólida (por ejemplo, para matrices, espectros, convexidad) y agentes más capaces que puedan gestionar trayectorias de prueba de largo horizonte.

Los autores mantienen una postura modesta, señalando que, aunque los sistemas agentes mejoran el rendimiento, la benchmark sigue siendo desafiante y los resultados deben verse como estimaciones de las capacidades actuales en lugar de un problema resuelto. La benchmark tiene la intención de ser un componente de una suite de evaluación más amplia para sistemas de razonamiento matemático.