miniF2F-Lean Revisited: Eine Überprüfung der Grenzen und die Skizzierung eines Weges nach vorn

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

Wir führen eine gründliche Analyse der formalen und informellen Aussagen im miniF2F-Benchmark aus der Perspektive eines KI-Systems durch, das an einer Mathematik-Olympiade teilnehmen soll, die aus den Problemen in miniF2F besteht. In einem solchen Szenario muss das Modell die Probleme in natürlicher Sprache lesen und verstehen, sie in die Lean-Sprache formalisieren und anschließend mit dem Beweis der Probleme fortfahren. Es erhält für jedes Problem Anerkennung, wenn der formale Beweis der ursprünglichen, dem Modell präsentierten informellen Aussage entspricht. Unsere Evaluierungsergebnisse zeigen, dass die beste Genauigkeit einer solchen Pipeline unter Verwendung der State-of-the-Art-Modelle (SoTA) aus der Literatur bei etwa 36 % liegen kann, was deutlich niedriger ist als die einzelnen in der Autoformalisierungs- und Theorembeweis-Literatur berichteten SoTA-Genauigkeiten von 97 % bzw. 69 %. Durch die Analyse der Fehlermodi führen wir einen beträchtlichen Teil dieses Rückgangs auf Diskrepanzen zwischen den formalen und informellen Aussagen für mehr als die Hälfte der Probleme in miniF2F zurück. Wir korrigieren daraufhin alle Fehler, Diskrepanzen und Vereinfachungen in den formalen und informellen Aussagen und präsentieren miniF2F-v2 mit vollständig verifizierten formalen und informellen Aussagen sowie Beweisen. Die Evaluierung der vollständigen Theorembeweis-Pipeline auf miniF2F-v2 führt zu einer besten Genauigkeit von 70 %, einer signifikanten Verbesserung gegenüber 40 % auf dem ursprünglichen miniF2F, was jedoch auf eine erhebliche Fehlausrichtung zwischen Autoformalisierungsmodellen und Theorembeweisern hindeutet. Unsere tiefgehende Analyse legt nahe, dass ein Benchmark von höherer Qualität der Gemeinschaft helfen kann, Fortschritte auf dem Gebiet des formalen Schließens besser zu bewerten und gleichzeitig die Fehler- und Erfolgsmodi von Autoformalisierungs- und Theorembeweisermodellen besser zu diagnostizieren. Unser Datensatz ist verfügbar unter 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.