Resumen Técnico: Construcción–Verificación: Un Benchmark para la Formalización de las Matemáticas Aplicadas en Lean 4

1. Declaración del Problema

Los benchmarks actuales para la demostración automática de teoremas, como MiniF2F y ProofNet, se centran predominantemente en la verificación lógica de proposiciones declarativas (es decir, demostrar la existencia de una solución). Este paradigma es insuficiente para las matemáticas aplicadas, donde el objetivo principal es a menudo la derivación de valores concretos, algoritmos ejecutables o transformaciones estructurales, en lugar de la mera demostración de existencia.

Los conjuntos de datos existentes sufren dos limitaciones críticas en este dominio:

1. Brecha de Alcance: Carecen de cobertura de matemáticas aplicadas de nivel de pregrado y superior, incluyendo análisis convexo, optimización, álgebra numérica y probabilidad de alta dimensión.
2. Déficit Constructivo: No logran imponer un flujo de trabajo de "construcción–verificación". En las matemáticas aplicadas, un modelo debe sintetizar explícitamente una solución (por ejemplo, un algoritmo o un valor específico) antes de probar su corrección. Los benchmarks actuales permiten que los modelos eludan esto mediante el uso de tácticas no constructivas (por ejemplo, demostrar la existencia mediante el teorema del valor extremo sin calcular el óptimo específico), lo que representa erróneamente la capacidad del modelo para realizar razonamiento computacional.

2. Metodología

El Marco de Construcción–Verificación

Los autores proponen un paradigma de formalización en Lean 4 que impone estructuralmente un flujo de trabajo de dos etapas: Construcción seguida de Verificación. Este marco evita que los agentes exploten atajos no constructivos al requerir definiciones explícitas antes de las demostraciones. El marco aborda tres categorías específicas de tareas matemáticas aplicadas:

• Problemas de Evaluación: En lugar de demostrar $\exists x, Q(x)$, el agente debe definir una función def x (V) := ... que compute la solución $x(V)$ basada en parámetros $V$, seguido de un teorema que demuestre $Q(x(V), V)$. La firma de la función restringe estrictamente las entradas a los parámetros brutos, evitando que el modelo utilice la propiedad objetivo para "hacer trampa" en la construcción.
• Problemas de Diseño de Algoritmos: El agente debe definir una función recursiva que represente un proceso iterativo (por ejemplo, el Descenso de Gradiente). La tarea requiere completar la regla de transición (el cuerpo del bucle) para el paso $(n+1)$, seguido de una prueba de propiedades como la convergencia o la monotonicidad.
• Transformación de Representación: El agente debe modelar una instancia de problema bruto como una forma canónica objetivo (por ejemplo, transformar un problema de corte de grafo en una formulación de agrupamiento espectral). Esto implica definir el nuevo dominio, las restricciones y la función objetivo, y demostrar una relación de relajación o equivalencia entre el problema de origen y el de destino.
• Demostración de Teoremas: Se incluye un subconjunto base de tareas deductivas tradicionales para medir las capacidades de razonamiento lógico puro de forma independiente.

Curación del Benchmark (AMBER)

Los autores introducen AMBER (Applied Mathematics BEnchmark for Reasoning), un conjunto de datos que abarca cuatro dominios principales:

1. Análisis Convexo
2. Optimización
3. Álgebra Numérica
4. Probabilidad de Alta Dimensión

Fuentes de Datos y Dificultad: Los problemas se extraen de libros de texto clásicos (por ejemplo, Boyd & Vandenberghe, Vershynin) y se categorizan por dificultad (Fácil: ejercicios estándar; Difícil: nivel de examen de doctorado).
Formalización y Validación: 50 problemas por subcampo fueron formalizados por usuarios experimentados de Lean. La validación implicó un proceso de dos etapas: una verificación semántica basada en LLM seguida de una rigurosa validación manual por parte de contribuyentes de Mathlib para asegurar la alineación estricta con las declaraciones matemáticas originales.
Métricas de Complejidad: El benchmark se caracteriza por una alta densidad de dependencia semántica. Utilizando un análisis de grafo de dependencia ($k=3$), AMBER exhibe una densidad de dependencia promedio de 164.21, significativamente mayor que MiniF2F (29.72), ProofNet (33.95) y FATE (53.14), lo que indica un requisito más profundo para la recuperación y el razonamiento sobre conceptos matemáticos complejos.

3. Contribuciones Clave

1. Cambio de Paradigma: El artículo propone un cambio de la verificación de proposiciones existenciales hacia la síntesis de soluciones constructivas, alineando las tareas formales con la intuición computacional de las matemáticas aplicadas.
2. Benchmark AMBER: Un conjunto de datos exhaustivo que cubre núcleos de dominios aplicados con niveles de dificultad variables, presentando tareas complejas como el diseño de algoritmos y la transformación de representación, no solo la demostración de teoremas.
3. Patrones de Formalización: Plantillas especializadas de Lean 4 para evaluación, diseño de algoritmos y transformación de representación que imponen barreras sintácticas estrictas contra el razonamiento no constructivo.
4. Análisis Empírico: Una evaluación sistemática que revela un compromiso fundamental en los sistemas neuro-simbólicos actuales: la tensión entre la competencia táctica local (probadores especializados) y la síntesis algorítmica de alto nivel (modelos generales).

4. Resultados Experimentales

Rendimiento de los Modelos

Los autores evaluaron un conjunto diverso de modelos, incluyendo agentes de razonamiento de propósito general (DeepSeek-V3.2-Thinking, GPT-5.1, Gemini-3.0 Pro) y demostradores de teoremas especializados (Goedel Prover-32B, Kimina Prover-72B).

• Dificultad General: El rendimiento en todos los modelos es notablemente bajo. En el subconjunto "Difícil", las tasas de éxito son cercanas a cero para casi todos los modelos.
• General vs. Especializado: Contrario a la tendencia en los benchmarks de matemáticas puras, los modelos de razonamiento de propósito general superan consistentemente a los demostradores de teoremas especializados.
  • Pass@16 (AMBER Completo): Los modelos generales lograron entre 4.50% y 6.00%, mientras que los demostradores especializados lograron un 4.00%.
  • Pass@16 (Subconjunto Difícil): Los modelos generales lograron 0%–0% (con alguna variación en los subconjuntos Fáciles), mientras que los demostradores especializados también tuvieron dificultades significativas.
• Estudio de Ablación: La estrategia de prompt de construcción–verificación obtuvo una tasa de éxito del 8% en un subconjunto de 100 problemas, superando la completitud de código estándar (6%) y los prompts tradicionales de solo demostración (5%). Los prompts de solo demostración llevaron frecuentemente a los modelos a utilizar atajos no constructivos (por ejemplo, Classical.choice).

Análisis de Errores

Un análisis de 3,189 mensajes de error del modelo DeepSeek-R1 reveló:

1. Alucinación (47.3%): El modo de fallo más común, donde los modelos invocan teoremas o definiciones inexistentes (por ejemplo, convexHull eq sInter).
2. Competencia de Formalización (32.7%): Aplicación incorrecta de tácticas válidas o incapacidad para satisfacer las condiciones laterales.
3. Salidas Incompletas (15.2%): Fallo al proporcionar código plenamente ejecutable, dejando a menudo marcadores de posición sorry en pasos inductivos complejos.
4. Formato/Sintaxis (4.8%): Errores básicos de markdown o sintaxis.

5. Significado y Reivindicaciones

El artículo sostiene que el panorama actual de la formalización automática enfrenta un fenómeno de "sobreajuste táctico". Los modelos especializados, ajustados extensamente en corpora de demostración, parecen degradar sus capacidades de seguimiento de instrucciones generales. Tratan cada desafío estructural como una tarea de demostración pura, ignorando a menudo los requisitos de múltiples etapas de las matemáticas aplicadas (por ejemplo, definir una función antes de probarla).

En contraste, los modelos de propósito general retienen la versatilidad necesaria para tender un puente entre la intención informal y la sintaxis formal, sintetizando exitosamente objetos matemáticos antes de entrar en la etapa de verificación. Los autores concluyen que el avance de las matemáticas aplicadas formalizadas requiere ir más allá de la búsqueda de pruebas pura hacia sistemas neuro-simbólicos que integren el razonamiento algorítmico de alto nivel con la verificación formal rigurosa. El benchmark AMBER sirve como base para la investigación futura en la expansión de las fronteras de las matemáticas aplicadas formalizadas, proporcionando un estándar que exige la síntesis constructiva en lugar de la mera validez lógica.