miniF2F-Lean Rivisitato: Analisi delle Limitazioni e Tracciamento di una Direzione Futura

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

November 5, 2025

Autori: Azim Ospanov, Farzan Farnia, Roozbeh Yousefzadeh

cs.AI

Abstract

Effettuiamo un'analisi approfondita degli enunciati formali e informali nel benchmark miniF2F dalla prospettiva di un sistema di IA incaricato di partecipare a un'Olimpiade della matematica composta dai problemi in miniF2F. In tale contesto, il modello deve leggere e comprendere i problemi in linguaggio naturale, formalizzarli nel linguaggio Lean, procedere quindi alla dimostrazione dei problemi, e otterrà un punteggio per ogni problema se la dimostrazione formale corrisponde all'enunciato informale originale presentato al modello. I nostri risultati di valutazione rivelano che la massima accuratezza di una tale pipeline può essere circa del 36% utilizzando i modelli state-of-the-art (SoTA) presenti in letteratura, considerevolmente inferiore alle accuratezze SoTA individuali, rispettivamente del 97% e del 69%, riportate in letteratura per l'autoformalizzazione e la dimostrazione automatica di teoremi. Analizzando le modalità di fallimento, attribuiamo una parte considerevole di questo calo a discrepanze tra gli enunciati formali e informali per più della metà dei problemi in miniF2F. Procediamo quindi a correggere tutti gli errori, le discrepanze e le semplificazioni negli enunciati formali e informali, e presentiamo miniF2F-v2 con enunciati e dimostrazioni formali e informali completamente verificati. La valutazione della pipeline completa di dimostrazione automatica su miniF2F-v2 porta a un'accuratezza massima del 70%, un miglioramento significativo rispetto al 40% ottenuto sul miniF2F originale, che tuttavia indica un considerevole disallineamento tra i modelli di autoformalizzazione e i dimostratori di teoremi. La nostra analisi approfondita suggerisce che un benchmark di qualità superiore può aiutare la comunità a valutare meglio i progressi nel campo del ragionamento formale e anche a diagnosticare più efficacemente le modalità di fallimento e successo dei modelli di autoformalizzazione e dimostrazione automatica di teoremi. Il nostro dataset è disponibile all'indirizzo 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.