miniF2F-Lean revisité : Examen des limites et tracé d'une voie vers l'avant

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

November 5, 2025

papers.authors: Azim Ospanov, Farzan Farnia, Roozbeh Yousefzadeh

cs.AI

papers.abstract

Nous réalisons une analyse approfondie des énoncés formels et informels du benchmark miniF2F du point de vue d'un système d'IA chargé de participer à une olympiade de mathématiques composée des problèmes de miniF2F. Dans ce contexte, le modèle doit lire et comprendre les problèmes en langage naturel, les formaliser dans le langage Lean, puis procéder à leur démonstration ; il obtiendra un crédit pour chaque problème si la preuve formelle correspond à l'énoncé informel original qui lui a été présenté. Nos résultats d'évaluation révèlent que la meilleure précision d'un tel pipeline peut atteindre environ 36 % avec les modèles de l'état de l'art (SoTA) de la littérature, ce qui est considérablement inférieur aux précisions individuelles de l'état de l'art, 97 % et 69 %, rapportées respectivement dans la littérature sur l'autoformalisation et la démonstration de théorèmes. En analysant les modes d'échec, nous attribuons une part importante de cette baisse à des divergences entre les énoncés formels et informels pour plus de la moitié des problèmes de miniF2F. Nous procédons à la correction de toutes les erreurs, divergences et simplifications dans les énoncés formels et informels, et présentons miniF2F-v2 avec des énoncés et des preuves formels et informels entièrement vérifiés. L'évaluation du pipeline complet de démonstration de théorèmes sur miniF2F-v2 aboutit à une précision maximale de 70 %, une amélioration significative par rapport aux 40 % obtenus sur le miniF2F original, mais indiquant toujours un désalignement considérable entre les modèles d'autoformalisation et les démonstrateurs de théorèmes. Notre analyse approfondie suggère qu'un benchmark de meilleure qualité peut aider la communauté à mieux évaluer les progrès dans le domaine du raisonnement formel et à mieux diagnostiquer les modes d'échec et de réussite des modèles d'autoformalisation et de démonstration de théorèmes. Notre jeu de données est disponible à l'adresse 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.