miniF2F-Lean Revisited: Анализ ограничений и определение путей развития

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

November 5, 2025

Авторы: Azim Ospanov, Farzan Farnia, Roozbeh Yousefzadeh

cs.AI

Аннотация

Мы проводим тщательный анализ формальных и неформальных утверждений в бенчмарке miniF2F с точки зрения системы искусственного интеллекта, задача которой — участвовать в математической олимпиаде, состоящей из задач miniF2F. В такой постановке модель должна прочитать и понять условия задач на естественном языке, формализовать их на языке Lean, затем перейти к доказательству задач и получать баллы за каждую задачу, если формальное доказательство соответствует исходному неформальному утверждению, представленному модели. Наши результаты оценки показывают, что наилучшая точность такого конвейера может составлять около 36% при использовании современных моделей (SoTA) из литературы, что значительно ниже индивидуальных показателей точности SoTA — 97% и 69%, заявленных в литературе по автоформализации и автоматическому доказательству теорем. Анализируя типы ошибок, мы обнаруживаем, что значительная часть этого снижения связана с расхождениями между формальными и неформальными утверждениями более чем для половины задач в miniF2F. Мы исправляем все ошибки, несоответствия и упрощения в формальных и неформальных утверждениях и представляем miniF2F-v2 с полностью верифицированными формальными и неформальными утверждениями и доказательствами. Оценка полного конвейера доказательства теорем на miniF2F-v2 показывает наилучшую точность в 70%, что является значительным улучшением по сравнению с 40% на исходном miniF2F, но указывает на существенное несоответствие между моделями автоформализации и доказателями теорем. Наш глубокий анализ позволяет предположить, что более качественный бенчмарк может помочь сообществу лучше оценивать прогресс в области формальных рассуждений, а также точнее диагностировать причины неудач и успехов моделей автоформализации и доказательства теорем. Наш набор данных доступен по адресу 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.