Resumen: Realizamos un análisis exhaustivo de las declaraciones formales e informales en el punto de referencia miniF2F desde la perspectiva de un sistema de inteligencia artificial que tiene la tarea de participar en una Olimpiada de matemáticas que consta de los problemas en miniF2F. En tal entorno, el modelo tiene que leer y comprender los problemas en lenguaje natural, formalizarlos en lenguaje Lean, luego proceder a probar los problemas y obtendrá crédito por cada problema si la prueba formal corresponde a la declaración informal original presentada al modelo. Los resultados de nuestra evaluación revelan que la mejor precisión de dicha canalización puede ser de alrededor del 36% utilizando los modelos SoTA en la literatura, considerablemente más baja que las precisiones SoTA individuales, 97% y 69% reportadas en la literatura de autoformalización y demostración de teoremas. Al analizar los modos de falla, rastreamos una parte considerable de esta caída a discrepancias entre las declaraciones formales e informales para más de la mitad de los problemas en miniF2F. Procedemos a corregir todos los errores, discrepancias y simplificaciones en declaraciones formales e informales, y presentamos el miniF2F-v2 con declaraciones y pruebas formales e informales totalmente verificadas. La evaluación de todo el proceso de demostración de teoremas en miniF2F-v2 conduce a la mejor precisión del 70%, una mejora significativa del 40% en el miniF2F original, pero indica una desalineación considerable entre los modelos de autoformalización y los demostradores de teoremas. Nuestro análisis profundo sugiere que un punto de referencia de mayor calidad puede ayudar a la comunidad a evaluar mejor el progreso en el campo del razonamiento formal y también a diagnosticar mejor los modos de fracaso y éxito de los modelos de autoformalización y demostración de teoremas. Nuestro conjunto de datos está disponible en esta URL https.
Publicado originalmente en export.arxiv.org el 5 de noviembre de 2025.
Ver fuente original
