💻 computer science

ITPEval: Benchmarking Formal Translation Across Interactive Theorem Provers

Este artículo presenta ITPEval, el primer referente e infraestructura unificada para evaluar la traducción automatizada de pruebas formales a través de cuatro de los principales probadores de teoremas interactivos, revelando que los modelos de lenguaje extensos actuales tienen dificultades significativas con la traducción de pruebas debido a desajustes de librerías y que la comprobación de tipos nativa por sí sola a menudo sobreestima la fidelidad semántica.

Autores originales: Jiayi Wu, Robert Joseph George, Anima Anandkumar

Publicado 2026-07-23

📖 3 min de lectura☕ Lectura para el café

CC BY 4.0

Autores originales: Jiayi Wu, Robert Joseph George, Anima Anandkumar

Artículo original bajo licencia CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta es una explicación generada por IA del artículo a continuación. No ha sido escrita ni avalada por los autores. Para mayor precisión técnica, consulte el artículo original. Leer descargo de responsabilidad completo

Imagina un mundo donde los matemáticos hablan cuatro lenguas diferentes, pero todos intentan resolver exactamente los mismos acertijos. En la arena de alto riesgo de la "demostración formal de teoremas", las computadoras actúan como los árbitros definitivos, verificando cada uno de los pasos de una demostración matemática para asegurar que sea 100% correcta. Sin embargo, al igual que los humanos que hablan francés, japonés, suajili y árabe, estos sistemas informáticos (llamados Probadores de Teoremas Interactivos, o ITP, por sus siglas en inglés) tienen su propia gramática, vocabulario y bibliotecas de hechos previamente aprobados. Una demostración escrita perfectamente en un sistema suele ser un galimatías para los demás. Esto crea un problema solitario: si una demostración brillante se escribe en un lenguaje, no puede ser fácilmente utilizada o verificada por los otros. Los científicos han estado tratando de construir "traductores universales" para cerrar esta brecha, con la esperanza de que la Inteligencia Artificial (IA) pudiera aprender a traducir estas demostraciones matemáticas automáticamente, permitiendo que toda la comunidad comparta su trabajo.

Presentamos ITPEVAL, un nuevo estudio que actúa como un examen de idiomas masivo y riguroso para la IA. Los investigadores querían ver si los modelos de IA más inteligentes de la actualidad podrían realmente traducir demostraciones matemáticas formales entre cuatro sistemas principales: Lean 4, Rocq, Isabelle y HOL Light. No se limitaron a pedirle a la IA que adivinara; construyeron un campo de pruebas especializado con más de 1,500 archivos fuente y casi 7,000 teoremas. Dividieron la prueba en dos niveles: un nivel "Controlado" con problemas matemáticos simples y autónomos (como un quiz de vocabulario sin referencias externas), y un nivel de "Ecosistema" que utiliza código de biblioteca real y desordenado que depende de reglas complejas y específicas del sistema (como una conversación completa con jerga y referencias culturales).

Los resultados fueron una mezcla de "nada mal" y "todavía muy difícil". Cuando la IA intentaba traducir solo los enunciados de los teoremas (el "qué"), los mejores modelos acertaron aproximadamente el 29.1% de las veces. Pero cuando se le pidió traducir las demostraciones reales (el "cómo"), la tasa de éxito cayó estrepitosamente a solo un 10.5%. El estudio encontró que el mayor obstáculo no era la matemática en sí o los diferentes fundamentos lógicos; era el "ecosistema". La IA tuvo más dificultades cuando tenía que navegar por las bibliotecas específicas, las convenciones de nomenclatura y los estilos de automatización del sistema de destino. Es como si la IA pudiera entender la frase "El gato se sentó en la alfombra", pero fallara cuando se le pedía traducir esa frase a un dialecto específico que requería usar una marca específica de alfombra y un tipo específico de gato.

Además, los investigadores descubrieron que el simple hecho de lograr que una computadora diga "Esto parece correcto" (una verificación de tipos) no es suficiente. Realizaron una "verificación de significado" más profunda y encontraron que, incluso cuando la traducción de la IA pasaba la prueba básica de la computadora, a menudo era matemáticamente más débil o ligeramente diferente de la original en el 46% de los casos. El estudio sugiere que, si bien la IA está mejorando en lo básico, todavía necesita aprender cómo adaptarse a la "cultura" única de cada sistema matemático antes de que pueda convertirse verdaderamente en un traductor universal. Los autores también exploraron una prueba de "ida y vuelta", donde tradujeron matemáticas a lenguaje natural y viceversa, encontrando que los resultados variaban enormemente dependiendo de qué sistema se utilizara, lo que insinúa que usar múltiples sistemas juntos podría ayudar, pero aún no es una solución mágica.

Resumen Técnico: ITPEVAL – Evaluación comparativa de la traducción formal entre probadores de teoremas interactivos

1. Planteamiento del problema

El ecosistema de la demostración formal de teoremas está actualmente fragmentado. Si bien los modelos de lenguaje de gran tamaño (LLM) han logrado un éxito significativo en la demostración automática de teoremas y la autoformalización, los resultados verificados permanecen aislados dentro de Probadores de Teoremas Interactivos (ITP) incompatibles. Cada sistema (por ejemplo, Lean 4, Rocq, Isabelle, HOL Light) implementa su propia base lógica, lenguaje de tácticas y bibliotecas matemáticas. En consecuencia, un teorema demostrado en un sistema no puede ser invocado directamente en otro, lo que conduce a la duplicación de esfuerzos de formalización y limita los datos de entrenamiento disponibles para los probadores basados en aprendizaje.

La traducción entre ITP (Cross-ITP translation)—la tarea de convertir pruebas formales entre sistemas preservando la corrección—ha recibido poco estudio sistemático. Los esfuerzos existentes, como los catálogos de "Formalización de 100 Teoremas" o los marcos de interoperabilidad como Dedukti, se centran en rastrear la cobertura o permitir el intercambio de pruebas a través de representaciones intermedias, pero carecen de benchmarks estandarizados para evaluar la calidad de la traducción. Además, las metodologías de evaluación existentes son insuficientes; la simple comprobación de tipos suele arrojar altas tasas de falsos positivos en cuanto a la corrección semántica, y los benchmarks de traducción de código no tienen en cuenta las profundas diferencias de la base lógica inherentes a los ITP.

2. Metodología y diseño del benchmark

Los autores presentan ITPEVAL, el primer benchmark diseñado para evaluar la traducción automática de pruebas formales entre cuatro ITP principales: Lean 4, Rocq (anteriormente Coq), Isabelle y HOL Light. El benchmark abarca dos bases lógicas distintas: el Cálculo de Construcciones Inductivas (CIC) y la Lógica de Orden Superior (HOL).

2.1. Estructura de datos

El benchmark consta de 1,560 archivos fuente y 6,848 teoremas, organizados en dos niveles distintos para aislar las fuentes de dificultad:

Nivel A (Controlado): Contiene 64 archivos auto-contenidos y axiomatizados (660 lemas) derivados del benchmark Babel-formal. Estos archivos incluyen sus propias definiciones y suposiciones, evitando la dependencia de bibliotecas específicas de cada probador. Este nivel aísla los problemas de traducción fundacional (p. ej., teoría de tipos, niveles de universo, argumentos implícitos).
Nivel B (Ecosistema): Contiene formalizaciones extraídas de bibliotecas reales de la comunidad, exponiendo desajustes de API, convenciones de nomenclatura y diferencias en el estilo de prueba. Este nivel incluye:
- 232 archivos de Formalizing 100 Theorems (4,924 lemas), alineados en los cuatro sistemas.
- 1,264 archivos de un solo teorema de miniF2F (solo enunciados), que proporcionan contenido diverso de matemáticas de competición.

El diseño impone un requisito de intersección de cuatro vías: cada archivo debe estar formalizado en los cuatro ITP para asegurar comparaciones direccionales limpias sin confusión por falta de datos.

2.2. Tareas de traducción

ITPEVAL evalúa dos tareas primarias:

Traducción de enunciados (Statement Translation): Generar código del ITP de destino donde los cuerpos de las pruebas son reemplazados por marcadores de posición (p. ej., sorry). La verificación requiere que el archivo generado pase la comprobación de tipos en el sistema de destino.
Traducción de pruebas (Proof Translation): Generar archivos de prueba completos y compilables sin marcadores de posición. La verificación requiere que el archivo completo compile con éxito en el probador de destino.

2.3. Infraestructura de verificación

Un componente crítico de la metodología es itpeval, una infraestructura de verificación unificada para múltiples ITP. Para abordar la heterogeneidad de los modelos de ejecución de los ITP (p. ej., altos costos de inicio en Isabelle y HOL Light), el sistema emplea:

Backends cálidos con aislamiento de estado: Garantizando que cada comprobación sea observacionalmente equivalente a verificar un artefacto en un entorno fresco, evitando la fuga de declaraciones.
Comprobación nativa del probador de destino: Todas las etiquetas son producidas por los ITP de destino reales, no por heurísticas superficiales.
Programación adaptativa: Uso de trabajadores persistentes, procesamiento por lotes de sesiones y servidores de bifurcación (fork servers) para gestionar el rendimiento mientras se preservan las semánticas de comprobación por archivo.

2.4. Comprobación de equivalencia semántica

Reconociendo que la comprobación de tipos es necesaria pero insuficiente para la fidelidad semántica, los autores implementan una comprobación de Equivalencia Definicional Extendida Bidireccional (BEq) para los objetivos de Lean 4. Esta comprobación determinista verifica si un enunciado generado $G$ y un enunciado de referencia $R$ se implican mutuamente ( $G \vdash R$ y $R \vdash G$ ) utilizando una búsqueda de pruebas restringida, evitando la varianza adicional dependiente del modelo.

3. Contribuciones clave

Benchmark alineado de cuatro vías: Un conjunto de datos de 1,560 archivos y 6,848 teoremas a través de Lean 4, Rocq, Isabelle y HOL Light, estructurado en niveles controlados y de ecosistema para cuantificar el costo de las dependencias de las bibliotecas.
Infraestructura de verificación unificada: Un cliente con aislamiento de estado (itpeval) que permite la evaluación escalable y reproducible a través de ITP heterogéneos con semánticas de comprobación nativas.
Evaluación sistemática de LLM: Una evaluación de cinco modelos de frontera y de pesos abiertos (GPT-5.5, Claude Sonnet 4.6, Gemini 3.1 Pro, DeepSeek-V4-Pro, Qwen3-235B-A22B) sobre 12 pares de traducción dirigidos.
Análisis de fidelidad semántica: La aplicación de BEq para demostrar que la comprobación de tipos nativa por sí sola puede sobreestimar sustancialmente la corrección semántica.
Estudio exploratorio de ida y vuelta (Round-Trip): Una investigación de los bucles de autoformalización y auto-informalización para evaluar los patrones de verificación dependientes del objetivo y los beneficios potenciales del contexto multi-ITP.

4. Resultados

4.1. Rendimiento de la traducción

Traducción de enunciados: El modelo con mejor desempeño, GPT-5.5, logró una tasa de pass@1 del 29.1% global. DeepSeek-V4-Pro le siguió con un 27.1%. El rendimiento cayó significativamente para otros modelos (Gemini al 14.0%, Qwen y Claude por debajo del 10%).
Traducción de pruebas: El rendimiento fue sustancialmente menor, con GPT-5.5 logrando solo un 10.5% de pass@1 global.
Brecha de niveles (Tier Gap): El nivel controlado (Nivel A) fue consistentemente más fácil que el nivel de ecosistema (Nivel B). Para la traducción de pruebas, GPT-5.5 alcanzó un 29.7% en archivos controlados pero solo un 5.2% en archivos de ecosistema. Esto indica que el desajuste de bibliotecas (APIs, nomenclatura, automatización) es la mayor fuente observada de fallo, más que las diferencias de la base lógica.
Asimetría direccional: La dificultad de traducción varía significamente según el objetivo. Isabelle y HOL Light son objetivos fuertes para la traducción de enunciados, pero Isabelle se convierte en el objetivo más difícil para la traducción de pruebas. La similitud de la base lógica (p. ej., de CIC a CIC) no garantiza mayores tasas de éxito; las convenciones del ecosistema de destino juegan un papel más importante.

4.2. Equivalencia semántica (BEq)

Al aplicar la comprobación BEq a las traducciones de enunciados de Lean 4 verificadas de miniF2F:

Solo el 54.0% de las traducciones verificadas pasaron la comprobación de equivalencia.
Claude Sonnet 4.6 mostró la mayor tasa de paso de BEq (83.8%) entre las traducciones verificadas, mientras que los demás oscilaron entre 34.5% y 48.4%.
Este resultado demuestra que un enunciado puede ser sintácticamente válido (pasa la comprobación de tipos) pero semánticamente más débil o desplazado respecto al teorema original.

4.3. Ida y vuelta (Round-Trip) y Autoformalización

En un estudio de ida y vuelta multi-ITP (Lenguaje Natural $\to$ Formal $\to$ Lenguaje Natural $\to$ Formal), Rocq y HOL Light verificaron aproximadamente un tercio de las salidas en ambos pasos de formalización, mientras que Lean 4 se mantuvo cerca del 11% e Isabelle cayó al 4.3% en el paso final. El contexto multi-ITP mostró beneficios potenciales para combinaciones específicas de modelo-objetivo (p. ej., mejorando las tasas de paso del paso 1 de Lean 4 del 4.8% al 10.6%), pero los resultados no fueron uniformes en todos los sistemas.

5. Significado y Reivindicaciones

El artículo afirma que ITPEVAL proporciona el primer benchmark sistemático de cuatro vías para la traducción formal, revelando que la barrera principal para la traducción entre ITP no es la base lógica en sí misma, sino las dependencias a nivel de ecosistema (bibliotecas, APIs y modismos de prueba).

Los autores enfatizan que:

La verificación nativa es esencial: Las heurísticas superficiales o la comprobación de tipos por sí solas son insuficientes para evaluar la fidelidad semántica.
La infraestructura importa: La evaluación fiable entre ITP requiere una verificación con aislamiento de estado para evitar factores de confusión como la fuga de declaraciones.
Direcciones futuras: El campo debe priorizar la recuperación, el mapeo de bibliotecas y la alineación de APIs por encima de la pura traducción fundacional. El artículo también señala limitaciones, incluyendo la configuración de evaluación zero-shot, la restricción de BEq a los objetivos de Lean 4 y el potencial de contaminación de datos de entrenamiento en conjuntos de datos públicos como miniF2F.

El trabajo establece una base para medir el progreso en la traducción formal, sugiriendo que los sistemas futuros deben abordar el problema del "desajuste de bibliotecas" para lograr una interoperabilidad robusta entre los ecosistemas de pruebas formales.