La compilación en Lean infla la precisión de la formalización: una brecha de hasta 29,5 p. p.

Lean acepta una declaración si está correctamente tipada. El compilador no comprueba qué dice esa declaración en cuanto al significado. Los autores del trabajo «Beyond Compilation» han medido cuánto sobrestima la métrica «compila» la calidad de la autoformalización, es decir, de la traducción de enunciados matemáticos del lenguaje natural a Lean. La cifra más llamativa: el agente con herramientas compila el 87,2% de los 227 enunciados universitarios, pero el criterio semántico solo deja pasar el 57,7%. La diferencia de 29,5 puntos porcentuales corresponde a código Lean que parece impecable y formula algo distinto de lo que se pedía.

Cómo funciona la verificación

La mayoría de las tareas no tiene una traducción de referencia en Lean, así que no es posible comparar con una respuesta «de oro». Los autores introducen un criterio compuesto: un enunciado se acepta si compila en Lean y dos modelos LLM de familias distintas lo consideran, de forma independiente, una traducción fiel de la formulación original.

El criterio se contrastó con una auditoría aleatoria independiente. Coincidió con la opinión de la mayoría de los anotadores humanos en el 91,5% de los casos. Sus errores son asimétricos: rara vez deja pasar una traducción incorrecta, pero rechaza una parte de las correctas. Es decir, la evaluación es conservadora y tiende a infravalorar el resultado de los sistemas.

Principales resultados en los ocho sistemas:

• la brecha entre la proporción de enunciados compilados y aceptados va de 1,3 a 29,5 p. p.;
• agente con herramientas: 87,2% de compilación frente a 57,7% de enunciados aceptados;
• los humanos revisaron todos los rechazos del agente: 23,8 de los 29,5 p. p. eran errores reales de traducción;
• en seis de los siete sistemas de un solo paso (one-shot), entre el 78% y el 100% de la brecha son errores de traducción genuinos, según la revisión en dos etapas de Claude Opus 5.5 con Lean y GPT-6.1 Sol, contrastada con la anotación humana.

Cuando se equivoca el juez

La parte más inesperada tiene que ver con los modelos nuevos. GPT-5.2 fue uno de los dos jueces. Los autores le pidieron evaluar las traducciones de dos modelos posteriores, GPT-6 Astra y Claude Opus 5.5. El juez aceptó el 83% de los enunciados de cada uno. El resultado one-shot del propio GPT-5.2 es, sin embargo, del 21%.

La revisión en dos etapas analizó después los rechazos de esos dos modelos. De 54 enunciados rechazados, solo 4 eran errores reales de traducción, es decir, el 7%. El resto de los rechazos son fallos del juez. Esto concuerda con una lógica simple: cuanto menos se equivoca un sistema, menos errores genuinos hay entre sus rechazos y más se nota el ruido del propio juez. Un juez que no mejora al ritmo de los modelos que evalúa se convierte en el cuello de botella del benchmark.

Para la industria, la conclusión es incómoda. Una métrica basada en un LLM-juez es casi honesta con los sistemas débiles, pero con los fuertes empieza a infravalorar la calidad. No se pueden comparar con ella modelos de distintas generaciones sin volver a revisar los rechazos.

Qué mostró la ablación de herramientas

Los autores sometieron al agente a una ablación 2^3: activaron y desactivaron tres herramientas en las ocho combinaciones posibles. La mayor parte de la mejora en compilación procede de la retroalimentación de Lean: el agente ve los errores y corrige el código. Pero casi la mitad de esa mejora no supera el criterio semántico. El agente aprende a lograr que el código compile, no a preservar el significado. El efecto típico: para eliminar un error, el enunciado pierde una condición, se debilita un cuantificador o se sustituye la estructura.

Qué cambiar en la práctica

Si construyes un pipeline de autoformalización o entrenas un modelo con la señal de Lean, la compilación como única recompensa produce una estimación sesgada y empuja hacia formulaciones degeneradas. Hace falta al menos una capa semántica: jueces de familias distintas y revisión humana por muestreo de los rechazos.

Al trabajar con modelos nuevos conviene comprobar si el juez se está quedando por detrás del sistema evaluado. Si la mayoría de los rechazos resultan ser errores del juez y no de la traducción, es hora de revisar la métrica. El código y los datos están publicados en GitHub (grenadeComing/beyond-compilation), de modo que el enfoque puede reproducirse con enunciados propios.