Revisitando o miniF2F-Lean: Revisando Limitações e Traçando um Caminho à Frente

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

November 5, 2025

Autores: Azim Ospanov, Farzan Farnia, Roozbeh Yousefzadeh

cs.AI

Resumo

Realizamos uma análise aprofundada das declarações formais e informais no benchmark miniF2F sob a perspectiva de um sistema de IA incumbido de participar de uma olimpíada de matemática composta pelos problemas do miniF2F. Nesse cenário, o modelo deve ler e compreender os problemas em linguagem natural, formalizá-los na linguagem Lean e, em seguida, prosseguir com a demonstração dos problemas, recebendo crédito por cada problema se a prova formal corresponder à declaração informal original apresentada ao modelo. Nossos resultados de avaliação revelam que a melhor precisão de tal pipeline pode ser de cerca de 36% usando os modelos state-of-the-art (SoTA) da literatura, consideravelmente inferior às precisões SoTA individuais de 97% e 69% reportadas na literatura de autoformalização e prova de teoremas. Analisando os modos de falha, rastreamos uma parcela considerável dessa queda até discrepâncias entre as declarações formais e informais em mais da metade dos problemas do miniF2F. Prosseguimos corrigindo todos os erros, discrepâncias e simplificações nas declarações formais e informais, e apresentamos o miniF2F-v2 com declarações e provas formais e informais totalmente verificadas. A avaliação do pipeline completo de prova de teoremas no miniF2F-v2 resulta numa precisão máxima de 70%, uma melhoria significativa em relação aos 40% no miniF2F original, mas ainda indicando um desalinhamento considerável entre os modelos de autoformalização e os provadores de teoremas. Nossa análise detalhada sugere que um benchmark de maior qualidade pode ajudar a comunidade a avaliar melhor o progresso no campo do raciocínio formal e também a diagnosticar de modo mais eficaz os modos de falha e sucesso dos modelos de autoformalização e prova de teoremas. Nosso conjunto de dados está disponível em 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.