miniF2F-Lean Revisitado: Revisión de Limitaciones y Trazado de un Camino a Seguir

miniF2F-Lean Revisited: Reviewing Limitations and Charting a Path Forward

November 5, 2025

Autores: Azim Ospanov, Farzan Farnia, Roozbeh Yousefzadeh

cs.AI

Resumen

Realizamos un análisis exhaustivo de los enunciados formales e informales en el benchmark miniF2F desde la perspectiva de un sistema de IA cuya tarea es participar en una olimpiada matemática que consta de los problemas de miniF2F. En este contexto, el modelo debe leer y comprender los problemas en lenguaje natural, formalizarlos en el lenguaje Lean, proceder a demostrar los problemas y obtendrá crédito por cada problema si la prueba formal corresponde al enunciado informal original presentado al modelo. Nuestros resultados de evaluación revelan que la precisión máxima de dicho pipeline puede ser de aproximadamente un 36% utilizando los modelos estado del arte (SoTA) de la literatura, considerablemente inferior a las precisiones SoTA individuales del 97% y 69% reportadas en la literatura de autoformalización y demostración de teoremas. Analizando los modos de fallo, atribuimos una parte considerable de esta disminución a discrepancias entre los enunciados formales e informales en más de la mitad de los problemas de miniF2F. Procedemos a corregir todos los errores, discrepancias y simplificaciones en los enunciados formales e informales, y presentamos miniF2F-v2 con enunciados y demostraciones formales e informales completamente verificados. La evaluación del pipeline completo de demostración de teoremas en miniF2F-v2 arroja una precisión máxima del 70%, una mejora significativa respecto al 40% obtenido en el miniF2F original, aunque aún indica un desalineamiento considerable entre los modelos de autoformalización y los demostradores de teoremas. Nuestro análisis en profundidad sugiere que un benchmark de mayor calidad puede ayudar a la comunidad a evaluar mejor el progreso en el campo del razonamiento formal y también a diagnosticar de manera más efectiva los modos de fallo y éxito de los modelos de autoformalización y demostración de teoremas. Nuestro conjunto de datos está disponible en https://github.com/roozbeh-yz/miniF2F_v2.

English

We perform a thorough analysis of the formal and informal statements in the miniF2F benchmark from the perspective of an AI system that is tasked to participate in a math Olympiad consisting of the problems in miniF2F. In such setting, the model has to read and comprehend the problems in natural language, formalize them in Lean language, then proceed with proving the problems, and it will get credit for each problem if the formal proof corresponds to the original informal statement presented to the model. Our evaluation results reveal that the best accuracy of such pipeline can be about 36% using the SoTA models in the literature, considerably lower than the individual SoTA accuracies, 97% and 69% reported in the autoformalization and theorem proving literature. Analyzing the failure modes, we trace back a considerable portion of this drop to discrepancies between the formal and informal statements for more than half of the problems in miniF2F. We proceed with correcting all the errors, discrepancies and simplifications in formal and informal statements, and present the miniF2F-v2 with fully verified formal and informal statements and proofs. Evaluating the full theorem proving pipeline on miniF2F-v2 leads to the best accuracy of 70%, a significant improvement from the 40% on the original miniF2F, yet indicating considerable misalignment between the autoformalization models and theorem provers. Our deep analysis suggests that a higher quality benchmark can help the community better evaluate progress in the field of formal reasoning and also better diagnose the failure and success modes of autoformalization and theorem proving models. Our dataset is available at https://github.com/roozbeh-yz/miniF2F_v2.