miniF2F-Lean Revisited: Een evaluatie van de beperkingen en een route naar de toekomst

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

November 5, 2025

Auteurs: Azim Ospanov, Farzan Farnia, Roozbeh Yousefzadeh

cs.AI

Samenvatting

Wij voeren een grondige analyse uit van de formele en informele beweringen in de miniF2F-benchmark vanuit het perspectief van een AI-systeem dat de taak heeft deel te nemen aan een wiskunde-olympiade bestaande uit de problemen in miniF2F. In een dergelijke setting moet het model de problemen in natuurlijke taal lezen en begrijpen, ze formaliseren in de Lean-taal, vervolgens doorgaan met het bewijzen van de problemen, en het krijgt punten voor elk probleem als het formele bewijs overeenkomt met de oorspronkelijke informele bewering die aan het model werd voorgelegd. Onze evaluatieresultaten tonen aan dat de beste nauwkeurigheid van een dergelijke pijplijn ongeveer 36% kan zijn bij gebruik van de state-of-the-art modellen in de literatuur, aanzienlijk lager dan de individuele state-of-the-art nauwkeurigheden van 97% en 69% die gerapporteerd worden in de literatuur over autoformalizatie en stellingbewijzen. Door de faalwijzen te analyseren, herleiden we een aanzienlijk deel van deze daling naar discrepanties tussen de formele en informele beweringen voor meer dan de helft van de problemen in miniF2F. Wij gaan vervolgens over tot het corrigeren van alle fouten, discrepanties en vereenvoudigingen in de formele en informele beweringen, en presenteren miniF2F-v2 met volledig geverifieerde formele en informele beweringen en bewijzen. Evaluatie van de volledige stellingbewijspijplijn op miniF2F-v2 leidt tot een beste nauwkeurigheid van 70%, een significante verbetering ten opzichte van de 40% op de originele miniF2F, maar wijst toch op een aanzienlijke mismatch tussen de autoformalizatiemodellen en stellingbewijzers. Onze diepgaande analyse suggereert dat een benchmark van hogere kwaliteit de gemeenschap kan helpen om de vooruitgang op het gebied van formeel redeneren beter te evalueren en ook de faal- en succeswijzen van autoformalizatie- en stellingbewijzermodellen beter te diagnosticeren. Onze dataset is beschikbaar op 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.